Quartz: A Framework for Engineering Secure Smart Contracts

semanticscholar(2020)

引用 0|浏览23
暂无评分
摘要
We present Quartz, a language and framework for developing and validating smart contracts. A user writes a Quartz contract as an extended finite-state machine in a domain-specific language.Quartz translates this description into a formal specification in TLA+. The specification captures both the contract’s logic and the execution semantics of the blockchain. Quartz uses bounded model checking to automatically determine if a contract adheres to user-defined properties. Once validated, the contract’s author uses Quartz to generate a Solidity implementation for deployment on a blockchain. We used a survey of 16 contract case studies, drawn from a variety of domains, to motivate the design of Quartz’s DSL and to evaluate its effectiveness. We show that Quartz contracts are consistently more concise than handwritten Solidity equivalents. We present two in-depth case studies where Quartz identifies multiple significant contract vulnerabilities and provides useful execution traces to assist the developer in addressing them. Finally, we demonstrate that Quartz imposes only modest overhead in terms of generated code size and execution efficiency over handwritten Solidity. Quartz is able to automatically verify functional, contract-specific properties. It is the first tool of this type that detects vulnerabilities arising from interactions with external code, such as reentrancy.
更多
查看译文
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络
Chat Paper
正在生成论文摘要