Formal Verification for n00bs — Part 1: The K ecosystem

Marek Kirejczyk
Jan 25, 2019 · 4 min read

This is first in a series of blog posts on Formal Verification:
Part 1: The K ecosystem
Part 2: Proving the correctness of a token
Part 3: Formal Verification for n00bs -Part 3: An attempt to prevent classic hack with Act
Part 4: Understanding K language

The motivation for Formal Verification

Security of smart contracts is still a crucial challenge: we all remember the DAO, parity hacks, a bunch of smaller attacks and the most recent delayed hard fork. We would like to see the future in which we can be way more confident about our code.

Depending how you count, event over a half a billion dollars (by today’s Ethereum evaluation), was lost in a couple of biggest smart contract hacks.

What about if behind every responsible piece of code stands pure solid mathematics instead of personal conviction of developers? With formal verification tools for Ethereum finally maturing, it is now not only possible but also practical.

In this and following post we will be getting step by step into the world of K-framework, which allows to formally verify EVM smart contracts.

The heart: Semantics and the K language

The heart of the whole ecosystem is language K. K is a language specially designed for defining semantics. Semantics describes the behavior of computer programs. For example, when we say that a construction x++ for x that is uint means that a program in Solidity executing it will always increase the value of x by 1, except for one value x = 2^256–1:

Example of “low-level” semantics in plain words:
x++ set value of x to 0, if x = 2^256–1;
x++ sets value of x to x+1; otherwise.

This type of semantics, describing the meaning of every single instruction, is a kind of low-level definition. Besides that, what K also allows is to create high-level semantics, feasible to formulate semantics like the one below.

Example of “high-level” semantics in plain words:
Function bool isPrime(int x) returns true only if x is a prime.

To formally prove that your smart contract behaves as you wish, you need to provide:

  • low-level semantics of the language you use.
  • code of your program (EVM bytecode)
  • provide high-level (intended) semantics of your program
Image for post
Image for post

Providing high-level semantics is the most interesting and at the same time most challenging: you have to formulate how you actually wish that your program behaves.

Magic

Then the magic starts. The verifier is proving (or finding a counter-example) that your program together with low-level semantics of the programming language that you use, is indeed doing exactly the same stuff as behavior described by provided high-level semantics.

The K ecosystem

The K-framework ecosystem is somewhat complex but contains all you need:

  • K language that allows you to write any kind of semantics;
  • Tooling that allows proving semantics using Z3 - a tool for automatic proving created by Microsoft Research;
  • Semantics for Ethereum Virtual Machine - KEVM, written by Everett Hildenbrandt;
  • Two (EDIT) c̶o̶m̶p̶e̶t̶i̶n̶g̶ DSLs to create high-level semantics: act (part of KLAB created by dapphub) and eDSL (created by runtimeverification).
The ecosystem for creating proofs on EVM

So the only additional work to do after the developing process is to write high-level intended semantics and put all the machinery to work.

The high-level semantics you can do it directly in K or use one of the mentioned DSLs tailored, particularly for Solidity.

Let’s take a look at the example

The natural questions are born here: how complicated high-level semantics is possible to formulate in K? Below is an example of high-level semantics of a ERC20 transfer function, written in Dapphub/klab specification language:

What does it all mean? We will answer this question in the very next blog post in the series. Spring is coming for formal verification!

Special thanks to Tomasz Kazana who’s work on formal verification in Ethworks lead to writing this blog post.

Stay tuned

To get updates on formal verification and other Ethereum related topic follow us on twitter: @ethworks

You can also follow us on Medium if you like the story 👏 👏 👏.

Ethworks

On the blockchain, software engineering and running a company.

Sign up for 💡 Waffle News 💡

By Ethworks

Best practices in testing smart contracts with Waffle: our sweeter and simpler library built for Ethereum developers Take a look

By signing up, you will create a Medium account if you don’t already have one. Review our Privacy Policy for more information about our privacy practices.

Check your inbox
Medium sent you an email at to complete your subscription.

Marek Kirejczyk

Written by

Ethereum blockchain Engineer. Ethworks, Universal Login.

Ethworks

Ethworks

Software is eating the world. Blockchain is eating money. Ethworks is cooking.

Marek Kirejczyk

Written by

Ethereum blockchain Engineer. Ethworks, Universal Login.

Ethworks

Ethworks

Software is eating the world. Blockchain is eating money. Ethworks is cooking.

Medium is an open platform where 170 million readers come to find insightful and dynamic thinking. Here, expert and undiscovered voices alike dive into the heart of any topic and bring new ideas to the surface. Learn more

Follow the writers, publications, and topics that matter to you, and you’ll see them on your homepage and in your inbox. Explore

If you have a story to tell, knowledge to share, or a perspective to offer — welcome home. It’s easy and free to post your thinking on any topic. Write on Medium

Get the Medium app

A button that says 'Download on the App Store', and if clicked it will lead you to the iOS App store
A button that says 'Get it on, Google Play', and if clicked it will lead you to the Google Play store