1 of 52

09 September 2021, ICTAC

Formal Design, Implementation and Verification of Blockchain Languages using K

Grigore Rosu

Professor of CS, University of Illinois at Urbana

President & CEO, Runtime Verification Inc.

2 of 52

What is ?

2

3 of 52

Ideal Language Framework Vision

3

Deductive program verifier

Parser

Interpreter

Compiler

(semantic) Debugger

Symbolic execution

Model checker

Formal Language Definition

(Syntax and Semantics)

…

4 of 52

Current State-of-the-Art�- Sharp Contrast to Ideal Vision -

4

C

Java

JavaScript

Solidity

Ethereum VM

…

Interpreter

Symbolic Execution

Compiler

Model Checker

Deductive Verifier

…

Separate tools, by separate teams, little to no code shared

Before I dive into how we approach the ideal language framework vision with K, let me tell you a few words about the state-of-the-art.

Unfortunately, the state-of-the-art is still far from the ideal vision.

The PL and FM communities still develop each tool individually for each programming language.

[CLICK]

Compilers are perhaps the most known language-specific tools, like gcc and clang for C, but there are many many other tools besides compilers that are being developed specifically for each language.

[CLICK]

For example, there are also interpreters for C that target detecting undefined behavior (like the TrustInSoft interpreter).

[CLICK]

Then we have model checkers for C, like CBMC.

[CLICK]

Then symbolic execution and deductive program verifiers, like Microsoft’s VCC.

[CLICK]

Many of these tools are developed essentially from scratch, sharing very little code or functionality with each other.

And when the C language evolves, eg from C11 to C17, all the tools need to be updated.

5 of 52

Current State-of-the-Art�- Sharp Contrast to Ideal Vision -

5

C

Java

JavaScript

Solidity

Ethereum VM

…

Interpreter

Symbolic Execution

Compiler

Model Checker

Deductive Verifier

…

The story of the PL/FM community.

Maintenance hell

(L * T systems).

Uneconomical.

Wasted talent!

L

T

And then the same story unfolds for other popular languages, like Java.

[CLICK]

Or JavaScript, among others.

[CLICK]

And now we see the same happening again, with blockchain languages like Solidity and EVM.

Over and over again, the same story repeated for more than 50 years, and still going.

[CLICK]

The story of our PL/FM community.

At best uneconomical.

A maintenance hell: indeed, if you have L languages and T tools, then we need to develop and maintain L * T systems!

Not to mention all the talent and PhDs wasted doing the same thing, the same tools implementing the same fundamental algorithms and abstractions, but for different languages.

So no, we do NOT indent to “bring the state-of-ther-art in formal analysis to the blockchain”, because we firmly believe that the state-of-the-art is already obsolete and in need of a fundamental overhaul.

The blockchain comes with stringent requirements of correctness, where bugs in adhoc implemented tools are not acceptable anymore, and with new programming languages and virtual machines in immediate and rather desperate need of formal verification tools.

We regard the blockchain as an opportunity to do things right and push the state-of-the-art to the next level.

6 of 52

How It Should Be

6

C

Java

JavaScript

Solidity

Ethereum VM

…

Interpreter

Symbolic Execution

Compiler

Model Checker

Deductive Verifier

…

Ideal Language Framework

L

T

Ideally, we want a language framework that provides all the tools implemented in a language-agnostic,

[CLICK]

or better say, language-parametric manner.

[CLICK]

Specifically, we want the framework to take a language definition as input and provide all the tools specialized for that language, at no additional cost.

[CLICK]

Anything else is less than ideal and comes with significant technical debt.

If this ideal scenario is indeed possible, then there is no reason to do things any other way.

Period.

But is it feasible?

We firmly believe that the answer is a bold YES.

There is enough evidence that this IS the case.

The time has come to STOP compromising and do things RIGHT.

Instead of L * T different systems and a maintenance hell, we now have to develop and maintain only L + T systems, which is the minimum.

7 of 52

K Framework�http://kframework.org

We tried various semantic styles, for >15y and >100 top-tier conference and journal papers:

Small-/big-step SOS; Evaluation contexts; Abstract machines (CC, CK, CEK, SECD, …); Chemical abstract machine; Axiomatic; Continuations; Denotational;…

But each of the above had limitations

