Scar: Verification-Based Development of Smart Contracts (Tool Paper)

Compared to other kinds of computer programs, smart contracts have some unique characteristics, e.g., immutability, and the public availability of source code. This means that any vulnerability has a large probability of being exploited. Since smart contracts cannot be patched, it is very important that smart contracts are correct and secure upon deployment. While much research has been invested in this goal, smart contract correctness and security remains a challenging problem.
In this paper, we present the Scar approach for model-driven development of correct and secure smart contract applications. Before implementing an application, smart contract developers first describe it in terms of an intuitive, platform-agnostic metamodel. Within this model, they can also specify high-level security and behavioral correctness properties, and check whether the model contains any inconsistencies. Finally, a combination of code generation, static analyses, and formal verification of automatically generated formal annotations leads to an implementation that is correct and secure w.r.t. the initial model.