Symbolic execution PoC

flake.nix

@@ -49,7 +49,7 @@
         echidna = with pkgs; lib.pipe
           (haskellPackages.callCabal2nix "echidna" ./. { inherit hevm; })
           [
-            (haskell.lib.compose.addTestToolDepends [ haskellPackages.hpack slither-analyzer solc ])
+            (haskell.lib.compose.addTestToolDepends [ haskellPackages.hpack slither-analyzer solc z3])
             (haskell.lib.compose.disableCabalFlag "static")
           ];
       in rec {

lib/Echidna.hs

@@ -45,12 +45,13 @@ prepareContract
   -> NonEmpty FilePath
   -> Maybe ContractName
   -> Seed
-  -> IO (VM, World, GenDict)
+  -> IO (VM, World, GenDict, [Tx])
 prepareContract env contracts solFiles specifiedContract seed = do
   let solConf = env.cfg.solConf
 
   -- compile and load contracts
-  (vm, funs, testNames, signatureMap) <- loadSpecified env specifiedContract contracts
+  (vm, funs, testNames, signatureMap, symTxs) <-
+    loadSpecified env specifiedContract contracts
 
   -- run processors
   slitherInfo <- runSlither (NE.head solFiles) solConf
@@ -84,7 +85,7 @@ prepareContract env contracts solFiles specifiedContract seed = do
                      (returnTypes contracts)
 
   writeIORef env.testsRef echidnaTests
-  pure (vm, world, dict)
+  pure (vm, world, dict, symTxs)
 
 loadInitialCorpus :: Env -> World -> IO [[Tx]]
 loadInitialCorpus env world = do

lib/Echidna/Config.hs

@@ -119,6 +119,7 @@ instance FromJSON EConfigWithUsage where
         <*> v ..:? "testDestruction" ..!= False
         <*> v ..:? "allowFFI"        ..!= False
         <*> fnFilter
+        <*> v ..:? "symExec"         ..!= False
         where
         mode = v ..:? "testMode" >>= \case
           Just s  -> pure $ validateTestMode s

lib/Echidna/Solidity.hs

@@ -40,6 +40,7 @@ import Echidna.Etheno (loadEthenoBatch)
 import Echidna.Events (EventMap, extractEvents)
 import Echidna.Exec (execTx, initialVM)
 import Echidna.Processor
+import Echidna.SymExec qualified
 import Echidna.Test (createTests, isAssertionMode, isPropertyMode, isDapptestMode)
 import Echidna.Types.Config (EConfig(..), Env(..))
 import Echidna.Types.Signature
@@ -48,7 +49,7 @@ import Echidna.Types.Solidity
 import Echidna.Types.Test (EchidnaTest(..))
 import Echidna.Types.Tx
   ( basicTx, createTxWithValue, unlimitedGasPerBlock, initialTimestamp
-  , initialBlockNumber )
+  , initialBlockNumber, Tx )
 import Echidna.Types.World (World(..))
 import Echidna.Utility (measureIO)
 
@@ -189,7 +190,7 @@ loadSpecified
   :: Env
   -> Maybe Text
   -> [SolcContract]
-  -> IO (VM, [SolSignature], [Text], SignatureMap)
+  -> IO (VM, [SolSignature], [Text], SignatureMap, [Tx])
 loadSpecified env name cs = do
   let solConf = env.cfg.solConf
 
@@ -200,6 +201,10 @@ loadSpecified env name cs = do
   unless solConf.quiet $
     putStrLn $ "Analyzing contract: " <> T.unpack mainContract.contractName
 
+  symTxs <- if solConf.symExec
+    then Echidna.SymExec.exploreContract solConf.contractAddr mainContract
+    else pure []
+
   let
     -- generate the complete abi mapping
     abi = Map.elems mainContract.abiMap <&> \method -> (method.name, snd <$> method.inputs)
@@ -291,7 +296,7 @@ loadSpecified env name cs = do
 
     case vm4.result of
       Just (VMFailure _) -> throwM SetUpCallFailed
