diff --git a/src/EVM.hs b/src/EVM.hs index 349e0f040..53e2dc31c 100644 --- a/src/EVM.hs +++ b/src/EVM.hs @@ -1805,23 +1805,30 @@ create :: (?op :: Word8) -> W256 -> Word64 -> Expr EWord -> [Expr EWord] -> Expr EAddr -> Expr Buf -> EVM s () create self this xSize xGas xValue xs newAddr initCode = do vm0 <- get + -- are we exceeding the max init code size if xSize > 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: 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) @@ -1837,7 +1844,6 @@ create self this xSize xGas xValue xs newAddr initCode = do next touchAccount self touchAccount newAddr - -- are we overflowing the nonce False -> burn xGas $ do -- unfortunately we have to apply some (pretty hacky) -- heuristics here to parse the unstructured buffer read diff --git a/src/EVM/Expr.hs b/src/EVM/Expr.hs index 163d94c89..164c4e02c 100644 --- a/src/EVM/Expr.hs +++ b/src/EVM/Expr.hs @@ -1087,6 +1087,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/SMT.hs b/src/EVM/SMT.hs index b199031e2..b91266adb 100644 --- a/src/EVM/SMT.hs +++ b/src/EVM/SMT.hs @@ -411,9 +411,11 @@ declareVars names = SMT2 (["; variables"] <> fmap declare names) mempty cexvars -- 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) mempty cexvars +declareAddrs names = SMT2 (["; symbolic addresseses"] <> fmap declare names <> fmap assume names) mempty cexvars where declare n = "(declare-const " <> 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])] -> SMT2 diff --git a/src/EVM/SymExec.hs b/src/EVM/SymExec.hs index 5a02a45d9..2c560e38f 100644 --- a/src/EVM/SymExec.hs +++ b/src/EVM/SymExec.hs @@ -454,7 +454,7 @@ verifyContract solvers theCode signature' concreteArgs opts maybepre maybepost = runExpr :: Stepper.Stepper RealWorld (Expr End) runExpr = do vm <- Stepper.runFully - let asserts = vm.keccakEqs <> vm.constraints + let asserts = vm.keccakEqs <> vm.constraints <> consistentStorageKeys vm.env.contracts traces = Traces (Zipper.toForest vm.traces) vm.env.contracts pure $ case vm.result of Just (VMSuccess buf) -> Success asserts traces buf (fmap toEContract vm.env.contracts) @@ -462,6 +462,10 @@ runExpr = do Just (Unfinished p) -> Partial asserts traces p _ -> internalError "vm in intermediate state after call to runFully" +-- build constraints that ensure that symbolic storage keys cannot alias other storage keys +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.balance c.nonce diff --git a/test/test.hs b/test/test.hs index e6c2cd279..f64c24b5b 100644 --- a/test/test.hs +++ b/test/test.hs @@ -1101,8 +1101,7 @@ tests = testGroup "hevm" Just c <- solcRuntime "C" src res <- reachableUserAsserts c Nothing assertBool "unexpected cex" (isRight res) - -- TODO: implement missing aliasing rules - , expectFail $ testCase "deployed-contract-addresses-cannot-alias" $ do + , testCase "deployed-contract-addresses-cannot-alias" $ do Just c <- solcRuntime "C" [i| contract A {} @@ -1298,12 +1297,26 @@ tests = testGroup "hevm" Right e <- reachableUserAsserts c Nothing -- TODO: this should work one day assertBool "should be partial" (Expr.containsNode isPartial e) + , testCase "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 , testCase "addresses-in-context-are-symbolic" $ do Just a <- solcRuntime "A" [i| contract A { function f() external { - assert(msg.sender != address(0x0)); + assert(msg.sender != address(0x10)); } } |] @@ -1311,7 +1324,7 @@ tests = testGroup "hevm" [i| contract B { function f() external { - assert(block.coinbase != address(0x1)); + assert(block.coinbase != address(0x11)); } } |] @@ -1319,7 +1332,7 @@ tests = testGroup "hevm" [i| contract C { function f() external { - assert(tx.origin != address(0x2)); + assert(tx.origin != address(0x12)); } } |] @@ -1327,7 +1340,7 @@ tests = testGroup "hevm" [i| contract D { function f() external { - assert(address(this) != address(0x3)); + assert(address(this) != address(0x13)); } } |]