Formal design and modeling
Make your design precise by writing it in a formal language
We can prove properties of a design, generate an executable implementation, or build other tools on top of it. Every engagement differs, so rather than a template, here are four pieces of work that mark out the range.
Virtual machines: KEVM and IELE
A formal specification of a bytecode language produces the virtual machine that runs it.
Compilers turn programs written in high-level languages into programs written in raw bytes. Those bytes are then interpreted by what is misleadingly called a "machine". Sometimes the machine is implemented in silicon (a CPU, a core), and sometimes it is another program: a virtual machine, or VM.
The raw bytes can be translated into text, but the result is unfriendly to human readers. Here is part of one:
mstore(0x40, 0x80) callvalue dup1 iszero tag_1 jumpi
That is the language interpreted by the Ethereum Virtual Machine, or EVM: a blockchain VM that supports smart contracts.
In 2017, IOHK funded the University of Illinois and Runtime Verification to develop KEVM, a formal specification for the EVM; use that specification to automatically generate a correct-by-construction implementation; and make it fast enough to run a test network. The project was a success.
The work also included proofs of correctness (and of incorrectness) of smart contracts. The same specification that produces KEVM is what shows that a contract does what it is supposed to. That is the approach in miniature: do the hard work of writing a formal specification first, then get the tools and capabilities out of it for less than it would cost to build each independently.
KEVM formalized an existing design. That experience, plus prior work on the LLVM compiler framework, suggested a new virtual machine: potentially faster than the EVM, inherently more resistant to smart contract exploits, and designed to make proofs of contract correctness easier. IOHK funded that machine, IELE, and later deployed it to their test network.
Dynamic analysis: undefined behavior in C
If the standard says anything may happen, the useful thing to do is tell the programmer what did.
We began with an existing executable formal semantics for C, written using the K toolkit. It obeyed the official C11 specification, which takes care to call out undefined behavior. If a program does something defined to be undefined, such as dividing by zero, anything is allowed to happen. Because compiler writers can exploit undefined behavior to produce faster code in the defined cases, the scope of "anything" can be surprisingly broad. A compiler could, metaphorically, reason: if this variable is zero here, there would have been a divide-by-zero back there, so "anything" gives me licence to discard this entire chunk of code. In the name of efficiency, that escalates a wrong answer into a much more severe bug, such as a security breach.
Our first C semantics produced an interpreter that handled undefined behavior the usual way: it did whatever was convenient for the interpreter, not the programmer. But if anything is allowed and efficiency is not the overriding goal, why not do something useful, like print "you divided by zero on line 3838"?
Support from NASA, Boeing, Toyota and Denso had us do exactly that: extend the semantics so undefined behavior was explicitly defined to be helpful to the programmer. There are a great many undefined behaviors in C, so this was a big undertaking, and it is where the RV-Match tool came from.
Language specifications: C, Solidity, Vyper and more
Specify a high-level language and you get an interpreter, a compiler, and somewhere to hang every tool after that.
Alongside the C specification above, we have formalized specifications for the Solidity, Plutus and Vyper blockchain languages. Just as a formal specification of a virtual machine's bytecode language produces a virtual machine, a formal specification of a high-level language produces an interpreter or a compiler. Once the specification exists, specialized tools such as the undefined-behavior checker above can be built from it.
Distributed system algorithms: RANDAO
How badly could an affordable set of computers bias a blockchain’s random numbers? A question you can answer before anyone ships.
Blockchains evolve as their earlier limitations start to matter and new applications appear, and each change requires the many computers that collectively run the chain to implement new algorithms. Ethereum's Serenity release required those computers to use RANDAO, an algorithm that forces all of them to agree on random numbers. It is as if every computer in the world agreed to get heads or tails by flipping one particular coin.
Like all blockchain algorithms, RANDAO has to resist active subversion. Here the attackers would be trying to bias the random numbers: by analogy, shaving that single worldwide coin so it comes up heads 50.01 percent of the time. At small scale that would not matter. At the scale of a blockchain, a difference that small multiplies into large illicit gains.
Blockchain systems are open, in that anyone can buy computers and help compute the chain. So the question the Ethereum Foundation put to Runtime Verification was: how badly could an affordable set of computers bias the random numbers?
We determined that term rewriting (using Maude) and statistical model checking (using PVeStA) best suited the problem, and with them found that a large number of computers would be required to produce only a small bias, unless the attack were continuous and lengthy. A lengthy attack raises the chance of detection and costs the attacker increasing amounts of money: computers in RANDAO must deposit to participate, and the attack requires forfeiting those deposits. In realistic situations the attacker's gain is unlikely to be worth the investment.
As a result, RANDAO could be deployed with more confidence.
Have a design that would be worth writing down precisely?
Talk to our team