KAURORA

GIF
kaurora run test demo

Inspiration

The KEVM project successfully brought formal verification and symbolic execution of smart contracts to the Ethereum ecosystem. It is now the reference implementation for the EVM. As a blockchain security professional I thought that NEAR and Aurora might benefit from this technology. As it can improve the security of smart contracts.

What it does

KAURORA implements the Aurora EVM modifications in a KEVM fork. This enables Solidity smart contract developers to verify properties expressed in Solidity using the following command line tool: kontrol build kontrol prove --test CounterTest.testSetNumber

See also kontrol-examples at https://docs.runtimeverification.com/kontrol/guides/kontrol-example

How we built it

We installed the K Framework, we forked the evm-semantics github project and installed all required tools. We modified the evm.md file to change four opcodes implementation in the K language: DIFFICULTY, GASLIMIT, COINBASE, BLOCKHASH

We prepared implementing the following precompiles: predecessorAccountId getPromiseResults prepaidGas exitToNear exitToEthereum

Challenges we ran into

There are many tools to install and some do not install well or compile on Apple Silicon. The documentation of these projects can be unclear at times. We found a minor error in the Aurora spec for opcode COINBASE. https://doc.aurora.dev/evm/opcodes/ 1) COINBASE returns 0x4444588443C3a91288c5002483449Aba1054192b but in the table it is written 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff

Accomplishments that we're proud of

Just compiling the evm-semantics even without any opcode modification is an accomplishment. There is a wide array of tools and technologies involved in this: nix, kup, kevm, kontrol, makefiles, python, poetry, apple silicon, gcc/llvm, haskell, solidity Time management was also an issue.

What we learned

How to modify EVM opcodes in the K Framework Better understanding of K, EVM, Aurora. Ask help from both Aurora and KFramework on their discord projects.