main| new issue| archive| editorial board| for the authors| publishing house|
Πσρρκθι
Main page
New issue
Archive of articles
Editorial board
For the authors
Publishing house

 

 


ABSTRACTS OF ARTICLES OF THE JOURNAL "INFORMATION TECHNOLOGIES".
No. 1. Vol. 31. 2025

DOI: 10.17587/it.31.42-55

S. M. Avdoshin, Ph. D., Professor, A. M. Litvinenko, Master's Student,
HSE University, Moscow, 101000, Russian Federation

A Review of Smart Contract Verification Methods

Smart contracts are software algorithms that represent an agreement in digital form with a mechanism for forcing the parties to fulfill their obligations. Smart contracts are already firmly entrenched in the fields of finance, but this is not the only possible field of application. The disadvantage of such a digital agreement is that smart contracts can contain errors that can lead to financial losses. The verification process is designed to reduce such errors. This paper provides an overview of methods and tools in the field of smart contract verification.
Keywords: smart contract, formal verification, Ethereum, distributed ledger technology, vulnerabilities detection

P. 42-55

References

  1. Blockchain Statistics 2024 (Market Size & Users), available at: https://www.demandsage.com/blockchain-statistics/
  2. Capitalizatsiya Ethereum, available at: https://ru.tradingview.com/symbols/ETH/ (in Russian).
  3. Szabo N. Smart Contracts, Satoshi Nakamoto Institute, available at: https://nakamotoinstitute.org/smart-contracts/
  4. Kostenetskiy P. S., Chulkevich R. A., Kozyrev V. I. HPC Resources of the Higher School of Economics, J. Phys. Conf. Ser. IOP Publishing, 2021, vol. 1740, no. 1, pp. 012050.
  5. Ethereum Whitepaper, available at: https://ethereum.org/en/whitepaper
  6. Tolmach P., Li Y., Lin S., Liu Y., Li Z. A Survey of Smart Contract Formal Specification and Verification, ACM Computing Surveys, 2021, vol. 54, pp. 1—38.
  7. Draft Federal Law No. 419059-7 "On Digital Financial Assets" (in Russian).
  8. Siegel D. Understanding the DAO attack, CoinDesk, 2016, available at: https://www.coindesk.com/learn/understand-ing-the-dao-attack/
  9. Kriticheskaya uyazvimost' v multisig koshel'ke Parity, available at: https://habr.com/ru/articles/333754/ (in Russian).
  10. Lazarenko A., Avdoshin S. Financial Risks of the Block-chain Industry: A Survey of Cyberattacks: Vol. 2, Proceedings of the Future Technologies Conference (FTC) 2018, 2019, pp. 368—384.
  11. Ethereum Smart Contracts Vulnerable to Hacks: $4 Million in Ether at Risk, available at: https://www.investopedia.com/news/ethereum-smart-contracts-vulnerable-hacks-4-million-ether-risk/.
  12. Uyazvimost' v protokole Seneca privela k krazhe 1900 ETH, Novosti TradingView, available at: https://ru.tradingview.com/news/forklog:07cc9c9cc67b8:0/ (in Russian).
  13. Amani S., B'egel M., Bortin M., Staples M. Towards verifying ethereum smart contract bytecode in isabelle/hol, Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2018, pp. 66—77.
  14. Sotnichek M. Formal verification of smart contracts with the k framework, 2018, available at: https://www.apriorit.com/dev-blog/592-formal-verification-with-k-framework
  15. Grishchenko I. et al, EtherTrust: Sound Static Analysis of Ethereum bytecode, 2018, available at: https://www.netidee.at/sites/default/files/2018-07/staticanalysis.pdf
  16. Li A., Choi J. A., Long F. Securing smart contract with runtime validation, Proc. of ACM PLDI, 2020, pp. 438—453.
  17. Fedotov I. A. Research and development of probabilistic methods for verification of distributed registry systems, 2022 (in Russian).
  18. Almakhour M., Sliman L., Samhat A. E., Mellouk A. Verification of smart contracts: A survey, Pervasive and Mobile Computing, 2020, vol. 67, pp. 101—227.
  19. Hassani H., Huang X., Silva E. Banking with blockchained big data, Journal of Management Analytics, 2018, vol. 5, no. 4, pp. 256—275.
  20. Demirkan S., Demirkan I., McKee A. Blockchain technology in the future of business cyber security and accounting, Journal of Management Analytics, 2020, vol. 7, no. 2, pp. 189—208.
  21. Griggs K. N., Ossipova O., Kohlios C. P., Baccarini A. N., Howson E. A., Hayajneh T. Healthcare blockchain system using smart contracts for secure automated remote patient monitoring, Journal of medical systems, 2018, vol. 42, no. 7.
  22. Perera S., Nanayakkara S., Rodrigo M., Senaratne S., Weinand R. Blockchain technology: Is it hype or real in the construction industry? Journal of Industrial Information Integration, 2020, vol.17, no. 3, pp. 100—125.
  23. Zhang C., Chen Y. A review of research relevant to the emerging industry trends: Industry 4.0, IoT, block chain, and business analytics, Journal of Industrial Integration and Management, 2019, vol.5, no. 10.
  24. Viriyasitavat W., Da Xu L., Bi Z., Sapsomboon A. New blockchain-based architecture for service interoperations in internet of things, IEEE Transactions on Computational Social Systems, 2019, vol. 6, no. 4, pp. 739—748.
  25. "Nornikel'" provol vypusk tsifrovykh finansovykh aktivov na blokcheyn-platforme "Atomayz", available at: https://www.nornickel.ru/news-and-media/press-releases-and-news/nornikel-provy-el-vypusk-tsifrovykh-finansovykh-aktivov-na-blokcheyn-platforme-atomayz/%60/$%7Bthis.$root.lang%7D/other-sites/%60 (in Russian).
  26. Sber vnedril smart-kontrakt v kreditnom protsesse, available at: https://sber.pro/publication/sber-vnedril-smart-kontrakt-v-kreditnom-protsesse/ (in Russian).
  27. S7 sovershila pervuyu v Rossii sdelku s ispol'zovaniyem blokcheyn, available at: https://nsk.rbc.ru/nsk/freenews/585133769a79472423b133b9 (in Russian).
  28. How Barclays Used R3's Tech to Build a Smart Contracts Prototype, available at: https://bankingonblockchain.com/uncategorized/how-barclays-used-r3s-tech-to-build-a-smart-contracts-prototype/.
  29. Murray Y., Anisi D. A. Survey of formal verification methods for smart contracts on blockchain, 10th IFIP International Con­ference on New Technologies, Mobility and Security, 2019, pp. 1—6.
  30. Rushby J. Theorem proving for verification, Summer School on Modeling and Verification of Parallel Processes, Springer, 2000, pp. 39—57.
  31. Hu Y. Exploring formal verification methodology for fpga-based digital systems, IET Computers & Digital Techniques, 2017, vol. 11, no. 6.
  32. Nesi M. A brief introduction to higher order logic and the hol proof assistant, Nipkow T., Wenzel M., Paulson L. C. (eds) Isabelle/HOL, Lecture Notes in Computer Science, vol. 2283, Springer Berlin, Heidelberg, 2011.
  33. Gange G., Navas J., Schachte P., Sondergaard H., Stuckey P. Horn Clauses as an Intermediate Representation for Program Analysis and Transformation, Theory and Practice of Logic Programming, 2015, vol. 15, pp. 526—542.
  34. De Moura L., Bjorner N. Z3: An efficient SMT solver, International conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer, 2008, pp. 337—340.
  35. Yang Z., Lei H., Qian W. A Hybrid Formal Verification System in Coq for Ensuring the Reliability and Security of Ethereum-Based Service Smart Contracts, IEEE Access, 2020, vol. 8, pp. 21411—21436.
  36. Abhishek A., Boulier S., Cohen C. Towards Certified Meta-Programming with Typed Template-Coq, Interactive Theorem Proving, 2018, pp. 23—29.
  37. Yang Z., Lei H. FEther: An Extensible Definitional Interpreter for Smart-contract Verifications in Coq, IEEE Access, 2019, pp. 13—18.
  38. Swamy N., Hritcu C., Keller C., Rastogi A., Delignat-Lavaud A., Forest S., Bhargavan K., Fournet C., Strub P., Kohlweiss M., Zinzindohoue J. K., Beguelin S. Z. Dependent types and multi-monadic effects in F, Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2016, pp. 256—270.
  39. Barthe G., Fournet C., Gregoire B., Strub P., Swamy N., Beguelin S. Z. Probabilistic relational verification for cryptographic implementations, The 41st Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2014, pp. 193—206.
  40. Annenkov D., Nielsen J. B., Spitters B. ConCert: A smart contract certification framework in Coq, Proc.of ACM CCP, 2020, pp. 215—228.
  41. Fedotov I. A., Khritankov A. S. Systematic Review of Automatic Verification of Smart-Contracts, Programmnaya Ingeneria, 2020, vol. 11, no. 1, pp. 3—13. DOI: 10.17587/prin.11.3-13 (in Russian).
  42. Nehai Z., Piriou P., Daumas F. F. Model-checking of smart contracts, IEEE International Conference on Internet of Things (iThings) and IEEE Green Computing and Communications (GreenCom) and IEEE Cyber, Physical and Social Computing (CPSCom) and IEEE Smart Data (SmartData), 2018, pp. 980—987.
  43. Cavada R., Cimatti A., Dorigatti M., Griggio A., Mariotti A., Micheli A., Mover S., Roveri M., Tonetta S. The nuxmv symbolic model checker, Computer Aided Verification — 26th International Conference, Held as Part of the Vienna Summer of Logic, 2014, pp. 334—342.
  44. Browne M. C., Clarke E. M., Grumberg O. Characterizing finite kripke structures in propositional temporal logic, Theoritical Computer Science, 1988, vol. 59, pp. 115—131.
  45. Lahiri S. K., Chen S., Wang Y., Dillig I. Formal specification and verification of smart contracts for azure blockchain, 2018, available at: https://arxiv.org/pdf/1812.08829v1.
  46. Kalra S., Goel S., Dhawan M., Sharma S. ZEUS: analyzing safety of smart contracts, 2018, available at: https://www. ndss-symposium.org/wp-content/uploads/2018/02/ndss2018_09-1_Kalra_paper.pdf.
  47. Sinnema R., Wilde E. Extensible access control markup language (xacml) xml media type, Internet Engineering Task Force (IETF), 2013, pp. 1—8.
  48. Mavridou A., Laszka A., Stachtiari E., Dubey A. Verisolid: Correct-by-design smart contracts for ethereum, Financial Cryptography and Data Security — 23rd International Conference, 2019, pp. 446—465.
  49. Transition system, Wikipedia, available at: https://en.wikipedia.org/wiki/Transition_system.
  50. Basu A., Bozga M., Sifakis J. Modeling heterogeneous real-time components in bip, Fourth IEEE International Conference on Software Engineering and Formal Methods, 2006, pp. 3—12.
  51. Cavada R., Cimatti A., Dorigatti M., Griggio A., Mariotti A., Micheli A., Mover S., Roveri M., Tonetta S. The nuxmv symbolic model checker, Computer Aided Verification — 26th International Conference, Held as Part of the Vienna Summer of Logic, 2014, pp. 334—342.
  52. Bradley A.R. Theory and Applications of Satisfiability Testing, SAT 2012, vol. 7317.
  53. Bai X., Cheng Z., Duan Z., Hu K. Formal Modeling and Verification of Smart Contracts, 7th International Conference on Software and Computer Applications, 2018, pp. 324—326.
  54. Holzmann G. J. The model checker SPIN, IEEE Transactions on Pattern Analysis and Machine Intelligence, Software Engineering, 1997, vol. 23, no. 5, pp. 279—295.
  55. Mikk E., Lakhnech Y., Siegel M., Holzmann G. J. Imple­menting statecharts in PROMELA/SPIN, 2nd Workshop on Industrial-Strength Formal Specification Techniques, 1998, pp. 90—101.
  56. PAT: Process Analysis Toolkit — An Enhanced Simulator, Model Checker and Refinement Checker for Concurrent and Real-time Systems, available at: https://pat.comp.nus.edu.sg/
  57. Shishkin E. S. Verifying functional properties of smart contracts using symbolic model-checking, Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS), 2018, vol. 30, no. 5, pp. 265—288 (in Russian).
  58. Certora Prover, available at: https://www.certora.com/.
  59. Valmari A. The state explosion problem, Reisig W., Rozenberg G. (eds) Lectures on Petri Nets I: Basic Models, Lecture Notes in Computer Science, vol. 1491, Springer, Berlin, Heidelberg.
  60. Ellul J., Pace G. J. Runtime verification of ethereum smart contracts, 2018 14th European Dependable Computing Conference, 2018, pp. 158—163.
  61. Colombo C., Pace G. J. Runtime verification using LARVA, An International Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools, 2017, pp. 55—63.
  62. Torres C. F., Baden M., Norvill R., Jonker H. AEGIS: Smart shielding of smart contracts, Proc. of ACM CCS, 2019, pp. 2589—2591.
  63. Chen T., Cao R., Li T., Luo X., Gu G., Zhang Y., Liao Z., Zhu H., Chen G., He Z., Tang Y., Lin X., Zhang X. SODA: A generic online detection framework for smart contracts, 2020, available at: https://www.ndss-symposium.org/wp-content/uploads/2020/02/24449.pdf
  64. Luu L., Chu D., Olickel H., Saxena P., Hobor A. Making smart contracts smarter, Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security, 2016, pp. 254—269.
  65. Nikolic I., Kolluri A., Sergey I., Saxena P., Hobor A. Finding the greedy, prodigal, and suicidal contracts at scale, Proceedings of the 34th Annual Computer Security Applications Conference, 2018, pp. 653—663.
  66. Tikhomirov S., Voskresenskaya E., Ivanitskiy I., Takhaviev R., Marchenko E., Alexandrov Y. Smartcheck: Static analysis of ethereum smart contracts, 1st IEEE/ACM International Workshop on Emerging Trends in Software Engineering for Blockchain, WETSEB@ICSE 2018, 2018, pp. 9—16.
  67. Feist J., Grieco G., Groce A. Slither: a static analysis framework for smart contracts, Proceedings of the 2nd International Workshop on Emerging Trends in Software Engineering for Blockchain, WETSEB@ICSE 2019, 2019, pp. 8—15.
  68. Chen T., Li X., Luo X., Zhang X. Under-optimized smart contracts devour your money, IEEE 24 th International Conference on Software Analysis, Evolution and Reengineering, 2017, pp. 442—446.
  69. Mueller B. Smashing Ethereum Smart Contracts for Fun and Real Profit, Proc. of the 9th Annual HITB Security Conference, 2018.
  70. Torres C. F., Schutte J., State R. Osiris: Hunting for integer bugs in ethereum smart contracts, Proceedings of the 34th Annual Computer Security Applications Conference, 2018, pp. 664—676.
  71. Cousot P. Formal verification by abstract interpretation // A. Goodloe, S. Person (Eds.), NASA Formal Methods — 4th International Symposium, 2012, vol. 7226 of Lecture Notes in Computer Science, Springer, pp. 3—7.
  72. Cousot P. Formal verification by abstract interpretation, A. Goodloe, S. Person (Eds.), NASA Formal Methods — 4th International Symposium, Proceedings, vol. 7226 of Lecture Notes in Computer Science, Springer, 2012, pp. 3—7.
  73. Jordan H., Scholz B., Subotic P. Souffl'e: On synthesis of program analyzers, International Conference on Computer Aided Verification, Springer, 2016, pp. 422—430.
  74. Brent L., Jurisevic A., Kong M., Liu E., Gauthier F., Gramoli V., Holz R., Scholz B. Vandal: A scalable security analysis framework for smart contracts, ArXiv, 2019, vol. abs/1809.03981.
  75. Overview of Vandal, available at: https://github.com/usyd-blockchain/vandal/wiki.
  76. Grech N., Kong M., Jurisevic A., Brent L., Scholz B., Smaragdakis Y. MadMax: Surviving Out-of-Gas Conditions in Ethereum Smart Contracts, Proceedings of the ACM on Programming Languages, 2018, vol. 2, pp. 1—27.
  77. 77. Albert E., Gordillo P., Livshits B., Rubio A., Sergey I. Ethir: A framework for high-level analysis of ethereum bytecode, Automated Technology for Verification and Analysis — 16th International Symposium, Proceedings, 2018, pp. 513—520.
  78. Tsankov P., Dan A. M., Drachsler-Cohen D., Gervais A., Bunzli F., Vechev M. T. Securify: Practical security analysis of smart contracts, Proceedings of the 2018 ACM SIGSAC Conference on Computer and Communications Security, 2018, pp. 67—82.
  79. Jiang B., Liu Y., Chan W. Contractfuzzer: Fuzzing smart contracts for vulnerability detection, Proceedings of the 33rd ACM/ IEEE International Conference on Automated Software Engineering, 2018, pp. 259—269.
  80. Liu C., Liu H., Cao Z., Chen Z., Chen B., Roscoe B. Reguard: finding reentrancy bugs in smart contracts, 2018 IEEE/ ACM 40th International Conference on Software Engineering: Com­panion (ICSE-Companion), 2018, pp. 65—68.
  81. Liu H., Liu C., Zhao W., Jiang Y., Sun J. S-gram: Towards semantic-aware security auditing for Ethereumsmart contracts, Proc. of ACM/IEEE ASE, 2018, pp. 814—819.
  82. Wang W., Song J., Xu G., Li Y., Wang H., Su C. ContractWard: Automated vulnerability detection modelsfor Ethereum smart contracts, IEEE Transactions. on Network Science and Engineering, 2020, vol. 8, no. 2, pp. 1133—1144.
  83. Tann W. J.-W., Han X. J., Gupta S. S., Ong Y.-S. Towards safer smart contracts: A sequence learning approach to detecting security threats, ArXiv, 2018, vol. abs/1811.06632.

To the contents