SEMANTIC APPROACH TO SMART CONTRACT VERIFICATION

Nenad Petrović, Milorad Tošić

DOI Number
https://doi.org/10.22190/FUACR2001021P
First page
021
Last page
037

Abstract


Vulnerabilities of smart contract are certainly one of the limiting factors for wider adoption of blockchain technology. Smart contracts written in Solidity language are considered due to common adoption of the Ethereum blockchain platform. Despite its popularity, the semantics of the language is not completely documented and relies on implicit mechanisms not publicly available and as such vulnerable to possible attacks. In addition, creating formal semantics for the higher-level language provides support to verification mechanisms. In this paper, a novel approach to smart contact verification is presented that uses ontologies in order to leverage semantic annotations of the smart contract source code combined with semantic representation of domain-specific aspects. The following aspects of smart contracts, apart from source code are taken into consideration for verification: business logic, domain knowledge, run-time state changes and expert knowledge about vulnerabilities. Main advantages of the proposed verification approach are platform independence and extendability.


Keywords

blockchain, Ethereum, semantic technology, smart contract, Solidity, software verification

Full Text:

PDF

References


N. Balani and R. Hathi, Enterprise Blockchain: A Definitive Handbook, 2017.

S. Palladino, “Ethereum for Web Developers (chapter 1)”, pp. 1-16, 2019. Available: https://doi.org/10.1007/

-1-4842-5278-9_1

A. Narayanan and J. Clark, “Bitcoin’s academic pedigree”, Communications of the ACM, 60(12), pp. 36–45, 2017.

“A Next-Generation Smart Contract and Decentralized Application Platform”. [Online]. Available: https://github.com/ethereum/wiki/wiki/White-Paper . Last accessed: 24/03/2019.

K. Zīle, R. Strazdiņa, “Blockchain Use Cases and Their Feasibility”, Applied Computer Systems, 23(1), pp. 12–20, 2018. https://doi.org/10.2478/acss-2018-0002

X. Feng, Q. Wang, X. Zhu, S. Wen, “Bug Searching in Smart Contract”, pp. 1-8, 2019. [Online]. Available on: https://arxiv.org/abs/1905.00799

D. Harz, W. Knottenbelt, “Towards Safer Smart Contracts: A Survey of Languages and Verification Methods”, pp. 1-20, 2018. Available on: https://arxiv.org/abs/1809.09805v4

V. Mathur, “Literature Review: Smart Contract Semantics”, pp. 1-9, 2018.

“Smart Contract Best Practices: Known Attacks”. [Online]. Available: https://consensys.github.io/smart-contract-best-practices/known_attacks/ . Last accessed 12/10/2019.

T. Gruber,“Toward Principles for the Design of Ontologies Used for Knowledge Sharing”, International Journal Human-Computer Studies 43 (5-6), 907-928 (1995).

C. A. R. Hoare, “An axiomatic basis for computer programming”, Communications of the ACM. 12 (10), pp. 576–580, 1969 [Online]. Available: https://doi.org/10.1145/363235.363259.

C. Furia, C. Poskitt, J. Tschannen, “The AutoProof Verifier: Usability by Non-Experts and on Standard Code”, EPTCS 187, pp. 42-55, 2015.

Z. Nehai, P. Y. Piriou, F. Daumas,, “Model-Checking of Smart Contracts”, The 2018 IEEE International Conference on Blockchain pp. 1-8 (2018). https://doi.org/10.1109/Cybermatics_2018.2018.00185

D. Annenkov, J. B. Nielsen, B. Spitters, “ConCert: a smart contract certification framework in Coq”, CPP 2020: Proceedings of the 9th ACM SIGPLAN International Conference on Certified Programs and Proofs, pp. 215-228, 2020. https://doi.org/10.1145/3372885.3373829

W. Ahrendt et al., “Verification of Smart Contract Business Logic Exploiting a Java Source Code Verifier”, FSEN 2019, LNCS 11761, pp. 228-243, 2019.

A. Hajdu and D. Jovanovic, “solc-verify: A Modular Verifier for Solidity Smart Contracts”, Verified Software: Theories, Tools, and Experiments (VSTTE 2019), pp. 1-18, 2019.

L. Brent et al., “Vandal: A Scalable Security Analysis Framework for Smart Contracts”, pp. 1-28, 2018. https://arxiv.org/pdf/1809.03981.pdf

B. Mueller, “Introducing Mythril: A framework for bug hunting on the Ethereum blockchain”. [Online], https://medium.com/hackernoon/introducing-mythril-a-framework-for-bug-hunting-on-the-ethereum-blockchain-9dc5588f82f6 . Last accessed 06/03/2020.

V. Nejkovic, N. Petrovic, M. Tosic, N. Milosevic, “Semantic approach to RIoT autonomous robots mission coordination”, Robotics and Autonomous Systems, 103438, pp. 1-19, 2020. https://doi.org/10.1016/

j.robot.2020.103438

N. Petrovic, M. Tosic, “SMADA-Fog: Semantic model driven approach to deployment and adaptivity in Fog Computing”, Simulation Modelling Practice and Theory, 102033, pp. 1-25, 2019. https://doi.org/10.1016/

j.simpat.2019.102033

N. Petrovic, “Adopting Semantic-Driven Blockchain Technology to Support Newcomers in Music Industry”, CIIT 2019, Mavrovo, North Macedonia, pp. 2-7, 2019.

N. Petrović, Đ. Kocić, “Data-driven Framework for Energy-Efficient Smart Cities”, Serbian Journal of Electrical Engineering, Vol. 17, No. 1, Feb. 2020, pp. 41-63. https://doi.org/10.2298/SJEE2001041P

T. Durieux, J. F. Ferreira, R. Abreu, P. Cruz, "Empirical Review of Automated Analysis Tools on 47,587 Ethereum Smart Contracts", pp. 1-12, 2020. [Online]. Available on: https://arxiv.org/pdf/1910.10601.pdf




DOI: https://doi.org/10.22190/FUACR2001021P

Refbacks

  • There are currently no refbacks.


Print ISSN: 1820-6417
Online ISSN: 1820-6425