Skip to content

Veridise/Eurus

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

18 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Eurus - Precise Attack Synthesis for DeFi Apps

Eurus is an open-source general framework for smart contract verification and synthesis. Eurus performs reasoning using a builtin symbolic virtual machine based on the YUL intermediate language from Solidity.

Eurus is still under active development. Please see different branches for history versions (e.g. demo version).

Building from Docker

docker build -t eurus:v0 .
docker run -it --rm eurus:v0 bash

Building from Source

Python Yul Parser

This parses the Yul source code into json representation, and generates a helper configuration file which includes:

  • mapping of call codes and function names (signatures)
usage: yul_parser.py [-h] [--yul YUL] [--verbose VERBOSE]

optional arguments:
  -h, --help         show this help message and exit
  --yul YUL          input yul file
  --verbose VERBOSE  show more info for debugging

It will automatically outputs filename.json and filename.config.json in the same folder.

Example Usage

There are two sets of examples in examples/ showing how to use Eurus to perform concrete and symbolic execution with verification performed. The ex/ corresponds to the concrete reasoning part of Eurus, and the symex/ corresponds to the symbolic reasoning part. To run them, you'll need to first prepare them by running:

cd examples/
bash ./prepare-ex.sh
# or:
#   bash ./prepare-symex.sh

Then you can run different Eurus script to perform different tasks:

racket ./test-ex5.rkt
# or:
#   racket ./test-symex1.rkt

You can find out more details by reading ex/ex.sol and symex/symex.sol, as well as the test-*.rkt Eurus scripts. More documentations are on the way. For detailed steps, please see the "Other Commands" section.

Other Commands

  • Automatically generate the core Yul parser:

    cd ./utils/YulAntlr/
    antlr4 -Dlanguage=Python3 Yul.g4
  • Compile a solidity source code into Yul:

    # ex (examples)
    solc ./examples/ex/ex.sol --ir --overwrite -o ./examples/ex
  • Translate original Yul to Eurus Yul:

    # examples
    python ./utils/yul_translator.py --yul ./examples/ex/ex0.yul
    python ./utils/yul_translator.py --yul ./examples/ex/ex1.yul
    python ./utils/yul_translator.py --yul ./examples/ex/ex2.yul
    python ./utils/yul_translator.py --yul ./examples/ex/ex3.yul
  • Pre-process the Yul code and generated parsed json and config:

    # examples
    python ./utils/yul_parser.py --yul ./examples/ex/ex0.eurus.yul
    python ./utils/yul_parser.py --yul ./examples/ex/ex1.eurus.yul
    python ./utils/yul_parser.py --yul ./examples/ex/ex2.eurus.yul
    python ./utils/yul_parser.py --yul ./examples/ex/ex3.eurus.yul
  • run test script

    racket ./test-ex5.rkt
  • External ABI Encoding

    python ./utils/abiencode.py "['string'],['abcd']"
  • External ABI Decoding

    python ./utils/abidecode.py "['string'],b'\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x20\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x06\x6d\x79\x6e\x61\x6d\x65\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00'"
  • External Keccak256

    python ./utils/keccak256.py "fun(uint256,bool)"