Overview of the Languages for Safe Smart Contract Programming
Alexey Valerievitch Tyurin,
Ivan Vladimirovitch Tyulyandin,
Vladimir S. Maltsev,
Jacob Alexandrovitch Kirilenko,
Daniil Andreevitch Berezun https://doi.org/10.15514/ISPRAS-2019-31(3)-13
Abstract
Blockchain technologies are gradually being found an application in many areas, especially in FinTech. As a result, a lot of blockchain platforms have emerged with the support of smart contracts that are intended to automate party interactions. However, it has been shown that they are prone to attacks and errors which lead to money loss. To date, there has been a wide range of approaches for making smart contracts safer that included analysis tools, reasoning models, and safer and more rigorous programming languages. In this paper, we provide an overview of smart contract programming languages design principles, related vulnerabilities, and future research areas. The provided overview is meant to outline the to date state of languages and to become a possible basis for future proceedings, and show approaches, used by the community, to reach safe and usable language for smart contracts. We have split all found vulnerabilities by source of their arising. Various languages’ characteristics such as abstraction level, paradigm, Turing completeness and main features are summarized in the table. Additional information about languages is provided, e.g. model of execution and tools for static analysis.
About the Authors
Alexey Valerievitch Tyurin
Saint Petersburg State University
Russian Federation
Software engineering chair, mathematics and mechanics faculty
Russian Federation
Software engineering chair, mathematics and mechanics faculty
Ivan Vladimirovitch Tyulyandin
Saint Petersburg State University
Russian Federation
Software engineering chair, mathematics and mechanics faculty
Russian Federation
Software engineering chair, mathematics and mechanics faculty
Vladimir S. Maltsev
Saint Petersburg State University
Russian Federation
Software engineering chair, mathematics and mechanics faculty
Russian Federation
Software engineering chair, mathematics and mechanics faculty
Jacob Alexandrovitch Kirilenko
Saint Petersburg State University
Russian Federation
Software engineering chair, mathematics and mechanics faculty
Russian Federation
Software engineering chair, mathematics and mechanics faculty
Daniil Andreevitch Berezun
Higher School of Economics National Research University
Russian Federation
Department of Computer Science at the Higher School of Economics.
Russian Federation
Department of Computer Science at the Higher School of Economics.
References
1. Bitcoin contract. URL: https://en.bitcoin.it/wiki/Contract (Date: 2019-01-30).
2. Solidity-example-crowdfunding. URL: https://github.com/ zupzup/solidity-example-crowdfunding (Date: 2019-01-30).
3. D. Macrinici, C. Cartofeanu, and S. Gao. Smart contract applications within blockchain technology: A systematic mapping study. Telematics and Informatics, vol. 35, no. 8, 2018, pp. 2337 – 2354.
4. C. D. Clack, V. A. Bakshi, and L. Braine. Smart contract templates: foundations, design landscape and research directions. CoRR, vol. abs/1608.00771, 2016.
5. A 50 million hack just showed that the dao was all too human. URL: https://www.wired.com/2016/06/ 50-million-hack-just-showed-dao-human/ (Date: 2019-01-30).
6. D. McAdams. An ontology for smart contracts. URL: https://cryptochainuni.com/wp-content/uploads/ Darryl-McAdams-An-Ontology-for-Smart-Contracts.pdf (Date: 2019-02-07).
7. N. Atzei, M. Bartoletti, and T. Cimoli. A survey of attacks on ethereum smart contracts sok. In Proc. of the 6th International Conference on Principles of Security and Trust, 2017, pp. 164–186.
8. G. Destefanis, A. Bracciali, R. Hierons, M. Marchesi, M. Ortu, and R. Tonelli. Smart contracts vulnerabilities: A call for blockchain software engineering. ResearchGate, 2018.
9. Safer smart contracts through type-driven development. URL: https://publications.lib.chalmers.se/records/fulltext/ 234939/234939.pdf (Date: 2019-01-30).
10. Bitcoin script. URL: https://en.bitcoin.it/wiki/ Script (Date: 2019-01-30)
11. R. O’Connor. Simplicity: A new language for blockchains. CoRR, vol. abs/1711.03028, 2017.
12. Flint. URL: https://github.com/flintlang/flint (Date: 2019-01- 30).
13. Vyper. URL: https://github.com/ethereum/vyper (Date: 2019- 01-29).
14. T. Kasampalis, D. Guth, B. Moore, T. Serbanuta, V. Serbanuta, D. Filaretti, G. Rosu, and R. Johnson. Iele: An intermediate-level blockchain language designed and implemented using formal semantics. University of Illinois, Tech. Rep., http://hdl.handle.net/2142/100320, July 2018.
15. Sergey, A. Kumar, and A. Hobor. Scilla: a smart contract intermediate-level language. CoRR, vol. abs/1801.00687, 2018.
16. Plutus core specification. URL: https://github. com/input-output-hk/plutus/tree/master/plutus-core-spec (Date: 2019-01-30).
17. D. Harz and W. J. Knottenbelt. Towards safer smart contracts: A survey of languages and verification methods. CoRR, vol. abs/1809.09805, 2018.
18. P. L. Seijas, S. Thompson, and D. McAdams. Scripting smart contracts for distributed ledger technology. Cryptology ePrint Archive, Report 2016/1156, 2016, https://eprint.iacr.org/2016/ 1156.
19. Contract. URL: https://en.bitcoin.it/wiki/Contract (Date: 2019- 01-30).
20. Ethereum contract security techniques and tips. URL: https: //github.com/ethereum/wiki/wiki/Safety (Date: 2019-01-29).
21. E. Androulaki, A. Barger, V. Bortnikov, C. Cachin, K. Christidis, A. De Caro, D. Enyeart, C. Ferris, G. Laventman, Y. Manevich, S. Muralidharan, C. Murthy, B. Nguyen, M. Sethi, G. Singh, K. Smith, A. Sorniotti, C. Stathakopoulou, M. Vukolic, S. W. Cocco, and J. Yellick. Hyperledger fabric: A ´ distributed operating system for permissioned blockchains. In Proc. of the Thirteenth EuroSys Conference, 2018, pp. 30:1–30:15.
22. K. Yamashita, Y. Nomura, E. Zhou, B. Pi, and S. Jun. Potential risks of hyperledger fabric smart contracts. In Proc. of the 2019 IEEE International Workshop on Blockchain Oriented Software Engineering (IWBOSE), 2019, pp. 1–10.
23. 300m in cryptocurrency accidentally lost forever due to bug. URL: https://www.theguardian.com/technology/2017/nov/ 08/cryptocurrency-300m-dollars-stolen-bug-ether (Date: 2019- 01-30).
24. Smart contract weakness classification and test cases. URL: https://smartcontractsecurity.github.io/SWC-registry/ (Date: 2019-01-29).
25. Decentralized application security project. URL: https://dasp.co (Date: 2019-01-29).
26. Security considerations. URL: https://solidity.readthedocs.io/en/ latest/security-considerations.html (Date: 2019-01-29).
27. Vulnerabilities description. URL: https://github.com/trailofbits/ slither/wiki/Vulnerabilities-Description (Date: 2019-01-30).
28. Smart contract weakness classification and test cases. URL: https://smartcontractsecurity.github.io/SWC-registry/ (Date: 2019-01-22).
29. N. Atzei, M. Bartoletti, and T. Cimoli. A survey of attacks on ethereum smart contracts sok. In Proc. of the 6th International Conference on Principles of Security and, 2017, pp. 164–186.
30. Ether — the crypto-fuel for the ethereum network. URL: https://www.ethereum.org/ether (Date: 2019-01-30).
31. L. Luu, D.-H. Chu, H. Olickel, P. Saxena, and A. Hobor. Making smart contracts smarter. In Proc. of the 2016 ACM SIGSAC Conference on Computer and Communications Security, 2016, pp. 254–269.
32. D. G. Wood. Ethereum: A secure decentralised generalised transaction ledger. URL: https://ethereum.github.io/ yellowpaper/paper.pdf (Date: 2019-01-31).
33. Michelson language. URL: https://www.michelson-lang.com/ (Date: 2019-01-31).
34. B. C. Pierce. Types and Programming Languages, 1st ed. The MIT Press, 2002.
35. Solidity. URL: https://github.com/ethereum/solidity (Date: 2019-01-29).
36. Liquidity. URL: https://github.com/OCamlPro/liquidity (Date: 2019-01-29).
37. Grigore Roșu and T. F. Șerbănută. An overview of the k semantic framework. The Journal of Logic and Algebraic Programming, vol. 79, no. 6, 2010, pp. 397–434.
38. S. Tikhomirov, E. Voskresenskaya, I. Ivanitskiy, R. Takhaviev, E. Marchenko, and Y. Alexandrov. Smartcheck: Static analysis of ethereum smart contracts. In Proc. of the 1st International Workshop on Emerging Trends in Software Engineering for Blockchain, 2018, pp. 9–16.
39. S. Kalra, S. Goel, M. Dhawan, and S. Sharma. Zeus: Analyzing safety of smart contracts. In Proc. of the Network and Distributed Systems Security (NDSS) Symposium, 2018.
40. K. Bhargavan, A. Delignat-Lavaud, C. Fournet, A. Gollamudi, G. Gonthier, N. Kobeissi, N. Kulatova, A. Rastogi, T. SibutPinote, N. Swamy, and S. Zanella-Béguelin. Formal verification of smart contracts: Short paper. In Proc. of the 2016 ACM Workshop on Programming Languages and Analysis for Security, 2016, pp. 91–96.
41. P. Tsankov, A. Dan, D. Drachsler-Cohen, A. Gervais, F. Bünzli, and M. Vechev. Securify: Practical security analysis of smart contracts. In Proc. of the 2018 ACM SIGSAC Conference on Computer and Communications Security, 2018, pp. 67–82.
42. E. Hildenbrandt, M. Saxena, X. Zhu, N. Rodrigues, P. Daian, D. Guth, B. Moore, Y. Zhang, D. Park, A. Stefanescu, and G. Rosu. Kevm: A complete semantics of the ethereum virtual machine. In Proc. of the 2018 IEEE 31st Computer Security Foundations Symposium, 2018, pp. 204–217.
43. Mythril. URL: https://github.com/ConsenSys/mythril-classic (Date: 2019-01-29).
44. L. Brent, A. Jurisevic, M. Kong, E. Liu, F. Gauthier, V. Gramoli, R. Holz, and B. Scholz. Vandal: A scalable security analysis framework for smart contracts. CoRR, vol. abs/1809.03981, 2018.
45. Rattle. URL: https://github.com/trailofbits/rattle (Date: 2019- 01-30).
46. Manticore. URL: https://github.com/trailofbits/manticore (Date: 2019-01-30).
47. L. G. Meredith and M. Radestock. A reflective higher-order calculus. Electronic Notes in Theoretical Computer Science, vol. 141, 2005, pp. 49– 67.
48. Bitcoin weaknesses. URL: https://en.bitcoin.it/wiki/Weaknesses (Date: 2019-01-30).
49. Back, M. Corallo, L. Dashjr, M. Friedenbach, G. Maxwell, A. Miller, A. Poelstra, J. Timón, and P. Wuille, Enabling blockchain innovations with pegged sidechains. 2014. https://blockstream.com/sidechains.pdf (Date: 2019-01-30).
50. Mediawiki. URL: https://github.com/bitcoin/bips/blob/master/ bip-0016.mediawiki (Date: 2019-02-5).
51. Simplicity. URL: https://github.com/ElementsProject/simplicity (Date: 2019-02-5).
52. Grishchenko I., Maffei M., Schneidewind, C. A semantic framework for the security analysis of ethereum smart contracts – technical report (2018). URL: https://secpriv.tuwien. ac.at/tools/ethsemantics. (Date: 2019-01-30).
53. Formalization of ethereum virtual machine in lem. URL: https://github.com/pirapira/eth-isabelle (Date: 2019-01-30).
54. Ewasm: design overview and specification. URL: https: //github.com/ewasm/design (Date: 2019-01-30).
55. Michelson: the language of smart contracts in tezos. URL: http: //www.liquidity-lang.org/doc/reference/michelson.html (Date: 2019-01-30).
56. Why michelson? URL: https://www.michelson-lang.com/ why-michelson.html (Date: 2019-02-5).
57. Plutus core semantics. URL: https://github.com/kframework/ plutus-core-semantics (Date: 2019-01-30).
58. Plutus implementation and tools. URL: https://github.com/ input-output-hk/plutus (Date: 2019-01-30).
59. The extended utxo model. URL: https://github.com/ input-output-hk/plutus/tree/master/docs/extended-utxo (Date: 2019-02-5).
60. Is it smart to use smart contracts? URL: https://plutusfest.io/ presentations/Philip-Wadler/Wadler30.pdf (Date: 2019-02-5).
61. Solidityx. URL: https://solidityx.org/ (Date: 2019-01-30).
62. Bamboo. URL: https://github.com/pirapira/bamboo (Date: 2019-01-30).
63. Logikon. URL: https://github.com/logikon-lang/logikon (Date: 2019-01-31).
64. Ivy: Bitcoin smart contracts. URL: https://github.com/ivy-lang/ ivy-bitcoin (Date: 2019-01-30).
65. Çagdas Bozman, M. Iguernlala, M. Laporte, F. L. Fessant, and A. Mebsout. Liquidity: Ocaml pour la blockchain. Journées Francophones des Langages Applicatifs 2018, 2018.
66. Yul. URL: https://solidity.readthedocs.io/en/latest/yul.html (Date: 2019-01-30).
67. Rchain and rholang. URL: https://www.rchain.coop/platform (Date: 2019-01-30).
68. D. Ancona, V. Bono, and M. Bravetti. Behavioral Types in Programming Languages. Hanover, MA, USA: Now Publishers Inc., 2016.
69. G. Wood. LLL. URL: https://lll-docs.readthedocs.io/en/latest/ index.html (Date: 2019-01-30).
70. Upgradable contract with solidity. URL: https://gist.github.com/ Arachnid/4ca9da48d51e23e5cfe0f0e14dd6318f (Date: 2019-01- 30).
71. Proxy libraries in solidity. URL: https://blog.zeppelin.solutions/ proxy-libraries-in-solidity-79fbe4b970fd (Date: 2019-01-30).
72. The pact smart-contract language. URL: http://kadena.io/docs/ Kadena-PactWhitepaper.pdf (Date: 2019-01-30).
73. T. Chen, X. Li, Y. Wang, J. Chen, Z. Li, X. Luo, M. H. Au, and X. Zhang. An adaptive gas cost mechanism for ethereum to defend against under-priced dos attacks. CoRR, vol. abs/1712.06438, 2017.
74. E. Albert, P. Gordillo, A. Rubio, and I. Sergey. GASTAP: A gas analyzer for smart contracts. CoRR, vol. abs/1811.10403, 2018.
75. M. Marescotti, M. Blicha, A. E. J. Hyvärinen, S. Asadi, and N. Sharygina. Computing exact worst-case gas consumption for smart contracts. In Proc. of the International Symposium on Leveraging Applications of Formal Methods, 2018.
76. J. Hoffmann, A. Das, and S. Weng. Towards automatic resource bound analysis for ocaml. CoRR, vol. abs/1611.00692, 2016.
77. J. Baeten. A brief history of process algebra. Theoretical Computer Science, vol. 335, no. 2, 2005, pp. 131–146.
78. H. Deyoung and F. Pfenning. Reasoning about the consequences of authorization policies in a linear epistemic logic. In Proc. of the Workshop on Foundations of Computer Security, 2009.
79. S. Thompson and P. L. Seijas. Marlowe: Financial contracts on blockchain. Lecture Notes in Computer Science, vol. 11247, 2018, pp 356-375.
80. G. Bigi, A. Bracciali, G. Meacci, and E. Tuosto. Validation of decentralized smart contracts through game theory and formal methods. Lecture Notes in Computer Science, vol. 9465, 2015, pp. 142–161.
81. M. Bartoletti and R. Zunino. Bitml: A calculus for bitcoin smart contracts. In Proc. of the 2018 ACM SIGSAC Conference on Computer and Communications Security, 2018, pp. 83–100.
82. Y. Hirai. Defining the ethereum virtual machine for interactive theorem provers. Lecture Notes in Computer Science, vol. 10323) 2017, pp. 520–535.
Review
For citations:
Tyurin A.V., Tyulyandin I.V., Maltsev V.S., Kirilenko J.A., Berezun D.A. Overview of the Languages for Safe Smart Contract Programming. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2019;31(3):157-176. https://doi.org/10.15514/ISPRAS-2019-31(3)-13
Email this article 