From 69075cba28851340c938264ab8c7076a79c2bc4a Mon Sep 17 00:00:00 2001 From: dxo Date: Fri, 28 Jul 2023 14:50:12 +0200 Subject: [PATCH] SymExec: default symbolic values when displaying calldata Sometimes we get back a model that does not mention all variables that are present in the input calldata buffer. This can happen if those variables are not relevant to the branch that we are producing a model for. In this case we can simply set the values that remain symbolic afters subsituting in our cex to some default value. We will still have issues here if we have lost some constraints over those variables during simplification, but it's better than what we're doing now (i.e. just printing "Any" if we can't get a fully concrete model for calldata out). A fully general (and hopefully correct) approach could look like: https://github.com/ethereum/hevm/issues/334 --- CHANGELOG.md | 1 + src/EVM/SymExec.hs | 70 +++++++++++++++++++++++++++++++++------------ src/EVM/UnitTest.hs | 4 +-- test/test.hs | 2 +- 4 files changed, 56 insertions(+), 21 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index f96df4ed4..3f8e787ab 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -11,6 +11,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 - CopySlice wraparound issue especially during CopyCallBytesToMemory - EVM.Solidity.toCode to include contractName in error string +- Better cex reconstruction in cases where branches do not refer to all input variables in calldata ## Changed diff --git a/src/EVM/SymExec.hs b/src/EVM/SymExec.hs index 95c484549..5d91870a0 100644 --- a/src/EVM/SymExec.hs +++ b/src/EVM/SymExec.hs @@ -812,7 +812,7 @@ formatCex cd m@(SMTCex _ _ store blockContext txContext) = T.unlines $ -- it for branches that do not refer to calldata at all (e.g. the top level -- callvalue check inserted by solidity in contracts that don't have any -- payable functions). - cd' = prettyBuf $ Expr.simplify $ subModel m cd + cd' = prettyBuf . Expr.simplify . defaultSymbolicValues $ subModel m cd storeCex :: [Text] storeCex @@ -871,23 +871,55 @@ formatCex cd m@(SMTCex _ _ store blockContext txContext) = T.unlines $ prettyBuf :: Expr Buf -> Text prettyBuf (ConcreteBuf "") = "Empty" prettyBuf (ConcreteBuf bs) = formatBinary bs - prettyBuf _ = "Any" - --- | Takes a buffer and a Cex and replaces all abstract values in the buf with + prettyBuf b = internalError $ "Unexpected symbolic buffer:\n" <> T.unpack (formatExpr b) + +-- | If the expression contains any symbolic values, default them to some +-- concrete value The intuition here is that if we still have symbolic values +-- in our calldata expression after substituing in our cex, then they can have +-- any value and we can safely pick a random value. This is a bit unsatisfying, +-- we should really be doing smth like: https://github.com/ethereum/hevm/issues/334 +-- but it's probably good enough for now +defaultSymbolicValues :: Expr a -> Expr a +defaultSymbolicValues e = subBufs (foldTerm symbufs mempty e) + . subVars (foldTerm symwords mempty e) $ e + where + symbufs :: Expr a -> Map (Expr Buf) ByteString + symbufs = \case + a@(AbstractBuf _) -> Map.singleton a "" + _ -> mempty + symwords :: Expr a -> Map (Expr EWord) W256 + symwords = \case + a@(Var _) -> Map.singleton a 0 + a@Origin -> Map.singleton a 0 + a@Coinbase -> Map.singleton a 0 + a@Timestamp -> Map.singleton a 0 + a@BlockNumber -> Map.singleton a 0 + a@PrevRandao -> Map.singleton a 0 + a@GasLimit -> Map.singleton a 0 + a@ChainId -> Map.singleton a 0 + a@BaseFee -> Map.singleton a 0 + _ -> mempty + +-- | Takes an expression and a Cex and replaces all abstract values in the buf with -- concrete ones from the Cex. subModel :: SMTCex -> Expr a -> Expr a -subModel c expr = - subBufs (fmap forceFlattened c.buffers) . subVars c.vars . subStore c.store - . subVars c.blockContext . subVars c.txContext $ expr +subModel c + = subBufs (fmap forceFlattened c.buffers) + . subStore c.store + . subVars c.vars + . subVars c.blockContext + . subVars c.txContext where forceFlattened (SMT.Flat bs) = bs forceFlattened b@(SMT.Comp _) = forceFlattened $ fromMaybe (internalError $ "cannot flatten buffer: " <> show b) (SMT.collapse b) - subVars model b = Map.foldlWithKey subVar b model +subVars :: Map (Expr EWord) W256 -> Expr a -> Expr a +subVars model b = Map.foldlWithKey subVar b model + where subVar :: Expr a -> Expr EWord -> W256 -> Expr a - subVar b var val = mapExpr go b + subVar a var val = mapExpr go a where go :: Expr a -> Expr a go = \case @@ -896,9 +928,11 @@ subModel c expr = else v e -> e - subBufs model b = Map.foldlWithKey subBuf b model +subBufs :: Map (Expr Buf) ByteString -> Expr a -> Expr a +subBufs model b = Map.foldlWithKey subBuf b model + where subBuf :: Expr a -> Expr Buf -> ByteString -> Expr a - subBuf b var val = mapExpr go b + subBuf x var val = mapExpr go x where go :: Expr a -> Expr a go = \case @@ -907,10 +941,10 @@ subModel c expr = else a e -> e - subStore :: Map W256 (Map W256 W256) -> Expr a -> Expr a - subStore m b = mapExpr go b - where - go :: Expr a -> Expr a - go = \case - AbstractStore -> ConcreteStore m - e -> e +subStore :: Map W256 (Map W256 W256) -> Expr a -> Expr a +subStore model b = mapExpr go b + where + go :: Expr a -> Expr a + go = \case + AbstractStore -> ConcreteStore model + e -> e diff --git a/src/EVM/UnitTest.hs b/src/EVM/UnitTest.hs index ec6908429..173f99afa 100644 --- a/src/EVM/UnitTest.hs +++ b/src/EVM/UnitTest.hs @@ -19,7 +19,7 @@ import EVM.FeeSchedule qualified as FeeSchedule import EVM.Fetch qualified as Fetch import EVM.Format import EVM.Solidity -import EVM.SymExec (defaultVeriOpts, symCalldata, verify, isQed, extractCex, runExpr, subModel, VeriOpts(..)) +import EVM.SymExec (defaultVeriOpts, symCalldata, verify, isQed, extractCex, runExpr, subModel, defaultSymbolicValues, VeriOpts(..)) import EVM.Types import EVM.Transaction (initTx) import EVM.RLP @@ -777,7 +777,7 @@ prettyCalldata cex buf sig types = head (Text.splitOn "(" sig) <> showCalldata c showCalldata :: (?context :: DappContext) => SMTCex -> [AbiType] -> Expr Buf -> Text showCalldata cex tps buf = "(" <> intercalate "," (fmap showVal vals) <> ")" where - argdata = Expr.drop 4 $ simplify $ subModel cex buf + argdata = Expr.drop 4 . simplify . defaultSymbolicValues $ subModel cex buf vals = case decodeBuf tps argdata of CAbi v -> v _ -> internalError $ "unable to abi decode function arguments:\n" <> (Text.unpack $ formatExpr argdata) diff --git a/test/test.hs b/test/test.hs index ea406b78b..f49948690 100644 --- a/test/test.hs +++ b/test/test.hs @@ -57,7 +57,7 @@ import EVM.SMT hiding (one) import EVM.Solidity import EVM.Solvers import EVM.Stepper qualified as Stepper -import EVM.SymExec +import EVM.SymExec hiding (subStore) import EVM.Test.Tracing qualified as Tracing import EVM.Test.Utils import EVM.Traversals