Skip to main content
SpringerLink
Log in

Smart Contracts and Opportunities for Formal Methods

  • Conference paper
  • First Online:
Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice (ISoLA 2018)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11247))

Included in the following conference series:

Abstract

Smart contracts are programs that run atop of a blockchain infrastructure. They have emerged as an important new programming model in cryptocurrencies like Ethereum, where they regulate flow of money and other digital assets according to user-defined rules. However, the most popular smart contract languages favor expressiveness rather than safety, and bugs in smart contracts have already lead to significant financial losses from accidents. Smart contracts are also appealing targets for hackers since they can be monetized. For these reasons, smart contracts are an appealing opportunity for systematic auditing and validation, and formal methods in particular. In this paper, we survey the existing smart-contract ecosystem and the existing tools for analyzing smart contracts. We then pose research challenges for formal-methods and program analysis applied to smart contracts.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Notes

  1. 1.

    https://cryptocoincharts.info/markets/show/etherdelta.

  2. 2.

    Here “verified” means the Solidity source code corresponds to the EVM bytecodes.

References

  1. Bitcoin Script Wiki. https://en.bitcoin.it/wiki/Script. Accessed 21 Apr 2018

  2. CertiK: building fully trustworthy smart contracts and blockchain ecosystems. https://certik.org/docs/white_paper.pdf. Accessed 28 Mar 2018

  3. Decompiler and security analysis tool for blockchain-based ethereum smart-contracts. https://github.com/comaeio/porosity. Accessed 25 Mar 2018

  4. Ethereum smart contract security best practices. https://consensys.github.io/smart-contract-best-practices/. Accessed 29 Mar 2018

  5. ethereum/vyper - new experimental programming language. https://github.com/ethereum/vyper. Accessed 26 Mar 2018

  6. K semantics of the ethereum virtual machine (EVM). https://github.com/kframework/evm-semantics. Accessed 26 Mar 2018

  7. Liquidity: a smart contract language for Tezos. https://github.com/OCamlPro/liquidity. Accessed 19 Apr 2018

  8. MAIAN: automatic tool for finding trace vulnerabilities in ethereum smart contracts. https://github.com/MAIAN-tool/MAIAN. Accessed 24 Mar 2018

  9. Manticore 0.1.7 release - symbolic execution tool. https://github.com/trailofbits/manticore. Accessed 24 Mar 2018

  10. Manticore documentation, release 0.1.0. https://media.readthedocs.org/pdf/manticore/latest/manticore.pdf. Accessed 25 Mar 2018

  11. Manticore: Symbolic execution for humans. https://blog.trailofbits.com/2017/04/27/manticore-symbolic-execution-for-humans/. Accessed 24 Mar 2018

  12. Michelson: the language of smart contracts in Tezos. https://www.tezos.com/static/papers/language.pdf. Accessed 19 Apr 2018

  13. Mythril 0.14.9 - security analysis tool for ethereum smart contracts. https://pypi.python.org/pypi/mythril. Accessed 24 Mar 2018

  14. Openzepplin/zeppelin-solidity/contracts/math/safemath.sol. https://github.com/OpenZeppelin/zeppelin-solidity/blob/master/contracts/math/SafeMath.sol. Accessed 24 Mar 2018

  15. Oyente - an analysis tool for smart contracts, version 0.2.7. https://github.com/melonproject/oyente. Accessed 9 Oct 2017

  16. Oyente web access. https://oyente.melon.fund. Accessed 24 Mar 2018

  17. Plutus language prototype. https://github.com/input-output-hk/plutus-prototype. Accessed 20 Apr 2018

  18. Remix - solidity IDE, v0.4.21. http://remix.ethereum.org. Accessed 28 Mar 2018

  19. Rholang. https://github.com/rchain/rchain/tree/master/rholang. Accessed 26 Mar 2018

  20. Securify - formal verification of ethereum smart contracts. https://securify.ch/. Accessed 24 Mar 2018

  21. Security considerations - pitfalls - tx.origin. https://solidity.readthedocs.io/en/develop/security-considerations.html#tx-origin. Accessed 24 Mar 2018

  22. Smartcheck. https://tool.smartdec.net/. Accessed 24 Mar 2018

  23. Smartcheck - a static analysis tool that detects vulnerabilities and bugs in solidity programs. https://github.com/smartdec/smartcheck. Accessed 24 Mar 2018

  24. Solidity v0.4.21. https://solidity.readthedocs.io/en/v0.4.21/. Accessed 28 Mar 2018

  25. The source code of ethereum virtual machine bytecode f* formalization. https://secpriv.tuwien.ac.at/tools/ethsemantics. Accessed 26 Mar 2018

  26. Try Michelson. https://try-michelson.com/. Accessed 19 Apr 2018

  27. Vyper. https://vyper.readthedocs.io/en/latest/index.html. Accessed 27 Mar 2018

  28. Atzei, N., Bartoletti, M., Cimoli, T.: A survey of attacks on ethereum smart contracts (SoK). In: Maffei, M., Ryan, M. (eds.) POST 2017. LNCS, vol. 10204, pp. 164–186. Springer, Heidelberg (2017). https://doi.org/10.1007/978-3-662-54455-6_8

    Chapter  Google Scholar 

  29. Bartoletti, M., Pompianu, L.: An empirical analysis of smart contracts: platforms, applications, and design patterns. In: Brenner, M., et al. (eds.) FC 2017. LNCS, vol. 10323, pp. 494–509. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-70278-0_31

    Chapter  Google Scholar 

  30. Bhargavan, K., et al.: Formal verification of smart contracts: short paper. In: Proceedings of the 2016 ACM Workshop on Programming Languages and Analysis for Security, PLAS 2016, pp. 91–96. ACM, New York (2016). https://doi.org/10.1145/2993600.2993611

  31. Blockstream: Simplicity itself for blockchains. https://blockstream.com/2017/10/30/simplicity.html. Accessed 20 Apr 2018

  32. BOScoin: Smart contracts and trust contracts: part 3. https://medium.com/@boscoin/smart-contracts-trust-contracts-part-3-6cf76bf5882e. Accessed 21 Apr 2018

  33. Buterin, V.: Bootstrapping a decentralized autonomous corporation: part I. Bitcoin Mag. (2013)

    Google Scholar 

  34. Crary, K., Sullivan, M.J.: Peer-to-peer affine commitment using bitcoin. In: Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2015, pp. 479–488. ACM, New York (2015). https://doi.org/10.1145/2737924.2737997

  35. Daian, P.: Analysis of the DAO exploit (2016). http://hackingdistributed.com/2016/06/18/analysis-of-the-dao-exploit/

  36. Daian, P.: An in-depth look at the parity multisig bug, July 2017. http://hackingdistributed.com/2017/07/22/deep-dive-parity-bug/

  37. Danezis, G., Meiklejohn, S.: Centrally banked cryptocurrencies. In: NDSS (2016)

    Google Scholar 

  38. Gencer, A.E., van Renesse, R., Sirer, E.G.: Short paper: service-oriented sharding for blockchains. In: Kiayias, A. (ed.) FC 2017. LNCS, vol. 10322, pp. 393–401. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-70972-7_22

    Chapter  Google Scholar 

  39. Grishchenko, I., Maffei, M., Schneidewind, C.: A semantic framework for the security analysis of ethereum smart contracts. arXiv preprint arXiv:1802.08660 (2018)

  40. Grossman, S.: Online detection of effectively callback free objects with applications to smart contracts. Proc. ACM Program. Lang. 2(POPL), 48 (2017)

    Google Scholar 

  41. Higgins, S.: Ethereum developers launch white hat counter-attack on the DAO, June 2016. https://www.coindesk.com/ethereum-developers-draining-dao/

  42. Hildenbrandt, E., et al.: KEVM: a complete semantics of the ethereum virtual machine. http://hdl.handle.net/2142/97207. Accessed 27 Mar 2018

  43. Hileman, G.: State of blockchain Q1 2016: blockchain funding overtakes bitcoin (2016). http://www.coindesk.com/state-of-blockchain-q1-2016/

  44. Hirai, Y.: Dr. Y’s ethereum contract analyzer. https://github.com/pirapira/dry-analyzer. Accessed 25 Mar 2018

  45. Hirai, Y.: A lem formalization of EVM and some Isabelle/HOL proofs. https://github.com/pirapira/eth-isabelle. Accessed 25 Mar 2018

  46. Hirai, Y.: Defining the ethereum virtual machine for interactive theorem provers. In: Brenner, M., et al. (eds.) FC 2017. LNCS, vol. 10323, pp. 520–535. Springer, Cham (2017). https://doi.org/10.1007/978-3-319-70278-0_33

    Chapter  Google Scholar 

  47. Kalra, S., Goel, S., Dhawan, M., Sharma, S.: Zeus: Analyzing safety of smart contracts. In: NDSS (2018)

    Google Scholar 

  48. Kokoris-Kogias, E., Jovanovic, P., Gasser, L., Gailly, N., Syta, E., Ford, B.: OmniLedger: a secure, scale-out, decentralized ledger via sharding (2018)

    Google Scholar 

  49. Kosba, A., Miller, A., Shi, E., Wen, Z., Papamanthou, C.: Hawk: The blockchain model of cryptography and privacy-preserving smart contracts. In: 2016 IEEE Symposium on Security and Privacy (SP), pp. 839–858. IEEE (2016)

    Google Scholar 

  50. Kuske, D., Muscholl, A.: Communicating automata. http://eiche.theoinf.tu-ilmenau.de/kuske/Submitted/cfm-final.pdf. Accessed 27 Mar 2018

  51. Larimer, D.: Overpaying for security: the hidden costs of bitcoin, September 2013. https://letstalkbitcoin.com/is-bitcoin-overpaying-for-false-security

  52. Luu, L., Chu, D.H., Olickel, H., Saxena, P., Hobor, A.: Making smart contracts smarter. In: Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, pp. 254–269. ACM (2016)

    Google Scholar 

  53. Mark, D., Zamfir, V., Sirer, E.G.: A call for a temporary moratorium on “the DAO”, May 2016

    Google Scholar 

  54. Mavridou, A.: Smartcontracts - the FSolidM framework. https://github.com/anmavrid/smart-contracts. Accessed 26 Mar 2018

  55. Mavridou, A., Laszka, A.: Designing secure ethereum smart contracts: a finite state machine based approach. arXiv preprint arXiv:1711.09327 (2017)

  56. McAdams, D.: Formal specification of the plutus (core) language. https://github.com/input-output-hk/plutus-prototype/tree/master/docs/spec. Accessed 20 Apr 2018

  57. Meredith, L., Radestock, M.: A reflective higher-order calculus. Electron. Notes Theor. Comput. Sci. 141(5), 49–67 (2005). https://doi.org/10.1016/j.entcs.2005.05.016. Proceedings of the Workshop on the Foundations of Interactive Computation (FInCo 2005). http://www.sciencedirect.com/science/article/pii/S1571066105051893

    Article  MATH  Google Scholar 

  58. Morgan Stanley Research: Global insight: blockchain in banking: disruptive threat or tool? (2016)

    Google Scholar 

  59. Morris, D.Z.: Blockchain-based venture capital fund hacked for $60 million, June 2016. http://fortune.com/2016/06/18/blockchain-vc-fund-hacked/

  60. Mueller, B.: Analyzing ethereum smart contracts for vulnerabilities. https://hackernoon.com/scanning-ethereum-smart-contracts-for-vulnerabilities-b5caefd995df. Accessed 24 Mar 2018

  61. Mueller, B.: Introducing Mythril: a framework for bug hunting on the ethereum blockchain. https://hackernoon.com/introducing-mythril-a-framework-for-bug-hunting-on-the-ethereum-blockchain-9dc5588f82f6. Accessed 24 Mar 2018

  62. Mueller, B.: Mythril. https://github.com/ConsenSys/mythril. Accessed 24 Mar 2018

  63. Nakamoto, S.: Bitcoin: a peer-to-peer electronic cash system (2008)

    Google Scholar 

  64. Nikolic, I., Kolluri, A., Sergey, I., Saxena, P., Hobor, A.: Finding the Greedy, Prodigal, and Suicidal Contracts at Scale. ArXiv e-prints, February 2018

    Google Scholar 

  65. OCamlPRO: Liquidity online. http://www.liquidity-lang.org/edit/. Accessed 19 Apr 2018

  66. O’Connor, R.: Simplicity: a new language for blockchains. CoRR abs/1711.03028 (2017). http://arxiv.org/abs/1711.03028

  67. Revere, R.: solgraph - visualize solidity control flow for smart contract security analysis. https://github.com/raineorshine/solgraph. Accessed 24 Mar 2018

  68. Securify: Automatically detecting the bug that froze parity wallets. https://medium.com/@SecurifySwiss/automatically-detecting-the-bug-that-froze-parity-wallets-ad2bebebd3b0. Accessed 24 Mar 2018

  69. Seijas, P.L., Thompson, S.J., McAdams, D.: Scripting smart contracts for distributed ledger technology. IACR Cryptology ePrint Archive 2016/1156 (2016). http://eprint.iacr.org/2016/1156

  70. Sergey, I.: Scilla-Coq, state-transition systems for smart contracts. https://github.com/ilyasergey/scilla-coq. Accessed 25 Mar 2018

  71. Sergey, I., Kumar, A., Hobor, A.: Scilla: a smart contract intermediate-level language. arXiv preprint arXiv:1801.00687 (2018)

  72. Suiche, M.: DEF CON 25: Porosity. https://blog.comae.io/porosity-18790ee42827. Accessed 24 Mar 2018

  73. Suiche, M.: Porosity: a decompiler for blockchain-based smart contracts bytecode. https://www.comae.io/reports/dc25-msuiche-Porosity-Decompiling-Ethereum-Smart-Contracts-wp.pdf. Accessed 25 Mar 2018

  74. Szabo, N.: The idea of smart contracts. Nick Szabos Papers and Concise Tutorials, vol. 6 (1997)

    Google Scholar 

  75. Vigna, P.: Cryptocurrency platform ethereum gets a controversial update. Wall Street J. (2016). http://www.wsj.com/articles/cryptocurrency-platform-ethereum-gets-a-controversial-update-1469055722

  76. Wadler, P.: Simplicity and Michelson: a programming language that is too simple. https://iohk.io/blog/simplicity-and-michelson/. Accessed 21 Apr 2018

Download references

Author information

Authors and Affiliations

  1. University of Illinois at Urbana-Champaign, Champaign, USA

    Andrew Miller

  2. University of Wisconsin Madison, Madison, USA

    Zhicheng Cai & Somesh Jha

Authors
  1. Andrew Miller
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Zhicheng Cai
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Somesh Jha
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Andrew Miller .

Editor information

Editors and Affiliations

  1. University of Limerick, Limerick, Ireland

    Tiziana Margaria

  2. TU Dortmund, Dortmund, Germany

    Bernhard Steffen

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Miller, A., Cai, Z., Jha, S. (2018). Smart Contracts and Opportunities for Formal Methods. In: Margaria, T., Steffen, B. (eds) Leveraging Applications of Formal Methods, Verification and Validation. Industrial Practice. ISoLA 2018. Lecture Notes in Computer Science(), vol 11247. Springer, Cham. https://doi.org/10.1007/978-3-030-03427-6_22

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-03427-6_22

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-03426-9

  • Online ISBN: 978-3-030-03427-6

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation