2018/01/02 by Ilya Sergey, Amrit Kumar, Sergey, Ilya +3 · 1 voice · 5 citations
Computer Science · #Security and Verification in Computing #Formal Methods in Verification #Logic, programming, and type systems
paper · pdf · doi:10.48550/arxiv.1801.00687
This paper outlines key design principles of Scilla---an intermediate-level language for verified smart contracts. Scilla provides a clean separation between the communication aspect of smart contracts on a blockchain, allowing for the rich interaction patterns, and a programming component, which enjoys principled semantics and is amenable to formal verification. Scilla is not meant to be a high-level programming language, and we are going to use it as a translation target for high-level languages, such as Solidity, for performing program analysis and verification, before further compilation to an executable bytecode. We describe the automata-based model of Scilla, present its programming component and show how contract definitions in terms of automata streamline the process of mechanised verification of their safety and temporal properties.