AN ALGEBRAIC APPROACH TO THE VERIFICATION OF SMART CONTRACTS IN TEAL
Abstract
Blockchain and smart contracts have transformed the modern world. They help ensure security and trust in transactions, revolutionize finance, logistics, healthcare, and many other industries. Smart contracts are based on software code, so they can contain errors that lead to incorrect execution of the contract. Since the area of use of smart contracts is often related to finance, the cost of such errors can be quite high. Also, errors in smart contracts that have already been sent to the network cannot be corrected due to the immutable nature of the blockchain. This problem can be solved through smart contract code analysis, which allows developers to check the correctness of their code and protect it from possible errors and vulnerabilities.
This article proposes the use of insertional modeling to analyze smart contract code for the Algorand blockchain. This blockchain is one of the fastest, low-cost, carbon-negative blockchains that has advanced smart contract capabilities with low transaction fees. The language used to create smart contracts in Algorand is called Transaction Execution Approval Language (TEAL).
In this work, we review existing tools for TEAL code verification and describe the capabilities that each of them provides. Among these tools are Graviton, Tealer, Algo Builder/runtime. In this paper we describe the features of the TEAL language, as well as give examples of writing a smart contract using it.
We offer our method for verification created smart contract. It consists in using the algebraic approach, which is implemented in the scope of the insertion modeling system to verify the smart contract code. This approach will allow us to check the smart contract code for some state reachability and deadlocks.
Downloads
Metrics
References
2. What are smart contracts on blockchain?, IBM. https://www.ibm.com/topics/smart-contracts
3. Jesse Coghlan. (2022, May 03). More than $1.6 billion exploited from DeFi so far in 2022. Cointelegraph. https://cointelegraph.com/news/more-than-1-6-billion-exploited-from-defi-so-far-in-2022
4. The world’s most powerful and sustainable blockchain. https://algorand.com/
5. The smart contract language. Algorand Developer Portal. https://developer.algorand.org/docs/get-details/dapps/avm/teal/
6. Graviton. https://github.com/algorand/graviton
7. Graviton Algorand, https://github.com/algorand/graviton/blob/main/graviton/README.md
8. Tealer. https://github.com/crytic/tealer
9. Vara Prasad Bandaru. (2022, February 09). Detector Documentation. https://github.com/crytic/tealer/wiki/Detector-Documentation#missing-assetcloseto-field-validation
10. Algo Builder. Testing TEAL. //https://algobuilder.dev/guide/testing-teal.html
11. Letichevsky, A., & Gilbert, D. (2000). A model for interaction of agents and environments. In Recent Trends in Algebraic Development Techniques: 14th International Workshop, WADT’99, Château de Bonas, September 15-18, 1999 Selected Papers 14 (pp. 311-328). Springer Berlin Heidelberg.
12. Letichevsky, A. A., & Gilbert, D. R. (1996, October). A universal interpreter for nondeterministic concurrent programming languages. In Fifth Compulog network area meeting on language design and semantic analysis methods.
13. Letichevsky, A., Letychevskyi, O., Peschanenko, V., & Poltorackij, M. (2017, September). An algebraic approach for analyzing of legal requirements. In 2017 IEEE 25th International Requirements Engineering Conference Workshops (REW) (pp. 209-212). IEEE.
14. Letychevskyi, O. O., Peschanenko, V. S., & Poltorackiy, M. Y. (2022). Algebraic approach to the analysis of legal documents. PROBLEMS IN PROGRAMMING, (3-4), 117-127.
15. Letychevskyi, O., Peschanenko, V., Radchenko, V., Poltoratskyi, M., & Tarasich, Y. (2019). Formalization and algebraic modeling of tokenomics projects. In CEUR Workshop Proceedings (pp. 577-584).
16. Letychevskyi, O., Peschanenko, V., Poltoratskyi, M., & Tarasich, Y. (2020). Our approach to formal verification of token economy models. In Information and Communication Technologies in Education, Research, and Industrial Applications: 15th International Conference, ICTERI 2019, Kherson, Ukraine, June 12–15, 2019, Revised Selected Papers 15 (pp. 348-363). Springer International Publishing.
17. Letychevskyi, O. O., Peschanenko, V. S., Poltorackiy, M. Y., Tarasich, Y. H., & Vinnyk, M. O. (2022). Formal semantics and analysis of tokenomics properties. PROBLEMS IN PROGRAMMING, (3-4), 128-138.
18. Letychevskyi, O., Tarasich, Y., Peschanenko, V., Volkov, V., Sokolova, H., & Poltoratskyi, M. (2022, November). Algebraic Modeling as One of the Methods for Solving Organic Chemistry Problems. In Information and Communication Technologies in Education, Research, and Industrial Applications: 17th International Conference, ICTERI 2021, Kherson, Ukraine, September 28–October 2, 2021, Revised Selected Papers (pp. 180-202). Cham: Springer International Publishing.
19. Letychevskyi, O. A., Peschanenko, V., Poltoratskyi, M., & Tarasich, Y. (2020). Platform for Modeling of Algebraic Behavior: Experience and Conclusions. In ICTERI Workshops (pp. 42-57).
20. Jacobson, F., & Andersson Kasche, G. (2022). Tracing of Second-Life Computer Components using Smart Contracts on the Algorand Blockchain: A study on how blockchain technology can benefit the life cycle of computer components.
21. Letichevsky, A. A., Kapitonova, Y. V., Volkov, V. A., Letichevsky, A. A., Baranov, S. N., Kotlyarov, V. P., & Weigert, T. (2005). Systems specification by basic protocols. Cybernetics and Systems Analysis, 41, 479-493.
22. Letichevsky, A., Kapitonova, J., Letichevsky Jr, A., Volkov, V., Baranov, S., Weigert, T.: Basic protocols, message sequence charts, and the verification of requirements specifications. Computer Networks 49(5), 661-675 (2005).
