K Framework Enables Verification of Smart Contracts
The age of cryptocurrency is here. A high percentage of cryptocurrency transactions are taking place on the Ethereum blockchain, which uses a computer program or “smart contract” to execute them. In December, Ethereum became the first cryptocurrency to amass one million transactions in a single 24-hour period.
However, any programming mistakes create openings for the theft of the virtual currency. While there are many safeguards to protect against security breaches, to date there hasn’t been a way to guarantee the formal verification of these contracts. For instance, last month hackers in Tokyo broke into the Coincheck, Inc. and stole $500 million in digtal tokens.
In a fruitful collaboration with Prof. Grigore Rosu's Formal Systems Laboratory (FSL) at UIUC, Runtime Verification (RV) has used the K framework to successfully build and test a mathematical model of the Etherem Virtual Machine, which makes it possible to formally verify the accuracy of smart contracts.
“The question of whether a program is correct cannot even be formulated if you don’t have a mathematical model of the computing environment in which this program runs,” Rosu said. “Auditors carefully read smart contract implementations and write comprehensive reports explaining their understanding of the code. Often they also suggest changes that improve the code quality or readability. But they and nobody else can guarantee correctness of an Ethereum smart contract without a formal model of the Ethereum Virtual Machine.”
RV and the FSL have mathematically formulated the Ethereum Virtual Machine (EV) in their K framework, and successfully tested the formal model, which they call KEVM, with around 40,000 programs. They found the KEVM model to be faithful to the actual EVM.
“The objective here is not to replace the EVM, but to complement its already amazing functionality with a means to formally verify the smart contracts that it executes, based on a rigorous mathematical formalization of the EVM”. Rosu noted.
The K Framework, and its potential to help tighten up blockchain security, also caught the attention of a research and engineering company that builds blockchains, IOHK, which helped fund the effort that led to the development of KEVM.
“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,” Charles Hoskinson, CEO and founder of IOHK, said.
KEVM gives RV the ability to find security and functional correctness flaws in smart contracts, and recommend fixes for them. There is currently no one in the industry with this capability, so for peace of mind, companies that plan to deploy smart contracts can hire RV to prove their smart contracts correct or help them find flaws and recommend fixes for them.
“Without formal verification, how can you trust your transactions?” Rosu said. “There are currently thousands of smart contracts that aren’t verified, but that should be verified.”
For further details on the semantics of KEVM, Rosu and his team have published a paper at http://bit.ly/2GCy9Az. The KEVM is freely available on Github, under the permissive UIUC License.
