From 10525566a4b08a14ca728c6bc18b34517bda4a40 Mon Sep 17 00:00:00 2001
From: dxo <hi@d-xo.org>
Date: Mon, 11 Sep 2023 17:23:28 +0200
Subject: [PATCH 1/3] EVM: OpCreate: better comments
---
src/EVM.hs | 7 ++++++-
1 file changed, 6 insertions(+), 1 deletion(-)
diff --git a/src/EVM.hs b/src/EVM.hs
index 349e0f040..227ff1423 100644
--- a/src/EVM.hs
+++ b/src/EVM.hs
@@ -1805,23 +1805,29 @@ 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: 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)
@@ -1837,7 +1843,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
From 34364f7c12ea90d0c89785a5a98d0abb93f056fc Mon Sep 17 00:00:00 2001
From: dxo <hi@d-xo.org>
Date: Mon, 11 Sep 2023 17:23:54 +0200
Subject: [PATCH 2/3] 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 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/test/test.hs b/test/test.hs
index e6c2cd279..e62f2deac 100644
--- a/test/test.hs
+++ b/test/test.hs
@@ -1303,7 +1303,7 @@ tests = testGroup "hevm"
[i|
contract A {
function f() external {
- assert(msg.sender != address(0x0));
+ assert(msg.sender != address(0x10));
}
}
|]
@@ -1311,7 +1311,7 @@ tests = testGroup "hevm"
[i|
contract B {
function f() external {
- assert(block.coinbase != address(0x1));
+ assert(block.coinbase != address(0x11));
}
}
|]
@@ -1319,7 +1319,7 @@ tests = testGroup "hevm"
[i|
contract C {
function f() external {
- assert(tx.origin != address(0x2));
+ assert(tx.origin != address(0x12));
}
}
|]
@@ -1327,7 +1327,7 @@ tests = testGroup "hevm"
[i|
contract D {
function f() external {
- assert(address(this) != address(0x3));
+ assert(address(this) != address(0x13));
}
}
|]
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 3/3] 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|