-      _ -> pure (vm4, neFuns, fst <$> tests, abiMapping)
+      _ -> pure (vm4, neFuns, fst <$> tests, abiMapping, symTxs)
 
   where
     choose [] _ = throwM NoContracts
@@ -369,7 +374,7 @@ loadSolTests
 loadSolTests env fp name = do
   let solConf = env.cfg.solConf
   BuildOutput{contracts = Contracts (Map.elems -> contracts)} <- compileContracts solConf fp
-  (vm, funs, testNames, _signatureMap) <- loadSpecified env name contracts
+  (vm, funs, testNames, _signatureMap, _) <- loadSpecified env name contracts
   let
     eventMap = Map.unions $ map (.eventMap) contracts
     world = World solConf.sender mempty Nothing [] eventMap

lib/Echidna/SymExec.hs

@@ -0,0 +1,68 @@
+{-# LANGUAGE DataKinds #-}
+
+module Echidna.SymExec where
+
+import Control.Monad (forM)
+import Data.ByteString qualified as BS
+import Data.ByteString.Lazy qualified as BS
+import Data.Functor ((<&>))
+import Data.Map qualified as Map
+import Data.Maybe (fromMaybe, mapMaybe)
+import Data.Text qualified as T
+
+import EVM.ABI
+import EVM.Expr (simplify)
+import EVM.Fetch qualified as Fetch
+import EVM.SMT
+import EVM.Solidity (SolcContract(..), Method(..))
+import EVM.Solvers (withSolvers, Solver(Z3), CheckSatResult(Sat))
+import EVM.SymExec (interpret, runExpr, abstractVM, mkCalldata, produceModels, Sig(Sig), LoopHeuristic (Naive))
+import EVM.Types
+
+import Echidna.Types.Tx
+
+exploreContract :: Addr -> SolcContract -> IO [Tx]
+exploreContract dst contract = do
+  let methods = Map.elems contract.abiMap
+      timeout = Just 30 -- seconds
+
+  res <- withSolvers Z3 2 timeout $ \solvers -> do
+    forM methods $ \method -> do
+      let
+        calldata = mkCalldata (Just (Sig method.methodSignature (snd <$> method.inputs))) []
+        vmSym = abstractVM calldata contract.runtimeCode Nothing (ConcreteStore mempty)
+        maxIter = Just 10
+        askSmtIters = 5
+        rpcInfo = Nothing
+
+      exprInter <- interpret (Fetch.oracle solvers rpcInfo) maxIter askSmtIters Naive vmSym runExpr
+      models <- produceModels solvers (simplify exprInter)
+      pure $ mapMaybe (modelToTx dst method) models
+
+  pure $ mconcat res
+
+modelToTx :: Addr -> Method -> (Expr 'End, CheckSatResult) -> Maybe Tx
+modelToTx dst method (_end, result) =
+  case result of
+    Sat cex ->
+      let
+        args = (zip [1..] method.inputs) <&> \(i::Int, (_argName, argType)) ->
+          case Map.lookup (Var ("arg" <> T.pack (show i))) cex.vars of
+            Just w ->
+              decodeAbiValue argType (BS.fromStrict (word256Bytes w))
+            Nothing -> -- put a placeholder
+              decodeAbiValue argType (BS.repeat 0)
+
+        value = fromMaybe 0 $ Map.lookup (CallValue 0) cex.txContext
+
+      in Just Tx
+        { call = SolCall (method.name, args)
+        , src = 0
+        , dst = dst
+        , gasprice = 0
+        , gas = maxGasPerBlock
+        , value = value
+        , delay = (0, 0)
+        }
+
+    _ -> Nothing

lib/Echidna/Types/Solidity.hs

@@ -78,6 +78,7 @@ data SolConf = SolConf
   , testDestruction :: Bool             -- ^ Whether or not to add a property to detect contract destruction
   , allowFFI        :: Bool             -- ^ Whether or not to allow FFI hevm cheatcode
   , methodFilter    :: Filter           -- ^ List of methods to avoid or include calling during a campaign
+  , symExec         :: Bool
   }
 
 -- | List of contract names from every source cache

src/Main.hs

@@ -116,12 +116,13 @@ main = withUtf8 $ withCP65001 $ do
 
   -- take the seed from config, otherwise generate a new one
   seed <- maybe (getRandomR (0, maxBound)) pure cfg.campaignConf.seed
-  (vm, world, dict) <-
+  (vm, world, dict, symTxs) <-
     prepareContract env contracts cliFilePath cliSelectedContract seed
 
   initialCorpus <- loadInitialCorpus env world
+  let corpus = initialCorpus <> (pure <$> symTxs)
   -- start ui and run tests
-  _campaign <- runReaderT (ui vm world dict initialCorpus) env
+  _campaign <- runReaderT (ui vm world dict corpus) env
 
   contractsCache <- readIORef cacheContractsRef
   slotsCache <- readIORef cacheSlotsRef
@@ -146,8 +147,8 @@ main = withUtf8 $ withCP65001 $ do
       measureIO cfg.solConf.quiet "Saving test reproducers" $
         saveTxs (dir </> "reproducers") (filter (not . null) $ (.reproducer) <$> tests)
       measureIO cfg.solConf.quiet "Saving corpus" $ do
-        corpus <- readIORef corpusRef
-        saveTxs (dir </> "coverage") (snd <$> Set.toList corpus)
+        finalCorpus <- readIORef corpusRef
+        saveTxs (dir </> "coverage") (snd <$> Set.toList finalCorpus)
 
       -- TODO: We use the corpus dir to save coverage reports which is confusing.
       -- Add config option to pass dir for saving coverage report and decouple it

src/test/Common.hs

@@ -113,9 +113,8 @@ runContract f selectedContract cfg = do
                 , eventQueue
                 , testsRef
                 , chainId = Nothing }
