Blockchain research and development company IOHK announced its research project conducted in collaboration with the University of Illinois at Urbana-Champaign has modeled what they say is the world’s first complete fully-executable formal semantics of the Ethereum Virtual Machine (EVM).
The resulting framework, KEVM, allows for the formal execution, analysis and verification of EVM smart contracts.
KEVM, led by Professor Grigore Rosu and his PhD student Everett Hildenbrandt, was selected following “IC3-Ethereum Crypto Boot Camp”, a week-long blockchain development event staged by the Ethereum Foundation and IC3, an initiative of faculty members at Cornell University, Cornell Tech, UC Berkeley, the University of Illinois at Urbana-Champaign, and the Technion.
“The pressing need to address repeated security vulnerabilities and high-profile failures in Ethereum smart contracts hasn’t been adequately addressed by existing formal verification and program analysis tools,” Prof. Rosu said. “No fully-formal, rigorous, comprehensive, and executable semantics of EVM existed until now, leaving a lack of rigor on which to base such tools.
“KEVM, which allows us to formally verify properties of EVM-based smart contracts in a correct-by-construction and cost-effective manner, is significant because Ethereum users need the guarantees of formal verification to safeguard against financial losses due to software bugs. This work serves as a foundation for the development of new smart contract analysis tools; more importantly, it gives us invaluable insight on how to design better programming languages for smart contracts.”
KEVM passes the official 40,683-test stress test suite for EVM implementations and reveals ambiguities and potential sources of error in the existing on-paper formalization of EVM semantics.
“KEVM has demonstrated that our unique approach based on K formal executable semantics is feasible and not computationally restrictive,” Prof. Rosu added. “We hope our work serves as a strong basis for the development of a wide range of useful, formally-derived tools for Ethereum, like model checkers, certified compilers, and program equivalence checkers.”
IOHK said in a statement they value formal verification in cryptocurrency development due to the important role of mathematical proofs. They participated due to K’s language-independent nature, wide potential application, and academic success, where K has been used to formalize several real-world languages, like JavaScript, Java, C, Python, and PHP.
Charles Hoskinson
Several language-independent analysis tools for K also exist. It supports a semantic debugger, symbolic execution engine, and verification infrastructure for each developed language.
KEVM’s development remains open-source in keeping with IOHK’s desire to improve the entire blockchain industry.
“This research has given us a great degree of insight into what one should do to redesign the EVM to make it more secure, faster, and more efficient,” IOHK CEO Charles Hoskinson said. “It will now be easier to build tooling for the EVM, such as verified compilers. This white paper is the result of our first wave of research into this area. Based on this research, IOHK will begin building prototypes and our hope is to have an EVM 2.0 ready next year, as part of Cardano, a product we are currently building.”
Our Social Networks: Facebook Instagram Pinterest Reddit Telegram Twitter Youtube
