From 05a1c6ac018c5f40f226a3aa87b485bb06dfa32b Mon Sep 17 00:00:00 2001
From: dxo <hi@d-xo.org>
Date: Thu, 14 Sep 2023 19:03:54 +0200
Subject: [PATCH] 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 |  6 +++++-
 test/test.hs       | 17 +++++++++++++++--
 4 files changed, 27 insertions(+), 5 deletions(-)

diff --git a/src/EVM.hs b/src/EVM.hs
index 227ff1423..53e2dc31c 100644
--- a/src/EVM.hs
+++ b/src/EVM.hs
@@ -1826,8 +1826,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 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/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 e62f2deac..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,6 +1297,20 @@ 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|