Conference：The Network and Distributed System Security (NDSS)
CCF level：CCF A
Categories：network and information security
Year：2025
Conference time： 24 to 28 February 2025 in San Diego, California.
1
Title:
Silence False Alarms: Identifying Anti-Reentrancy Patterns on Ethereum to Refine Smart Contract Reentrancy Detection
沉默误报：识别以太坊上的反重入模式以改进智能合约重入检测
Authors:
Qiyang Song (Institute of Information Engineering, Chinese Academy of Sciences; School of Cyber Security, University of Chinese Academy of Sciences), Heqing Huang (Institute of Information Engineering, Chinese Academy of Sciences), Xiaoqi Jia (Institute of Information Engineering, Chinese Academy of Sciences; School of Cyber Security, University of Chinese Academy of Sciences), Yuanbo Xie (Institute of Information Engineering, Chinese Academy of Sciences; School of Cyber Security, University of Chinese Academy of Sciences), Jiahao Cao (Institute for Network Sciences and Cyberspace, Tsinghua University)
Abstract:
Reentrancy vulnerabilities in Ethereum smart contracts have caused significant financial losses, prompting the creation of several automated reentrancy detectors. However, these detectors frequently yield a high rate of false positives due to coarse detection rules, often misclassifying contracts protected by anti-reentrancy patterns as vulnerable. Thus, there is a critical need for the development of specialized automated tools to assist these detectors in accurately identifying anti-reentrancy patterns. While existing code analysis techniques show promise for this specific task, they still face significant challenges in recognizing anti-reentrancy patterns. These challenges are primarily due to the complex and varied features of anti-reentrancy patterns, compounded by insufficient prior knowledge about these features.
This paper introduces AutoAR, an automated recognition system designed to explore and identify prevalent anti-reentrancy patterns in Ethereum contracts. AutoAR utilizes a specialized graph representation, RentPDG, combined with a data filtration approach, to effectively capture anti-reentrancy-related semantics from a large pool of contracts. Based on RentPDGs extracted from these contracts, AutoAR employs a recognition model that integrates a graph auto-encoder with a clustering technique, specifically tailored for precise anti-reentrancy pattern identification. Experimental results show AutoAR can assist existing detectors in identifying 12 prevalent anti-reentrancy patterns with 89% accuracy, and when integrated into the detection workflow, it significantly reduces false positives by over 85%.
以太坊智能合约中的重入漏洞造成了重大的财务损失，促使创建了几个自动重入检测器。然而，由于检测规则粗糙，这些检测器经常产生高误报率，通常会将受反重入模式保护的合约误分类为易受攻击的合约。因此，迫切需要开发专门的自动化工具来帮助这些检测器准确识别反重入模式。虽然现有的代码分析技术显示出完成这项特定任务的希望，但它们在识别反重入模式方面仍然面临着重大挑战。这些挑战主要是由于反重入模式的复杂多样的特征，再加上对这些特征的先验知识不足。
本文介绍了AutoAR，这是一个自动识别系统，旨在探索和识别以太坊合约中流行的反重入模式。AutoAR利用专门的图表示RentPDG，结合数据过滤方法，从大量合约中有效地捕获与反重入相关的语义。基于从这些合约中提取的RentPDGs，AutoAR采用了一种识别模型，该模型将图自动编码器与聚类技术相结合，专门为精确的抗重入模式识别而定制。实验结果表明，AutoAR可以帮助现有的检测器识别12种流行的抗重入模式，准确率为89%，当集成到检测工作流程中时，它可以将误报率显著降低85%以上。
Pdf下载链接:
https://www.ndss-symposium.org/wp-content/uploads/2025-167-paper.pdf
2
Title:
PropertyGPT: LLM-driven Formal Verification of Smart Contracts through Retrieval-Augmented Property Generation
PropertyGPT:通过检索增强属性生成实现LLM驱动的智能合约形式验证
Authors:
Ye Liu (Singapore Management University), Yue Xue (MetaTrust Labs), Daoyuan Wu (The Hong Kong University of Science and Technology), Yuqiang Sun (Nanyang Technological University), Yi Li (Nanyang Technological University), Miaolei Shi (MetaTrust Labs), Yang Liu (Nanyang Technological University)
Abstract:
Formal verification is a technique that can prove the correctness of a system with respect to a certain specification or property. It is especially valuable for security-sensitive smart contracts that manage billions in cryptocurrency assets. Although existing research has developed various static verification tools (or provers) for smart contracts, a key missing component is the automated generation of comprehensive properties, including invariants, pre-/post-conditions, and rules. Hence, industry-leading players like Certora have to rely on their own or crowdsourced experts to manually write properties case by case.
With recent advances in large language models (LLMs), this paper explores the potential of leveraging state-of-the-art LLMs, such as GPT-4, to transfer existing human-written properties (e.g., those from Certora auditing reports) and automatically generate customized properties for unknown code. To this end, we embed existing properties into a vector database and retrieve a reference property for LLM-based in-context learning to generate a new property for a given code. While this basic process is relatively straightforward, ensuring that the generated properties are (i) compilable, (ii) appropriate, and (iii) verifiable presents challenges. To address (i), we use the compilation and static analysis feedback as an external oracle to guide LLMs in iteratively revising the generated properties. For (ii), we consider multiple dimensions of similarity to rank the properties and employ a weighted algorithm to identify the top-K properties as the final result. For (iii), we design a dedicated prover to formally verify the correctness of the generated properties. We have implemented these strategies into a novel LLM-based property generation tool called PropertyGPT. Our experiments show that PropertyGPT can generate comprehensive and high-quality properties, achieving an 80% recall compared to the ground truth. It successfully detected 26 CVEs/attack incidents out of 37 tested and also uncovered 12 zero-day vulnerabilities, leading to $8,256 in bug bounty rewards.
形式验证是一种可以证明系统相对于特定规范或属性的正确性的技术。它对于管理数十亿加密货币资产的安全敏感智能合约尤其有价值。尽管现有的研究已经为智能合约开发了各种静态验证工具（或证明工具），但一个关键的缺失部分是自动生成综合属性，包括不变量、前置/后置条件和规则。因此，像Certora这样的行业领先企业必须依靠自己或众包专家逐案手动编写房产。
随着大型语言模型（LLM）的最新进展，本文探讨了利用GPT-4等最先进的LLM来转移现有的人工编写属性（例如，来自Certora审计报告的属性）并自动为未知代码生成自定义属性的潜力。为此，我们将现有属性嵌入到向量数据库中，并基于上下文学习检索LLM的引用属性，为给定代码生成新属性。虽然这个基本过程相对简单，但确保生成的属性是（i）可编译的，（ii）适当的，以及（iii）可验证的，这带来了挑战。为了解决（i）问题，我们使用编译和静态分析反馈作为外部预言机来指导LLM迭代修改生成的属性。对于（ii），我们考虑多个维度相似性对属性进行排序，并采用加权算法将前K个属性识别为最终结果。对于（iii），我们设计了一个专用的证明器来正式验证所生成属性的正确性。我们已经将这些策略实现到一个名为PropertyGPT的新型基于LLM的属性生成工具中。我们的实验表明，PropertyGPT可以生成全面和高质量的属性，与真实数据相比，召回率达到80%。它成功检测到37个测试中的26个CVE/攻击事件，还发现了12个零日漏洞，获得了8256美元的漏洞赏金。
Pdf下载链接:
https://www.ndss-symposium.org/wp-content/uploads/2025-1357-paper.pdf
3
Title:
Alba: The Dawn of Scalable Bridges for Blockchains
Alba：区块链可扩展桥梁的黎明
Authors:
Giulia Scaffino (TU Wien), Lukas Aumayr (TU Wien), Mahsa Bastankhah (Princeton University), Zeta Avarikioti (TU Wien), Matteo Maffei (TU Wien)
Abstract:
Over the past decade, cryptocurrencies have garnered attention from academia and industry alike, fostering a diverse blockchain ecosystem and novel applications. The inception of bridges improved interoperability, enabling asset transfers across different blockchains to capitalize on their unique features. Despite their surge in popularity and the emergence of Decentralized Finance (DeFi), trustless bridge protocols remain inefficient, either relaying too much information (e.g., light-client-based bridges) or demanding expensive computation (e.g., zk-based bridges). These inefficiencies arise because existing bridges securely prove a transaction's on-chain inclusion on another blockchain. Yet this is unnecessary as off-chain solutions, like payment and state channels, permit safe transactions without on-chain publication. However, existing bridges do not support the verification of off-chain payments.
This paper fills this gap by introducing the concept of Pay2Chain bridges that leverage the advantages of off-chain solutions like payment channels to overcome current bridges' limitations. Our proposed Pay2Chain bridge, named Alba, facilitates the efficient, secure, and trustless execution of conditional payments or smart contracts on a target blockchain based on off-chain events. Alba, besides its technical advantages, enriches the source blockchain's ecosystem by facilitating DeFi applications, multi-asset payment channels, and optimistic stateful off-chain computation.
We formalize the security of Alba against Byzantine adversaries in the UC framework and complement it with a game theoretic analysis. We further introduce formal scalability metrics to demonstrate Alba's efficiency. Our empirical evaluation confirms Alba's efficiency in terms of communication complexity and on-chain costs, with its optimistic case incurring only twice the cost of a standard Ethereum transaction of token ownership transfer.
在过去的十年里，加密货币引起了学术界和工业界的关注，培育了一个多样化的区块链生态系统和新的应用。桥接器的出现提高了互操作性，使不同区块链之间的资产转移能够利用其独特的功能。尽管无信任网桥协议越来越受欢迎，并且出现了去中心化金融（DeFi），但它们仍然效率低下，要么传递了太多的信息（例如，基于轻量级客户端的网桥），要么需要昂贵的计算（例如，基于zk的网桥）。这些低效的出现是因为现有的桥梁安全地证明了交易在另一个区块链上的链上包含。然而，这是不必要的，因为支付和状态渠道等链下解决方案允许在没有链上发布的情况下进行安全交易。然而，现有的桥梁不支持链下支付的验证。
本文通过引入Pay2Chain网桥的概念来填补这一空白，该网桥利用支付渠道等链下解决方案的优势来克服当前网桥的局限性。我们提出的名为Alba的Pay2Chain桥有助于基于链下事件在目标区块链上高效、安全和无信任地执行有条件支付或智能合约。Alba除了其技术优势外，还通过促进DeFi应用程序、多资产支付渠道和乐观的有状态链下计算来丰富源区块链的生态系统。
我们在UC框架中正式确定了Alba对拜占庭对手的安全性，并用博弈论分析对其进行了补充。我们进一步引入正式的可扩展性指标来证明Alba的效率。我们的实证评估证实了Alba在通信复杂性和链上成本方面的效率，其乐观情况下的成本仅为标准以太坊代币所有权转移交易成本的两倍。
Pdf下载链接:
https://www.ndss-symposium.org/wp-content/uploads/2025-1286-paper.pdf
4
Title:
Horcrux: Synthesize, Split, Shift and Stay Alive; Preventing Channel Depletion via Universal and Enhanced Multi-hop Payments
魂器：合成、分裂、转换和保持活力；通过通用和增强的多跳支付防止频道耗尽
Authors:
Anqi Tian (Institute of Software, Chinese Academy of Sciences; School of Computer Science and Technology, University of Chinese Academy of Sciences), Peifang Ni (Institute of Software, Chinese Academy of Sciences; Zhongguancun Laboratory, Beijing, P.R.China), Yingzi Gao (Institute of Software, Chinese Academy of Sciences; University of Chinese Academy of Sciences), Jing Xu (Institute of Software, Chinese Academy of Sciences; University of Chinese Academy of Sciences；Zhongguancun Laboratory, Beijing, P.R.China)
Abstract:
Payment Channel Networks (PCNs) have been highlighted as viable solutions to address the scalability issues in current permissionless blockchains. They facilitate off-chain transactions, significantly reducing the load on the blockchain. However, the extensive reuse of multi-hop routes in the same direction poses a risk of channel depletion, resulting in involved channels becoming unidirectional or even closing, thereby compromising the sustainability and scalability of PCNs. Even more concerning, existing rebalancing protocol solutions heavily rely on trust assumptions and scripting languages, resulting in compromised universality and reliability.
In this paper, we present Horcrux, a universal and efficient multi-party virtual channel protocol without relying on extra trust assumptions, scripting languages, or the perpetual online requirement. Horcrux fundamentally addresses the channel depletion problem using a novel approach termed textit{flow neutrality}, which minimizes the impact on channel balance allocations during multi-hop payments (MHPs). Additionally, we formalize the security properties of Horcrux by modeling it within the Global Universal Composability framework and provide a formal security proof.
We implement Horcrux on a real Lightning Network dataset, comprising 10,529 nodes and 38,910 channels, and compare it to the state-of-the-art rebalancing schemes such as Shaduf [NDSS'22], Thora [CCS'22], and Revive [CCS'17]. The experimental results demonstrate that (1) the entire process of Horcrux costs less than 1 USD, significantly lower than Shaduf; (2) Horcrux achieves a $12%$-$30%$ increase in payment success ratio and reduces user deposits required for channels by $70%$-$91%$; (3) the performance of Horcrux improves by $1.2x$-$1.5x$ under long-term operation; and (4) Horcrux maintains a nearly zero channel depletion rate, whereas both Revive and Shaduf result in thousands of depleted channels.
支付渠道网络（PCNs）已被强调为解决当前无许可区块链中可扩展性问题的可行解决方案。它们促进了链下交易，大大减轻了区块链的负担。然而，在同一方向上广泛重复使用多跳路由会带来信道耗尽的风险，导致相关信道变得单向甚至关闭，从而损害多氯化萘的可持续性和可扩展性。更令人担忧的是，现有的再平衡协议解决方案严重依赖于信任假设和脚本语言，导致通用性和可靠性受损。
在本文中，我们提出了Horcrux，这是一种通用且高效的多方虚拟通道协议，不依赖于额外的信任假设、脚本语言或永久在线要求。魂器使用一种称为textit{流中立性}的新方法从根本上解决了信道耗尽问题，该方法最大限度地减少了多跳支付（MHP）期间对信道平衡分配的影响。此外，我们通过在全局通用可组合性框架内对魂器进行建模，将其安全属性形式化，并提供正式的安全证明。
我们在由10529个节点和38910个通道组成的真实闪电网络数据集上实现了魂器，并将其与Shaduf[NDSS'22]、Thora[CCS'22]和Revive[CCS'17]等最先进的再平衡方案进行了比较。实验结果表明：（1）魂器的整个工艺成本低于1美元，明显低于Shaduf；（2） 魂器的支付成功率提高了12%-30%$，渠道所需的用户存款减少了70%-91%$；（3） 在长期运营下，魂器的性能提高了1.2倍至1.5倍；（4）魂器保持几乎为零的通道耗尽率，而Revive和Shaduf都会导致数千个通道耗尽。
Pdf下载链接:
https://www.ndss-symposium.org/wp-content/uploads/2025-495-paper.pdf