Especially related to modularity, notation, verification

K framework initially engineered: keep advantages and avoid limitations of various semantic styles

Then theory came

7

The K framework is our attempt to implement the ideal language framework vision.

I am not saying that all the work around K is complete and everything is functional and ready to use out of the box.

What I am saying is that everything that we and others have done in terms of foundations and implementation of the K framework has been fueled by the strong belief that the ideal language framework is not only possible, but within our reach in short term.

And that it can be both scientifically transformative and economically viable.

It took us more than 15 years of sustained research and development, published in more than 100 papers, to get K where it is now.

As a programming languages professor and researcher, I have taught and experimented in class and in my lab with almost all existing formal language semantics approaches, to deeply understand their strengths and their limitations.

While doing so, I have learned two important lessons:

1) They all have mathematically beautiful foundations and work very well … with small languages, like IMP, but break apart when you attempt to define large languages like C or Java; especially in terms of basic engineering aspects that mathematicians tend to disregard, such as modularity (in the presence of language extensions) and heavy notation, or in terms of serving more than one purpose, eg incapability to do formal verification. And

2) That it is simply impractical to first develop the theory underlying such a universal framework, hoping that you are somehow smart enough to create the right foundation out of the blue, and then try to implement it in a way that satisfies both the theoretical and the practical needs. This just does not work. Not anymore, not with all the variety of programming languages, underlying paradigms, and formal analysis tools that it needs to support today.

Consequently, we deliberately decided to take an engineering approach: we incorporated all the features we encountered in the various semantic approaches that appeared to work well while defining real languages like C and Java, and avoided all the features that were inconvenient or demotivating for the working semanticist.

For example, in many semantic approaches one has to modify or duplicate many unrelated semantic rules when adding a new feature to a language, for example when adding side effects to a language, or a new internal stack say for exceptions, or I/O, or concurrency, etc.

Such break of modularity or need for duplication are simply unacceptable in practice, so in K we engineered mechanisms and notations to avoid them.

Then, once several large languages were formalized across various language paradigms and there were no significant requests from users for new features or changes to K itself, we have decided to develop the mathematical details of its underlying theory.

The result is an astoundingly simple and beautiful theoretical foundation, matching logic, that works as a practical foundation for a complex and feature-rich framework like K.

8 of 52

Complete K Definition of KernelC

8

9 of 52

Complete K Definition of KernelC

9

Syntax declared using annotated BNF

…

10 of 52

Complete K Definition of KernelC

10

Configuration given as a nested cell structure.

Leaves can be sets, multisets, lists, maps, or syntax

11 of 52

Complete K Definition of KernelC

11

Semantic rules given contextually

rule

Semantic rules given contextually

rule

k: X = V => V …

env: … X |-> (_ => V) …

Once the syntax and configuration are defined, we can start adding semantic rules.

K rules are contextual: they mention a configuration context in which they apply, together with local changes they make to that context.

To enhance the modularity of your language definition, you typically aim at only mentioning the absolutely necessary context in your rules; the remaining details are filled in automatically by the tool.

For example, here is the K rule for assignment, both in graphical and in ASCII formats.

In ASCII, we use an XML-like notation to state where cells start and end; if you do not like XML, no worry: syntax in K is easy to change; we are also experimenting with this alternative syntax

[CLICK]

where the cell name is followed by a colon and then by its contents; in fact, many of the K tools handle K definitions in JSON format internally.

Recall that assignment was strict(2), so we can assume that its second argument is a value, say V.

The context of this rule involves two cells, the k cell which holds the current code and the env cell which holds the current environment.

Moreover, from each cell, we only need certain pieces of information: from the k cell we only need the first task, which is the assignment X=V, and from the env cell we only need the binding X |-> _.

The underscore stands for an anonymous variable, the intuition here being that that value is discarded anyway, so there is no need to bother naming it.

The unnecessary parts of the cells, which we call structural frames, are metaphorically “torn away” and ignored, as suggested by the tears in the graphical notation, or `…` in ASCII.

Then, once the local context is established, we identify the parts of the context which need to change, underlying them, and then provide the changes under the lines, or after the rewrite symbol `=>` in ASCII.

In our case, we rewrite both the assignment expression and the value of X in the environment to the assigned value V.

