| 摘要: |
| 智能合约是区块链技术的重要组成部分之一,具有不可篡改、自动执行等特点,为去中心化应用提供了丰富的编程基础。近年来相关安全漏洞事件频发,使得智能合约的安全性研究逐渐成为热点。其中,智能合约编译器的误编译问题会令源代码编译产生不符合开发者原本预期的目标代码,导致部署在区块链上的代码存在安全隐患,然而现有工作较少考虑到这一问题。因此,首先从避免合约安全漏洞的原则出发,设计一种非图灵完备的智能合约领域专用语言isCL。作为可信编译的源语言,它支持复合数据类型与内置函数,以便于开发人员编写合约;然后设计可信编译器i2c的整体架构,实现以C语言子集Clight语言为目标语言的完整翻译过程;再针对基于CompCert内存模型的智能合约中间语言的翻译阶段,定义消除复合类型、出参入参合并、生成Clight三个翻译阶段的相关语法、语义,并给出语义保持性的证明思路;最后通过服装供应链分账应用实例和Solidity、Rust的编译漏洞案例来分别说明isCL语言的实用性与智能合约可信编译的有效性。本文工作为智能合约的可信编译提供了研究思路,有利于促进智能合约开发的安全性研究,为实现更加安全可信的区块链应用提供有力支撑。 |
| 关键词: 区块链 智能合约语言 领域专用语言 形式化验证 经过验证的编译器 |
| DOI：10.19363/J.cnki.cn10-1380/tn.2026.01.03 |
| Received:February 04, 2024Revised:July 24, 2024 |
| 基金项目:国家重点研发计划(No.2022YFB2702202)资助。 |
|
| Trusted Compilation of Smart Contract Intermediate Language Based on the CompCert Memory Model |
| XU Ying,ZHANG Yafeng,XU Jinghang,KANG Yuexin,XIA Qing,YUAN Feng,ZUO Chun,LI Yucheng |
| Laboratory of Parallel Software and Computational Science, Institute of Software, Chinese Academy of Sciences, Beijing 100190, China;School of Computer Science and Technology, University of Chinese Academy of Sciences, Beijing 100049, China;Laboratory of Parallel Software and Computational Science, Institute of Software, Chinese Academy of Sciences, Beijing 100190, China;Key Laboratory of Systems Software and State Key Laboratory of Computer Science, Institute of Software, Chinese Academy of Sciences, Beijing 100190, China;Institute of Software Application Technology, Guangzhou, Guangzhou 511458, China;Sinosoft Co., Ltd., Beijing 100190, China |
| Abstract: |
| Smart contracts are one of the critical components of blockchain technology, characterized by their immutability and automatic execution, providing a rich programming foundation for decentralized applications. In recent years, the frequent occurrence of security vulnerabilities has made the security research of smart contracts a hot topic.Among these issues, the problem of miscompilation by smart contract compilers can result in the generation of target code that does not meet the original expectations of developers, leading to security risks in the code deployed on the blockchain.However, existing works has seldom considered this issue. To tackle this problem, we first designed a non-Turing-complete domain-specific language for smart contracts, named isCL, based on the principle of avoiding contract security vulnerabilities. To serve as a trusted source language for compilation, isCL supports composite data types and built-in functions to facilitate developers in writing smart contracts. Following this, we designed the overall architecture of a trusted compiler, i2c, which implements a complete translation process into the Clight language, a subset of the C language, as the target language. Furthermore, focusing on the translation phase of the smart contract intermediate language based on the Comp Cert memory model, we define the relevant syntax and semantics for three translation stages:eliminating composite types, merging input and output parameters, and generating Clight, then provided the proof idea for semantic preservation in these stages. Finally, to demonstrate the practicality of the is CL language and the effectiveness of trusted compilation for smart contracts, we presented a case study of a clothing supply chain ledger application and examined compilation vulnerability cases in Solidity and Rust. This work provides a research approach for the trustworthy compilation of smart contracts, which is beneficial to the security research of smart contract development. It offers strong support for achieving more secure and trustworthy blockchain applications. |
| Key words: blockchain smart contract formal verification theorem proving verified compiler |
