A Security Type Verifier For Smart Contracts
COMPUTERS & SECURITY(2021)
摘要
The widespread adoption of smart contracts demands strong security guarantees. Our work is motivated by the problem of statically checking potential information tampering in smart contracts. This paper presents a security type verification framework for smart contracts based on type systems. We introduce a formal calculus for reasoning smart contract operations and interactions and design a lightweight type system for checking secure information flow in Solidity (a popular high-level programming language for writing smart contracts). The soundness of our type system is proved w.r.t. non-interference. In addition, a type verifier based on our type system is proposed to assist users to automatically find an optimal secure type assignment for state variables, which makes contracts well-typed. We also prove that finding the optimal secure type assignment is theoretically a NP-complete problem. We develop a prototype implementation of the Solidity Type Verifier (STV) including the Solidity Type Checker (STC) based on the K-framework, and demonstrate its effectiveness on real world smart contracts. (C) 2021 Elsevier Ltd. All rights reserved.
更多查看译文
关键词
Smart contracts, Information-flow integrity, Type system, Soundness proofs, K-framework
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要