区块链论文速读A会-ISSTA 2023（1/2）法律协议如何变成智能合约代码？

Conference：ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA)

CCF level：CCF A

Categories：Software Engineering/System Software/Programming Languages

Year：2023

Title:

Automated Generation of Security-Centric Descriptions for Smart Contract Bytecode

自动生成以智能合约字节码安全为中心的描述

Authors:

Key words:

decentralized apps; smart contracts; textual description; program analysis; natural language generation

去中心化应用；智能合约；文本描述；程序分析；自然语言生成

Abstract:

Smart contract and DApp users are taking great risks, as they do not obtain necessary knowledge that can help them avoid using vulnera- ble and malicious contract code. In this paper, we develop a novel system Tx2TXT that can automatically create security-centric textual descriptions directly from smart contract bytecode. To capture the security aspect of financial applications, we formally define a funds transfer graph to model critical funds flows in smart contracts. To ensure the expressiveness and conciseness of the descriptions de- rived from these graphs, we employ a GCN-based model to identify security-related condition statements and selectively add them to our graph models. To convert low-level bytecode instructions to human- readable textual scripts, we leverage robust API signatures to recover bytecode semantics. We have evaluated Tx2TXT on 890 well-labeled vulnerable, malicious and safe contracts where developer-crafted descriptions are available. Our results have shown that Tx2TXT out- performs state-of-the-art solutions and can effectively help end users avoid risky contracts

智能合约和 DApp 用户承担着巨大的风险，因为他们没有获得必要的知识来帮助他们避免使用易受攻击和恶意的合约代码。在本文中，我们开发了一个新颖的系统 Tx2TXT，该系统可以直接从智能合约字节码自动创建以安全为中心的文本描述。为了捕捉金融应用程序的安全性，我们正式定义了一个资金转移图来模拟智能合约中的关键资金流动。为了确保从这些图中得出的描述的表达性和简洁性，我们采用基于 GCN 的模型来识别与安全相关的条件语句并有选择地将它们添加到我们的图模型中。为了将低级字节码指令转换为人类可读的文本脚本，我们利用强大的 API 签名来恢复字节码语义。我们已经在 890 个标记良好的易受攻击、恶意和安全合约上评估了 Tx2TXT，这些合约都有开发人员精心制作的描述。我们的结果表明，Tx2TXT 的表现优于最先进的解决方案，可以有效地帮助最终用户避免有风险的合约

Pdf link:

https://dl.acm.org/doi/10.1145/3597926.3598132

Title:

Beyond “Protected” and “Private”: An Empirical Security Analysis of Custom Function Modifiers in Smart Contracts

超越“受保护”和“隐私”：智能合约中自定义函数修饰符的实证安全性分析

Authors:

Key words:

Smart Contract Security, Taint Analysis, Access Control, Modifiers

智能合约安全、污点分析、访问控制、修饰符

Abstract:

A smart contract is a piece of application-layer code running on blockchain ledgers and it provides programmatic logic via transaction-based execution of pre-defined functions. Smart contract functions are by default invokable by any party. To safeguard them, the mainstream smart contract language, i.e., Solidity of the popular Ethereum blockchain, proposed a unique language-level keyword called “modifier,” which allows developers to define custom function access control policies beyond the traditional “protected” and “private” modifiers in classic programming languages.

In this paper, we aim to conduct a large-scale security analysis of the modifiers used in real-world Ethereum smart contracts. To achieve this, we design and implement a novel smart contract analysis tool called SoMo. Its main objective is to identify insecure modifiers that can be bypassed from one or more unprotected smart contract functions. This is challenging because of the complicated relationship between modifiers and their variables/functions and the ambiguity of attacker-accessible entry functions. To overcome them, we first propose a new structure, the Modifier Dependency Graph (MDG), to connect all the modifier-related control/data flows. Over MDGs, we then model system variables, generate symbolic path constraints, and iteratively test each candidate entry function. Our extensive evaluation shows that SoMo outperforms the state-of-the-art SPCon tool by detecting all its true positives and correctly avoiding 9 out of 11 false positives. It also achieves high precision of 91.2% when analyzing a large dataset of 62,464 contracts, over 400 of which were identified with bypassable modifiers. Our analysis further reveals three interesting security findings about modifiers and nine major types of modifier usage in the wild. SoMo has been integrated into an online security scanning service, MetaScan.

智能合约是运行在区块链账本上的一段应用层代码，它通过基于交易的预定义函数执行提供编程逻辑。默认情况下，任何一方都可以调用智能合约函数。为了保护它们，主流智能合约语言，即流行的以太坊区块链的 Solidity，提出了一个独特的语言级关键字“modifier”，它允许开发人员定义自定义函数访问控制策略，超越传统编程语言中传统的“protected”和“private”修饰符。

