本文介绍了使用Lean 4证明助手对StarkWare的S-two证明器中的代数中间表示（AIR）进行形式化验证的工作。S-two证明器用于在区块链上高效地证明用Cairo虚拟机语言编写的程序能够运行完成。该证明器通过一个代数中间表示（AIR）捕获Cairo语言的语义，该AIR断言存在满足特定代数约束的有限域值表。然后，加密交互式证明系统circle STARK提供一个高效验证的证书，证明AIR是可满足的。本文的核心贡献在于，利用Lean 4证明助手对AIR编码的可靠性（soundness）进行了形式化验证，即证明AIR的可满足性蕴含相应的计算性声明。这一验证确保了AIR编码不会错误地声称一个无效的程序运行完成。论文详细描述了验证过程，包括如何在Lean 4中形式化AIR的语义、约束以及soundness证明。该工作对于提高Cairo智能合约和区块链应用的安全性具有重要价值，因为它提供了一个数学上严谨的保证，防止因AIR编码错误导致的虚假计算声明。读者包括对形式化验证、区块链安全性以及零知识证明感兴趣的研究者和工程师。

本文提出了首个经过机器检查的OpenZeppelin重入防护模式正确性证明，该证明针对生产部署的Solidity源代码的Lean 4状态机模型。所有十三个定理都经过了机器检查，没有使用任何“sorry”或用户引入的公理，公理足迹仅由[propext]（一个标准的mathlib4公理）限定，并集成在持续集成中。智能合约重入攻击自2016年以来已导致超过5亿美元的损失，其中DAO 2016攻击盗取了约360万ETH，并迫使以太坊硬分叉。OpenZeppelin ReentrancyGuard模式是生产DeFi中的事实标准防御措施，但此前没有工作建立其判别能力：即该防护能阻止对易受攻击实例的攻击，保持非攻击交易的正确执行，并区分相邻的安全和易受攻击变体。以往的工作要么形式化了玩具合约上的防护正确性，要么形式化了孤立实例上的攻击可行性，但未同时涵盖两个方向及针对生产源码的边界情况。本文通过变异测试验证了三种生产实例：DAO 2016、Compound v2和Aave V3的flashLoan，以及Aave V3 flashLoan的一个最小差异突变体（flashLoanVulnerable），该突变体隔离了一个安全关键差异。三方向结构包括：(a) DAO 2016模式的攻击复现，(b) Compound v2的正确性证明，(c) 区分Aave V3符合CEI模式的flashLoan与突变体的边界案例证明。一个顶层的元定理在“无改造”原则下组合了这三个方向，并在首次跨协议压力测试（从Compound v2到Aave V3）中进行了演示；更广泛的家族可移植性是未来工作。完整的Lean 4源码、CI配置和复现命令可在GitHub上获取。

该论文提出了一种结合大型语言模型（LLMs）与形式化方法的智能合约验证新框架。当前智能合约验证面临两大挑战：自然语言表达的属性内在存在歧义，且LLM的答案缺乏正确性保证。作者通过两个创新点同时解决这些问题：1）设计了一种扩展Solidity语言的正式规范语言，支持抽象类型，使得属性表达无歧义；2）开发了一个工作流，将LLM与类型检查和具体执行相结合，自动生成并验证违规见证（即反例）。其核心思想是将规范编码为包含存在量化抽象类型变量的Solidity测试；通过为这些变量实例化具体值（符合正确类型），测试将转换为可执行的反例（概念验证），直观展示属性为何被违反。作者将该流程实现为工具Neuroforger，并在来自文献的智能合约验证数据集上实验评估，获得了有前景的结果，证明了其在真实场景中的潜在适用性。本文适合对智能合约安全、形式化验证及LLM应用感兴趣的读者。

本文研究在统计发布场景下的成员推理攻击（Membership Inference Attack, MIA）问题。现有攻击通常仅利用数据集的边缘分布来建模总体，并假设总体服从独立同分布或乘积分布，这忽略了属性之间的依赖关系，从而限制了攻击效果。作者提出一种基于贝叶斯网络的框架，将总体建模为贝叶斯网络（BN），使得攻击者可以利用先验知识（如人口属性依赖结构）发起更有效的定制化攻击。该框架将成员推理问题重新定义为贝叶斯决策问题，并引入概率编程语言Roulette实现贝叶斯后验计算的具体攻击实例。理论证明表明，该攻击在具有强属性依赖的两个总体下等价于最优的似然比检验攻击变体。实验基于五个常用贝叶斯网络数据集，比较了似然比检验和内积攻击等基线方法，结果表明所提方法在总体依赖结构复杂、现有攻击难以手动适配的场景下显著优于基线。本文主要贡献包括：形式化了考虑属性依赖的成员推理问题、设计了基于贝叶斯决策的通用框架、提供了概率编程实现的理论与实验验证。适合从事差分隐私、统计发布安全、以及对抗性机器学习的研究人员阅读。

本文针对软件中普遍存在的内容组合漏洞（如XSS、注入），指出现有缓解手段（开发者培训、静态分析、模板语言）效果递减，且AI代码生成继承了训练数据中的不安全模式并缺乏自我纠正的可靠上下文。作者提出一个通用安全内容组合框架，该框架跨内容语言扩展，通过修改字符串表达式语法直接集成到通用编程语言中。核心设计目标是最小化安全与不安全惯用语之间的词汇距离，使开发者更自然编写安全代码。该目标支撑了实用的编译策略：基于动态语义的静态分析、运行时性能接近原生字符串拼接，以及编译时错误/警告等开发者诊断。框架实现有效分工：安全工程师一次性将组合危险编码到库中；开发者或AI编码助手选择合适的库原语即可正确实现功能，无需深入安全知识；编译器诊断提供客观的、基于位置的反馈，支持人工审查和AI迭代自我纠正；安全响应者专注于保持库的更新，而非审计分散在代码库中的临时安全决策。实验（假设存在）证明了方法的可行性与高效性。适合安全工程师、编译器开发者和AI安全研究人员阅读。

本文提出了一种名为“基于语言的智能体控制”（LBAC）的新型编程模型，旨在解决智能体应用中的安全控制问题。传统的编程语言中，静态类型和运行时强制执行已被用于确保程序满足用户指定的策略（如访问控制、信息流、数据来源等）。LBAC的核心思想是将这些保证扩展到智能体应用：要求智能体生成的程序本身在周围脚手架代码的上下文中是良好类型的。不安全的程序在执行前会被类型检查器拒绝，从而允许策略统一应用于整个应用程序，包括智能体生成的行为和开发者编写的脚手架。同时，LBAC保留了相当大的表达能力：智能体可以执行任意的无副作用计算，并递归调用子智能体，这些子智能体在相同或更严格的策略下保留完整的工具访问权限。本文通过三个案例研究展示了LBAC：基于文件系统能力的I/O沙箱、数据来源和信息流控制。该工作为智能体安全提供了新的形式化方法，适合编程语言和安全领域的研究者阅读。