本文提出一种名为 VetSC 的新型自动化安全审查技术，针对去中心化应用（DApps）中的智能合约。由于 DApps 的业务逻辑通常由链上合约与链下界面共同组成，传统静态分析难以直接从合约代码中提取高层业务语义，也无法自动确定需要验证的安全属性，导致安全审查高度依赖人工。VetSC 采用界面驱动（UI-driven）的程序分析引导的模型检测方法：首先从合约代码中提取业务模型图（business model graphs），以捕获其内在的业务和安全逻辑；随后，从 DApp 的用户界面中检索文本语义，自动推理出应检查的安全规范（safety specifications）。为了防止不可信的界面文本误导分析，VetSC 还会校验界面与合约逻辑的一致性，检测二者之间的偏差。作者实现了 VetSC 原型，并将其应用于 34 个真实 DApp。实验表明，VetSC 能够准确解释智能合约代码、实现自主安全审查，并在真实 DApp 中发现安全风险。利用该工具，作者在真实场景中发现了 19 个新的安全风险，例如过期的彩票仍可兑奖、同一用户重复投票等问题。该技术的主要贡献在于将自然语言界面信息与合约代码分析结合，实现了安全属性的自动推导，显著降低了 DApps 安全审查的人工门槛。适合区块链安全研究人员、智能合约审计人员以及 DApp 开发者阅读。