research-article

Open access

Safer smart contract programming with Scilla

Authors:

Vaivaswatha Nagaraj,

Jacob Johannsen,

Ken Chan Guan HaoAuthors Info & Claims

Proceedings of the ACM on Programming Languages, Volume 3, Issue OOPSLA

Article No.: 185, Pages 1 - 30

https://doi.org/10.1145/3360611

Published: 10 October 2019 Publication History

Abstract

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.

Supplementary Material

a185-sergey (a185-sergey.webm)

Presentation at OOPSLA '19

Download
110.19 MB

References

[1]

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.

[2]

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 .

[3]

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/ .

[4]

Leonardo Alt and Christian Reitwießner. 2018. SMT-Based Verification of Solidity Smart Contracts. In ISoLA (LNCS), Vol. 11247. Springer, 376–388.

[5]

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.

[6]

Nada Amin and Tiark Rompf. 2017. Type soundness proofs with definitional interpreters. In POPL. ACM, 666–679.

[7]

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.

[8]

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).

[9]

Kshitij Bansal, Eric Koskinen, and Omer Tripp. 2018. Automatic Generation of Precise and Useful Commutativity Conditions. In TACAS (LNCS), Vol. 10805. Springer, 115–132.

[10]

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.

[11]

Bitcoin Wiki. 2017. Bitcoin Script. https://en.bitcoin.it/wiki/Script, accessed on Apr 5, 2019.

[12]

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 .

[13]

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).

[14]

Arthur Charguéraud. 2013. Pretty-Big-Step Semantics. In ESOP (LNCS), Vol. 7792. Springer, 41–60.

[15]

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.

[16]

Michael Coblenz. 2017. Obsidian: A Safer Blockchain Programming Language. In ICSE (Companion). IEEE Press, 97–99.

[17]

Coq Development Team. 2019. The Coq Proof Assistant Reference Manual - Version 8.9. http://coq.inria.fr .

[18]

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.

Digital Library

[19]

Olivier Danvy. 2019. Folding left and right over Peano numbers. J. Funct. Program. 29 (2019), e6.

[20]

Olivier Danvy and Andrzej Filinski. 1990. Abstracting Control. In LISP and Functional Programming. 151–160.

[21]

Olivier Danvy and Andrzej Filinski. 1992. Representing Control: A Study of the CPS Transformation. Mathematical Structures in Computer Science 2, 4 (1992), 361–391.

[22]

Olivier Danvy and J. Michael Spivey. 2007. On Barron and Strachey’s cartesian product function. In ICFP. ACM, 41–46.

[23]

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.

[24]

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.

[25]

Ethereum Foundation. 2018a. Decentralized Autonomous Organization. https://www.ethereum.org/dao .

[26]

Ethereum Foundation. 2018b. ERC20 Token Standard. https://theethereum.wiki/w/index.php/ERC20_Token_Standard .

[27]

Ethereum Foundation. 2018c. List of Known Solidity Bugs. https://solidity.readthedocs.io/en/v0.5.7/bugs.html, accessed on Apr 5, 2019.

[28]

Ethereum Foundation. 2018d. Solidity Documentation. http://solidity.readthedocs.io .

[29]

Ethereum Foundation. 2018e. Vyper. https://vyper.readthedocs.io .

[30]

Ethereum Foundation. 2018f. Yul. https://solidity.readthedocs.io/en/latest/yul.html .

[31]

Andrzej Filinski. 1994. Representing Monads. In POPL. ACM Press, 446–457.

[32]

Cormac Flanagan, Amr Sabry, Bruce F. Duba, and Matthias Felleisen. 1993. The Essence of Compiling with Continuations. In PLDI. ACM, 237–247.

[33]

Jean-Yves Girard. 1987. Linear Logic. Theor. Comput. Sci. 50 (1987), 1–102.

Digital Library

[34]

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.

[35]

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.

Digital Library

[36]

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.

[37]

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).

[38]

Emin Gün Sirer. 2016. Reentrancy Woes in Smart Contracts. http://hackingdistributed.com/2016/07/13/reentrancy-woes/

[39]

Robert Harper. 2012. Practical Foundations for Programming Languages. Version 1.32.

[40]

Yoichi Hirai. 2018. Bamboo. https://github.com/pirapira/bamboo .

[41]

Jan Hoffmann, Ankush Das, and Shu-Chun Weng. 2017. Towards automatic resource bound analysis for OCaml. In POPL. ACM, 359–373.

