Quartz: A Framework for Engineering Secure Smart Contracts

John Kolb, John Yang, Randy H. Katz and David E. Culler

EECS Department
University of California, Berkeley
Technical Report No. UCB/EECS-2020-178
August 31, 2020

http://www2.eecs.berkeley.edu/Pubs/TechRpts/2020/EECS-2020-178.pdf

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.


BibTeX citation:

@techreport{Kolb:EECS-2020-178,
    Author = {Kolb, John and Yang, John and Katz, Randy H. and Culler, David E.},
    Title = {Quartz: A Framework for Engineering Secure Smart Contracts},
    Institution = {EECS Department, University of California, Berkeley},
    Year = {2020},
    Month = {Aug},
    URL = {http://www2.eecs.berkeley.edu/Pubs/TechRpts/2020/EECS-2020-178.html},
    Number = {UCB/EECS-2020-178},
    Abstract = {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.}
}

EndNote citation:

%0 Report
%A Kolb, John
%A Yang, John
%A Katz, Randy H.
%A Culler, David E.
%T Quartz: A Framework for Engineering Secure Smart Contracts
%I EECS Department, University of California, Berkeley
%D 2020
%8 August 31
%@ UCB/EECS-2020-178
%U http://www2.eecs.berkeley.edu/Pubs/TechRpts/2020/EECS-2020-178.html
%F Kolb:EECS-2020-178