KEVM, a framework developed by the University of Illinois at Urbana-Champaign (UIUC) with support from IOHK, has won this year’s IC3-Ethereum Crypto Boot Camp, a blockchain development event and competition.
The team has modeled the world’s first complete, fully executable formal semantics of the Ethereum Virtual Machine (EVM), and produced the KEVM framework, which allows for formal execution, analysis, and verification of EVM smart contracts.
“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,” said Prof. Grigore Rosu of the UIUC’s Siebel Center for Computer Science and CEO of Runtime Verification. Until now, no fully-formal, rigorous, comprehensive, and executable semantics of EVM existed, leaving a lack of rigor on which to base such tools.
“KEVM allows us to formally verify properties of EVM-based smart contracts in a correct-by-construction and cost-effective manner. It is significant because Ethereum users need the guarantees of formal verification to safeguard against financial losses due to software bugs,” he said.
“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.”
IOHK said it chose to invest in the search and development of a formal semantics of the EVM based on the K framework due to K’s language-independent nature, wide potential application, and its success in academia, where K has been used to formalize several real-world languages such as JavaScript, Java, C, Python, and PHP.
“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. It will now be easier to build tooling for the EVM, such as verified compilers,” said Charles Hoskinson, CEO and founder of IOHK, an engineering company that builds cryptocurrencies and blockchains for academic institutions, government entities and corporations.
“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.”
Held at the Connell University, the IC3’s second annual Ethereum Crypto Boot Camp brought together professors, Ethereum Foundation contributors and top students and developers for an immersive week-long coding and learning experience in blockchains and smart contracts.
The boot camp featured daily keynote presentations by smart contract and blockchain experts such as Vitalik Buterin, founder of the Ethereum Foundation, Dr. Ittay Eyal from IC3 and Cornell University, Casey Detrio from the Ethereum Foundation, Andrew Miller from IC3 and UMD, among others.
The team behind KEVM competed against nine other teams tasked with solving with solving some of the problems currently facing the Ethereum ecosystem.