Everything else stays unchanged.

The concurrent semantics of K regards each rule as a transaction: all changes in a rule happen concurrently; moreover, rules themselves apply concurrently, provided their changes do not overlap.

This is it, this is how K definitions look like.

If you have minimal background in functional or logic programming, you should have no difficulty to understand K.

12 of 52

K Scales

Several large languages were recently defined in K:

JavaScript ES5: by Park etal [PLDI’15]

Passes existing conformance test suite (2872 programs)
Found (confirmed) bugs in Chrome, IE, Firefox, Safari

Java 1.4: by Bogdanas etal [POPL’15]
x86: by Dasgupta etal [PLDI’19]
C11: Ellison etal [POPL’12, PLDI’15]

192 different types of undefined behavior
10,000+ program tests (gcc torture tests, obfuscated C, …)
Commercialized by startup (Runtime Verification, Inc.)

+ EVM[CSF’18], Solidity, IELE[FM’19], WASM, Michelson, …

K scales!

Besides a series of smaller and paradigmatic languages that are used for teaching purposes, there are several large and real languages that have been given semantics in K.

As previously explained, K itself has been designed and developed while defining the semantics of these languages.

Javascript was defined by Park etal, and not only passed all the conformance tests proposed by the standards committee, but also found weaknesses in it and confirmed bugs in all major broswers; these bugs were fixed immediately, as JavaScript bugs are considered security critical.
Java by Bogdanas; this semantics also resulted in the most semantics-complete test suite for Java, almost 1000 small programs that cover all the semantic rules;
X86 by Dasgupta etal; this defines the semantics of more than 3000 x86 instructions and variants, and it is the only complete x86 semantics to date
C by Ellison etal; this was by far our most complex semantics, which took more than 10 man-years to develop; since C’s undefined behavior is so notoriously hard to define, we had discovered many bugs in our C semantics, likely in the order of one per day. The nice consequence of K being K is that you need to fix such bugs in only one place, the semantics, and not in each tool separately, like in other approaches.

Recently, semantics of blockchain languages has also been defined, like the low-level Ethereum VM language, Solidity, WASM, and so on.

New blockchain languages have also been defined in K and deployed via K as execution engine, like IELE, which is an LLVM-like language for the blockchain.

All these language semantics have been thoroughly tested, on large benchmarks of programs, same as compilers and interpreters are.

Many other large K semantics are under development.

13 of 52

K Configuration and Definition of C

13

120 Cells!

… plus ~5000 rules …

To give you an idea what it takes to define a large language, here is, for example, the configuration of C.

It has more than 100 semantic cells, and more than 5000 rules.

After defining so many languages and encountering countless bugs in language manuals, definitions, and implementations, not to mention problems in our own understanding of language features behavior, we reached the conclusion that any semantic framework which is not executable should simply not be trusted.

The only exception is when the non-executable language semantics comes with proofs of soundness wrt a trusted, executable model, but those tend to be very tedious and technically involved; it takes a PhD or more to prove such a soundness result for a real language like C, Java or JavaScript.

Consequently, only very few such soundness of non-executable semantics results have been ever proved.

These are also hard to maintain as the language evolves.

But fortunately, as K demonstrated repeatedly, non-executable semantics of languages are simply unnecessary for tools.

They may be interesting and insightful to understand complex language features from an axiomatic perspective, but not necessary for tool development.

For tools, one semantics, executable, suffices.

14 of 52

Ideal Language Framework Vision [K]

14

Deductive program verifier

Parser

Interpreter

Compiler

(semantic) Debugger

Symbolic execution

Model checker

Formal Language Definition

(Syntax and Semantics)

…

K -> LLVM -> x86

As mentioned, K is our attempt to implement this ideal language framework vision.

We already discussed how we define languages formally in K, the yellow box in this figure.

Next I’d like to give you more details about the blue boxes, which implement various language tools, language-independently.

That is, in a way where you plug-and-play your language in the tool.

[CLICK]

Let me start with the most used of the tools, which is the interpreter.

It is the most used because each time we define a language semantics, we test it extensively by running as many programs as we can using the auto-generated interpreter.

In fact, the Parser is the most used of the K tools, and it is highly non-trivial to non-ambiguously parse K definitions that mix language-specific syntax with K syntax, at the same time inferring the sorts of variables.