[42]

IOHK Foundation. 2019a. Marlowe: A Contract Language For The Financial World. https://testnet.iohkdev.io/marlowe/ .

[43]

IOHK Foundation. 2019b. Plutus: A Functional Contract Platform. https://testnet.iohkdev.io/plutus/ .

[44]

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.

Digital Library

[45]

Sukrit Kalra, Seep Goel, Mohan Dhawan, and Subodh Sharma. 2018. Zeus: Analyzing Safety of Smart Contracts. In NDSS.

[46]

Andrew Kennedy. 1997. Relational Parametricity and Units of Measure. In POPL. ACM Press, 442–455.

[47]

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.11605

[48]

Johannes Krupp and Christian Rossow. 2018. teEther: Gnawing at Ethereum to Automatically Exploit Smart Contracts. In USENIX Security Symposium. USENIX Association, 1317–1333.

[49]

Ramana Kumar, Magnus O. Myreen, Michael Norrish, and Scott Owens. 2014. CakeML: a verified implementation of ML. In POPL. ACM, 179–192.

[50]

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.

Digital Library

[51]

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.

[52]

James J. Leifer, Gilles Peskine, Peter Sewell, and Keith Wansbrough. 2003. Global abstraction-safe marshalling with hash types. In ICFP. ACM, 87–98.

[53]

Sheng Liang, Paul Hudak, and Mark P. Jones. 1995. Monad Transformers and Modular Interpreters. In POPL. ACM Press, 333–343.

[54]

LSP 2018. Language Server Protocol. https://langserver.org .

[55]

Loi Luu, Duc-Hiep Chu, Hrishi Olickel, Prateek Saxena, and Aquinas Hobor. 2016. Making Smart Contracts Smarter. In CCS. ACM, 254–269.

[56]

Nancy A. Lynch and Mark R. Tuttle. 1989. An Introduction to Input/Output Automata. CWI Quarterly 2 (1989), 219–246.

[57]

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.

[58]

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 .

[59]

John C. Mitchell. 2003. Concepts in programming languages. Cambridge University Press.

[60]

Steven S. Muchnick. 1997. Advanced Compiler Design and Implementation. Morgan Kaufmann.

[61]

Satoshi Nakamoto. 2008. Bitcoin: A peer-to-peer electronic cash system. Abailable at http://bitcoin.org/bitcoin.pdf .

[62]

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.

[63]

Russell O’Connor. 2017. Simplicity: A New Language for Blockchains. https://blockstream.com/simplicity.pdf .

[64]

Scott Owens, Magnus O. Myreen, Ramana Kumar, and Yong Kiam Tan. 2016. Functional Big-Step Semantics. In ESOP (LNCS), Vol. 9632. Springer, 589–615.

[65]

Simon L. Peyton Jones. 1987. The Implementation of Functional Programming Languages. Prentice-Hall.

Digital Library

[66]

Simon L. Peyton Jones. 2013. Type-Directed Compilation in the Wild: Haskell and Core. In TLCA (LNCS), Vol. 7941. Springer.

[67]

George Pîrlea and Ilya Sergey. 2018. Mechanising Blockchain Consensus. In CPP. ACM, 78–90.

[68]

Robert Pollack. 1990. Implicit Syntax. In Informal Proceedings of First Workshop on Logical Frameworks, Antibes.

[69]

Stuart Popejoy. 2017. The Pact Smart-Contract Language, Revision 1.5. http://kadena.io/docs/Kadena-PactWhitepaper.pdf .

[70]

RChain Cooperative. 2019. Rholang. https://rholang.rchain.coop .

[71]

Christian Reitwiessner. 2017. Babbage—a mechanical smart contract language. Online blog post.

[72]

John C. Reynolds. 1974. Towards a theory of type structure. In Programming Symposium (LNCS), Vol. 19. Springer, 408–423.

[73]

John C. Reynolds. 1998. Definitional Interpreters for Higher-Order Programming Languages. Higher-Order and Symbolic Computation 11, 4 (1998), 363–397.

Digital Library

[74]

Michael Rodler, Wenting Li, Ghassan O. Karame, and Lucas Davi. 2019. Sereum: Protecting Existing Smart Contracts Against Re-Entrancy Attacks. In NDSS.

[75]

Grigore Rosu. 2018. IELE: A New Virtual Machine for the Blockchain. https://iohk.io/blog/iele-a-new-virtual-machine-forthe-blockchain .

