Compositional Security for Reentrant Applications.
该论文聚焦于智能合约等可重入应用(Reentrant Applications)的组合安全(Compositional Security)问题。智能合约中反复出现的灾难性漏洞(如著名的重入攻击)表明,在编写需要与恶意代码组合运行的软件时,我
共收录 3 条相关情报。
← 返回所有主题该论文聚焦于智能合约等可重入应用(Reentrant Applications)的组合安全(Compositional Security)问题。智能合约中反复出现的灾难性漏洞(如著名的重入攻击)表明,在编写需要与恶意代码组合运行的软件时,我
以太坊智能合约的重入漏洞曾导致巨大的经济损失,为此社区开发了多种自动化重入检测器。然而,这些检测器因检测规则过于粗糙而频繁产生大量误报,常将已采用防重入模式(如互斥锁、检查-生效-交互模式等)保护的合约误判为存在漏洞。现有代码分析技术在识别
本文提出了首个经过机器检查的OpenZeppelin重入防护模式正确性证明,该证明针对生产部署的Solidity源代码的Lean 4状态机模型。所有十三个定理都经过了机器检查,没有使用任何“sorry”或用户引入的公理,公理足迹仅由[pro