The rise of programmable open distributed consensus platforms based on the blockchain technology has aroused a lot of interest in replicated stateful computations, aka smart contracts. As blockchains are used predominantly in financial applications, smart contracts frequently manage millions of dollars worth of virtual coins. Since smart contracts cannot be updated once deployed, the ability to reason about their correctness becomes a critical task. Yet, the de facto implementation standard, pioneered by the Ethereum platform, dictates smart contracts to be deployed in a low-level language, which renders independent audit and formal verification of deployed code infeasible in practice.
We report an ongoing experiment held with an industrial blockchain vendor on designing, evaluating, and deploying Scilla, a new programming language for safe smart contracts. Scilla is positioned as an intermediate-level language, suitable to serve as a compilation target and also as an independent programming framework. Taking System F as a foundational calculus, Scilla offers strong safety guarantees by means of type soundness. It provides a clean separation between pure computational, state-manipulating, and communication aspects of smart contracts, avoiding many known pitfalls due to execution in a byzantine environment. We describe the motivation, design principles, and semantics of Scilla, and we report on Scilla use cases provided by the developer community. Finally, we present a framework for lightweight verification of Scilla programs, and showcase it with two domain-specific analyses on a suite of real-world use cases.
Thu 24 OctDisplayed time zone: Beirut change
11:00 - 12:30
|DeepSEA: A Language for Certified System Software|
Vilhelm Sjöberg Yale University, Yuyang Sang Yale University, Shu-chun Weng Yale University, Zhong Shao Yale UniversityDOI Pre-print
Conrad Watt University of Cambridge, Andreas Rossberg Dfinity Stiftung, Jean Pichon-Pharabod University of CambridgeDOI
|Safer Smart Contract Programming with Scilla|
Ilya Sergey Yale-NUS College and National University of Singapore, Vaivaswatha Nagaraj Zilliqa Research, Jacob Johannsen Zilliqa Research, Amrit Kumar Zilliqa Research, Anton Trunov Zilliqa Research, Ken Chan Zilliqa ResearchDOI Pre-print File Attached
|Scala Implicits Are Everywhere: A Large-Scale Study of the Use of Scala Implicits in the Wild|
Filip Křikava Czech Technical University, Heather Miller Carnegie Mellon University, Jan Vitek Northeastern UniversityDOI Pre-print