[76]

Franklin Schrans. 2018. Writing Safe Smart Contracts in Flint. Master’s thesis. Imperial College London, Department of Computing.

[77]

Franklin Schrans, Susan Eisenbach, and Sophia Drossopoulou. 2018. Writing safe smart contracts in Flint. In <Programming> (Companion). ACM, 218–219.

[78]

Ilya Sergey, Dominique Devriese, Matthew Might, Jan Midtgaard, David Darais, Dave Clarke, and Frank Piessens. 2013. Monadic Abstract Interpreters. In PLDI. ACM, 399–410.

[79]

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.00687

[80]

Ilya Sergey, Amrit Kumar, and Aquinas Hobor. 2018b. Temporal Properties of Smart Contracts. In ISoLA (LNCS), Vol. 11247. Springer, 323–338.

[81]

Ilya Sergey, Dimitrios Vytiniotis, and Simon L. Peyton Jones. 2014. Modular, higher-order cardinality analysis in theory and practice. In POPL. ACM, 335–348.

[82]

Peter Sestoft. 1996. ML Pattern Match Compilation and Partial Evaluation. In International Seminar on Partial Evaluation, Dagstuhl Castle (LNCS), Vol. 1110. Springer, 446–464.

[83]

Amin Shali and William R. Cook. 2011. Hybrid Partial Evaluation. In OOPSLA. ACM, 375–390.

[84]

Dieter Shirley. 2018. ERC-721. http://erc721.org/ .

[85]

Jeremy Siek. 2012. Big-step, diverging or stuck? http://siek.blogspot.com/2012/07/big-step-diverging-or-stuck.html .

[86]

Jeremy Siek. 2013. Type safety in three easy lemmas. http://siek.blogspot.com/2013/05/type-safety-in-three-easylemmas.html .

[87]

Flora Sun. 2018. UTXO vs Account/Balance Model. Online blog post, available at https://medium.com/@sunflora98/utxovs-account-balance-model-5e6470f4e0cf .

[88]

Nick Szabo. 1994. Smart Contracts. Online manuscript.

[89]

Tezos Foundation. 2018a. Michelson: the language of Smart Contracts in Tezos. http://tezos.gitlab.io/mainnet/whitedoc/ michelson.html .

[90]

Tezos Foundation. 2018b. Liquidity. http://www.liquidity-lang.org/ .

[91]

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.

[92]

Anton Trunov. 2019. A Scilla vs Move case study. Blog post available at https://medium.com/@anton_trunov/a-scilla-vsmove-case-study-afa9b8df5146 .

[93]

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.

[94]

Peng Wang. 2019. Type System for Resource Bounds with Type-Preserving Compilation. Ph.D. Dissertation. Massachusetts Institute of Technology.

[95]

Gavin Wood. 2014. Ethereum: A Secure Decentralized Generalised Transaction Ledger.

[96]

Andrew K. Wright and Matthias Felleisen. 1994. A Syntactic Approach to Type Soundness. Inf. Comput. 115, 1 (1994), 38–94.

Digital Library

[97]

Zilliqa Team. 2017. The Zilliqa Technical Whitepaper. https://docs.zilliqa.com/whitepaper.pdf Version 0.1.

Cited By

Delmo ADespi JArpon P(2024)A 5 Year Bibliometric Review of Programming Language Research Dynamics in Southeast Asia (2018-2023)SSRN Electronic Journal10.2139/ssrn.4706647Online publication date: 2024
https://doi.org/10.2139/ssrn.4706647
Chen HLu LMassey BWang YLoo BRoychoudhury APaiva AAbreu RStorey M(2024)Verifying Declarative Smart ContractsProceedings of the IEEE/ACM 46th International Conference on Software Engineering10.1145/3597503.3639203(1-12)Online publication date: 20-May-2024
https://dl.acm.org/doi/10.1145/3597503.3639203
Bartoletti MMarchesin RZunino R(2024)Secure compilation of rich smart contracts on poor UTXO blockchains2024 IEEE 9th European Symposium on Security and Privacy (EuroS&P)10.1109/EuroSP60621.2024.00021(235-267)Online publication date: 8-Jul-2024
https://doi.org/10.1109/EuroSP60621.2024.00021
Show More Cited By

Index Terms

Safer smart contract programming with Scilla
1. Software and its engineering
  1. Software notations and tools
    1. General programming languages
      1. Language types
        Distributed programming languages
        Functional languages
