KEVM - LayerX Research

KEVM

#KEVM #formal_verification

TL;DR

KEVMはK FrameworkによるEVMのセマンティック GitHub Repo, paper

Runtime Verification Inc. がこれらを研究・開発

K Framework自体の研究開発チーム(UIUC)とメンバー被ってたりするので大学発ベンチャー的な感じなのか？

Cardanoを開発するIOHKがKEVMとKIELEの開発を支援した模様記事

K Framework

https://gyazo.com/9fd30b39d15bba04edb35299e409da6e

プログラミング言語・型システム・形式的検証の実行可能なセマンティクを構築するフレームワーク

CやJava, JavaScript, WebAssemblyのセマンティックなどが既に構築されている

UIUCなどが中心となって研究開発

Kを使って言語の定義を構成することで、Kの言語に依存しないデバッガや検証ツールなどが利用できる

参考

日本語の解説記事

全体感が書いてあるスライド Semantics-Based Program Verifiers for All Languages

ユーザーグループ

言語としてのK

ビルトインの無限精度演算

Builtin sorts: Int, String

=>: "rewrites to"

~>: "followed by"

->: "implies"(matching logic)

|->: used for getting the value of a key, e.g. the <storage> cell is implemented as a `Map

KEVM

KによるEVMの形式的なセマンティック定義

KEVMより生成されたEVMインタプリタは40,683のテストを全てパスした

暗号系の高級な命令についてはKのモジュールとしてimportされているプラグインの実装を呼び出している

ML言語での実装(つまり形式的なセマンティック定義ではない？)

例: keccak256

参考

KEVMのpaper KEVM: A Complete Formal Semantics of the Ethereum Virtual Machine

例: 演算

算術系の命令の定義

code: evm.k(k)

syntax BinStackOp ::= "ADD" | "MUL" | "SUB" | "DIV" | "EXP" | "MOD"

// -------------------------------------------------------------------

rule <k> ADD W0 W1 => W0 +Word W1 ~> #push ... </k>

rule <k> MUL W0 W1 => W0 *Word W1 ~> #push ... </k>

rule <k> SUB W0 W1 => W0 -Word W1 ~> #push ... </k>

rule <k> DIV W0 W1 => W0 /Word W1 ~> #push ... </k>

rule <k> EXP W0 W1 => W0 ^Word W1 ~> #push ... </k>

rule <k> MOD W0 W1 => W0 %Word W1 ~> #push ... </k>

+Wordは256-bitオーバーフローをチェックするrule

code: data.k(k)

syntax Int ::= Int "+Word" Int function

| Int "*Word" Int function

| Int "-Word" Int function

| Int "/Word" Int function

| Int "%Word" Int function

// -----------------------------------------

rule W0 +Word W1 => chop( W0 +Int W1 )

rule W0 -Word W1 => chop( W0 -Int W1 ) requires W0 >=Int W1

rule W0 -Word W1 => chop( (W0 +Int pow256) -Int W1 ) requires W0 <Int W1

rule W0 *Word W1 => chop( W0 *Int W1 )

rule W0 /Word W1 => 0 requires W1 ==Int 0

rule W0 /Word W1 => chop( W0 /Int W1 ) requires W1 =/=Int 0

rule W0 %Word W1 => 0 requires W1 ==Int 0

rule W0 %Word W1 => chop( W0 modInt W1 ) requires W1 =/=Int 0

chopはIntを2^256のモジュラーにする

code: data.k(k)

syntax Int ::= chop ( Int ) function, smtlib(chop)

// ----------------------------------------------------

rule chop ( I:Int ) => I modInt pow256 concrete, smt-lemma

例: CALL

CALLは#checkCall, #callの連続に。#callの後にCcallgasもある

code: evm.k(k)

syntax CallOp ::= "CALL"

// ------------------------

rule <k> CALL GCAP ACCTTO VALUE ARGSTART ARGWIDTH RETSTART RETWIDTH

=> #checkCall ACCTFROM VALUE

~> #call ACCTFROM ACCTTO ACCTTO Ccallgas(SCHED, #accountNonexistent(ACCTTO), GCAP, GAVAIL, VALUE) VALUE VALUE #range(LM, ARGSTART, ARGWIDTH) false

~> #return RETSTART RETWIDTH

...

</k>

<schedule> SCHED </schedule>

<id> ACCTFROM </id>

<previousGas> GAVAIL </previousGas>

上記にマッチするrule

code: evm.k(k)

syntax InternalOp ::= "#checkCall" Int Int

| "#call" Int Int Int Exp Int Int WordStack Bool strict(4)

| "#callWithCode" Int Int Map WordStack Int Int Int WordStack Bool

| "#mkCall" Int Int Map WordStack Int Int Int WordStack Bool

// --------------------------------------------------------------------------------

rule <k> #checkCall ACCT VALUE ~> #call _ _ _ GLIMIT _ _ _ _

=> #refund GLIMIT ~> #pushCallStack ~> #pushWorldState

~> #end #if VALUE >Int BAL #then EVMC_BALANCE_UNDERFLOW #else EVMC_CALL_DEPTH_EXCEEDED #fi

...

</k>

<output> _ => .WordStack </output>

...

</account>

requires VALUE >Int BAL orBool CD >=Int 1024

CcallgasはCgascapにrewrite

code: evm.k(k)

rule <k> Ccallgas(SCHED, ISEMPTY:Bool, GCAP, GAVAIL, VALUE)

=> Cgascap(SCHED, GCAP, GAVAIL, Cextra(SCHED, VALUE, ISEMPTY)) +Int #if VALUE ==Int 0 #then 0 #else Gcallstipend < SCHED > #fi ... </k>

Gcallstipendは2300、Reentrancy対策のためのgas上限

Formal verification with KEVM

KのReachability Logic proverをKEVMにおいて使い、EVMバイトコードを形式的に検証する

その他Kによるブロックチェーン関連PJ

Ethereum関連

Solidityのセマンティック定義

KVyper: Vyperのセマンティック定義 GitHub Repo, GitHub Wiki

"semantics by translation"

VyperからLLL、LLLからEVMの二つのtranslationの定義によって構成される

定義を作っていく過程でVyperコンパイラのバグをたくさん見つけたとのこと

Vyperのコンパイラとして使える

eWASM系

WASMのセマンティック GitHub Repo

EEIのセマンティック定義 GitHub Repo

Cardano関連

IELE in K

IELEはCardanoのVMで、LLVMベースで作られている

EVMのようにスタックマシンではなくレジスタマシン

KEVM, KLLVMを参考にしたらしい

Cardanoのスマートコントラクト言語Plutusのセマンティック GitHub Repo

Haskellのサブセット？であるPlutusを開発中

その他

Rholang GitHub Repo

pirapiraさんのコメント