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 Oct Times are displayed in time zone: Beirut change
11:00 - 12:30
|DeepSEA: A Language for Certified System Software|
Vilhelm SjöbergYale University, Yuyang SangYale University, Shu-chun WengYale University, Zhong ShaoYale UniversityDOI Pre-print
Conrad WattUniversity of Cambridge, Andreas RossbergDfinity Stiftung, Jean Pichon-PharabodUniversity of CambridgeDOI
|Safer Smart Contract Programming with Scilla|
Ilya SergeyYale-NUS College and National University of Singapore, Vaivaswatha NagarajZilliqa Research, Jacob JohannsenZilliqa Research, Amrit KumarZilliqa Research, Anton TrunovZilliqa Research, Ken ChanZilliqa ResearchDOI Pre-print File Attached
|Scala Implicits Are Everywhere: A Large-Scale Study of the Use of Scala Implicits in the Wild|
Filip KřikavaCzech Technical University, Heather MillerCarnegie Mellon University, Jan VitekNortheastern UniversityDOI Pre-print