在本文中，我们旨在对现实世界中以太坊智能合约中使用的修饰符进行大规模安全分析。为此，我们设计并实现了一种名为 SoMo 的新型智能合约分析工具。其主要目标是识别可以从一个或多个不受保护的智能合约函数中绕过的不安全修饰符。这很有挑战性，因为修饰符与其变量/函数之间的关系很复杂，而且攻击者可访问的入口函数很模糊。为了克服这些问题，我们首先提出了一种新结构，即修饰符依赖图 (MDG)，以连接所有与修饰符相关的控制/数据流。然后，我们在 MDG 上对系统变量进行建模，生成符号路径约束，并迭代测试每个候选输入函数。我们进行的广泛评估表明，SoMo 的表现优于最先进的 SPCon 工具，因为它可以检测到所有真阳性，并正确避免了 11 个假阳性中的 9 个。在分析 62,464 份合同的大型数据集时，它还实现了 91.2% 的高精度，其中 400 多个合同被识别为具有可绕过的修饰符。我们的分析进一步揭示了有关修饰符的三个有趣的安全发现和九种主要的修饰符使用类型。SoMo 已集成到在线安全扫描服务 MetaScan 中。

Pdf link:

https://dl.acm.org/doi/10.1145/3597926.3598125

Title:

Definition and Detection of Defects in NFT Smart Contracts

NFT 智能合约缺陷的定义及检测

Authors:

Key words:

smart contracts, NFTs, defects definition and detection, symbolic execution

智能合约、NFT、缺陷定义和检测、符号执行

Abstract:

Recently, the birth of non-fungible tokens (NFTs) has attracted great attention. NFTs are capable of representing users’ ownership on the blockchain and have experienced tremendous market sales due to their popularity. Unfortunately, the high value of NFTs also makes them a target for attackers. The defects in NFT smart contracts could be exploited by attackers to harm the security and reliability of the NFT ecosystem. Despite the significance of this issue, there is a lack of systematic work that focuses on analyzing NFT smart contracts, which may raise worries about the security of users’ NFTs. To address this gap, in this paper, we introduce 5 defects in NFT smart contracts. Each defect is defined and illustrated with a code example highlighting its features and consequences, paired with possible solutions to fix it. Furthermore, we propose a tool named NFTGuard to detect our defined defects based on a symbolic execution framework. Specifically, NFTGuard extracts the information of the state variables from the contract abstract syntax tree (AST), which is critical for identifying variable-loading and storing operations during symbolic execution. Furthermore, NFTGuard recovers source-code-level features from the bytecode to effectively locate defects and report them based on predefined detection patterns. We run NFTGuard on 16,527 real-world smart contracts and perform an evaluation based on the manually labeled results. We find that 1,331 contracts contain at least one of the 5 defects, and the overall precision achieved by our tool is 92.6%.

最近，非同质化代币（NFT）的诞生引起了极大的关注。NFT 能够代表用户在区块链上的所有权，并且由于其受欢迎程度而经历了巨大的市场销售。不幸的是，NFT 的高价值也使它们成为攻击者的目标。攻击者可以利用 NFT 智能合约中的缺陷来损害 NFT 生态系统的安全性和可靠性。尽管这个问题很重要，但缺乏专注于分析 NFT 智能合约的系统工作，这可能会引发对用户 NFT 安全性的担忧。为了解决这一空白，在本文中，我们介绍了 NFT 智能合约中的 5 个缺陷。每个缺陷都用一个代码示例来定义和说明，突出显示其特征和后果，并附上可能的修复解决方案。此外，我们提出了一个名为 NFTGuard 的工具来基于符号执行框架检测我们定义的缺陷。具体来说，NFTGuard 从合约抽象语法树（AST）中提取状态变量的信息，这对于识别符号执行期间的变量加载和存储操作至关重要。此外，NFTGuard 从字节码中恢复源代码级特征，以有效定位缺陷并根据预定义的检测模式报告它们。我们在 16,527 个真实智能合约上运行 NFTGuard，并根据手动标记的结果进行评估。我们发现 1,331 个合约至少包含 5 个缺陷中的一个，我们的工具实现的整体精度为 92.6%。

Pdf link:

https://dl.acm.org/doi/10.1145/3597926.3598063

Title:

iSyn: Semi-automated Smart Contract Synthesis from Legal Financial Agreements

iSyn：基于合法金融协议的半自动化智能合约合成

Authors:

Key words:

Smart Contracts; Program Synthesis; Natural Language Processing

智能合约；程序合成；自然语言处理

Abstract:

