symevm#

symbolic EVM implin Haskell for smart contract analysis/ equivalence checking and verification that tracks path constraints through JUMPI branches, maintains symbolic state (stack, memory, storage) and has constraint analysis of contract behavior

Usage#

import SymbolicExpression
import SymbolicState
import Executor
import qualified Data.ByteString as BS

let bytecode = BS.pack [0x33, 0x61, 0x12, 0x34, 0x14, 0x60, 0x0b, 0x57, ...]
let paths = explore bytecode (initState BS.empty) 1000

mapM_ analyzeConstraints paths

Single path execution:

run :: ByteString -> ExecState -> Int -> [ExecState]

Path exploration:

explore :: ByteString -> ExecState -> Int -> [ExecState]

Build#

cabal build
cabal run symevm

Example#

let code = BS.pack [
  0x60, 0x00, 
  0x35,        
  0x60, 0x64,  
  0x11,       
  0x60, 0x0a,  
  0x57,       
  0xfd,        
  0x5b,        
  0x00       
  ]

let paths = explore code (initState BS.empty) 50

Yields 2 paths:

Path 1: calldataload(0) > 100 → PC=10, halted Path 2: calldataload(0) <= 100 → reverted