A team from the University of Illinois at Urbana-Champaign took first place at this year's IC3-Ethereum Crypto Boot Camp. The winning project, KEVM, is a framework that produces the first complete, ex
A team from the University of Illinois at Urbana-Champaign took first place at this year's IC3-Ethereum Crypto Boot Camp. The winning project, KEVM, is a framework that produces the first complete, executable formal semantics of the Ethereum Virtual Machine. PhD student Everett Hildenbrandt led the team with support from IOHK.
Prof. Grigore Rosu, who directs the Siebel Center for Computer Science at UIUC and heads Runtime Verification, identified a critical problem in the smart contract ecosystem. "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," Rosu said.
Before KEVM, no one had created a complete, rigorous, executable semantics of the EVM. This left developers without a solid foundation for verification 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," Rosu 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," he added.
IOHK chose the K framework because it avoids language lock-in and has proven successful in academia. Researchers have used K to formalize JavaScript, Java, C, Python, and PHP.
Charles Hoskinson, CEO of IOHK, said the research provided substantial perspective. "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," he said.
Hoskinson outlined the roadmap emerging from the work. "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," he said.
The boot camp took place at Cornell University. The IC3 brought together professors, Ethereum Foundation members, students and developers for a week of intensive work. The program featured keynote speakers including Vitalik Buterin, founder of the Ethereum Foundation; Ittay Eyal from IC3 and Cornell; Casey Detrio from the Ethereum Foundation; and Andrew Miller from IC3 and UMD. The IC3 held the event for a second consecutive year.
Ten teams competed. The KEVM team won.
