该论文聚焦于智能合约等可重入应用（Reentrant Applications）的组合安全（Compositional Security）问题。智能合约中反复出现的灾难性漏洞（如著名的重入攻击）表明，在编写需要与恶意代码组合运行的软件时，我们尚缺乏可靠的构造安全代码的方法。信息流控制（Information Flow Control, IFC）长期以来被视为实现组合安全的有效途径，能够在组合来自不同信任域的软件时提供强安全保证。然而，当存在重入（reentrancy）攻击时，传统信息流控制的理论保证会被破坏，使得这一方案在现实中难以奏效。论文的主要贡献包括：第一，形式化定义了通用意义上的重入概念，厘清了何种行为构成重入；第二，提出一种新的安全条件，允许智能合约等软件模块在保留安全重入形式表达力的同时，保护其关键不变量；第三，设计并实现了一个安全类型系统，该类型系统可证明地执行安全信息流策略；第四，将类型系统与运行时机制相结合，使得在存在未知恶意代码的情况下，依然能够强制实施安全的重入约束；第五，通过该类型系统成功定位并修正了若干近期备受关注的高危漏洞实例。实验评估表明，该方法既保持了实用性，又显著提升了组合安全性。该研究为构建抗重入的智能合约及类似可重入应用提供了形式化基础与工具支撑，适合安全编程语言研究者、智能合约开发者以及系统安全工程师阅读。

以太坊智能合约的重入漏洞曾导致巨大的经济损失，为此社区开发了多种自动化重入检测器。然而，这些检测器因检测规则过于粗糙而频繁产生大量误报，常将已采用防重入模式（如互斥锁、检查-生效-交互模式等）保护的合约误判为存在漏洞。现有代码分析技术在识别这些防重入模式时面临挑战，主要原因是防重入模式的特征复杂且多样，且缺乏对这些特征的先验知识。本文提出 AutoAR，一个自动化识别系统，用于探索和识别以太坊合约中普遍存在的防重入模式。AutoAR 利用一种专门的图表示 RentPDG（Reentrancy Protection Dependency Graph），结合数据过滤方法，从大量合约中有效捕获与防重入相关的语义信息。基于从合约中提取的 RentPDG，AutoAR 采用一个集成图自编码器与聚类技术的识别模型，专门用于精确识别防重入模式。实验结果表明，AutoAR 能够帮助现有检测器识别 12 种常见的防重入模式，准确率达到 89%；将其集成到检测流程后，误报率降低了超过 85%。该工作为提升智能合约安全检测的准确性提供了有力工具。

本文提出了首个经过机器检查的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上获取。