我院在智能合约信息流安全策略综合研究方面取得进展

       近日，我院宋富研究员与同济大学、北卡罗莱纳州立大学联合研究团队在智能合约信息流安全策略综合研究方面取得进展。团队针对智能合约信息流安全分析中保密性分析缺失与对外部实体交互建模不足的问题，提出了一种全自动安全策略综合方案SmartIFSyn。其核心思路是利用类型推导与约束求解技术，自动识别合约潜在漏洞并综合生成信息流安全策略修复漏洞。该方案使合约能有效避免隐私泄露或数据篡改行为，实现了从漏洞精准检测到自动消除的闭环。相关成果论文《SmartIFSyn: Automated Information Flow Security Policy Synthesis for Smart Contracts》被软件工程领域顶级会议FSE 2026接受。

       信息流安全（Information Flow Security，IFS）技术可同时用于保障保密性与完整性：其中，保密性确保私有信息仅能被授权主体访问，而完整性则保证可信数据不会被未授权的修改所破坏。尽管已有相关工作涉及智能合约的信息流安全分析，但它们仍面临三大挑战：（1）忽略保密性需求带来的隐私泄露风险；（2）针对外部实体交互的全局安全性建模不足；（3）现有方案多侧重漏洞检测，缺乏有效的自动修复能力。

       针对上述挑战，该工作提出了首个兼顾保密性与完整性、涵盖局部变量与全局交互安全的策略综合方案SmartIFSyn。不同于传统仅侧重完整性检测的方法，SmartIFSyn通过形式化定义包含区块链记录的Solidity操作语义，系统地从局部变量与全局交互两个维度，构建了智能合约信息流安全属性模型，并实现了从“漏洞检测”到“自动消除”的跨越。其核心流程分为两个阶段：

       类型推导：基于Solidity形式化操作语义设计了一套类型系统，实现了局部变量安全的可靠分析并识别出潜在的信息流漏洞。系统能够自动识别并提取出那些同时符合全局交互安全要求的策略，兼顾了分析效率与严谨性。

       约束求解：针对无法直接通过类型推导解决的复杂安全漏洞，方案将其转化为约束求解问题。利用MaxSAT求解器，在强制满足安全约束的前提下，通过优化安全等级的分配，最大程度地保留了合约原始的业务逻辑与用户意愿。

       最后，SmartIFSyn通过动态跟踪安全等级并自动注入程序规范（如require语句），将抽象的安全策略转化为合约内置的可执行规范。这种“推导－求解－注入”的一体化机制，确保了合约在复杂的运行环境下，能从局部与全局两个维度实现对信息流漏洞的精准检测与主动防御。

SmartIFSyn示意图

       团队在17,160个真实世界的以太坊智能合约上对SmartIFSyn进行了系统评估。实验结果表明，该方法在保密性与完整性两个维度上均能有效检测并消除信息流漏洞。尤其是，SmartIFSyn在整体性能上优于多种具有代表性的智能合约分析工具（包括AChecker、Ethainter、LLM-SmartAudit、Securify、SoMo以及STC/STV），并在223个真实世界智能合约中检测出243个信息流安全漏洞。

       SmartIFSyn聚焦于智能合约中长期被忽视的隐私泄露风险与复杂交互安全问题，研发了基于形式化语义的类型推导与约束求解的安全策略生成框架。该方法不仅填补了智能合约在全局交互安全建模方面的空白，更通过注入程序规范为区块链应用的自动化安全保障提供了可靠的系统化解决方案。