Embracing software-driven smart contracts to fulfill legal agreements is a promising direction for digital transformation in the legal sector. Existing solutions mostly consider smart contracts as simple add-ons, without leveraging the programmability of smart contracts to realize complex semantics of legal agreements. In this paper, we propose iSyn, the first end-to-end system that synthesizes smart contracts to fulfill the semantics of financial legal agreements, with minimal human interventions. The design of iSyn centers around a novel intermediate representation (SmartIR) that closes the gap between the natural language sentences and smart contract statements. Specifically, iSyn includes a synergistic pipeline that unifies multiple NLP-techniques to accurately construct SmartIR instances given legal agreements, and performs template-based synthesis based on the SmartIR instances to synthesize smart contracts. We also design a validation framework to verify the correctness and detect known vulnerabilities of the synthesized smart contracts.We evaluate iSyn using legal agreements centering around financial transactions. The results show that iSyn-synthesized smart contracts are syntactically similar and semantically correct (or within a few edits), compared with the “ground truth” smart contracts manually developed by inspecting the legal agreements.

采用软件驱动的智能合约来履行法律协议是法律领域数字化转型的一个有希望的方向。现有的解决方案大多将智能合约视为简单的附加组件，而没有利用智能合约的可编程性来实现法律协议的复杂语义。在本文中，我们提出了 iSyn，这是第一个端到端系统，它可以合成智能合约以履行金融法律协议的语义，同时尽量减少人工干预。iSyn 的设计围绕一种新颖的中间表示 (SmartIR) 展开，它缩小了自然语言句子和智能合约语句之间的差距。具体来说，iSyn 包含一个协同管道，它统一了多种 NLP 技术，以根据法律协议准确构建 SmartIR 实例，并根据 SmartIR 实例执行基于模板的合成以合成智能合约。我们还设计了一个验证框架来验证合成智能合约的正确性并检测已知的漏洞。我们使用以金融交易为中心的法律协议来评估 iSyn。结果表明，与通过检查法律协议手动开发的“基本事实”智能合约相比，iSyn 合成的智能合约在语法上相似且语义上正确（或在几次编辑之内）。

Pdf link:

https://dl.acm.org/doi/10.1145/3597926.3598091

Title:

ItyFuzz: Snapshot-Based Fuzzer for Smart Contract

ItyFuzz：基于快照的智能合约模糊测试器

Authors:

Key words:

fuzzing, on-chain testing, smart contract, blockchain, DeFi security

模糊测试、链上测试、智能合约、区块链、DeFi 安全

Abstract:

Smart contracts are critical financial instruments, and their security is of utmost importance. However, smart contract programs are difficult to fuzz due to the persistent blockchain state behind all transactions. Mutating sequences of transactions are complex and often lead to a suboptimal exploration for both input and program spaces. In this paper, we introduce a novel snapshot-based fuzzer ItyFuzz for testing smart contracts. In ItyFuzz, instead of storing sequences of transactions and mutating from them, we snapshot states and singleton transactions. To explore interesting states, ItyFuzz introduces a dataflow waypoint mechanism to identify states with more potential momentum. ItyFuzz also incorporates comparison waypoints to prune the space of states. By maintaining snapshots of the states, ItyFuzz can synthesize concrete exploits like reentrancy attacks quickly. Because ItyFuzz has second-level response time to test a smart contract, it can be used for on-chain testing, which has many benefits compared to local development testing. Finally, we evaluate ItyFuzz on real-world smart contracts and some hacked on-chain DeFi projects. ItyFuzz outperforms existing fuzzers in terms of instructional coverage and can find and generate realistic exploits for on-chain projects quickly.

智能合约是重要的金融工具，其安全性至关重要。然而，由于所有交易背后都存在持久的区块链状态，因此智能合约程序很难进行模糊测试。交易序列的变异非常复杂，通常会导致对输入和程序空间的探索都不够理想。在本文中，我们介绍了一种基于快照的新型模糊测试器 ItyFuzz，用于测试智能合约。在 ItyFuzz 中，我们不是存储交易序列并从中进行变异，而是对状态和单例交易进行快照。为了探索有趣的状态，ItyFuzz 引入了一种数据流航点机制来识别具有更多潜在动量的状态。ItyFuzz 还结合了比较航点来修剪状态空间。通过维护状态快照，ItyFuzz 可以快速合成具体的漏洞利用，例如重入攻击。由于 ItyFuzz 具有秒级响应时间来测试智能合约，因此它可以用于链上测试，与本地开发测试相比，这有很多好处。最后，我们在现实世界的智能合约和一些被黑客入侵的链上 DeFi 项目上对 ItyFuzz 进行了评估。ItyFuzz 在指令覆盖范围方面优于现有的模糊器，并且可以快速找到并生成针对链上项目的实际漏洞利用。