%0 Conference Proceedings
%T Towards a Formally Verified EVM in Production Environment
%+ Peking University [Beijing]
%+ School of Mathematical Sciences
%+ Center for Quantum Computing [Shenzhen] (CQC)
%A Zhang, Xiyue
%A Li, Yi
%A Sun, Meng
%Z Part 9: Verification and Analysis
%< avec comité de lecture
%( Lecture Notes in Computer Science
%B 22th International Conference on Coordination Languages and Models (COORDINATION)
%C Valletta, Malta
%Y Simon Bliudze
%Y Laura Bocchi
%I Springer International Publishing
%3 Coordination Models and Languages
%V LNCS-12134
%P 341-349
%8 2020-06-15
%D 2020
%R 10.1007/978-3-030-50029-0_21
%K EVM
%K Why3
%K Verification
%K Testing
%Z Computer Science [cs]
%Z Computer Science [cs]/Networking and Internet Architecture [cs.NI]Conference papers
%X Among dozens of decentralized computing platforms, Ethereum attracts widespread attention for its native support of smart contracts by means of a virtual machine called Ethereum Virtual Machine (EVM). Programs can be developed in various front-end languages. For example, Solidity can be deployed to the blockchain in the form of compiled EVM opcodes. However, such flexibility leads to critical safety challenges. In this paper, we formally define the behavior of EVM in Why3, a platform for deductive program verification, which facilitates the verification of different properties. The extracted implementation in OCaml can be directly integrated into the production environment and tested against the standard test suite. The combination of proofs and testing in our framework serves as a powerful analysis basis for EVM and smart contracts.
%G English
%Z TC 6
%Z WG 6.1
%2 https://inria.hal.science/hal-03273991/document
%2 https://inria.hal.science/hal-03273991/file/495623_1_En_21_Chapter.pdf
%L hal-03273991
%U https://inria.hal.science/hal-03273991
%~ IFIP-LNCS
%~ IFIP
%~ IFIP-TC
%~ IFIP-WG
%~ IFIP-TC6
%~ IFIP-WG6-1
%~ IFIP-COORDINATION
%~ IFIP-LNCS-12134