diff --git a/CHANGELOG.md b/CHANGELOG.md index 644984ee1..13c927437 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -6,6 +6,9 @@ The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/), and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.html). ## Added +- When a staticcall is made to a contract that does not exist, we overapproximate + and return symbolic values +- More simplification rules for Props - JoinBytes simplification rule - New simplification rule to help deal with abi.encodeWithSelector - More simplification rules for Props diff --git a/src/EVM.hs b/src/EVM.hs index e5a3033f8..d53a7b754 100644 --- a/src/EVM.hs +++ b/src/EVM.hs @@ -165,6 +165,7 @@ makeVm o = do , currentFork = 0 , labels = mempty , osEnv = mempty + , freshVar = 0 } where env = Env @@ -287,6 +288,17 @@ getOpW8 state = case state.code of getOpName :: forall (t :: VMType) s . FrameState t s -> [Char] getOpName state = intToOpName $ fromEnum $ getOpW8 state +-- If the address is already in the cache, or can be obtained via API, return True +-- otherwise, return False +canFetchAccount :: forall (t :: VMType) s . VMOps t => Expr EAddr -> EVM t s (Bool) +canFetchAccount addr = do + use (#env % #contracts % at addr) >>= \case + Just _ -> pure True + Nothing -> case addr of + LitAddr _ -> pure True + SymAddr _ -> pure False + GVar _ -> internalError "GVar not allowed here" + -- | Executes the EVM one step exec1 :: forall (t :: VMType) s. VMOps t => EVM t s () exec1 = do @@ -982,26 +994,38 @@ exec1 = do case stk of xGas:xTo:xInOffset:xInSize:xOutOffset:xOutSize:xs -> case wordToAddr xTo of - Nothing -> do - loc <- codeloc - let msg = "Unable to determine a call target" - partial $ UnexpectedSymbolicArg (snd loc) opName msg [SomeExpr xTo] - Just xTo' -> + Nothing -> fallback + Just xTo' -> do case gasTryFrom xGas of Left _ -> vmError IllegalOverflow - Right gas -> do - overrideC <- use $ #state % #overrideCaller - delegateCall this gas xTo' xTo' (Lit 0) xInOffset xInSize xOutOffset xOutSize xs $ - \callee -> do - zoom #state $ do - assign #callvalue (Lit 0) - assign #caller $ fromMaybe self overrideC - assign #contract callee - assign #static True - touchAccount self - touchAccount callee + Right gas -> canFetchAccount xTo' >>= \case + False -> fallback + True -> do + overrideC <- use $ #state % #overrideCaller + delegateCall this gas xTo' xTo' (Lit 0) xInOffset xInSize xOutOffset xOutSize xs $ + \callee -> do + zoom #state $ do + assign #callvalue (Lit 0) + assign #caller $ fromMaybe self overrideC + assign #contract callee + assign #static True + touchAccount self + touchAccount callee _ -> underrun + where + fallback = do + -- Reset caller if needed + resetCaller <- use $ #state % #resetCaller + when resetCaller $ assign (#state % #overrideCaller) Nothing + -- overapproximate by returning a symbolic value + freshVar <- use #freshVar + assign #freshVar (freshVar + 1) + let freshVarExpr = Var ("staticcall-result-stack-" <> (pack . show) freshVar) + pushSym freshVarExpr + modifying #constraints ((:) (PLEq freshVarExpr (Lit 1) )) + assign (#state % #returndata) (AbstractBuf ("staticall-result-data-" <> (pack . show) freshVar)) + next OpSelfdestruct -> notStatic $ diff --git a/src/EVM/Types.hs b/src/EVM/Types.hs index bd12c0fbc..13aac47f3 100644 --- a/src/EVM/Types.hs +++ b/src/EVM/Types.hs @@ -670,6 +670,9 @@ data VM (t :: VMType) s = VM , currentFork :: Int , labels :: Map Addr Text , osEnv :: Map String String + , freshVar :: Int + -- ^ used to generate fresh symbolic variable names for overapproximations + -- during symbolic execution. See e.g. OpStaticcall } deriving (Generic) diff --git a/test/test.hs b/test/test.hs index 6a9e618a8..3b1c60c6f 100644 --- a/test/test.hs +++ b/test/test.hs @@ -2060,10 +2060,197 @@ tests = testGroup "hevm" } } |] - let sig = Just (Sig "checkval(uint256,uint256)" [AbiUIntType 256, AbiUIntType 256]) + let sig = Just (Sig "checkval(uint8)" [AbiUIntType 8]) (res, [Qed _]) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c sig [] defaultVeriOpts putStrLnM $ "successfully explored: " <> show (Expr.numBranches res) <> " paths" + , test "staticcall-check-orig" $ do + Just c <- solcRuntime "C" + [i| + contract Target { + function add(uint256 x, uint256 y) external pure returns (uint256) { + unchecked { + return x + y; + } + } + } + + contract C { + function checkval(uint256 x, uint256 y) public { + Target t = new Target(); + address realAddr = address(t); + bytes memory data = abi.encodeWithSignature("add(uint256,uint256)", x, y); + (bool success, bytes memory returnData) = realAddr.staticcall(data); + assert(success); + + uint result = abi.decode(returnData, (uint256)); + uint expected; + unchecked { + expected = x + y; + } + assert(result == expected); + } + } + |] + let sig = Just (Sig "checkval(uint256,uint256)" [AbiAddressType, AbiUIntType 256, AbiUIntType 256]) + (res, ret) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c sig [] defaultVeriOpts + putStrLnM $ "successfully explored: " <> show (Expr.numBranches res) <> " paths" + let numCexes = sum $ map (fromEnum . isCex) ret + let numErrs = sum $ map (fromEnum . isError) ret + let numQeds = sum $ map (fromEnum . isQed) ret + assertEqualM "number of counterexamples" 0 numCexes + assertEqualM "number of errors" 0 numErrs + assertEqualM "number of qed-s" 1 numQeds + , test "staticcall-check-orig2" $ do + Just c <- solcRuntime "C" + [i| + contract Target { + function add(uint256 x, uint256 y) external pure returns (uint256) { + assert(1 == 0); + } + } + contract C { + function checkval(uint256 x, uint256 y) public { + Target t = new Target(); + address realAddr = address(t); + bytes memory data = abi.encodeWithSignature("add(uint256,uint256)", x, y); + (bool success, bytes memory returnData) = realAddr.staticcall(data); + assert(success); + } + } + |] + let sig = Just (Sig "checkval(uint256,uint256)" [AbiAddressType, AbiUIntType 256, AbiUIntType 256]) + (res, ret) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c sig [] defaultVeriOpts + putStrLnM $ "successfully explored: " <> show (Expr.numBranches res) <> " paths" + -- let cexesExt = map (snd . fromJust . extractCex) ret + -- putStrLnM $ "Cexes: \n" <> (unlines $ map ("-> " ++) (map show cexesExt)) + let numCexes = sum $ map (fromEnum . isCex) ret + let numErrs = sum $ map (fromEnum . isError) ret + let numQeds = sum $ map (fromEnum . isQed) ret + assertEqualM "number of counterexamples" 1 numCexes + assertEqualM "number of errors" 0 numErrs + assertEqualM "number of qed-s" 0 numQeds + , test "staticcall-check-symbolic1" $ do + Just c <- solcRuntime "C" + [i| + contract C { + function checkval(address inputAddr, uint256 x, uint256 y) public { + bytes memory data = abi.encodeWithSignature("add(uint256,uint256)", x, y); + (bool success, bytes memory returnData) = inputAddr.staticcall(data); + assert(success); + } + } + |] + let sig = Just (Sig "checkval(address,uint256,uint256)" [AbiAddressType, AbiUIntType 256, AbiUIntType 256]) + (res, ret) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c sig [] defaultVeriOpts + putStrLnM $ "successfully explored: " <> show (Expr.numBranches res) <> " paths" + let numCexes = sum $ map (fromEnum . isCex) ret + let numErrs = sum $ map (fromEnum . isError) ret + let numQeds = sum $ map (fromEnum . isQed) ret + -- There are 2 CEX-es, in contrast to the above (staticcall-check-orig2). + -- This is because with one CEX, the return DATA + -- is empty, and in the other, the return data is non-empty (but symbolic) + assertEqualM "number of counterexamples" 2 numCexes + assertEqualM "number of errors" 0 numErrs + assertEqualM "number of qed-s" 0 numQeds + -- This checks that calling a symbolic address with staticcall will ALWAYS return 0/1 + -- which is the semantic of the EVM. We insert a constraint over the return value + -- even when overapproximation is used, as below. + , test "staticcall-check-symbolic-yul" $ do + Just c <- solcRuntime "C" + [i| + contract C { + function checkval(address inputAddr, uint256 x, uint256 y) public { + uint success; + assembly { + // Allocate memory for the call data + let callData := mload(0x40) + + // Function signature for "add(uint256,uint256)" is "0x771602f7" + mstore(callData, 0x771602f700000000000000000000000000000000000000000000000000000000) + + // Store the parameters x and y + mstore(add(callData, 4), x) + mstore(add(callData, 36), y) + + // Perform the static call + success := staticcall( + gas(), // Forward all available gas + inputAddr, // Address to call + callData, // Input data location + 68, // Input data size (4 bytes for function signature + 32 bytes each for x and y) + 0, // Output data location (0 means we don't care about the output) + 0 // Output data size + ) + } + assert(success <= 1); + } + } + |] + let sig = Just (Sig "checkval(address,uint256,uint256)" [AbiAddressType, AbiUIntType 256, AbiUIntType 256]) + (res, ret) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c sig [] defaultVeriOpts + putStrLnM $ "successfully explored: " <> show (Expr.numBranches res) <> " paths" + let numCexes = sum $ map (fromEnum . isCex) ret + let numErrs = sum $ map (fromEnum . isError) ret + let numQeds = sum $ map (fromEnum . isQed) ret + assertEqualM "number of counterexamples" 0 numCexes -- no counterexamples, because it is always 0/1 + assertEqualM "number of errors" 0 numErrs + assertEqualM "number of qed-s" 1 numQeds + , test "staticcall-check-symbolic2" $ do + Just c <- solcRuntime "C" + [i| + contract C { + function checkval(address inputAddr, uint256 x, uint256 y) public { + bytes memory data = abi.encodeWithSignature("add(uint256,uint256)", x, y); + (bool success, bytes memory returnData) = inputAddr.staticcall(data); + assert(success); + + uint result = abi.decode(returnData, (uint256)); + uint expected; + unchecked { + expected = x + y; + } + assert(result == expected); + } + } + |] + let sig = Just (Sig "checkval(address,uint256,uint256)" [AbiAddressType, AbiUIntType 256, AbiUIntType 256]) + (res, ret) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c sig [] defaultVeriOpts + putStrLnM $ "successfully explored: " <> show (Expr.numBranches res) <> " paths" + let numCexes = sum $ map (fromEnum . isCex) ret + let numErrs = sum $ map (fromEnum . isError) ret + let numQeds = sum $ map (fromEnum . isQed) ret + assertEqualM "number of counterexamples" 2 numCexes + assertEqualM "number of errors" 1 numErrs + assertEqualM "number of qed-s" 0 numQeds + , test "jump-symbolic" $ do + Just c <- solcRuntime "C" + [i| + // Target contract with a view function + contract Target { + } + + // Caller contract using staticcall + contract C { + function checkval(address inputAddr, uint256 x, uint256 y) public { + Target t = new Target(); + address realAddr = address(t); + + bytes memory data = abi.encodeWithSignature("add(uint256,uint256)", x, y); + (bool success, bytes memory returnData) = inputAddr.staticcall(data); + assert(success == true); + } + } + |] + let sig = Just (Sig "checkval(address,uint256,uint256)" [AbiAddressType, AbiUIntType 256, AbiUIntType 256]) + (res, ret) <- withDefaultSolver $ \s -> checkAssert s defaultPanicCodes c sig [] defaultVeriOpts + putStrLnM $ "successfully explored: " <> show (Expr.numBranches res) <> " paths" + let numCexes = sum $ map (fromEnum . isCex) ret + let numErrs = sum $ map (fromEnum . isError) ret + let numQeds = sum $ map (fromEnum . isQed) ret + assertEqualM "number of counterexamples" numCexes 2 + assertEqualM "number of symbolic copy errors" numErrs 0 + assertEqualM "number of qed-s" numQeds 0 , test "opcode-mul-assoc" $ do Just c <- solcRuntime "MyContract"