Medjai: A Symbolic Execution Tool for Cairo

Medjai is an open-sourced general framework for reasoning about Cairo programs based on symbolic execution.

Note: Medjai is still under active development. For development notes, please see here.

Features

• [Dev] Program Exploration: Medjai can execute Cairo program with symbolic inputs and explore all its possible program states.
• [Dev] Property Verification: Medjai can check whether certain properties hold on Cairo program.
• [Dev] Attack Synthesis: Medjai can automatically solve for concrete inputs that crash given Cairo program.
• [Dev] Integrations with Veridise Product Lines: Medjai integrates with [V] specication language that allows developers to express correctness properties.

Setup and Build

• Cairo (0.8.2 Tested): https://www.cairo-lang.org/
• Racket (8.0+): https://racket-lang.org/
  • Rosette (4.0+): https://github.com/emina/rosette
    • raco pkg install rosette
• V (latest): https://github.com/Veridise/V
  • This dependency is optional; needed only for parsing specifications in [V]. Can be ignored when using specifications in Cairo.
  • Follow build instructions: https://github.com/Veridise/V/blob/main/README.md
  • Add path to parse to PATH variable
• Cairo Compiler: https://github.com/Veridise/pip-cairo-lang
  • We use a custom Cairo/Starknet compiler. Instructions to install are in the repo's README.
• Symexec library: https://github.com/Veridise/lib-symexec
  • Installation instructions in the README of repo.

Quickstart: Running An ERC20 Demo (Docker)

First you need to build the demo from the latest version. Make sure you have Docker installed, and then type in the following command to build an image:

cd Medjai/
docker build -t medjai:demo .

It should take a short time to set up the environment. Then use the following command to start a container:

docker run -it --rm medjai:demo bash

Then you will enter a pre-set docker environment.

ERC20 Bug Detection

To test the buggy version, use the following command in the container:

cd Medjai/
racket ./cairo-run.rkt --cname ./benchmarks/overflowTest/erc20demo_bug_compiled.json

The tool will be invoked and run symbolic execution for bug detection. You'll see the following output if the command runs correctly:

Finished Symbolic Execution
Bug found with
total_supply = Uint256(1, 2)
amount = Uint256(340282366920938463463374607431768211455, 340282366920938463463374607431768211453)

ERC20 Symbolic Execution

For a non-buggy version, use the following command in the container to verify it:

racket ./cairo-run.rkt --cname ./benchmarks/overflowTest/erc20demo_fix_compiled.json

The tool will be invoked and also run symbolic execution for bug detection. You'll see the following output if the command runs correctly:

Finished Symbolic Execution
No bugs found!

This means this version of ERC20 is good.

End-To-End Example

This section shows how you can use Medjai to verify a protocol end-to-end. The file MCD/contracts/vat.cairo contains a StarkNet implementation of MakerDAO's Vat protocol.

Building Vat

To build Vat.cairo, run

cp -r utils/veridise MCD/
./compile-vat.sh

this should generate a file vat_compiled.json.

Maker DAO's VAT Protocol

We now show how you can use Medjai to prove properties about your Cairo programs. Consider the external method move from MakerDAO's Vat.cairo shown below

# function move(address src, address dst, uint256 rad) external {
@external
func move{
    syscall_ptr : felt*, pedersen_ptr : HashBuiltin*, range_check_ptr, bitwise_ptr : BitwiseBuiltin*
}(src : felt, dst : felt, rad : Uint256):
    alloc_locals

    check(rad)

    # require(wish(src, msg.sender), "Vat/not-allowed");
    let (caller) = get_caller_address()
    # let caller = 0
    let (src_consents) = wish(src, caller)
    with_attr error_message("Vat/not-allowed"):
        assert src_consents = 1
    end

    # dai[src] = dai[src] - rad;
    let (dai_src) = _dai.read(src)
    let (dai_src) = sub(dai_src, rad)
    _dai.write(src, dai_src)

    # dai[dst] = dai[dst] + rad;
    let (dai_dst) = _dai.read(dst)
    let (dai_dst) = add(dai_dst, rad)
    _dai.write(dst, dai_dst)

    # TODO
    # emit Move(src, dst, rad);

    return ()
end

move moves rad amount of Dai from address src to destination address dst. Suppose we want to use Medjai to prove that no matter what values we give for src, dst, and rad that the amount of dai in src should always decrease (or stay the same). Our first step is to create a specification for MEdjai.

Creating a specification

Medjai can accept multiple forms of specification but in this example we will express the spec as a Cairo method (shown below and found in vatspec.cairo).