We use constraint solving for parsing in K, but that is the topic of another presentation.

Here we take the parser for granted and discuss other tools.

15 of 52

1. Translate K def to LLVM�2. Compile LLVM to x86

Code (6-int-overflow.c)

RV-Match: Commercial tool

Instance of K concrete execution with C lang
Automatic debugger for subtle bugs other tools can't find, with no false positives
Seamless integration with unit tests, build infrastructure, and continuous integration
Platform for analyzing programs, boosting standards compliance and assurance

Concrete Execution Backend

16 of 52

RV-Match on Toyota ITC Benchmark�- Comparison with Other Analysis Tools -

Toyota Benchmark ISSRE ’15 (1276 tests)	RV-Match			GrammaTech CodeSonar			MathWorks Code Prover			MathWorks Bug Finder			GCC			Clang
	DR	FPR	PM	DR	FPR	PM	DR	FPR	PM	DR	FPR	PM	DR	FPR	PM	DR	FPR	PM
Static memory	100	100	100	100	100	100	97	100	98	97	100	98	0	100	0	15	100	39
Dynamic memory	94	100	97	89	100	94	92	95	93	90	100	95	0	100	0	0	100	0
Stack-related	100	100	100	0	100	0	60	70	65	15	85	36	0	100	0	0	100	0
Numerical	96	100	98	48	100	69	55	99	74	41	100	64	12	100	35	11	100	33
Resource management	93	100	96	61	100	78	20	90	42	55	100	74	6	100	25	3	100	18
Pointer-related	98	100	99	52	96	71	69	93	80	69	100	83	9	100	30	13	100	36
Concurrency	67	100	82	70	77	73	0	100	0	0	100	0	0	100	0	0	100	0
Inappropriate code	0	100	0	46	99	67	1	97	10	28	94	51	2	100	13	0	100	0
Miscellaneous	63	100	79	69	100	83	83	100	91	69	100	83	11	100	34	11	100	34
AVERAGE (Unweighted)	79	100	89	59	97	76	53	94	71	52	98	71	4	100	20	6	100	24
AVERAGE (Weighted)	82	100	91	68	98	82	53	95	71	62	99	78	5	100	22	7	100	26

[CAV’16]

17 of 52

From RV-Match to Blockchain

RV-Match currently commercialized within

Same K technology used for defining / executing blockchain languages: EVM, IELE, WASM, Michelson, …

17

18 of 52

Ideal Language Framework Vision [K]

18

Deductive program verifier

Parser

Interpreter

Compiler

(semantic) Debugger

Symbolic execution

Model checker

Formal Language Definition

(Syntax and Semantics)

…

19 of 52

State-of-the-Art

Redefine the language using a different semantic approach (Hoare/separation/dynamic logic)
Language specific, non-executable, error-prone

19

20 of 52

What We Want

Use directly the trusted

language model/semantics!

Language-independent proof system

Takes operational semantics as axioms
Derives reachability properties
Sound and relatively complete for all languages!

20

Formal Language Definition

(Syntax and Semantics)

Deductive program verifier

Symbolic execution

21 of 52

Matching μ-Logic

[…, LICS’13, RTA’15, OOPSLA’16, FSCD’16, LMCS’17, LICS’19, ICFP’20]

16 proof rules only!

Simple proof checker (200 LOC, vs Coq’s 30000 LOC)!

22 of 52

Expressiveness of Matching μ-Logic

23 of 52

K = (Best Effort) Implementation of ML

Reachability logic implemented in K, generically

23

EVM

Solidity

Michelson

WASM

…

Evaluated it with the existing semantics of C, Java, JavaScript, EVM, and several tricky programs
Morale:

Performance is comparable with language-specific provers!

24 of 52

for the Blockchain

24

25 of 52

K Framework Vision

25

Deductive program verifier

Parser

Interpreter

Compiler

(semantic) Debugger

Symbolic execution

Model checker

Formal Language Definition

(Syntax and Semantics)

…

Blockchain Language Definition

26 of 52

KEVM: Semantics of the Ethereum Virtual Machine (EVM) in K

Complete semantics of EVM in K

https://github.com/kframework/evm-semantics
Passes 60,000+ tests of C++ reference implementation
Faster (!) than EVM simulators, like ethereumjs (Truffle)
Used as canonical EVM spec (replacing Yellow Paper)

