From 6f0d8d107b4e18ed77d31e14469630f77c5017b3 Mon Sep 17 00:00:00 2001 From: Artur Cygan Date: Tue, 18 Apr 2023 03:13:33 +0200 Subject: [PATCH 1/2] Symbolic execution PoC Solve calldata per method --- flake.nix | 2 +- lib/Echidna.hs | 7 ++-- lib/Echidna/Config.hs | 1 + lib/Echidna/Solidity.hs | 13 ++++-- lib/Echidna/SymExec.hs | 68 +++++++++++++++++++++++++++++++ lib/Echidna/Types/Solidity.hs | 1 + src/Main.hs | 9 ++-- src/test/Common.hs | 5 +-- src/test/Spec.hs | 1 + src/test/Tests/Symbolic.hs | 13 ++++++ tests/solidity/basic/default.yaml | 1 + tests/solidity/symbolic/sym.sol | 13 ++++++ tests/solidity/symbolic/sym.yaml | 2 + 13 files changed, 121 insertions(+), 15 deletions(-) create mode 100644 lib/Echidna/SymExec.hs create mode 100644 src/test/Tests/Symbolic.hs create mode 100644 tests/solidity/symbolic/sym.sol create mode 100644 tests/solidity/symbolic/sym.yaml diff --git a/flake.nix b/flake.nix index a73236b55..a2c535241 100644 --- a/flake.nix +++ b/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 { diff --git a/lib/Echidna.hs b/lib/Echidna.hs index 63ed44ee5..d89641b42 100644 --- a/lib/Echidna.hs +++ b/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 diff --git a/lib/Echidna/Config.hs b/lib/Echidna/Config.hs index 575b1a1b4..0c6036b43 100644 --- a/lib/Echidna/Config.hs +++ b/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 diff --git a/lib/Echidna/Solidity.hs b/lib/Echidna/Solidity.hs index 3abae02ad..53de58c73 100644 --- a/lib/Echidna/Solidity.hs +++ b/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 diff --git a/lib/Echidna/SymExec.hs b/lib/Echidna/SymExec.hs new file mode 100644 index 000000000..a3e428769 --- /dev/null +++ b/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 AbstractStore + 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 diff --git a/lib/Echidna/Types/Solidity.hs b/lib/Echidna/Types/Solidity.hs index dec1c8739..70cf4098b 100644 --- a/lib/Echidna/Types/Solidity.hs +++ b/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 diff --git a/src/Main.hs b/src/Main.hs index d8427d199..ac2914493 100644 --- a/src/Main.hs +++ b/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 diff --git a/src/test/Common.hs b/src/test/Common.hs index a69013c15..ff3fdf814 100644 --- a/src/test/Common.hs +++ b/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 diff --git a/src/test/Spec.hs b/src/test/Spec.hs index dbc39b59d..80a3a1288 100644 --- a/src/test/Spec.hs +++ b/src/test/Spec.hs @@ -32,4 +32,5 @@ main = withCurrentDirectory "./tests/solidity" . defaultMain $ , dapptestTests , encodingJSONTests , cheatTests + -- , symbolicTests ] diff --git a/src/test/Tests/Symbolic.hs b/src/test/Tests/Symbolic.hs new file mode 100644 index 000000000..2a35eb684 --- /dev/null +++ b/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") ] + ] diff --git a/tests/solidity/basic/default.yaml b/tests/solidity/basic/default.yaml index 9b2c6f71a..356422b42 100644 --- a/tests/solidity/basic/default.yaml +++ b/tests/solidity/basic/default.yaml @@ -89,3 +89,4 @@ rpcUrl: null rpcBlock: null # number of workers workers: 1 +symExec: false diff --git a/tests/solidity/symbolic/sym.sol b/tests/solidity/symbolic/sym.sol new file mode 100644 index 000000000..947f2fcfa --- /dev/null +++ b/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 + } + } +} diff --git a/tests/solidity/symbolic/sym.yaml b/tests/solidity/symbolic/sym.yaml new file mode 100644 index 000000000..79dd17d9f --- /dev/null +++ b/tests/solidity/symbolic/sym.yaml @@ -0,0 +1,2 @@ +testMode: assertion +symExec: true From aeb0d08cf17f9ab520d058f03191df0548e31df3 Mon Sep 17 00:00:00 2001 From: Artur Cygan Date: Wed, 14 Jun 2023 20:12:34 +0200 Subject: [PATCH 2/2] Change storage to concrete in symexec --- lib/Echidna/SymExec.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/Echidna/SymExec.hs b/lib/Echidna/SymExec.hs index a3e428769..e3b581ddb 100644 --- a/lib/Echidna/SymExec.hs +++ b/lib/Echidna/SymExec.hs @@ -30,7 +30,7 @@ exploreContract dst contract = do forM methods $ \method -> do let calldata = mkCalldata (Just (Sig method.methodSignature (snd <$> method.inputs))) [] - vmSym = abstractVM calldata contract.runtimeCode Nothing AbstractStore + vmSym = abstractVM calldata contract.runtimeCode Nothing (ConcreteStore mempty) maxIter = Just 10 askSmtIters = 5 rpcInfo = Nothing