The K Framework & Formal Verification Efforts in the Blockchain Space
In the past few years we witnessed the development of multiple smart contract languages — each of them requires resources for building formal verification toolsets, compilers, debuggers and other developer tools. Grigore Rosu is a Professor of Computer Science at University of Illinois at Urbana-Champaign, whose dream for the blockchain space is to see all smart contracts formally verified — and he has a tool to that purpose. The K framework is mathematic logic and language that enables language developers to formally define all programming languages, which has massive implications for smart contract programming language development and the formal verification efforts in the blockchain space. Read on or watch the full episode on Epicenter.
Prof. Grigore Rosu started off as a mathematician — when he joined NASA his job was to prove that the programs were running correctly. That’s when he started to explore formal methods and how to mathematically capture the meaning of programming languages — every single one of them had a deep mathematical meaning. The K framework, a mathematic logic and language that enables language developers to formally define all programming languages, started as a teaching tool and evolved out of that.
K was about engineering a framework that takes the best out of all the approaches of all of the programming languages — and getting rid of the limitations. It started off as an attempt to come up with mathematical structures and rules through which you can define any programming language. “You can think of it as a meta- programming language. A language in which you can express any programming language.” explains Prof. Rosu. Any property of any programming language can be proved with this language-independent framework. Once a language is formally specified in the K framework, the framework automatically outputs a range of formal verification toolsets, compilers, debuggers and other developer tools for it. Updates to the language can be made directly in K.
Why is the blockchain community interested in K? Because they are facing challenges that have never been there before. “On the blockchain everyone sees the code, making it susceptible to various attacks and there are huge incentives to get these blockchains correct and secure. That’s where formal semantics come in, which provide an actual mathematical proof that this program is secure. Thus, the likelihood of an attack is much lower”, explains Prof. Rosu.
“All smart contracts need to be verified — it’s insane that people bet their money on smart contracts that are not verified. And it’s not that hard to verify smart contracts”, says Prof. Rosu. His company Runtime Verification has been tasked with verifying various smart contracts — and it turns out that not a single smart contract they checked was flawless.
Thanks to the K framework, the proof of the correctness can also be stored on the blockchain. That proof is verifiable by third parties, and various program verifiers can be used to search for a proof. This allows for adding verifiable proofs to smart contracts on the blockchain, ensuring their security. “You don’t only verify the smart contract but also have the proof of correctness of the smart contract, on the blockchain”, explains Prof. Rosu.
Professor Rosu is now working to express the Ethereum virtual machine using the K framework, and to develop a new virtual machine technology, called IELE, specifically tailored to the blockchain space.
Show links
- Defining the undefinedness of C — formalisation of C using the K framework
- IELE — a new virtual machine for the blockchain
- Runtime verification — Grigore’s company
- K Semantics of the Ethereum Virtual Machine
- Short video on Grigore’s partnership with Cardano
- An overview of the K framework by Runtime Verification
- A detailed technical overview of the K semantic framework
Watch the full episode on Epicenter, and don’t forget to subscribe to the show on iTunes, YouTube & SoundCloud. Drop by our Gitter community channel to discuss the show and leave some feedback.
