Fixing badvault

ethereum · Dec 3, 2024 · d75d135 · d75d135
1 parent 9dc852c
commit d75d135
Show file tree

Hide file tree

Showing 4 changed files with 16 additions and 13 deletions.
diff --git 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
@@ -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
@@ -30,7 +30,9 @@ 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"
       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
@@ -36,7 +36,7 @@ contract BadVault {
 struct Call3Value {
     address target;
     uint256 value;
-    bytes4 sig;
+    bytes32 sig;
     bytes32 data;
 }
 
@@ -117,20 +117,20 @@ contract BadVaultTest is Test {
     }
 
     /// @custom:halmos --array-lengths data1=36,data2=36,deferredData=36
-    function test_prove_BadVault_usingExploitLaunchPad(
+    function prove_BadVault_usingExploitLaunchPad(
         address target1,
         uint256 amount1,
-        bytes4 sig1,
+        bytes32 sig1,
         bytes32 data1,
 
         address target2,
         uint256 amount2,
-        bytes4 sig2,
+        bytes32 sig2,
         bytes32 data2,
 
         address deferredTarget,
         uint256 deferredAmount,
-        bytes4 deferredSig,
+        bytes32 deferredSig,
         bytes32 deferredData
 
     ) public {
@@ -146,23 +146,23 @@ 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