-  (vm, world, dict) <- prepareContract env contracts (f :| []) selectedContract seed
-
-  let corpus = []
+  (vm, world, dict, symTxs) <- prepareContract env contracts (f :| []) selectedContract seed
+  let corpus = pure <$> symTxs
   (_stopReason, finalState) <- flip runReaderT env $
     runWorker (pure ()) vm world dict 0 corpus cfg.campaignConf.testLimit
 

src/test/Spec.hs

@@ -32,4 +32,5 @@ main = withCurrentDirectory "./tests/solidity" . defaultMain $
            , dapptestTests
            , encodingJSONTests
            , cheatTests
+           -- , symbolicTests
            ]

src/test/Tests/Symbolic.hs

@@ -0,0 +1,13 @@
+module Tests.Symbolic (symbolicTests) where
+
+import Test.Tasty (TestTree, testGroup)
+
+import Common (testContract, solved)
+
+symbolicTests :: TestTree
+symbolicTests = testGroup "Symbolic tests"
+  [
+    testContract "symbolic/sym.sol" (Just "symbolic/sym.yaml")
+      [ ("func_one passed", solved "func_one")
+      , ("func_two passed", solved "func_two") ]
+  ]

tests/solidity/basic/default.yaml

@@ -89,3 +89,4 @@ rpcUrl: null
 rpcBlock: null
 # number of workers
 workers: 1
+symExec: false

tests/solidity/symbolic/sym.sol

@@ -0,0 +1,13 @@
+contract VulnerableContract {
+   function func_one(int256 x) public pure {
+     if (x / 4 == -20) {
+       assert(false); // BUG
+     }
+   }
+
+   function func_two(int128 x) public payable {
+     if ((msg.value >> 30) / 7 == 2) {
+       assert(false); // BUG
+     }
+   }
+}

tests/solidity/symbolic/sym.yaml

@@ -0,0 +1,2 @@
+testMode: assertion
+symExec: true