Merge pull request #641 from ethereum/upd-more-precise-smt-address-encoding

Update more precise smt address encoding PR

Author: msooseth

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
 - Constant propagation for symbolic values
 
 ## Fixed

src/EVM.hs

@@ -1514,13 +1514,24 @@ 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
   let
     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
@@ -2141,23 +2152,30 @@ 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: 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)

src/EVM/Expr.hs

@@ -1393,6 +1393,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:

src/EVM/SMT.hs

@@ -219,7 +219,7 @@ assertPropsNoSimp psPreConc = do
  pure $ prelude
   <> (declareAbstractStores abstractStores)
   <> smt2Line ""
-  <> (declareAddrs addresses)
+  <> declareConstrainAddrs addresses
   <> smt2Line ""
   <> (declareBufs toDeclarePsElim bufs stores)
   <> smt2Line ""
@@ -268,7 +268,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)
@@ -294,11 +294,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]
@@ -435,10 +435,12 @@ 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) cexvars mempty
+declareConstrainAddrs :: [Builder] -> SMT2
+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
+    assume n = "(assert (bvugt " <> n <> " (_ bv9 160)))"
     cexvars = (mempty :: CexVars){ addrs = fmap toLazyText names }
 
 enforceGasOrder :: [Prop] -> SMT2
@@ -869,6 +871,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)"
   Gas freshVar -> pure $ fromLazyText $ "gas_"  <> (T.pack $ show freshVar)
 
   a -> internalError $ "TODO: implement: " <> show a

src/EVM/SymExec.hs

@@ -501,8 +501,8 @@ runExpr = do
   let traces = TraceContext (Zipper.toForest vm.traces) vm.env.contracts vm.labels
   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 (VMFailure e)   -> Failure vm.constraints traces e
+    Just (Unfinished p)  -> Partial vm.constraints traces p
     _ -> internalError "vm in intermediate state after call to runFully"
 
 toEContract :: Contract -> Expr EContract
@@ -963,7 +963,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
 

test/test.hs

@@ -1809,15 +1809,29 @@ 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
+    , 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));
               }
             }
           |]
@@ -2012,36 +2026,50 @@ 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
+        assertBoolM "unexpected cex" ok
     , test "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));
               }
             }
           |]
         Just b <- solcRuntime "B"
           [i|
             contract B {
               function f() external {
-                assert(block.coinbase != address(0x1));
+                assert(block.coinbase != address(0x11));
               }
             }
           |]
         Just c <- solcRuntime "C"
           [i|
             contract C {
               function f() external {
-                assert(tx.origin != address(0x2));
+                assert(tx.origin != address(0x12));
               }
             }
           |]
         Just d <- solcRuntime "D"
           [i|
             contract D {
               function f() external {
-                assert(address(this) != address(0x3));
+                assert(address(this) != address(0x13));
               }
             }
           |]
@@ -2050,10 +2078,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"
       [