Modeling, Specification and Verification of Smart Contract Applications

Smart contracts are programs which run in a blockchain network. They manage access to resources that are stored on the blockchain, such as cryptocurrencies or tokens representing real-world assets. Smart contracts are unique in that they allow anyone to run a program on a different computer, while still being certain about the execution semantics, and about what source code is being executed. This comes at the price of immutability: Once deployed, the source code smart contracts generally cannot be changed. Furthermore, the source code, including possible programming errors, is usually publicly available. 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.
Indeed, formal analysis of smart contracts has been a very active research area. Many tools for static analysis and formal verification of different classes of properties have been developed. However, a long and ongoing history of vulnerabilities and exploits of smart contract applications shows that security in this field is very much a pressing issue. ... mehrIn the domain of smart contract applications, correctness properties are highly application specific, which places them out of reach of static analysis tools. Existing tools for formal verification, where developers can provide a specification, still lack the mechanisms to express many typical correctness and security properties.
In my thesis, I contribute to the field of formal methods for smart contracts by creating 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.