Informacionnye TehnologiiInformacionnye TehnologiiИнформационные технологии1684-6400New Technologies Publishing House70225510.17587/it.31.42-55Information technologies in economy, management and productionИнформационные технологии в экономике, управлении и производствеResearch ArticleA review of smart contract verification methodsОбзор методов верификации смарт-контрактовAvdoshinS. M.АвдошинС. М.
Russian Federation

Cand. Tech. Sc., Professor

канд. техн. наук, проф.

savdoshin@hse.ruLitvinenkoA. M.ЛитвиненкоА. М.
Russian Federation

Master's Student

магистрант

amlitvinenko@edu.hse.ruHSE UniversityНациональный исследовательский университет "Высшая школа экономики" (НИУ ВШЭ)1501202531142550602202606022026Copyright ©; 2025, Informacionnye TehnologiiCopyright ©; 2025, Информационные технологии2025Informacionnye TehnologiiИнформационные технологииhttps://journals.eco-vector.com/1684-6400/article/view/702255

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.

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

smart contractformal verificationEthereumdistributed ledger technologyvulnerabilities detectionсмарт-контрактформальная верификацияEthereumтехнология распределенного реестрапоиск уязвимостейBlockchain Statistics 2024 (Market Size & Users), available at: https://www.demandsage.com/blockchain-statistics/.Blockchain Statistics 2024 (Market Size & Users). URL: https://www.demandsage.com/blockchain-statistics/ (дата обращения: 12 февраля 2024 года).Capitalizatsiya Ethereum, available at: https:// ru.tradingview.com/symbols/ETH/ (in Russian).Капитализация Ethereum. URL: https://ru.tradingview. com/symbols/ETH/ (дата обращения: 12 февраля 2024 года).Szabo N. Smart Contracts, Satoshi Nakamoto Institute, available at: https://nakamotoinstitute.org/smart-contracts/.Szabo N. Smart Contracts | Satoshi Nakamoto Institute. URL: https://nakamotoinstitute.org/smart-contracts/ (дата обращения: 12 февраля 2024 года).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.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, N. 1. P. 012050.Ethereum Whitepaper, available at: https://ethereum.org/ en/whitepaper.Ethereum Whitepaper. URL: https://ethereum.org/en/ whitepaper (дата обращения: 12 февраля 2024 года).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.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. P. 1—38.Draft Federal Law No. 419059-7 "On Digital Financial Assets" (in Russian).Проект Федерального Закона № 419059-7 "О цифровых финансовых активах".Siegel D. Understanding the DAO attack, CoinDesk, 2016, available at: https://www.coindesk.com/learn/understanding-the-dao-attack/.Siegel D. Understanding the DAO attack. URL: https:// www.coindesk.com/learn/understanding-the-dao-attack/ (дата обращения: 20 февраля 2024 года).Kriticheskaya uyazvimost’ v multisig koshel’ke Parity, available at: https://habr.com/ru/articles/333754/ (in Russian).Критическая уязвимость в multisig кошельке Parity. URL: https://habr.com/ru/articles/333754/ (дата обращения: 20 февраля 2024 года).Lazarenko A., Avdoshin S. Financial Risks of the Blockchain Industry: A Survey of Cyberattacks: Vol. 2, Proceedings of the Future Technologies Conference (FTC) 2018, 2019, pp. 368—384.Lazarenko A., Avdoshin S. Financial Risks of the Blockchain Industry: A Survey of Cyberattacks: Volume 2 // Proceedings of the Future Technologies Conference (FTC) 2018. 2019. P. 368—384.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/.Ethereum Smart Contracts Vulnerable to Hacks: $4 Million in Ether at Risk. URL: https://www.investopedia.com/news/ ethereum-smart-contracts-vulnerable-hacks-4-million-ether-risk/ (дата обращения: 17 февраля 2024 года).Uyazvimost’ v protokole Seneca privela k krazhe 1900 ETH, Novosti TradingView, available at: https://ru.tradingview. com/news/forklog:07cc9c9cc67b8:0/ (in Russian).Уязвимость в протоколе Seneca привела к краже 1900 ETH — Новости TradingView. URL: https://ru.tradingview.com/ news/forklog:07cc9c9cc67b8:0/ (дата обращения: 17 февраля 2024 года).Amani S., B¢egel M., Bortin M., Staples M. Towards verifying ethereum smart contract bytecode in isabelle/hol, Procee dings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2018, pp. 66—77.Amani S., Begel 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. P. 66—77.Sotnichek M. Formal verification of smart contracts with the k framework, 2018, available at: https://www.apriorit.com/devblog/592-formal-verification-with-k-framework.Sotnichek M. Formal verification of smart contracts with the k framework. 2018. URL: https://www.apriorit.com/devblog/592-formal-verification-with-k-framework.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.Grishchenko I. et al. EtherTrust: Sound Static Analysis of Ethereum bytecode. 2018. URL: https://www.netidee.at/sites/ default/files/2018-07/staticanalysis.pdf.Li A., Choi J. A., Long F. Securing smart contract with runtime validation, Proc. of ACM PLDI, 2020, pp. 438—453.Li A., Choi J. A., Long F. Securing smart contract with runtime validation // 41st ACM SIGPLAN International Conference on Programming Language Design and Implementation. 2020. P. 438—453.Fedotov I. A. Research and development of probabilistic methods for verification of distributed registry systems, 2022 (in Russian).Федотов И. А. Исследование и разработка вероятностных методов верификации систем распределенного реестра. Автореферат дисс., 2022.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.Almakhour M., Sliman L., Samhat A. E., Mellouk A. Verification of smart contracts: A survey // Pervasive and Mobile Computing. 2020. Vol. 67. P. 101—227.Hassani H., Huang X., Silva E. Banking with blockchained big data, Journal of Management Analytics, 2018, vol. 5, no. 4, pp. 256—275.Hassani H., Huang X., Silva E. Banking with blockchain-ed big data // Journal of Management Analytics. 2018. Vol. 5, № 4. P. 256—275.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.Demirkan S., Demirkan I., McKee A. Blockchain technology in the future of business cyber security and accounting // Journal of Management Analytics. 2020. Vol. 7, N. 2. P. 189—208.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.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, N. 130.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.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. P. 100—125.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.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, N. 10.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.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, N. 4. P. 739—748."Nornikel’" provol vypusk tsifrovykh finansovykh aktivov na blokcheyn-platforme "Atomayz", available at: https://www.nornickel.ru/news-and-media/press-releases-and-news/nornikel-provyel-vypusk-tsifrovykh-finansovykh-aktivov-na-blokcheyn-platformeatomayz/%60/$%7Bthis.$root.lang%7D/other-sites/%60 (in Russian)."Норникель" провел выпуск цифровых финансовых активов на блокчейн-платформе "Атомайз". URL: https:// www.nornickel.ru/news-and-media/press-releases-and-news/ nornikel-provyel-vypusk-tsifrovykh-finansovykh-aktivov-na-blokcheyn-platforme-atomayz/%60/$%7Bthis.$root.lang%7D/othersites/%60, 2022 (дата обращения: 1 марта 2024 года).Sber vnedril smart-kontrakt v kreditnom protsesse, available at: https://sber.pro/publication/sber-vnedril-smart-kontrakt-vkreditnom-protsesse/ (in Russian).Сбер внедрил смарт-контракт в кредитном процессе. URL: https://sber.pro/publication/sber-vnedril-smart-kontrakt-vkreditnom-protsesse/ (дата обращения: 1 марта 2024 года).S7 sovershila pervuyu v Rossii sdelku s ispol’zovaniyem blokcheyn, available at: https://nsk.rbc.ru/nsk/freenews/58513376 9a79472423b133b9 (in Russian).S7 совершила первую в России сделку с использованием блокчейн. URL: https://nsk.rbc.ru/nsk/freenews/58513376 9a79472423b133b9 (дата обращения: 1 марта 2024 года).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-contractsprototype/.How Barclays Used R3’s Tech to Build a Smart Contracts Prototype. URL: https://bankingonblockchain.com/uncategorized/how-barclays-used-r3s-tech-to-build-a-smart-contractsprototype/ (дата обращения: 1 марта 2024 года).Murray Y., Anisi D. A. Survey of formal verification methods for smart contracts on blockchain, 10th IFIP International Conference on New Technologies, Mobility and Security, 2019, pp. 1—6.Murray Y., Anisi D. A. Survey of formal verification methods for smart contracts on blockchain // 10th IFIP International Conference on New Technologies, Mobility and Security. 2019. P. 1—6.Rushby J. Theorem proving for verification, Summer School on Modeling and Verification of Parallel Processes, Springer, 2000, pp. 39—57.Rushby J. Theorem proving for verification // Modeling and Verification of Parallel Processes, 4th Summer School, MOVEP 2000, Nantes, France. Springer. 2000. P. 39—57.Hu Y. Exploring formal verification methodology for fpgabased digital systems, IET Computers & Digital Techniques, 2017, vol. 11, no. 6.Hu Y. Exploring formal verification methodology for fpgabased digital systems // IET Computers & Digital Techniques. 2017. Vol. 11, N. 6.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.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.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.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.De Moura L., Bjerner N. Z3: An efficient SMT solver, International conference on Tools and Algorithms for the Construction and Analysis of Systems, Springer, 2008, pp. 337—340.De Moura L., Bjerner N. Z3: An efficient SMT solver // International conference on Tools and Algorithms for the Construction and Analysis of Systems. Springer. 2008. Vol. 4963. P. 337—340.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.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. P. 21411—21436.Abhishek A., Boulier S., Cohen C. Towards Certified Meta-Programming with Typed Template-Coq, Interactive Theorem Proving, 2018, pp. 23—29.Abhishek A., Boulier S., Cohen C. Towards Certified Meta-Programming with Typed Template-Coq // Interactive Theorem Proving. 2018. P. 20—39.Yang Z., Lei H. FEther: An Extensible Definitional Interpreter for Smart-contract Verifications in Coq, IEEE Access, 2019, pp. 13—18.Yang Z., Lei H. FEther: An Extensible Definitional Interpreter for Smart-contract Verifications in Coq // IEEE Access. 2019. P. 13—18.Swamy N., Hritcu C., Keller C., Rastogi A., DelignatLavaud 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.Swamy N., Hritcu C., Keller C., Rastogi A., DelignatLavaud 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. P. 256—270.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.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. P. 193—206.Annenkov D., Nielsen J. B., Spitters B. ConCert: A smart contract certification framework in Coq, Proc.of ACM CCP, 2020, pp. 215—228.Annenkov D., Nielsen J. B., Spitters B. ConCert: A smart contract certification framework in Coq // Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs. 2020. P. 215—228.Fedotov I. A., Hritankov A. S. Systematic review of research in the field of automatic verification of smart contract code, Programmnaya ingeneriya, 2020, no. 1, pp. 3—13 (in Russian).Федотов И. А., Хританков А. С. Систематический обзор исследований в области автоматической верификации кода смарт-контрактов // Программная инженерия. 2020. № 1. С. 3—13.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.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), iThings/ GreenCom/CPSCom/SmartData. 2018. P. 980—987.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.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. 2014. P. 334—342.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.Browne M. C., Clarke E. M., Grumberg O. Characterizing finite kripke structures in propositional temporal logic // Theoretical Computer Science. 1988. Vol. 59, N. 1. P. 115—131.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.Lahiri S. K., Chen S., Wang Y., Dillig I. Formal specification and verification of smart contracts for azure blockchain. 2018. URL: https://arxiv.org/pdf/1812.08829v1.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_091_Kalra_paper.pdf.Kalra S., Goel S., Dhawan M., Sharma S. ZEUS: analyzing safety of smart contracts. 2018. URL: https://www. ndss-symposium.org/.wp-content/uploads/2018/02/ndss2018_091_Kalra_paper.pdfSinnema R., Wilde E. Extensible access control markup language (xacml) xml media type, Internet Engineering Task Force (IETF), 2013, pp. 1—8.Sinnema R., Wilde E. Extensible access control markup language (xacml) xml media type // Internet Engineering Task Force (IETF). 2013.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.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. P. 446—465.Transition system, Wikipedia, available at: https:// en.wikipedia.org/wiki/Transition_system.Transition system — Wikipedia. URL: https://en.wikipedia. org/wiki/Transition_system (дата обращения: 29 марта 2024 года).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.Basu A., Bozga M., Sifakis J. Modeling heterogeneous real-time components in bip // Fourth IEEE International Conference on Software Engineering and Formal Methods. 2006. P. 3—12.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.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. 2014. P. 334—342.Bradley A.R. Theory and Applications of Satisfiability Testing, SAT 2012, vol. 7317.Bradley A. R. Theory and Applications of Satisfiability Testing // SAT. 2012. Vol. 7317.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.Bai X., Cheng Z., Duan Z., Hu K. Formal Modeling and Verification of Smart Contracts // 7th International Conference on Software and Computer Applications. 2018. P. 322—326.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.Holzmann G. J. The model checker SPIN // IEEE Transactions on Pattern Analysis and Machine Intelligence. 1997. Vol. 23, N. 5. P. 279—295.Mikk E., Lakhnech Y., Siegel M., Holzmann G. J. Implementing statecharts in PROMELA/SPIN, 2nd Workshop on Industrial-Strength Formal Specification Techniques, 1998, pp. 90—101.Mikk E., Lakhnech Y., Siegel M., Holzmann G. J. Implementing statecharts in PROMELA/SPIN // 2nd Workshop on Industrial-Strength Formal Specification Techniques. 1998. P. 90—101.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/.PAT: Process Analysis Toolkit — An Enhanced Simulator, Model Checker and Refinement Checker for Concurrent and Real-time Systems. URL: https://pat.comp.nus.edu.sg/.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).Шишкин Е. С. Проверка функциональных свойств смарт-контрактов методом символьной верификации модели // Труды ИСП РАН. 2018. Vol. 30, N. 5. P. 265—288.Certora Prover, available at: https://www.certora.com/.Certora Prover. URL: https://www.certora.com/ (дата обращения: 2024 года).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.Valmari A. The state explosion problem // Reisig W., Rozenberg G. (eds) Lectures on Petri Nets I: Basic Models. ACPN 1996. Lecture Notes in Computer Science. Vol. 1491. Springer, Berlin, Heidelberg. 1998.Ellul J., Pace G. J. Runtime verification of ethereum smart contracts, 2018 14th European Dependable Computing Conference, 2018, pp. 158—163.Ellul J., Pace G. J. Runtime verification of ethereum smart contracts // International Workshop on Blockchain Dependability, in conjunction with 14th European Dependable Computing Conference. IEEE. 2018. N. 5. P. 158—163.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.Colombo C., Pace G. J. Runtime verification using LARVA // An International Workshop on Competitions, Usability, Benchmarks, Evaluation, and Standardisation for Runtime Verification Tools. 2017. Vol. 3. P. 55—63.Torres C. F., Baden M., Norvill R., Jonker H. ^GIS: Smart shielding of smart contracts, Proc. of ACM CCS, 2019, pp. 2589—2591.Ferreira Torres C., Baden M., Norvill R., Jonker H. ^GIS: Smart shielding of smart contracts // Proc. Of ACM CCS. 2019. P. 2589—2591.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.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. URL: https://www.ndss-symposium.org/wp-content/uploads/2020/02/24449.pdf.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.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. P. 254—269.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.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. P. 653—663.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.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. P. 9—16.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.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. P. 8—15.Chen T., Li X., Luo X., Zhang X. Under-optimized smart contracts devour your money, IEEE 24th International Conference on Software Analysis, Evolution and Reengineering, 2017, pp. 442—446.Chen T., Li X., Luo X., Zhang X. Under-optimized smart contracts devour your money // IEEE 24th International Conference on Software Analysis, Evolution and Reengineering, SANER. 2017. P. 442—446.Mueller B. Smashing Ethereum Smart Contracts for Fun and Real Profit, Proc. of the 9th Annual HITB Security Conference, 2018.Mueller B. Smashing Ethereum Smart Contracts for Fun and Real Profit // Proc. of the 9th Annual HITB Security Conference. 2018.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.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. P. 664—676.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.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. P. 3—7.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.Cousot P. Formal verification by abstract interpretation // A. Goodloe, S. Person (Eds.), NASA Formal Methods — 4th International Symposium, NFM 2012, Proceedings. Vol. 7226 of Lecture Notes in Computer Science, Springer. 2012. P. 3—7.Jordan H., Scholz B., Subotic P. Souffl’e: On synthesis of program analyzers, International Conference on Computer Aided Verification, Springer, 2016, pp. 422—430.Jordan H., Scholz B., Subotic P. Souffl’e: On synthesis of program analyzers // International Conference on Computer Aided Verification. Springer, 2016. P. 422—430.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.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.Overview of Vandal, available at: https://github.com/usydblockchain/vandal/wiki.Overview of Vandal. URL: https://github.com/usyd-blockchain/vandal/wiki (дата обращения: 23 марта 2024 года).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.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. P. 1—27.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.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. 2018. P. 513—520.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.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. P. 67—82.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.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. P. 259—269.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: Companion (ICSE-Companion), 2018, pp. 65—68.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: Companion (ICSE-Companion). IEEE. 2018. P. 65—68.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.Liu H., Liu C., Zhao W., Jiang Y., Sun J. S-gram: Towards semantic-aware security auditing for Ethereum smart contracts // The 33rd ACM/IEEE International Conference. 2018. P. 814—819.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.Wang W., Song J., Xu G., Li Y., Wang H., Su C. ContractWard: Automated vulnerability detection models for Ethereum smart contracts // IEEE Transactions on Network Science and Engineering. 2020. Vol. 8, N. 2. P. 1133—1144.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.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.