IOHK, a self-described blockchain engineering company, has revealed that a research project in conjunction with the University of Illinois at Urbana-Champaign (UIUC) has generated a fully-executable formal semantics model of the Ethereum Virtual Machine (EVM), called KEVM.
As per the announcement, KEVM assists in the execution, analysis, and verification of EVM executable distributed code contracts (EDDCs). It also has the distinction of being selected as the winner of the IC3-Ethereum Crypto Bootcamp, which the Ethereum Foundation hosted in partnership with the Initiative for Cryptocurrencies and Contracts (IC3). Prof. Grigore Rosu and PhD student Everett Hildenbrandt competed alongside nine other teams, rising to the top with their KEVM project, the funding for which stems from IOHK. The team’s first place prize included bragging rights, and $256 USD in Ether.
Runners up included second place winner Phil Daian of Cornell, with a project called “Writing Secure Smart Contracts,” for which 10,000 Dogecoins were awarded. An undisclosed quantity of Useless Ethereum Tokens were awarded to third place winners Nate Rush of Berkeley and Loi Luu, founder of SmartPool and developer of Oyente, from National University of Singapore, for their “ETH-ETC Peace Relay.” A similar award of UET was given to the recipients of an honorable mention, Haseeb Qureshi and Preethi Kasireddy, for their “Frontrunning Bancor” project.
Rosu expressed his delight in announcing KEVM as “the first complete and fully executable formal semantics of the Ethereum Virtual Machine." He went on to say:
"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 is built upon the rewrite-based executable semantic K-framework. It passed the official 40,683-test stress test suite which was designed to ready EVM implementations, and exposes errors present in paper representations of EVM semantics, according to IOHK.
“KEVM has demonstrated that our unique approach based on K formal executable semantics is feasible and not computationally restrictive," said Rosu. "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.”
According to the whitepaper, KEVM reduces the probability of bugs that can arise from encoding semantic models in existing software by creating a wide range of tools from the same reference semantics, reinforcing the team's "semantics first" development approach. The authors affirm a commitment towards contributing to the secure development of a bug-free EDCC ecosystem.
IOHK CEO Charles Hoskinson made comments on the next steps for IOHK, based on the groundwork his team has done.
"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. 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.”
As an open source project, KEVM will continue to be developed in the public realm, and ETHNews will continue to provide coverage of new innovations the team brings to light.