Обзор языков для безопасного программирования смарт-контрактов

Технология распределенного реестра блокчейн становится все более популярной и находит применение в различных областях, в том числе и в финансовых технологиях. Многие блокчейн-платформы поддерживают функциональность смарт-контрактов, которые предназначены для автоматизации заключения договоров. Известны примеры, где ошибки или небрежности в коде смарт-контракта приводят к потере активов, например, из-за атаки злоумышленника или непонимания разработчиком особенностей блокчейн-платформы. На сегодняшний день существует множество различных подходов, которые позволяют сделать смарт-контракты безопаснее. Среди них инструменты анализа кода, модели вычислений и семантики языков программирования смарт-контрактов. В этой работе мы приводим обзор языков программирования смарт-контрактов, принципов их построения, а также потенциальные ошибки в программе смарт-контракта. Основная цель этого обзора — рассмотреть текущее на момент написания статьи состояние языков смарт-контрактов и возможные направления для будущих исследований, а также показать подходы, используемые сообществом для создания безопасного и удобного (с точки зрения абстракции) языка. Характеристики множества языков, такие как: уровень абстракции, парадигма, Тьюринг-полнота, проект, где язык используется, инструменты для анализа кода, система ограничения и главные особенности — были рассмотрены и сведены в таблицу. Предоставлена дополнительная информация о языках, например, о модели выполнения. Также мы кратко описали и разделили все найденные нами уязвимости по источникам их возникновения.

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. I. 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 Trust, 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. Sibut-Pinote, 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. A. 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.