diff --git a/CHANGELOG.md b/CHANGELOG.md index 06cc26dc7..6c331e9dc 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -46,6 +46,7 @@ and this project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0 - Better and more pretty debug messages ## Fixed +- `vm.prank` is now respected during calls to create - `concat` is a 2-ary, not an n-ary function in SMT2LIB, declare-const does not exist in QF_AUFBV, replacing with declare-fun - CVC5 needs `--incremental` flag to work properly in abstraction-refinement mode diff --git a/src/EVM.hs b/src/EVM.hs index 11d7bc6ab..d0549501d 100644 --- a/src/EVM.hs +++ b/src/EVM.hs @@ -852,13 +852,20 @@ exec1 = do xValue:xOffset:xSize:xs -> accessMemoryRange xOffset xSize $ do availableGas <- use (#state % #gas) - let - (cost, gas') = costOfCreate fees availableGas xSize False - newAddr <- createAddress self this.nonce + let (cost, gas') = costOfCreate fees availableGas xSize False + + -- handle `prank` + let from' = fromMaybe self vm.state.overrideCaller + resetCaller <- use (#state % #resetCaller) + when resetCaller $ do + assign (#state % #overrideCaller) Nothing + assign (#state % #resetCaller) False + + newAddr <- createAddress from' this.nonce _ <- accessAccountForGas newAddr burn' cost $ do initCode <- readMemory xOffset xSize - create self this xSize gas' xValue xs newAddr initCode + create from' this xSize gas' xValue xs newAddr initCode _ -> underrun OpCall -> @@ -958,12 +965,18 @@ exec1 = do buf <- readMemory xOffset xSize forceConcreteBuf buf "CREATE2" $ \initCode -> do - let - (cost, gas') = costOfCreate fees availableGas xSize True + -- handle `prank` + let from' = fromMaybe self vm.state.overrideCaller + resetCaller <- use (#state % #resetCaller) + when resetCaller $ do + assign (#state % #overrideCaller) Nothing + assign (#state % #resetCaller) False + + let (cost, gas') = costOfCreate fees availableGas xSize True newAddr <- create2Address self xSalt initCode _ <- accessAccountForGas newAddr burn' cost $ - create self this xSize gas' xValue xs newAddr (ConcreteBuf initCode) + create from' this xSize gas' xValue xs newAddr (ConcreteBuf initCode) _ -> underrun OpStaticcall -> diff --git a/src/EVM/Format.hs b/src/EVM/Format.hs index 67b55093d..7c8a26efc 100644 --- a/src/EVM/Format.hs +++ b/src/EVM/Format.hs @@ -173,9 +173,11 @@ formatBinary = (<>) "0x" . T.decodeUtf8 . toStrict . toLazyByteString . byteStringHex formatSBinary :: Expr Buf -> Text -formatSBinary (ConcreteBuf bs) = formatBinary bs -formatSBinary (AbstractBuf t) = "<" <> t <> " abstract buf>" -formatSBinary _ = internalError "formatSBinary: implement me" +formatSBinary e = format $ Expr.concKeccakSimpExpr e + where + format (ConcreteBuf bs) = formatBinary bs + format (AbstractBuf t) = "<" <> t <> " abstract buf>" + format e2 = T.pack $ "Symbolic expression: " <> show e2 showTraceTree :: DappInfo -> VM t s -> Text showTraceTree dapp vm = diff --git a/src/EVM/UnitTest.hs b/src/EVM/UnitTest.hs index 707c15ade..3a9b87c29 100644 --- a/src/EVM/UnitTest.hs +++ b/src/EVM/UnitTest.hs @@ -143,7 +143,6 @@ initializeUnitTest opts theContract = do -- call setUp(), if it exists, to initialize the test contract let theAbi = theContract.abiMap setUp = abiKeccak (encodeUtf8 "setUp()") - when (isJust (Map.lookup setUp theAbi)) $ do abiCall opts.testParams (Left ("setUp()", emptyAbi)) popTrace diff --git a/test/EVM/Test/Utils.hs b/test/EVM/Test/Utils.hs index f23f701a8..7bc35ee62 100644 --- a/test/EVM/Test/Utils.hs +++ b/test/EVM/Test/Utils.hs @@ -30,7 +30,10 @@ runSolidityTestCustom runSolidityTestCustom testFile match timeout maxIter ffiAllowed rpcinfo projectType = do withSystemTempDirectory "dapp-test" $ \root -> do (compile projectType root testFile) >>= \case - Left e -> error e + Left e -> liftIO $ do + putStrLn e + internalError $ "Error compiling test file " <> show testFile <> " in directory " + <> show root <> " using project type " <> show projectType Right bo@(BuildOutput contracts _) -> do withSolvers Z3 1 1 timeout $ \solvers -> do opts <- liftIO $ testOpts solvers root (Just bo) match maxIter ffiAllowed rpcinfo diff --git a/test/contracts/fail/10_BadVault.sol b/test/contracts/fail/10_BadVault.sol index e1f570125..79da2bab0 100644 --- a/test/contracts/fail/10_BadVault.sol +++ b/test/contracts/fail/10_BadVault.sol @@ -5,7 +5,6 @@ pragma solidity ^0.8.15; import "forge-std/Test.sol"; import {console2} from "forge-std/console2.sol"; -// import {console2} from "ds-test/console2.sol"; // inspired by the classic reentrancy level in Ethernaut CTF contract BadVault { @@ -37,7 +36,8 @@ contract BadVault { struct Call3Value { address target; uint256 value; - bytes data; + bytes32 sig; + bytes32 data; } contract ExploitLaunchPad { @@ -58,7 +58,7 @@ contract ExploitLaunchPad { require(call.value <= address(this).balance, "insufficient balance"); reentered = true; - (bool success,) = call.target.call{value: call.value}(call.data); + (bool success,) = call.target.call{value: call.value}(abi.encodePacked(call.sig, call.data)); reentered = false; } @@ -74,7 +74,7 @@ contract ExploitLaunchPad { require(msg.sender == owner, "only owner"); require(_call.value <= address(this).balance, "insufficient balance"); - (bool success,) = _call.target.call{value: _call.value}(_call.data); + (bool success,) = _call.target.call{value: _call.value}(abi.encodePacked(_call.sig, _call.data)); } function deposit() external payable {} @@ -111,21 +111,27 @@ contract BadVaultTest is Test { exploit = new ExploitLaunchPad(); assert(exploit.owner() == attacker); + console2.log("HI"); + console2.log(exploit.owner()); + console2.log(attacker); } /// @custom:halmos --array-lengths data1=36,data2=36,deferredData=36 function prove_BadVault_usingExploitLaunchPad( address target1, uint256 amount1, - bytes memory data1, + bytes32 sig1, + bytes32 data1, address target2, uint256 amount2, - bytes memory data2, + bytes32 sig2, + bytes32 data2, address deferredTarget, uint256 deferredAmount, - bytes memory deferredData + bytes32 deferredSig, + bytes32 deferredData ) public { uint256 STARTING_BALANCE = 2 ether; @@ -140,22 +146,25 @@ contract BadVaultTest is Test { vm.prank(attacker); exploit.go(Call3Value({ - target: target1, + target: address(vault), value: amount1, + sig: sig1, data: data1 })); vm.prank(attacker); exploit.defer(Call3Value({ - target: deferredTarget, + target: address(vault), value: deferredAmount, + sig: deferredSig, data: deferredData })); vm.prank(attacker); exploit.go(Call3Value({ - target: target2, + target: address(vault), value: amount2, + sig: sig2, data: data2 })); @@ -167,7 +176,8 @@ contract BadVaultTest is Test { assert(attacker.balance <= STARTING_BALANCE); } - // running `forge test --match-test test_BadVault_solution -vvv` confirms the attack trace: took 6s Node system at 18:00:43 + // running `forge test --match-test test_BadVault_solution -vvv` confirms the attack trace: + //took 6s Node system at 18:00:43 // deposit 0x0000000000000000000000000000000000000001 1000000000000000000 // deposit 0x0000000000000000000000000000000000000002 1000000000000000000 // attacker starting balance 2000000000000000000 @@ -175,30 +185,30 @@ contract BadVaultTest is Test { // withdraw 0x5f4E4CcFF0A2553b2BDE30e1fC8531B287db9087 1000000000000000000 // withdraw 0x5f4E4CcFF0A2553b2BDE30e1fC8531B287db9087 1000000000000000000 // attacker final balance 3000000000000000000 - function test_BadVault_solution() public { - prove_BadVault_usingExploitLaunchPad( - // 1st call - address(vault), - 1 ether, - abi.encodeWithSelector( - vault.deposit.selector - ), - - // 2nd call - address(vault), - 0 ether, - abi.encodeWithSelector( - vault.withdraw.selector, - 1 ether - ), - - // deferred call - address(vault), - 0 ether, - abi.encodeWithSelector( - vault.withdraw.selector, - 1 ether - ) - ); - } + // function test_BadVault_solution() public { + // prove_BadVault_usingExploitLaunchPad( + // // 1st call + // address(vault), + // 1 ether, + // abi.encodeWithSelector( + // vault.deposit.selector + // ), + + // // 2nd call + // address(vault), + // 0 ether, + // abi.encodeWithSelector( + // vault.withdraw.selector, + // 1 ether + // ), + + // // deferred call + // address(vault), + // 0 ether, + // abi.encodeWithSelector( + // vault.withdraw.selector, + // 1 ether + // ) + // ); + // } } diff --git a/test/test.hs b/test/test.hs index ed2c209c5..e883f9d3b 100644 --- a/test/test.hs +++ b/test/test.hs @@ -1231,7 +1231,38 @@ tests = testGroup "hevm" Right e <- reachableUserAsserts c (Just $ Sig "f(address,uint256)" [AbiAddressType, AbiUIntType 256]) assertBoolM "The expression is not partial" $ Expr.containsNode isPartial e , - test "vm.prank-underflow" $ do + test "vm.prank-create" $ do + Just c <- solcRuntime "C" + [i| + interface Vm { + function prank(address) external; + } + contract Owned { + address public owner; + constructor() { + owner = msg.sender; + } + } + contract C { + function f() external { + Vm vm = Vm(0x7109709ECfa91a80626fF3989D68f67F5b1DD12D); + + Owned target = new Owned(); + assert(target.owner() == address(this)); + + address usr = address(1312); + vm.prank(usr); + target = new Owned(); + assert(target.owner() == usr); + target = new Owned(); + assert(target.owner() == address(this)); + } + } + |] + Right _ <- reachableUserAsserts c (Just $ Sig "f()" []) + liftIO $ putStrLn "no reachable assertion violations" + , + test "vm.prank underflow" $ do Just c <- solcRuntime "C" [i| interface Vm {