26

[CSL’18]

27 of 52

1) Formal documentation: http://jellopaper.org

27

What Can We Do with KEVM?

28 of 52

What Can We Do with KEVM?

2) Generate and deploy correct-by-construction EVM client/simulator/emulator

Firefly tool: KEVM to run, analyze and monitor tests

Cardano testnet: mantis executing KEVM

28

29 of 52

What Can We Do with KEVM?

3) Formally verify Ethereum smart contracts

RV does that commercially. Won first Ethereum Security grant to verify Casper, then were hired to formalize Beacon Chain (Serenity) and verify ETH1 -> ETH2 deposit contract

29

[ FSE’18 ]

30 of 52

Smart Contract Verification Workflow

ERC20 Informal Business Logic

Formalize

Refine

1

rule

transfer(T, V) => true

caller: F

account:

id: F

balance: BF => BF - V

account:

id: T

balance: BT => BT + V

log: . => Transfer(F,T,V)

requires

0 <= V /\

V <= BF /\

BT + V <= MAXVALUE

ERC20-K formal executable high-level spec

2

[transfer]

callData: #abiCallData("transfer", #address(TO_ID), #uint256(VALUE))

gas: {GASCAP} => _

refund: _ => _

requires:

andBool 0 <=Int TO_ID andBool TO_ID <Int (2 ^Int 160)

andBool 0 <=Int VALUE andBool VALUE <Int (2 ^Int 256)

andBool 0 <=Int BAL_FROM andBool BAL_FROM <Int (2 ^Int 256)

andBool 0 <=Int BAL_TO andBool BAL_TO <Int (2 ^Int 256)

[transfer-success]

k: #execute => (RETURN RET_ADDR:Int 32 ~> _)

