CS @ ILLINOIS student uses a tool called K to build a path towards more secure blockchains

Cryptocurrencies—and the blockchain technology that underlies them—are creating a wave of excitement that’s rising well beyond the financial world. They include the cryptocurrency Ethereum, which features the use of computer programs known as “smart contracts” to execute financial transactions.

But Ethereum’s contracts include a drawback. Any programming mistakes create openings for the theft of the virtual currency.

“The smart contracts are visible, they are on the blockchain. Everybody sees them,” says Grigore Rosu, a CS @ ILLINOIS professor. “And if an error can be exploited, somebody will, because people can immediately make money from these.”

In just one example, $50 million worth of cryptocurrency was stolen in June 2016 from a network built on the Ethereum blockchain, a loss so large that it created alarm at the Securities and Exchange Commission.

Rosu’s research group has added a powerful tool with a deceptively simple name to the arsenals of people trying to write secure smart contracts. The K Framework, developed over the last decade in Rosu’s Formal Systems Laboratory (FSL) in collaboration with his U of I-licensed startup Runtime Verification (RV), significantly eases the development of formal semantics of programming languages.

Rosu’s group used K to build the semantics of the Ethereum Virtual Machine, or EVM, the language that executes smart contracts on Ethereum.

Everett Hildenbrandt, a PhD student in Rosu’s group who is leading the KEVM (K semantics of EVM) effort, won first prize at the IC3-Ethereum Crypto Boot Camp in July by extending the EVM smart-contract language to resemble more modern imperative languages like C. EVM is a low-level assembly-like language, meaning that writing programs in it is difficult and error-prone.

Blockchains have generated buzz in the corporate and financial worlds because of their decentralized nature—an expanding ledger of transactions on a decentralized computing system, secured by cryptography. They have the potential to eliminate the middlemen who are now needed for all sorts of transactions. And cryptocurrencies have the potential to ease commerce in places that lack stable banking or legal systems because they rely on blockchains’ linked sets of transactions, which are both transparent to everyone involved and executed only after the agreed-upon terms of the contract have been met.

“Many people cannot easily get a credit card. They cannot buy, like you do, something from Amazon,” Rosu said. “Cryptocurrencies make all people equal in transactions.”

But as Hildenbrandt says, verifying that a given smart contract works as planned is time-consuming and expensive. KEVM provides a verification engine that can be used to help ensure contracts work as planned and aren’t vulnerable to attack.

Using K, “I just built a small language on top of EVM that made it easier to write EVM programs, essentially” Hildenbrandt said.

Writing a new language sounds like a major undertaking, particularly over the course of a few days at the boot camp.

“I think that’s why I won, honestly, because to most people that does sound daunting. They’ll say like, ‘There’s no way I can build a programming language, I can hardly write programs in a programming language,’” Hildenbrandt said.

“But that’s exactly the point of K,” Rosu says. “People tend to think that a programing language is like a big thing—that it’s there and you cannot touch. Programming languages are easy—should be easy—to design. If you have the right tools you should be able to design a programming language on a regular basis.”

K, 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 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.

Hildenbrandt said being part of and winning at IC3 boot camp provided a boost for him, Rosu’s group at Illinois, and for RV.

“It made it a lot clearer what the Ethereum community needs that we can offer here,” Hildenbrandt said.