From 811095a971b90d7709b96dd29c9a253e8eaa57f8 Mon Sep 17 00:00:00 2001 From: dxo Date: Mon, 11 Sep 2023 17:23:28 +0200 Subject: [PATCH 1/5] EVM: OpCreate: better comments --- src/EVM.hs | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) diff --git a/src/EVM.hs b/src/EVM.hs index 4279fd273..8c0087c79 100644 --- a/src/EVM.hs +++ b/src/EVM.hs @@ -2139,23 +2139,29 @@ create :: forall t s. (?op :: Word8, VMOps t) -> Expr EWord -> Gas t -> Expr EWord -> [Expr EWord] -> Expr EAddr -> Expr Buf -> EVM t s () create self this xSize xGas xValue xs newAddr initCode = do vm0 <- get + -- are we exceeding the max init code size if xSize > Lit (vm0.block.maxCodeSize * 2) then do assign (#state % #stack) (Lit 0 : xs) assign (#state % #returndata) mempty vmError $ MaxInitCodeSizeExceeded (vm0.block.maxCodeSize * 2) xSize + -- are we overflowing the nonce else if this.nonce == Just maxBound then do assign (#state % #stack) (Lit 0 : xs) assign (#state % #returndata) mempty pushTrace $ ErrorTrace NonceOverflow next + -- are we overflowing the stack else if length vm0.frames >= 1024 then do assign (#state % #stack) (Lit 0 : xs) assign (#state % #returndata) mempty pushTrace $ ErrorTrace CallDepthLimitReached next + -- are we deploying to an address that already has a contract? + -- note: this check is only sound to do statically if symbolic addresses + -- cannot have the value of any existing concrete addresses in the state. else if collision $ Map.lookup newAddr vm0.env.contracts then burn' xGas $ do assign (#state % #stack) (Lit 0 : xs) @@ -2171,9 +2177,23 @@ create self this xSize xGas xValue xs newAddr initCode = do next touchAccount self touchAccount newAddr +<<<<<<< HEAD -- are we overflowing the nonce False -> burn' xGas $ do case parseInitCode initCode of +======= + False -> burn xGas $ do + -- unfortunately we have to apply some (pretty hacky) + -- heuristics here to parse the unstructured buffer read + -- from memory into a code and data section + let contract' = do + prefixLen <- Expr.concPrefix initCode + prefix <- Expr.toList $ Expr.take prefixLen initCode + let sym = Expr.drop prefixLen initCode + conc <- mapM maybeLitByte prefix + pure $ InitCode (BS.pack $ V.toList conc) sym + case contract' of +>>>>>>> 10525566 (EVM: OpCreate: better comments) Nothing -> partial $ UnexpectedSymbolicArg vm0.state.pc (getOpName vm0.state) "initcode must have a concrete prefix" [] Just c -> do From a6bc0b09491888201cb5d231d61bc6f36685e880 Mon Sep 17 00:00:00 2001 From: dxo Date: Mon, 11 Sep 2023 17:23:54 +0200 Subject: [PATCH 2/5] SMT: assume that symbolic addresses cannot be the zero address or precompiles --- src/EVM/SMT.hs | 4 +++- test/test.hs | 8 ++++---- 2 files changed, 7 insertions(+), 5 deletions(-) diff --git a/src/EVM/SMT.hs b/src/EVM/SMT.hs index cb2e94181..093dc2346 100644 --- a/src/EVM/SMT.hs +++ b/src/EVM/SMT.hs @@ -433,9 +433,11 @@ declareVars names = SMT2 (["; variables"] <> fmap declare names) cexvars mempty -- Given a list of variable names, create an SMT2 object with the variables declared declareAddrs :: [Builder] -> SMT2 -declareAddrs names = SMT2 (["; symbolic addresseses"] <> fmap declare names) cexvars mempty +declareAddrs names = SMT2 (["; symbolic addresseses"] <> fmap declare names <> fmap assume names) mempty cexvars where declare n = "(declare-fun " <> n <> " () Addr)" + -- assume that symbolic addresses do not collide with the zero address or precompiles + assume n = "(assert (bvugt " <> n <> " (_ bv9 160)))" cexvars = (mempty :: CexVars){ addrs = fmap toLazyText names } declareFrameContext :: [(Builder, [Prop])] -> Err SMT2 diff --git a/test/test.hs b/test/test.hs index 54b06c82a..4475b68dd 100644 --- a/test/test.hs +++ b/test/test.hs @@ -1967,7 +1967,7 @@ tests = testGroup "hevm" [i| contract A { function f() external { - assert(msg.sender != address(0x0)); + assert(msg.sender != address(0x10)); } } |] @@ -1975,7 +1975,7 @@ tests = testGroup "hevm" [i| contract B { function f() external { - assert(block.coinbase != address(0x1)); + assert(block.coinbase != address(0x11)); } } |] @@ -1983,7 +1983,7 @@ tests = testGroup "hevm" [i| contract C { function f() external { - assert(tx.origin != address(0x2)); + assert(tx.origin != address(0x12)); } } |] @@ -1991,7 +1991,7 @@ tests = testGroup "hevm" [i| contract D { function f() external { - assert(address(this) != address(0x3)); + assert(address(this) != address(0x13)); } } |] From 63bf583e23642969959614e3278d0044c53133ca Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Tue, 28 Jan 2025 14:24:09 +0100 Subject: [PATCH 3/5] SymExec: add aliasing constraints for contract mapping keys Adds constraints that ensure that symbolic addresses that are used to key the contracts mapping cannot alias any other keys. --- src/EVM.hs | 5 +++-- src/EVM/Expr.hs | 4 ++++ src/EVM/SymExec.hs | 14 ++++++++++---- test/test.hs | 17 +++++++++++++++-- 4 files changed, 32 insertions(+), 8 deletions(-) diff --git a/src/EVM.hs b/src/EVM.hs index 8c0087c79..2600745e1 100644 --- a/src/EVM.hs +++ b/src/EVM.hs @@ -2160,8 +2160,9 @@ create self this xSize xGas xValue xs newAddr initCode = do pushTrace $ ErrorTrace CallDepthLimitReached next -- are we deploying to an address that already has a contract? - -- note: this check is only sound to do statically if symbolic addresses - -- cannot have the value of any existing concrete addresses in the state. + -- note: the symbolic interpreter generates constraints ensuring that + -- symbolic storage keys cannot alias other storage keys, making this check + -- safe to perform statically else if collision $ Map.lookup newAddr vm0.env.contracts then burn' xGas $ do assign (#state % #stack) (Lit 0 : xs) diff --git a/src/EVM/Expr.hs b/src/EVM/Expr.hs index 664718b2f..264387aaf 100644 --- a/src/EVM/Expr.hs +++ b/src/EVM/Expr.hs @@ -1390,6 +1390,10 @@ isPartial = \case Partial {} -> True _ -> False +isSymAddr :: Expr EAddr -> Bool +isSymAddr (SymAddr _) = True +isSymAddr _ = False + -- | Returns the byte at idx from the given word. indexWord :: Expr EWord -> Expr EWord -> Expr Byte -- Simplify masked reads: diff --git a/src/EVM/SymExec.hs b/src/EVM/SymExec.hs index a69d11001..76759613d 100644 --- a/src/EVM/SymExec.hs +++ b/src/EVM/SymExec.hs @@ -499,12 +499,18 @@ runExpr :: Stepper.Stepper Symbolic RealWorld (Expr End) runExpr = do vm <- Stepper.runFully let traces = TraceContext (Zipper.toForest vm.traces) vm.env.contracts vm.labels + let constraints = vm.constraints <> consistentStorageKeys vm.env.contracts pure $ case vm.result of - Just (VMSuccess buf) -> Success vm.constraints traces buf (fmap toEContract vm.env.contracts) - Just (VMFailure e) -> Failure vm.constraints traces e - Just (Unfinished p) -> Partial vm.constraints traces p + Just (VMSuccess buf) -> Success constraints traces buf (fmap toEContract vm.env.contracts) + Just (VMFailure e) -> Failure constraints traces e + Just (Unfinished p) -> Partial constraints traces p _ -> internalError "vm in intermediate state after call to runFully" +-- build constraints that ensure that symbolic storage keys cannot alias other storage keys + -- let asserts = vm.constraints <> consistentStorageKeys vm.env.contracts +consistentStorageKeys :: Map (Expr EAddr) Contract -> [Prop] +consistentStorageKeys (Map.keys -> addrs) = [a ./= b | a <- addrs, b <- filter Expr.isSymAddr addrs] + toEContract :: Contract -> Expr EContract toEContract c = C c.code c.storage c.tStorage c.balance c.nonce @@ -963,7 +969,7 @@ prettyCalldata cex buf sig types = headErr errSig (T.splitOn "(" sig) <> "(" <> ConcreteBuf c -> T.pack (bsToHex c) _ -> err SAbi _ -> err - headErr e l = fromMaybe e $ listToMaybe l + headErr e l = fromMaybe e $ listToMaybe l err = internalError $ "unable to produce a concrete model for calldata: " <> show buf errSig = internalError $ "unable to split sig: " <> show sig diff --git a/test/test.hs b/test/test.hs index 4475b68dd..2c3091309 100644 --- a/test/test.hs +++ b/test/test.hs @@ -1759,8 +1759,7 @@ tests = testGroup "hevm" Just c <- solcRuntime "C" src res <- reachableUserAsserts c Nothing assertBoolM "unexpected cex" (isRight res) - -- TODO: implement missing aliasing rules - , expectFail $ test "deployed-contract-addresses-cannot-alias" $ do + , testCase "deployed-contract-addresses-cannot-alias" $ do Just c <- solcRuntime "C" [i| contract A {} @@ -1962,6 +1961,20 @@ tests = testGroup "hevm" Right e <- reachableUserAsserts c Nothing -- TODO: this should work one day assertBoolM "should be partial" (Expr.containsNode isPartial e) + , test "symbolic-addresses-cannot-be-zero-or-precompiles" $ do + let addrs = [T.pack . show . Addr $ a | a <- [0x0..0x09]] + mkC a = fromJust <$> solcRuntime "A" + [i| + contract A { + function f() external { + assert(msg.sender != address(${a})); + } + } + |] + codes <- mapM mkC addrs + results <- mapM (flip reachableUserAsserts (Just (Sig "f()" []))) codes + let ok = and $ fmap (isRight) results + assertBool "unexpected cex" ok , test "addresses-in-context-are-symbolic" $ do Just a <- solcRuntime "A" [i| From 69b702b98eac93b64a6e3aae4bbe248ff656d22c Mon Sep 17 00:00:00 2001 From: Mate Soos Date: Tue, 28 Jan 2025 14:26:26 +0100 Subject: [PATCH 4/5] Update aliasing PR for newer setup --- CHANGELOG.md | 1 + src/EVM.hs | 25 +++++++++++-------------- src/EVM/SMT.hs | 15 ++++++++------- src/EVM/SymExec.hs | 12 +++--------- test/test.hs | 30 +++++++++++++++++++++++------- 5 files changed, 46 insertions(+), 37 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index d58b24a63..892789a0f 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -16,6 +16,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 and continue running, whenever possible - STATICCALL abstraction is now performed in case of symbolic arguments - Better error messages for JSON parsing +- Aliasing works much better for symbolic and concrete addresses ## Fixed - We now try to simplify expressions fully before trying to cast them to a concrete value diff --git a/src/EVM.hs b/src/EVM.hs index 2600745e1..a1220465f 100644 --- a/src/EVM.hs +++ b/src/EVM.hs @@ -1514,6 +1514,16 @@ accountEmpty c = -- TODO: handle symbolic balance... && c.balance == Lit 0 +-- Adds constraints such that two symbolic addresses cannot alias each other +-- and symbolic addresses cannot alias concrete addresses +addAliasConstraints :: EVM t s () +addAliasConstraints = do + vm <- get + let addrConstr = noClash $ Map.keys vm.env.contracts + modifying #constraints ((++) addrConstr) + where + noClash addrs = [a ./= b | a <- addrs, b <- addrs, Expr.isSymAddr b, a < b] + -- * How to finalize a transaction finalize :: VMOps t => EVM t s () finalize = do @@ -1521,6 +1531,7 @@ finalize = do revertContracts = use (#tx % #txReversion) >>= assign (#env % #contracts) revertSubstate = assign (#tx % #subState) (SubState mempty mempty mempty mempty mempty mempty) + addAliasConstraints use #result >>= \case Just (VMFailure (Revert _)) -> do revertContracts @@ -2178,23 +2189,9 @@ create self this xSize xGas xValue xs newAddr initCode = do next touchAccount self touchAccount newAddr -<<<<<<< HEAD -- are we overflowing the nonce False -> burn' xGas $ do case parseInitCode initCode of -======= - False -> burn xGas $ do - -- unfortunately we have to apply some (pretty hacky) - -- heuristics here to parse the unstructured buffer read - -- from memory into a code and data section - let contract' = do - prefixLen <- Expr.concPrefix initCode - prefix <- Expr.toList $ Expr.take prefixLen initCode - let sym = Expr.drop prefixLen initCode - conc <- mapM maybeLitByte prefix - pure $ InitCode (BS.pack $ V.toList conc) sym - case contract' of ->>>>>>> 10525566 (EVM: OpCreate: better comments) Nothing -> partial $ UnexpectedSymbolicArg vm0.state.pc (getOpName vm0.state) "initcode must have a concrete prefix" [] Just c -> do diff --git a/src/EVM/SMT.hs b/src/EVM/SMT.hs index 093dc2346..d7eb798e0 100644 --- a/src/EVM/SMT.hs +++ b/src/EVM/SMT.hs @@ -218,7 +218,7 @@ assertPropsNoSimp psPreConc = do pure $ prelude <> (declareAbstractStores abstractStores) <> smt2Line "" - <> (declareAddrs addresses) + <> declareConstrainAddrs addresses <> smt2Line "" <> (declareBufs toDeclarePsElim bufs stores) <> smt2Line "" @@ -265,7 +265,7 @@ assertPropsNoSimp psPreConc = do storeVals = Map.elems stores storageReads = Map.unionsWith (<>) $ fmap findStorageReads toDeclarePs abstractStores = Set.toList $ Set.unions (fmap referencedAbstractStores toDeclarePs) - addresses = Set.toList $ Set.unions (fmap referencedWAddrs toDeclarePs) + addresses = Set.toList $ Set.unions (fmap referencedAddrs toDeclarePs) -- Keccak assertions: concrete values, distance between pairs, injectivity, etc. -- This will make sure concrete values of Keccak are asserted, if they can be computed (i.e. can be concretized) @@ -291,11 +291,11 @@ referencedAbstractStores term = foldTerm go mempty term AbstractStore s idx -> Set.singleton (storeName s idx) _ -> mempty -referencedWAddrs :: TraversableTerm a => a -> Set Builder -referencedWAddrs term = foldTerm go mempty term +referencedAddrs :: TraversableTerm a => a -> Set Builder +referencedAddrs term = foldTerm go mempty term where go = \case - WAddr(a@(SymAddr _)) -> Set.singleton (formatEAddr a) + SymAddr a -> Set.singleton (formatEAddr (SymAddr a)) _ -> mempty referencedBufs :: TraversableTerm a => a -> [Builder] @@ -432,8 +432,8 @@ declareVars names = SMT2 (["; variables"] <> fmap declare names) cexvars mempty cexvars = (mempty :: CexVars){ calldata = fmap toLazyText names } -- Given a list of variable names, create an SMT2 object with the variables declared -declareAddrs :: [Builder] -> SMT2 -declareAddrs names = SMT2 (["; symbolic addresseses"] <> fmap declare names <> fmap assume names) mempty cexvars +declareConstrainAddrs :: [Builder] -> SMT2 +declareConstrainAddrs names = SMT2 (["; concretea and symbolic addresseses"] <> fmap declare names <> fmap assume names) cexvars mempty where declare n = "(declare-fun " <> n <> " () Addr)" -- assume that symbolic addresses do not collide with the zero address or precompiles @@ -852,6 +852,7 @@ exprToSMT = \case encPrev <- exprToSMT prev pure $ "(store" `sp` encPrev `sp` encIdx `sp` encVal <> ")" SLoad idx store -> op2 "select" store idx + LitAddr n -> pure $ fromLazyText $ "(_ bv" <> T.pack (show (into n :: Integer)) <> " 160)" a -> internalError $ "TODO: implement: " <> show a where diff --git a/src/EVM/SymExec.hs b/src/EVM/SymExec.hs index 76759613d..b94f275e5 100644 --- a/src/EVM/SymExec.hs +++ b/src/EVM/SymExec.hs @@ -499,18 +499,12 @@ runExpr :: Stepper.Stepper Symbolic RealWorld (Expr End) runExpr = do vm <- Stepper.runFully let traces = TraceContext (Zipper.toForest vm.traces) vm.env.contracts vm.labels - let constraints = vm.constraints <> consistentStorageKeys vm.env.contracts pure $ case vm.result of - Just (VMSuccess buf) -> Success constraints traces buf (fmap toEContract vm.env.contracts) - Just (VMFailure e) -> Failure constraints traces e - Just (Unfinished p) -> Partial constraints traces p + Just (VMSuccess buf) -> Success vm.constraints traces buf (fmap toEContract vm.env.contracts) + Just (VMFailure e) -> Failure vm.constraints traces e + Just (Unfinished p) -> Partial vm.constraints traces p _ -> internalError "vm in intermediate state after call to runFully" --- build constraints that ensure that symbolic storage keys cannot alias other storage keys - -- let asserts = vm.constraints <> consistentStorageKeys vm.env.contracts -consistentStorageKeys :: Map (Expr EAddr) Contract -> [Prop] -consistentStorageKeys (Map.keys -> addrs) = [a ./= b | a <- addrs, b <- filter Expr.isSymAddr addrs] - toEContract :: Contract -> Expr EContract toEContract c = C c.code c.storage c.tStorage c.balance c.nonce diff --git a/test/test.hs b/test/test.hs index 2c3091309..eea8a6052 100644 --- a/test/test.hs +++ b/test/test.hs @@ -1759,14 +1759,29 @@ tests = testGroup "hevm" Just c <- solcRuntime "C" src res <- reachableUserAsserts c Nothing assertBoolM "unexpected cex" (isRight res) - , testCase "deployed-contract-addresses-cannot-alias" $ do + , test "deployed-contract-addresses-cannot-alias1" $ do Just c <- solcRuntime "C" [i| contract A {} contract C { function f() external { A a = new A(); - if (address(a) == address(this)) assert(false); + uint256 addr = uint256(uint160(address(a))); + uint256 addr2 = uint256(uint160(address(this))); + assert(addr != addr2); + } + } + |] + res <- reachableUserAsserts c Nothing + assertBoolM "should not be able to alias" (isRight res) + , test "deployed-contract-addresses-cannot-alias2" $ do + Just c <- solcRuntime "C" + [i| + contract A {} + contract C { + function f() external { + A a = new A(); + assert(address(a) != address(this)); } } |] @@ -1974,7 +1989,7 @@ tests = testGroup "hevm" codes <- mapM mkC addrs results <- mapM (flip reachableUserAsserts (Just (Sig "f()" []))) codes let ok = and $ fmap (isRight) results - assertBool "unexpected cex" ok + assertBoolM "unexpected cex" ok , test "addresses-in-context-are-symbolic" $ do Just a <- solcRuntime "A" [i| @@ -2013,10 +2028,11 @@ tests = testGroup "hevm" assertEqualM "wrong number of addresses" 1 (length (Map.keys cex.addrs)) pure cex - assertEqualM "wrong model for a" (Addr 0) (fromJust $ Map.lookup (SymAddr "caller") acex.addrs) - assertEqualM "wrong model for b" (Addr 1) (fromJust $ Map.lookup (SymAddr "coinbase") bcex.addrs) - assertEqualM "wrong model for c" (Addr 2) (fromJust $ Map.lookup (SymAddr "origin") ccex.addrs) - assertEqualM "wrong model for d" (Addr 3) (fromJust $ Map.lookup (SymAddr "entrypoint") dcex.addrs) + -- Lowest allowed address is 0x10 due to reserved addresses up to 0x9 + assertEqualM "wrong model for a" (Addr 0x10) (fromJust $ Map.lookup (SymAddr "caller") acex.addrs) + assertEqualM "wrong model for b" (Addr 0x11) (fromJust $ Map.lookup (SymAddr "coinbase") bcex.addrs) + assertEqualM "wrong model for c" (Addr 0x12) (fromJust $ Map.lookup (SymAddr "origin") ccex.addrs) + assertEqualM "wrong model for d" (Addr 0x13) (fromJust $ Map.lookup (SymAddr "entrypoint") dcex.addrs) ] , testGroup "Symbolic execution" [ From 52e7187fa39e988855788a51951616c2f31fe5ac Mon Sep 17 00:00:00 2001 From: "Mate Soos @ Ethereum Foundation" <99662964+msooseth@users.noreply.github.com> Date: Mon, 3 Feb 2025 12:17:34 +0100 Subject: [PATCH 5/5] Update src/EVM/SMT.hs Co-authored-by: Martin Blicha --- src/EVM/SMT.hs | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/EVM/SMT.hs b/src/EVM/SMT.hs index e22319e7c..5f46cd789 100644 --- a/src/EVM/SMT.hs +++ b/src/EVM/SMT.hs @@ -436,7 +436,7 @@ declareVars names = SMT2 (["; variables"] <> fmap declare names) cexvars mempty -- Given a list of variable names, create an SMT2 object with the variables declared declareConstrainAddrs :: [Builder] -> SMT2 -declareConstrainAddrs names = SMT2 (["; concretea and symbolic addresseses"] <> fmap declare names <> fmap assume names) cexvars mempty +declareConstrainAddrs names = SMT2 (["; concrete and symbolic addresses"] <> fmap declare names <> fmap assume names) cexvars mempty where declare n = "(declare-fun " <> n <> " () Addr)" -- assume that symbolic addresses do not collide with the zero address or precompiles