2. Theory of computation
  1. Semantics and reasoning
    1. Program reasoning
      1. Program analysis

Recommendations

Smart Contract Locator (SCL) and Smart Contract Description Language (SCDL)
Service-Oriented Computing – ICSOC 2019 Workshops
Abstract
Today’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 Systems

This 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 Blockchain

The 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

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Proceedings of the ACM on Programming Languages

Proceedings of the ACM on Programming Languages Volume 3, Issue OOPSLA

October 2019

2077 pages

EISSN:2475-1421

DOI:10.1145/3366395

Issue’s Table of Contents

Copyright © 2019 Owner/Author.

This work is licensed under a Creative Commons Attribution International 4.0 License.

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 10 October 2019

Published in PACMPL Volume 3, Issue OOPSLA

Permissions

Request permissions for this article.

Request Permissions

Check for updates

Badges

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

63
Total Citations
View Citations
2,437
Total Downloads

Downloads (Last 12 months)235
Downloads (Last 6 weeks)55

Reflects downloads up to 22 Sep 2024

Other Metrics

View Author Metrics

Citations

Cited By

Delmo ADespi JArpon P(2024)A 5 Year Bibliometric Review of Programming Language Research Dynamics in Southeast Asia (2018-2023)SSRN Electronic Journal10.2139/ssrn.4706647Online publication date: 2024
https://doi.org/10.2139/ssrn.4706647
Chen HLu LMassey BWang YLoo BRoychoudhury APaiva AAbreu RStorey M(2024)Verifying Declarative Smart ContractsProceedings of the IEEE/ACM 46th International Conference on Software Engineering10.1145/3597503.3639203(1-12)Online publication date: 20-May-2024
https://dl.acm.org/doi/10.1145/3597503.3639203
Bartoletti MMarchesin RZunino R(2024)Secure compilation of rich smart contracts on poor UTXO blockchains2024 IEEE 9th European Symposium on Security and Privacy (EuroS&P)10.1109/EuroSP60621.2024.00021(235-267)Online publication date: 8-Jul-2024
https://doi.org/10.1109/EuroSP60621.2024.00021
Chakravarty M(2024)Smart ContractEncyclopedia of Cryptography, Security and Privacy10.1007/978-3-642-27739-9_1665-4(1-3)Online publication date: 30-Aug-2024
https://doi.org/10.1007/978-3-642-27739-9_1665-4
Caires LToninho B(2024)The Session Abstract MachineProgramming Languages and Systems10.1007/978-3-031-57262-3_9(206-235)Online publication date: 5-Apr-2024
https://doi.org/10.1007/978-3-031-57262-3_9
Cai ZFarokhnia SGoharshady AHitarth S(2023)Asparagus: Automated Synthesis of Parametric Gas Upper-Bounds for Smart ContractsProceedings of the ACM on Programming Languages10.1145/36228297:OOPSLA2(882-911)Online publication date: 16-Oct-2023
https://dl.acm.org/doi/10.1145/3622829
Richter DKretzler DWeisenburger PSalvaneschi GFaust SMezini M(2023) Prisma : A Tierless Language for Enforcing Contract-client Protocols in Decentralized ApplicationsACM Transactions on Programming Languages and Systems10.1145/360462945:3(1-41)Online publication date: 23-Sep-2023
https://dl.acm.org/doi/10.1145/3604629
Otoni RMarescotti MAlt LEugster PHyvärinen ASharygina N(2023)A Solicitous Approach to Smart Contract VerificationACM Transactions on Privacy and Security10.1145/356469926:2(1-28)Online publication date: 13-Mar-2023
https://dl.acm.org/doi/10.1145/3564699
Li JHu KWan JZhan WZou YAi YGao LYin Y(2023)The Specification of Blockchain Oracle System2023 24th IEEE International Conference on Mobile Data Management (MDM)10.1109/MDM58254.2023.00057(309-314)Online publication date: Jul-2023
https://doi.org/10.1109/MDM58254.2023.00057
Patrignani MBlackshear S(2023)Robust Safety for Move2023 IEEE 36th Computer Security Foundations Symposium (CSF)10.1109/CSF57540.2023.00045(308-323)Online publication date: Jul-2023
https://doi.org/10.1109/CSF57540.2023.00045
Show More Cited By

View Options

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Get Access

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Article

Media

Figures

Other

Tables

View Issue’s Table of Contents