本论文提出 EOSAFE，一个针对 EOSIO 智能合约的自动化安全分析框架。EOSIO 是一种新兴的区块链平台，其智能合约使用 C++ 编写，且具有独特的通信模型和资源管理机制，导致传统分析工具难以直接应用。EOSAFE 结合了静态分析和形式化验证技术，能够检测 EOSIO 智能合约中的典型漏洞，如伪随机数依赖、资源耗尽、回滚攻击等。作者在真实世界的 2000+ 个合约数据集上进行评估，成功发现了多个之前未知的漏洞，并报告给开发团队得到确认。实验表明 EOSAFE 具有较高的检测精度和较低的误报率。该工作为 EOSIO 生态的安全保障提供了有效工具，也填补了针对该平台系统化安全分析的研究空白。

该论文是系列正式验证分析掩码NTT（数论变换）硬件安全性论文的第7篇，针对后量子密码（PQC）硬件中的侧信道泄漏问题。论文证明了在任意深度k级流水线中，采用新鲜中间掩码和每级PF-PINI(≤2)小工具（gadgets）的掩码NTT实现，每个观察值的原像基数上界为2·q^{2k-2}（通过Lean 4机器检验，无漏洞）。在标准语义解释（除以总掩码元组空间大小q^{2k-1}）下，每个观察值的条件概率上界为2/q，与流水线深度k无关。主要贡献包括：1) k级组合定理，推广了之前2级结果，证明只有最后一级的PF-PINI参数影响界限；2) 证明Montgomery归约满足PF-PINI(2)且最大重数严格为2；3) 将各组件整合为端到端界限；4) 通过Lean验证的假设违反条件锚定先前的经验性和结构性Adams Bridge分析。该工作为掩码PQC硬件提供了可扩展的理论安全界，并经过正式验证。