LLM 智能体（agent）会生成并执行多步计划，计划中会调用外部工具；这些工具既可访问私有数据，也可执行命令。在此场景下，安全性并非某个单一步骤的属性，而是由计划所形成的整个执行过程的属性；计划本身就是关键工件，记录了工具调用、控制流与数据依赖关系。论文提出 CaMeLoT，作为已有防御方案 CaMeL（面向工具型 LLM 智能体的提示注入防御）的补充。CaMeLoT 在 CaMeL 基础上增加一个静态验证层，在调用任何工具之前对智能体计划进行检查。其核心方法为：把生成的计划翻译成有限状态迁移系统，用工具调用、provenance（数据来源）与污点信息对该系统进行标注，再使用 CTL（计算树逻辑）表达时序安全策略，并借助 nuXmv 模型检验器进行验证。由于验证发生在执行之前，不安全的计划会被直接拒绝，无需调用 LLM 或执行工具，从而节省运行时本会消耗的 token，也避免了回滚已发生的变更或拆除临时沙箱的成本。当验证失败时，模型检验器会返回反例，用于向智能体提供反馈以修复计划。评估方面，作者在来自 AgentDojo 基准、SOC 工作流和提示抽取（prompt-extraction）实验的策略集上对 CaMeLoT 进行了测试，结果表明它能够在执行前验证广泛的时序属性，同时保留 CaMeL 原有可运行时检查的覆盖范围。该工作属于形式化方法与 LLM 智能体安全的交叉方向，适合智能体安全、安全编排与形式化验证方向的研究者和工程师阅读。

该论文关注现代语义丰富系统与应用中的“应用逻辑漏洞”（application logic flaws）。这类漏洞与业务语义和威胁模型深度绑定，难以通过传统的模糊测试或静态分析规模化发现：真实系统往往包含多样的应用特性、复杂的协议逻辑与领域专属的威胁模型，需要大量人工投入与领域专家经验才能完成有效安全分析。作者提出 LL-Verifier——一个自动化逻辑漏洞发现框架，其核心由两部分构成：(1) 利用大语言模型完成自主建模（autonomous modeling）；(2) 利用逻辑模型检测器（logic model checker）完成严格推理。LL-Verifier 接受自然语言输入，尤其是协议描述与安全目标，自动生成形式化逻辑模型与安全属性；这些属性用一种新的逻辑语言表达，该语言构建在通用逻辑语言 Maude 之上，并针对“任意应用级语义”的建模进行了优化。随后，生成的形式化模型被转换为逻辑状态机，从而可以通过逻辑层面的模型检测实现穷尽式、严格的验证。该方案的目标是把原本高度依赖人工的应用级协议分析流程自动化，在逻辑约束范围内提供自动化、穷尽且精确的推理能力。为验证效果，作者在 27 个广泛使用的 IoT 设备的访问控制协议上进行了评估，这些协议带有厂商特有的逻辑流程与语义。论文声称在有效性、效率与实用性上均取得良好表现，并在 IoT 协议与设备中发现了多种复杂的逻辑漏洞，具有严重的安全与隐私影响。值得注意的是，该工作直面的正是应用安全中一个公认的难题——自动化的逻辑漏洞发现。 从研究视角看：研究问题是如何在缺乏人工领域知识的前提下，对具有任意应用语义的协议进行可规模化、可穷尽的安全推理；核心方法是“LLM 自主形式化建模 + Maude 系逻辑语言 + 逻辑状态机模型检测”的三段式流水线；主要贡献是提出该框架、给出一套面向应用级语义的建模语言与转换机制，并在 27 个真实 IoT 访问控制协议上完成实证评估，挖掘出新型逻辑漏洞。适合阅读的读者包括：从事形式化验证、协议安全、IoT 安全的研究人员，以及希望把形式化方法引入业务逻辑审计的安全工程团队。由于仅获取到摘要，方法细节、逻辑语言的具体语法语义、模型检测的可扩展性指标、以及漏洞细节均未展开。

本文提出一种名为 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设计的早期攻击发现辅助工具。该研究为硬件安全验证提供了新思路，尤其适用于新型内存防御机制的形式化分析。