| 引用本文： |
-
许颖,张亚丰,许晶航,康跃馨,夏清,袁峰,左春,李玉成.基于CompCert内存模型的智能合约中间语言的可信编译[J].信息安全学报,已采用 [点击复制]
- XU Ying,ZHANG Yafeng,XU Jinghang,KANG Yuexin,XIA Qing,YUAN Feng,ZUO Chun,LI Yucheng.Trusted Compilation of Smart Contract Intermediate Language Based on the CompCert Memory Model[J].Journal of Cyber Security,Accept [点击复制]
|
|
| |
|
|
| 本文已被：浏览 604次 下载 0次 |
|
| 基于CompCert内存模型的智能合约中间语言的可信编译 |
|
许颖1, 张亚丰2, 许晶航2, 康跃馨2, 夏清2, 袁峰3, 左春4, 李玉成2
|
|
|
| (1.中国科学院软件研究所并行软件与计算科学实验室和中国科学院大学计算机科学与技术学院;2.中国科学院软件研究所并行软件与计算科学实验室;3.广州软件应用技术研究院;4.中科软科技股份有限公司) |
|
| 摘要: |
| 智能合约是区块链技术的重要组成部分之一，具有不可篡改、自动执行等特点，为去中心化应用提供了丰富的编程基础。近年来相关安全漏洞事件频发，使得智能合约的安全性研究逐渐成为热点。其中，智能合约编译器的误编译问题会令源代码编译产生不符合开发者原本预期的目标代码，导致部署在区块链上的代码存在安全隐患，然而现有工作较少考虑到这一问题。因此，首先从避免合约安全漏洞的原则出发，设计一种非图灵完备的智能合约领域专用语言isCL。作为可信编译的源语言，它支持复合数据类型与内置函数，以便于开发人员编写合约；然后设计可信编译器i2c的整体架构，实现以C语言子集Clight语言为目标语言的完整翻译过程；再针对基于CompCert内存模型的智能合约中间语言的翻译阶段，定义消除复合类型、出参入参合并、生成Clight三个翻译阶段的相关语法、语义，并给出语义保持性的证明思路；最后通过服装供应链分账应用实例和Solidity、Rust的编译漏洞案例来分别说明isCL语言的实用性与智能合约可信编译的有效性。本文工作为智能合约的可信编译提供了研究思路，有利于促进智能合约开发的安全性研究，为实现更加安全可信的区块链应用提供有力支撑。 |
| 关键词: 区块链 智能合约语言 领域专用语言 形式化验证 经过验证的编译器 |
| DOI： |
| 投稿时间：2024-02-04修订日期：2024-07-24 |
| 基金项目:国家重点研发计划 |
|
| Trusted Compilation of Smart Contract Intermediate Language Based on the CompCert Memory Model |
|
XU Ying1, ZHANG Yafeng2, XU Jinghang2, KANG Yuexin2, XIA Qing2, YUAN Feng3, ZUO Chun4, LI Yucheng2
|
| (1.Laboratory of Parallel Software and Computational Science, Institute of Software, Chinese Academy of Sciences and School of Computer Science and Technology, University of Chinese Academy of Science;2.Laboratory of Parallel Software and Computational Science, Institute of Software, Chinese Academy of Sciences;3.Institute of Software Application Technology, Guangzhou;4.Sinosoft Co., Ltd.) |
| 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 fre-quent 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. How-ever, 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 vulnera-bilities. 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 com-piler, 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 CompCert memory model, we define the relevant syntax and semantics for three translation stages: eliminating compo-site 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 isCL 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 compi-lation 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 |
|
|
|
|
|
