Ilya Sergey
Vaivaswatha Nagaraj
Skip Abstract Section
Skip Supplemental Material SectionAbstract
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.
Supplemental Material
- Elvira Albert, Puri Arenas, Samir Genaim, and Germán Puebla. 2008. Automatic Inference of Upper Bounds for Recurrence Relations in Cost Analysis. In SAS (LNCS), Vol. 5079. Springer, 221–237.Google Scholar
- Gabriel Alfour. 2019. Introducing LIGO: a new smart contract language for Tezos. https://medium.com/tezos/introducingligo-a-new-smart-contract-language-for-tezos-233fa17f21c7 .Google Scholar
- JD Alois. 2017. Ethereum Parity Hack May Impact ETH 500,000 or $146 Million. https://www.crowdfundinsider.com/2017/ 11/124200-ethereum-parity-hack-may-impact-eth-500000-146-million/ .Google Scholar
- Leonardo Alt and Christian Reitwießner. 2018. SMT-Based Verification of Solidity Smart Contracts. In ISoLA (LNCS), Vol. 11247. Springer, 376–388.Google Scholar
- Sidney Amani, Myriam Bégel, Maksym Bortin, and Mark Staples. 2018. Towards verifying Ethereum smart contract bytecode in Isabelle/HOL. In CPP. ACM, 66–77.Google Scholar
- Nada Amin and Tiark Rompf. 2017. Type soundness proofs with definitional interpreters. In POPL. ACM, 666–679.Google Scholar
- Nicola Atzei, Massimo Bartoletti, and Tiziana Cimoli. 2017. A Survey of Attacks on Ethereum Smart Contracts (SoK). In POST (LNCS), Vol. 10204. Springer, 164–186.Google Scholar
- Shehar Bano, Alberto Sonnino, Mustafa Al-Bassam, Sarah Azouvi, Patrick McCorry, Sarah Meiklejohn, and George Danezis. 2017. Consensus in the Age of Blockchains. CoRR abs/1711.03936 (2017).Google Scholar
- Kshitij Bansal, Eric Koskinen, and Omer Tripp. 2018. Automatic Generation of Precise and Useful Commutativity Conditions. In TACAS (LNCS), Vol. 10805. Springer, 115–132.Google Scholar
- Karthikeyan Bhargavan, Antoine Delignat-Lavaud, Cédric Fournet, Anitha Gollamudi, Georges Gonthier, Nadim Kobeissi, Natalia Kulatova, Aseem Rastogi, Thomas Sibut-Pinote, Nikhil Swamy, and Santiago Zanella-Béguelin. 2016. Formal Verification of Smart Contracts: Short Paper. In PLAS. ACM, 91–96.Google Scholar
- Bitcoin Wiki. 2017. Bitcoin Script. https://en.bitcoin.it/wiki/Script , accessed on Apr 5, 2019.Google Scholar
- Sam Blackshear, Evan Cheng, David L. Dill, Victor Gao, Ben Maurer, Todd Nowacki, Alistair Pott, Shaz Qadeer, Rain, Dario Russi, Stephane Sezer, Tim Zakian, and Runtian Zhou. 2019. Move: A Language With Programmable Resources. https://developers.libra.org/docs/assets/papers/libra-move-a-language-with-programmable-resources.pdf .Google Scholar
- Jialiang Chang, Bo Gao, Hao Xiao, Jun Sun, and Zijiang Yang. 2018. sCompile: Critical Path Identification and Analysis for Smart Contracts. CoRR abs/1808.00624 (2018).Google Scholar
- Arthur Charguéraud. 2013. Pretty-Big-Step Semantics. In ESOP (LNCS), Vol. 7792. Springer, 41–60.Google Scholar
- Ting Chen, Xiaoqi Li, Xiapu Luo, and Xiaosong Zhang. 2017. Under-optimized smart contracts devour your money. In IEEE 24th International Conference on Software Analysis, Evolution and Reengineering, SANER. IEEE Computer Society, 442–446.Google ScholarCross Ref
- Michael Coblenz. 2017. Obsidian: A Safer Blockchain Programming Language. In ICSE (Companion). IEEE Press, 97–99.Google Scholar
- Coq Development Team. 2019. The Coq Proof Assistant Reference Manual - Version 8.9. http://coq.inria.fr .Google Scholar
- Patrick Cousot and Radhia Cousot. 1977. Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints. In POPL. ACM, 238–252.Google ScholarDigital Library
- Olivier Danvy. 2019. Folding left and right over Peano numbers. J. Funct. Program. 29 (2019), e6.Google ScholarCross Ref
- Olivier Danvy and Andrzej Filinski. 1990. Abstracting Control. In LISP and Functional Programming. 151–160.Google Scholar
- Olivier Danvy and Andrzej Filinski. 1992. Representing Control: A Study of the CPS Transformation. Mathematical Structures in Computer Science 2, 4 (1992), 361–391.Google ScholarCross Ref
- Olivier Danvy and J. Michael Spivey. 2007. On Barron and Strachey’s cartesian product function. In ICFP. ACM, 41–46.Google Scholar
- Michael del Castillo. 2016. The DAO Attacked: Code Issue Leads to $60 Million Ether Theft. https://www.coindesk.com/daoattacked-code-issue-leads-60-million-ether-theft/ , accessed on Dec 2, 2017.Google Scholar
- Werner Dietl, Stephanie Dietzel, Michael D. Ernst, Kivanç Muslu, and Todd W. Schiller. 2011. Building and using pluggable type-checkers. In ICSE. ACM, 681–690.Google Scholar
- Ethereum Foundation. 2018a. Decentralized Autonomous Organization. https://www.ethereum.org/dao .Google Scholar
- Ethereum Foundation. 2018b. ERC20 Token Standard. https://theethereum.wiki/w/index.php/ERC20_Token_Standard .Google Scholar
- Ethereum Foundation. 2018c. List of Known Solidity Bugs. https://solidity.readthedocs.io/en/v0.5.7/bugs.html , accessed on Apr 5, 2019.Google Scholar
- Ethereum Foundation. 2018d. Solidity Documentation. http://solidity.readthedocs.io .Google Scholar
- Ethereum Foundation. 2018e. Vyper. https://vyper.readthedocs.io .Google Scholar
- Ethereum Foundation. 2018f. Yul. https://solidity.readthedocs.io/en/latest/yul.html .Google Scholar
- Andrzej Filinski. 1994. Representing Monads. In POPL. ACM Press, 446–457.Google Scholar
- Cormac Flanagan, Amr Sabry, Bruce F. Duba, and Matthias Felleisen. 1993. The Essence of Compiling with Continuations. In PLDI. ACM, 237–247.Google Scholar
- Jean-Yves Girard. 1987. Linear Logic. Theor. Comput. Sci. 50 (1987), 1–102.Google ScholarDigital Library
- Jean-Yves Girard. 1972. Interprétation fonctionnelle et élimination des coupures de l’arithmétique d’ordre supérieur. Ph.D. Dissertation. Université Paris 7.Google Scholar
- Neville Grech, Michael Kong, Anton Jurisevic, Lexi Brent, Bernhard Scholz, and Yannis Smaragdakis. 2018. MadMax: surviving out-of-gas conditions in Ethereum smart contracts. PACMPL 2, OOPSLA (2018), 116:1–116:27.Google ScholarDigital Library
- Ilya Grishchenko, Matteo Maffei, and Clara Schneidewind. 2018. A Semantic Framework for the Security Analysis of Ethereum Smart Contracts. In POST (LNCS), Vol. 10804. Springer, 243–269.Google Scholar
- Shelly Grossman, Ittai Abraham, Guy Golan-Gueta, Yan Michalevsky, Noam Rinetzky, Mooly Sagiv, and Yoni Zohar. 2018. Online detection of effectively callback free objects with applications to smart contracts. PACMPL 2, POPL (2018).Google Scholar
- Emin Gün Sirer. 2016. Reentrancy Woes in Smart Contracts. http://hackingdistributed.com/2016/07/13/reentrancy-woes/Google Scholar
- Robert Harper. 2012. Practical Foundations for Programming Languages. Version 1.32.Google Scholar
- Yoichi Hirai. 2018. Bamboo. https://github.com/pirapira/bamboo .Google Scholar
- Jan Hoffmann, Ankush Das, and Shu-Chun Weng. 2017. Towards automatic resource bound analysis for OCaml. In POPL. ACM, 359–373.Google Scholar
- IOHK Foundation. 2019a. Marlowe: A Contract Language For The Financial World. https://testnet.iohkdev.io/marlowe/ .Google Scholar
- IOHK Foundation. 2019b. Plutus: A Functional Contract Platform. https://testnet.iohkdev.io/plutus/ .Google Scholar
- Mark P. Jones. 1997. First-class Polymorphism with Type Inference. In Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL). ACM, 483–496.Google ScholarDigital Library
- Sukrit Kalra, Seep Goel, Mohan Dhawan, and Subodh Sharma. 2018. Zeus: Analyzing Safety of Smart Contracts. In NDSS.Google Scholar
- Andrew Kennedy. 1997. Relational Parametricity and Units of Measure. In POPL. ACM Press, 442–455.Google Scholar
- Aashish Kolluri, Ivica Nikolić, Ilya Sergey, Aquinas Hobor, and Prateek Saxena. 2018. Exploiting The Laws of Order in Smart Contracts. CoRR abs/1810.11605 (2018). arXiv: 1810.11605Google Scholar
- Johannes Krupp and Christian Rossow. 2018. teEther: Gnawing at Ethereum to Automatically Exploit Smart Contracts. In USENIX Security Symposium. USENIX Association, 1317–1333.Google Scholar
- Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Scott Owens. 2014. CakeML: a verified implementation of ML. In POPL. ACM, 179–192.Google Scholar
- Ralf Lämmel and Simon Peyton Jones. 2003. Scrap your boilerplate: a practical design pattern for generic programming. In Proceedings of the 2003 ACM SIGPLAN International Workshop on Types in Languages Design and Implementation (TLDI). ACM, 26–37.Google ScholarDigital Library
- John Launchbury and Simon L. Peyton Jones. 1994. Lazy Functional State Threads. In Proceedings of the ACM SIGPLAN 1994 Conference on Programming Language Design and Implementation (PLDI). ACM, 24–35.Google Scholar
- James J. Leifer, Gilles Peskine, Peter Sewell, and Keith Wansbrough. 2003. Global abstraction-safe marshalling with hash types. In ICFP. ACM, 87–98.Google Scholar
- Sheng Liang, Paul Hudak, and Mark P. Jones. 1995. Monad Transformers and Modular Interpreters. In POPL. ACM Press, 333–343.Google Scholar
- LSP 2018. Language Server Protocol. https://langserver.org .Google Scholar
- Loi Luu, Duc-Hiep Chu, Hrishi Olickel, Prateek Saxena, and Aquinas Hobor. 2016. Making Smart Contracts Smarter. In CCS. ACM, 254–269.Google Scholar
- Nancy A. Lynch and Mark R. Tuttle. 1989. An Introduction to Input/Output Automata. CWI Quarterly 2 (1989), 219–246.Google Scholar
- Matteo Marescotti, Martin Blicha, Antti E. J. Hyvärinen, Sepideh Asadi, and Natasha Sharygina. 2018. Computing Exact Worst-Case Gas Consumption for Smart Contracts. In ISoLA (LNCS), Vol. 11247. Springer, 450–465.Google Scholar
- Yaron Minsky. 2016. Let syntax, and why you should use it. Blog post, available at https://blog.janestreet.com/let-syntaxand-why-you-should-use-it .Google Scholar
- John C. Mitchell. 2003. Concepts in programming languages. Cambridge University Press.Google Scholar
- Steven S. Muchnick. 1997. Advanced Compiler Design and Implementation. Morgan Kaufmann.Google Scholar
- Satoshi Nakamoto. 2008. Bitcoin: A peer-to-peer electronic cash system. Abailable at http://bitcoin.org/bitcoin.pdf .Google Scholar
- Ivica Nikolić, Aashish Kolluri, Ilya Sergey, Prateek Saxena, and Aquinas Hobor. 2018. Finding The Greedy, Prodigal, and Suicidal Contracts at Scale. In ACSAC. ACM. To appear.Google Scholar
- Russell O’Connor. 2017. Simplicity: A New Language for Blockchains. https://blockstream.com/simplicity.pdf .Google Scholar
- Scott Owens, Magnus O. Myreen, Ramana Kumar, and Yong Kiam Tan. 2016. Functional Big-Step Semantics. In ESOP (LNCS), Vol. 9632. Springer, 589–615.Google Scholar
- Simon L. Peyton Jones. 1987. The Implementation of Functional Programming Languages. Prentice-Hall.Google ScholarDigital Library
- Simon L. Peyton Jones. 2013. Type-Directed Compilation in the Wild: Haskell and Core. In TLCA (LNCS), Vol. 7941. Springer.Google Scholar
- George Pîrlea and Ilya Sergey. 2018. Mechanising Blockchain Consensus. In CPP. ACM, 78–90.Google Scholar
- Robert Pollack. 1990. Implicit Syntax. In Informal Proceedings of First Workshop on Logical Frameworks, Antibes.Google Scholar
- Stuart Popejoy. 2017. The Pact Smart-Contract Language, Revision 1.5. http://kadena.io/docs/Kadena-PactWhitepaper.pdf .Google Scholar
- RChain Cooperative. 2019. Rholang. https://rholang.rchain.coop .Google Scholar
- Christian Reitwiessner. 2017. Babbage—a mechanical smart contract language. Online blog post.Google Scholar
- John C. Reynolds. 1974. Towards a theory of type structure. In Programming Symposium (LNCS), Vol. 19. Springer, 408–423.Google ScholarCross Ref
- John C. Reynolds. 1998. Definitional Interpreters for Higher-Order Programming Languages. Higher-Order and Symbolic Computation 11, 4 (1998), 363–397.Google ScholarDigital Library
- Michael Rodler, Wenting Li, Ghassan O. Karame, and Lucas Davi. 2019. Sereum: Protecting Existing Smart Contracts Against Re-Entrancy Attacks. In NDSS.Google Scholar
- Grigore Rosu. 2018. IELE: A New Virtual Machine for the Blockchain. https://iohk.io/blog/iele-a-new-virtual-machine-forthe-blockchain .Google Scholar
- Franklin Schrans. 2018. Writing Safe Smart Contracts in Flint. Master’s thesis. Imperial College London, Department of Computing.Google Scholar
- Franklin Schrans, Susan Eisenbach, and Sophia Drossopoulou. 2018. Writing safe smart contracts in Flint. In <Programming> (Companion). ACM, 218–219.Google Scholar
- Ilya Sergey, Dominique Devriese, Matthew Might, Jan Midtgaard, David Darais, Dave Clarke, and Frank Piessens. 2013. Monadic Abstract Interpreters. In PLDI. ACM, 399–410.Google Scholar
- Ilya Sergey, Amrit Kumar, and Aquinas Hobor. 2018a. Scilla: a Smart Contract Intermediate-Level LAnguage. CoRR abs/1801.00687 (2018). http://arxiv.org/abs/1801.00687Google Scholar
- Ilya Sergey, Amrit Kumar, and Aquinas Hobor. 2018b. Temporal Properties of Smart Contracts. In ISoLA (LNCS), Vol. 11247. Springer, 323–338.Google Scholar
- Ilya Sergey, Dimitrios Vytiniotis, and Simon L. Peyton Jones. 2014. Modular, higher-order cardinality analysis in theory and practice. In POPL. ACM, 335–348.Google Scholar
- Peter Sestoft. 1996. ML Pattern Match Compilation and Partial Evaluation. In International Seminar on Partial Evaluation, Dagstuhl Castle (LNCS), Vol. 1110. Springer, 446–464.Google Scholar
- Amin Shali and William R. Cook. 2011. Hybrid Partial Evaluation. In OOPSLA. ACM, 375–390.Google Scholar
- Dieter Shirley. 2018. ERC-721. http://erc721.org/ .Google Scholar
- Jeremy Siek. 2012. Big-step, diverging or stuck? http://siek.blogspot.com/2012/07/big-step-diverging-or-stuck.html .Google Scholar
- Jeremy Siek. 2013. Type safety in three easy lemmas. http://siek.blogspot.com/2013/05/type-safety-in-three-easylemmas.html .Google Scholar
- Flora Sun. 2018. UTXO vs Account/Balance Model. Online blog post, available at https://medium.com/@sunflora98/utxovs-account-balance-model-5e6470f4e0cf .Google Scholar
- Nick Szabo. 1994. Smart Contracts. Online manuscript.Google Scholar
- Tezos Foundation. 2018a. Michelson: the language of Smart Contracts in Tezos. http://tezos.gitlab.io/mainnet/whitedoc/ michelson.html .Google Scholar
- Tezos Foundation. 2018b. Liquidity. http://www.liquidity-lang.org/ .Google Scholar
- Sergei Tikhomirov, Ekaterina Voskresenskaya, Ivan Ivanitskiy, Ramil Takhaviev, Evgeny Marchenko, and Yaroslav Alexandrov. 2018. SmartCheck: Static Analysis of Ethereum Smart Contracts. In WETSEB@ICSE. ACM, 9–16.Google Scholar
- Anton Trunov. 2019. A Scilla vs Move case study. Blog post available at https://medium.com/@anton_trunov/a-scilla-vsmove-case-study-afa9b8df5146 .Google Scholar
- Petar Tsankov, Andrei Marian Dan, Dana Drachsler-Cohen, Arthur Gervais, Florian Bünzli, and Martin T. Vechev. 2018. Securify: Practical Security Analysis of Smart Contracts. In CCS. ACM, 67–82.Google Scholar
- Peng Wang. 2019. Type System for Resource Bounds with Type-Preserving Compilation. Ph.D. Dissertation. Massachusetts Institute of Technology.Google Scholar
- Gavin Wood. 2014. Ethereum: A Secure Decentralized Generalised Transaction Ledger.Google Scholar
- Andrew K. Wright and Matthias Felleisen. 1994. A Syntactic Approach to Type Soundness. Inf. Comput. 115, 1 (1994), 38–94.Google ScholarDigital Library
- Zilliqa Team. 2017. The Zilliqa Technical Whitepaper. https://docs.zilliqa.com/whitepaper.pdf Version 0.1.Google Scholar
Index Terms
- Safer smart contract programming with Scilla
Recommendations
Smart Contract Locator (SCL) and Smart Contract Description Language (SCDL)
Service-Oriented Computing – ICSOC 2019 WorkshopsAbstractToday’s blockchain technologies focus mostly on isolated, proprietary technologies, yet there are application scenarios that ask for interoperability, e.g., among blockchains themselves or with external applications. This paper proposes the Smart ...
Smart Contract and Blockchain Based Contract Management System
ECBS 2021: 7th Conference on the Engineering of Computer Based SystemsThis paper presents theoretical and practical research on the possibilities of applying smart contracts in the field of law and a contract management system which allows users to conclude contracts based on blockchain technology. The transition from ...
Towards analyzing the complexity landscape of solidity based ethereum smart contracts
WETSEB '18: Proceedings of the 1st International Workshop on Emerging Trends in Software Engineering for BlockchainThe blockchain based decentralized cryptocurrency platforms are one of the hottest topics in tech at the moment. Though most of the interest is generated by cryptocurrency related activities, it is becoming apparent that a much wider spectrum of ...
Comments