Scilla: a Smart Contract Intermediate-Level LAnguage
arXiv:1801.00687
Abstract
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.
12 pages
References in corpus (1)
Cited by in corpus (13)
- A comprehensive survey on smart contract construction and execution: paradigms, tools, and systems
- A Survey on Ethereum Systems Security: Vulnerabilities, Attacks and Defenses
- Security Analysis Methods on Ethereum Smart Contract Vulnerabilities: A Survey
- ConCert: A Smart Contract Certification Framework in Coq
- Using Fault Injection to Assess Blockchain Systems in Presence of Faulty Smart Contracts
- Flint for Safer Smart Contracts
- A Revisit on Blockchain-based Smart Contract Technology
- WhylSon: Proving your Michelson Smart Contracts in Why3
- Implementation of Smart Contracts Using Hybrid Architectures with On- and Off-Blockchain Components
- A Hybrid Formal Verification System in Coq for Ensuring the Reliability and Security of Ethereum-based Service Smart Contracts
- Smart Contract Design Meets State Machine Synthesis: Case Studies
- Pluralize: a Trustworthy Framework for High-Level Smart Contract-Draft
- Compiling a Higher-Order Smart Contract Language to LLVM