@external
func move_demo_spec{
    syscall_ptr : felt*, pedersen_ptr : HashBuiltin*, range_check_ptr, bitwise_ptr : BitwiseBuiltin*
}():
    alloc_locals
    local otherUser
    local src
    local dst

    let (local src) = medjai_make_symbolic_felt()
    let (local dst) = medjai_make_symbolic_felt()

    # _dai.write(src, Uint256(low=0, high=340282366920938463463374607431768211455))
    let (local daiSrcBefore : Uint256) = _dai.read(src)
    medjai_assume_valid_uint256(daiSrcBefore)  # Assume the value is a valid uint256
    let (local daiDstBefore : Uint256) = _dai.read(dst)
    medjai_assume_valid_uint256(daiDstBefore)  # Assume the value is a valid uint256

    let (local rad : Uint256) = medjai_make_symbolic_uint256()  # Checked in move
    move(src, dst, rad)

    let (local daiSrcAfter : Uint256) = _dai.read(src)
    medjai_assert_le_uint256(daiSrcAfter, daiSrcBefore)
    return ()
end

The test first creates symbolic src and dst addresses by calling medjai_make_symbolic_felt. Next, it tells Medjai to assume that src and dst are well formed Uint256s via medjai_assume_valid_uint256. Afterwards, it creates a symbolic uint256 for rad and calls move. Finally, it tells Medjai to check whether the amount of Dai in the src address after the call is less than or equal to the amount before the call via medjai_assert_le_uint256.

Using Medjai

To use Medjai to check the specification we just need to do the following

racket ./cairo-run.rkt --starknet --cname vat_compiled.json --entry move_demo_spec

If everything goes correctly you should see a bug:

[tokamak:log] Bugs found with following variable assignments
[tokamak:log] x$1 = 10
[tokamak:log] x$4 = 3618502788666131213697322783095070105282824848410658236509717448704103809024
[tokamak:log] x$0 = 10
[tokamak:log] x$2 = 0
[tokamak:log] x$3 = 340282366920938463463374607431768211454
[tokamak:log] x$8 = 3618502788666131213697322783095070105623107215331596699973092056135872020480
[tokamak:log] x$5 = 340282366920938463463374607431768211458
[tokamak:log] x$6 = 340282366920938463463374607431768211457
[tokamak:log] x$7 = 340282366920938463463374607431768211452
[tokamak:log] Running again
[assert] failed
  context...:
   /Users/shankarapailoor/Library/Racket/8.5/pkgs/rosette/rosette/base/core/exn.rkt:59:11: raise-exn:fail:svm:assert:user
   /Users/shankarapailoor/Library/Racket/8.5/pkgs/rosette/rosette/base/form/control.rkt:16:25
   body of "/Users/shankarapailoor/Medjai/cairo-run.rkt"

Property Specification

Cairo Specifications

Medjai takes correctness specifications in the form of Cairo programs which emit special assertions and assumptions. To create a specification, users write a test as a Cairo function that performs some actions, including assuming and asserting properties using the Medjai verification library. Note that Cairo assert statements are treated as assumptions for Medjai. This is because, by default, Medjai will not consider reverts to be bugs.

Cairo specifications for Medjai can be compiled in the same way as normal Cairo contracts. See StarkNet documentation for instructions on compiling Cairo contracts.

[V] Specifications

[V] is a concise specification language developed by Veridise. In addition to taking Cairo specifications as input, Medjai can also automatically convert specifications in [V] to an equivalent Cairo specification. Generally, specifications in [V] are much smaller than their Cairo counterparts, so specifying properties is usually quicker and easier in [V] than in Cairo. However, for cases where symbolic execution performance is a concern, hand-written Cairo specifications are more desired. Note that since Medjai's [V]-to-Cairo parser can be used standalone, users can write specifications in [V], convert them to Cairo, and optimize as needed.

Below is an example [V] specification that expresses the same constraints as the specification for move in the above end-to-end example:

vars: contract c
spec: finished(c.move(src, dst, rad),
               valid_uint256(old(_dai.read(src))) && valid_uint256(old(_dai.read(dst)))
               |=>
               _dai.read(src) <= _dai.read(dst)

For full documentation on [V] specifications, see: https://github.com/Veridise/V/blob/main/docs/statements.rst.

Commands & Usages

Using Cairo Specification

racket cairo-run.rkt [options]

where options include:
 --cname <path>: Path to a compiled Cairo program
 --entry <func>: Name of a Cairo function to run
 --starknet: Used to indicate compiled file is %lang starknet
 --track-revert: Indicates testing necessary conditions for revert
 --verbose: Print all output
 --silent: Print no output
 --ambivalent: Used to indicate that Medjai should ignore hints

Using [V] Specification

run-medjai.sh <path-to-v.spec> <path-to-header.cairo> <source-dir> <contract-dir>

where each option specifies:
- path-to-v.spec: [V] specificaiton
- path-to-header.cairo: Cairo file that defines imports used by the specification
- source-dir: Source directory from which starknet-compile should be run
- path-to-header.cairo: Subdirectory within source-dir that contains the contract file (possibly .)

Parsing [V] into Cairo specifications

racket parser-run.rkt [options] <v-spec.json>

where options include:
 --header <path>: Path to a header for Cairo specifications (.cairo file)
 --spec-name <func>: Name of the generated specification function
 --output <path>: Path to the output file (.cairo)