localMem: .Map => ( .Map[ RET_ADDR := #asByteStackInWidth(1, 32) ] _:Map )

log: _:List ( .List => ListItem(#abiEventLog(ACCT_ID, "Transfer", #indexed(#address(CALLER_ID

……….

………

…….

ERC20-EVM formal executable low-level spec that contains all EVM details

3

31 of 52

Notable Contracts� We’ve Verified

Alchemix, Element
ETH2.0 Deposit
GnosisSafe
Ethereum Casper FFG
Uniswap
DappSys DSToken ERC20
Bihu KEY token

31

32 of 52

K Semantics of Other�Blockchain Languages

WASM (web assembly) – collaboration with the Ethereum Foundation, Web3, Emurgo, Elrond
Michelson – collaboration with Tezos; K interpreter comparable at performance with their OCAML reference implementation
Solidity, Vyper – with the Ethereum Foundation
TEAL + AlgoClarity – collaboration with Algorand
Plutus (functional) – collaboration with IOHK

…

32

33 of 52

Modelling and Verification of�Blockchain Protocols

Matching logic, rewriting and K can also be used to formally specify and verify consensus protocols, random number generators, etc.
Done or ongoing:

Casper FFG, Casper CBC (Ethereum Foundation)
RANDAO (Ethereum Foundation)
Algorand (Algorand)
ETH 2.0 / Beacon Chain (Ethereum Foundation)
Platon (Platon Networks)

Several others planned or in discussions

33

34 of 52

Taking K to the Next Level

Proof objects
Universal blockchain technology

34

35 of 52

Proof Object Generation

35

Deductive program verifier

Parser

Interpreter

Compiler

(semantic) Debugger

Symbolic execution

Model checker

Formal Language Definition

(Syntax and Semantics)

…

36 of 52

Proof Object Generation

Each of the K tools is a best-effort implementation of proof search in Matching µ-Logic:

New Haskell backend of K will explicitly generate proof objects for verification tasks

36

16 proof rules only!

Simple proof checker (<200 LOC)!

In contrast, Coq has about 45 proof rules, and its proof checker has 30000+ lines of OCAML

37 of 52

Proof Object Generation

No need to trust the (complex) K implementation, nor any company (including Runtime Verification)

It is known that program verifiers / tools can have bugs in spite of best efforts, bug finders and company prestige

Proof objects act as 3^rd-party checkable correctness certificates on the blockchain, in a proof-carrying code style (proofs can be stored offchain, or snarked)
In combination with domain-specific languages for requirements specifications, this will offer the highest level of software assurance known to man

37

38 of 52

Ultimate Goal�� a Universal Blockchain Technology

38

39 of 52

Goals

K-powered blockchain: blockchain of truth

Smart contracts in any programming language formalized in K
Or better, smart contracts directly as executable K specifications
Computation = proof: builtin proof checker will ensure valid computations and correctness claims on the blockchain

39

40 of 52

K – A Universal Blockchain Language

We want to be able to write (provably correct) smart contracts in any programming language.
All you need is a K-powered blockchain!

40

K language semantics will be stored on blockchain. Fast LLVM backend of K can be used as execution engine / VM.

Vyper

V1.2

Solidity

V0.2.21

Plutus

V2.1

41 of 52

Semantics-Based Compilation

41

Deductive program verifier

Parser

Interpreter

Compiler

(semantic) Debugger

Symbolic execution

Model checker

Formal Language Definition

(Syntax and Semantics)

…

42 of 52

Semantics-Based Compilation (SBC)

Goals

Execution of P in L equivalent to executing L_P in a start configuration
L_P should be “as simple as possible”, only capturing exactly the dynamics of L necessary to execute program P

Program P in Language L

Semantics-Based Compilation

𝕂 Semantics of Language L

𝕂 Semantics of Language L_P

43 of 52

K – A Universal Blockchain Language

K-powered blockchain enables (provably correct) smart contracts in any programming language!

43

Vyper

V1.2

Solidity

V0.2.21

Plutus

V2.1

1. Write contract P in any language, say L (unique address)

2. SBC[L] your P into L_P; verify P (or L_P) with K prover

44 of 52

K – A Universal Blockchain Language

When all the projected K tools will be completed, K will provide everything we need to

Design new smart contract languages, add them in the blockchain and start using them right away, with auto-generated correct(!) implementations and tools
Same for virtual machines(!) and consensus protocols(!)

Everything will be either a trusted formal specification or generated automatically from one
Proof objects will serve as correctness certificates
Perfect. No compromise! … moreover …

44

45 of 52

a Ultimate Smart Contract Language

45

46 of 52

K as a Smart Contract Language

Smart contracts implement transactions

Often using poorly designed and thus insecure languages, compilers and interpreters / VMs

K also implements transactions, directly!

Indeed, each K rule instance is a transaction

Each smart contract (Solidity, EVM, …) requires a formal specification in order to be verified

K formal specifications are already executable!

And indeed, they are validated by heavy testing

46

Hm, then why not write my smart contracts directly and only as K executable specifications?

47 of 52

Example: ERC20 Token in Solidity�- Snippet -

47

48 of 52

Example: ERC20 Compiled to EVM�- Snippet -

48

Bytecode:

Opcodes:

Unreadable
Slow: ~25ms to execute (ganache)
Untrusted compiler, so it needs to be formally verified to be trusted

We formally verify it using KEVM against the following K specification:

49 of 52

K Specification of ERC20�- Snippet, Sugared -

49

rule transfer(To, V) => true

caller: From

account: id: From balance: BalanceFrom => BalanceFrom - V

account: id: To balance: BalanceTo => BalanceTo + V

log: . => Transfer(From, To, V)

requires 0 <= V <= BalanceFrom /\ BalanceTo + V <= MAXVALUE

Formal, yet understandable by non-experts
Executable, thus testable (for increased confidence)
Fast: ~2ms to execute with LLVM backend of K
No compiler required, correct-by-construction
Use K as programming language for smart contracts!

(needed: gas model for K)

50 of 52

Blockchain of Truth

50

51 of 52

Blockchain of Truth (BoT)

There is only one known way that can be used to assert, with absolute certainty, correctness:

We envision a blockchain of truth, whose goal is to store and certify mathematical facts

Many correctness claims are mathematical facts

Formal verification, trusted computation, etc.

Trust reduces to a simple, <200 line program:

51

mathematical proof

proof checker

52 of 52

Correct-By-Construction and Fast�is Possible!

52

Deductive program verifier

Parser

Interpreter

Compiler

(semantic) Debugger

Symbolic execution

Model checker

Formal Language Definition

(Syntax and Semantics)

…