README.md

Note: Development of Medjai has been moved to Veridise (https://github.com/Veridise/Medjai). Maintenance of this (original) repo is temporarily suspended.

Medjai: A Symbolic Execution Tool for Cairo

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

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.

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.

Dependencies (Building from Source)

• 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

Getting Started: Interpretation

The repo comes with the simple example that you can also find on the official Cairo documentation:

# examples/test0.cairo: interpretation
func main():
    [ap] = 1000; ap++
    [ap] = 2000; ap++
    [ap] = [ap - 2] + [ap - 1]; ap++
    ret
end

where the user assigns two values 1000 and 2000 to corresponding memory addresses and assigns the result of adding them up to another memory address. By calling:

./run-medjai.sh ./examples/test0.cairo

Medjai can then execute the program and outputs the desired final memory states.

Getting Started: Symbolic Reasoning (Dev)

Medjai also supports reasoning and you can utilize it to verify several properties of Cairo programs. For example:

# examples/test1.cairo: symbolic reasoning
func main():
    [ap] = 1000; ap++
    [ap] = symbolic(type='integer', name='var0'); ap++
    [ap] = [ap - 2] / [ap - 1]; ap++
    ret
end

The above code snippet creates a symbolic integer var0 and assigns it to a certain memory address. We would like to find out whether this piece of code is correct or not by asking Medjai to find a counterexample of var0 that would potentially crash the execution of the program. By calling:

./run-medjai.sh ./examples/test0.cairo

Medjai will reason about all possible values of var0 together with all program states, and return one of them that can compromise the program execution, which is 0 that would cause a "division by 0" error.

As in the line of code after we create the symbolic variable, var0 is immediately used as denominator of a division arithmetic operation [ap] = [ap - 2] / [ap - 1]; ap++, which will cause an "unknown value for memory cell" exception if var0 is set to 0. This verifies the counterexample it found.

Commands & Usages

Using run-medjai.sh

usage: run-medjai.sh <path-to-cairo-program>

Using cairo-run.rkt

usage: cairo-run.rkt [ <option> ... ]

<option> is one of

  --cname <p-cname>
     path to a compiled Cairo program (.json)
  --help, -h
     Show this help
  --
     Do not treat any remaining argument as a switch (at this level)

 /|\ Brackets indicate mutually exclusive options.

 Multiple single-letter switches can be combined after
 one `-`. For example, `-h-` is the same as `-h --`.