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

DDR5内存标准引入了每行激活计数（PRAC）作为缓解Rowhammer攻击的机制，通过跟踪每行的激活次数并在超过阈值时触发缓解刷新。然而，当前PRAC设计的安全性评估依赖于人工构造的攻击模式，缺乏对安全属性的形式化验证或自动化漏洞发现技术。本文提出AutoPRAC，首个利用模型检查器自动化测试PRAC防御安全性的框架。AutoPRAC将PRAC实现建模为有界状态机，并针对最坏情况下的神谕攻击者检查安全关键属性。若属性被违反，框架会生成具体的反例轨迹，对应一次成功的攻击。使用AutoPRAC，作者在最新的PRAC防御方案MOAT中发现了一个此前未报告的缺陷：其计数器重置策略允许最多34次激活超过Rowhammer阈值而未被检测到。实验表明，AutoPRAC能够自动发现Rowhammer缓解措施中的细微安全缺陷，可作为PRAC设计的早期攻击发现辅助工具。该研究为硬件安全验证提供了新思路，尤其适用于新型内存防御机制的形式化分析。