Much better overapproximation, and maxBufSize limitation #658

msooseth · 2025-02-12T19:10:07Z

Description

This overapproximates and so allows us to move forward with the exploration for:

EXTCODESIZE/HASH and BALANCE always when the contract cannot be found. This is useful, because this is ONLY a check on the size of the contract. So we return a symbolic variable, and continue, potentially going into branches that may be impossible in normal circumstances.
CALL and CALLCODE, only when --promise-no-reent is given. This is a kind of a hack, where we assume that state is not changed of either us or any other contract, when a CALL is made to an unknown code. This is kinda okay when all important state-changing code is guarded by reentrancy locks.

I also refactored the STATICCALL abstraction so it is now much more straightforward, and uses the new generic abstraction system. I think it's a VERY cool now.

I have also added:

--max-buf-size so we can adjust the maximum buffer size. Default is still 2**64 but a lower one can be set, which can still be "good enough" but we won't get internalError-s for too large buffer Cex-es. The proper solution to this is halving the buffer limit and finding a new Cex, until fixedpoint. But that' s a lot of work, and this is good enough for the moment.
Improved a copyslice so it triggers more often
A bunch of test cases

Checklist

tested locally
added automated tests
updated the docs
updated the changelog

cli/cli.hs

Also improve rewrite rule

blishko

Unfortunately, I don't have any insight into these fallback mechanisms.

My superficial review says this is OK :)

blishko · 2025-02-24T09:37:53Z

cli/cli.hs

@@ -108,6 +108,8 @@ data Command w
      , loopDetectionHeuristic :: w ::: LoopHeuristic <!> "StackBased" <?> "Which heuristic should be used to determine if we are in a loop: StackBased (default) or Naive"
      , noDecompose   :: w ::: Bool               <?> "Don't decompose storage slots into separate arrays"
      , maxBranch     :: w ::: Int                <!> "100" <?> "Max number of branches to explore when encountering a symbolic value (default: 100)"
+      , promiseNoReent:: w ::: Bool               <!> "Promise no reentrancy is possible into the contrct(s) being examined"


Suggested change

, promiseNoReent:: w ::: Bool <!> "Promise no reentrancy is possible into the contrct(s) being examined"

, promiseNoReent:: w ::: Bool <!> "Promise no reentrancy is possible into the contract(s) being examined"

blishko · 2025-02-24T09:38:12Z

cli/cli.hs

@@ -131,6 +133,8 @@ data Command w
      , loopDetectionHeuristic :: w ::: LoopHeuristic <!> "StackBased" <?> "Which heuristic should be used to determine if we are in a loop: StackBased (default) or Naive"
      , noDecompose   :: w ::: Bool             <?> "Don't decompose storage slots into separate arrays"
      , maxBranch     :: w ::: Int              <!> "100" <?> "Max number of branches to explore when encountering a symbolic value (default: 100)"
+      , maxBufSize    :: w ::: Int              <!> "64" <?> "Maximum size of buffers such as calldata and returndata in exponents of 2 (default: 64, i.e. 2^64 bytes)"
+      , promiseNoReent:: w ::: Bool             <!> "Promise no reentrancy is possible into the contrct(s) being examined"


Suggested change

, promiseNoReent:: w ::: Bool <!> "Promise no reentrancy is possible into the contrct(s) being examined"

, promiseNoReent:: w ::: Bool <!> "Promise no reentrancy is possible into the contract(s) being examined"

blishko · 2025-02-24T09:39:15Z

cli/cli.hs

@@ -184,6 +188,8 @@ data Command w
      , maxBranch     :: w ::: Int                      <!> "100" <?> "Max number of branches to explore when encountering a symbolic value (default: 100)"
      , numCexFuzz    :: w ::: Integer                  <!> "3" <?> "Number of fuzzing tries to do to generate a counterexample (default: 3)"
      , askSmtIterations :: w ::: Integer               <!> "1" <?> "Number of times we may revisit a particular branching point before we consult the smt solver to check reachability (default: 1)"
+      , maxBufSize    :: w ::: Int                      <!> "64" <?> "Maximum size of buffers such as calldata and returndata in exponents of 2 (default: 64, i.e. 2^64 bytes)"
+      , promiseNoReent:: w ::: Bool                     <!> "Promise no reentrancy is possible into the contrct(s) being examined"


Suggested change

, promiseNoReent:: w ::: Bool <!> "Promise no reentrancy is possible into the contrct(s) being examined"

, promiseNoReent:: w ::: Bool <!> "Promise no reentrancy is possible into the contract(s) being examined"

Reminder to look into possibilities to avoid the duplication of command line arguments for the different modes.

blishko · 2025-02-24T09:42:49Z

src/EVM.hs

@@ -1407,16 +1391,18 @@ query q = assign #result $ Just $ HandleEffect (Query q)
 runBoth :: RunBoth s -> EVM Symbolic s ()
 runBoth c = assign #result $ Just $ HandleEffect (RunBoth c)

-- | Construct RPC Query and halt execution until resolved
-fetchAccount :: VMOps t => Expr EAddr -> (Contract -> EVM t s ()) -> EVM t s ()
+fetchAccount  :: VMOps t => Expr EAddr -> (Contract -> EVM t s ()) -> EVM t s ()


Suggested change

fetchAccount :: VMOps t => Expr EAddr -> (Contract -> EVM t s ()) -> EVM t s ()

fetchAccount :: VMOps t => Expr EAddr -> (Contract -> EVM t s ()) -> EVM t s ()

blishko · 2025-02-24T09:52:59Z

cli/cli.hs

@@ -228,6 +234,8 @@ main = withUtf8 $ do
    , dumpTrace = cmd.trace
    , decomposeStorage = Prelude.not cmd.noDecompose
    , maxBranch = cmd.maxBranch
+    , promiseNoReent = cmd.promiseNoReent
+    , maxBufSize = cmd.maxBufSize


Isn't 64 the maximum value that makes sense here?
Now user could even pass a larger value no?
Shouldn't we force reasonable value here? Maybe max(64, cmd.maxBufSize)?

blishko · 2025-02-24T10:01:28Z

test/test.hs

+      let numQeds = sum $ map (fromEnum . isQed) ret
+      assertEqualM "number of errors" 0 numErrs
+      assertEqualM "number of counterexamples" 0 numCexes
+      assertEqualM "number of qed-s" 1 numQeds


I am a bit confused here.
Because there is no promise of no reentrancy, the exploration ends with the call as partial and the assert is not visited at all?

msooseth force-pushed the symbolic-extcodesize branch 2 times, most recently from c45ddbf to ae72ba7 Compare February 13, 2025 13:10

msooseth changed the title ~~[DRAFT] Symbolic EXTCODESIZE return value when the address is symbolic~~ Symbolic EXTCODESIZE return value when the address is symbolic Feb 13, 2025

msooseth marked this pull request as ready for review February 13, 2025 13:34

msooseth changed the title ~~Symbolic EXTCODESIZE return value when the address is symbolic~~ Symbolic EXTCODESIZE & CALL return value when the address is symbolic Feb 13, 2025

blishko reviewed Feb 14, 2025

View reviewed changes

cli/cli.hs Show resolved Hide resolved

cli/cli.hs Outdated Show resolved Hide resolved

cli/cli.hs Outdated Show resolved Hide resolved

msooseth changed the title ~~Symbolic EXTCODESIZE & CALL return value when the address is symbolic~~ [DRAFT] Symbolic EXTCODESIZE & CALL return value when the address is symbolic Feb 17, 2025

This was referenced Feb 18, 2025

Make state Abstract after a CALL to unknown code -- or better yet, analyze what can change #653

Open

When doing equivalence checking, CALL to unknown code can be approximated in a different way #669

Open

msooseth force-pushed the symbolic-extcodesize branch 4 times, most recently from f494f38 to 32864e9 Compare February 20, 2025 16:40

Symbolic fallback for EXTCODESIZE and others, max buf size setting

7a1dded

Also improve rewrite rule

msooseth force-pushed the symbolic-extcodesize branch from 422af31 to 7a1dded Compare February 20, 2025 17:21

msooseth changed the title ~~[DRAFT] Symbolic EXTCODESIZE & CALL return value when the address is symbolic~~ Symbolic EXTCODESIZE & CALL return value when the address is symbolic Feb 20, 2025

msooseth changed the title ~~Symbolic EXTCODESIZE & CALL return value when the address is symbolic~~ Much better overapproximation, and maxBufSize limitation Feb 20, 2025

blishko reviewed Feb 24, 2025

View reviewed changes

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Much better overapproximation, and maxBufSize limitation #658

Much better overapproximation, and maxBufSize limitation #658

msooseth commented Feb 12, 2025 •

edited

Loading

blishko left a comment

blishko Feb 24, 2025

blishko Feb 24, 2025

blishko Feb 24, 2025

blishko Feb 24, 2025

blishko Feb 24, 2025

blishko Feb 24, 2025

	, promiseNoReent:: w ::: Bool <!> "Promise no reentrancy is possible into the contrct(s) being examined"
	, promiseNoReent:: w ::: Bool <!> "Promise no reentrancy is possible into the contract(s) being examined"

	fetchAccount :: VMOps t => Expr EAddr -> (Contract -> EVM t s ()) -> EVM t s ()
	fetchAccount :: VMOps t => Expr EAddr -> (Contract -> EVM t s ()) -> EVM t s ()

Much better overapproximation, and maxBufSize limitation #658

Are you sure you want to change the base?

Much better overapproximation, and maxBufSize limitation #658

Conversation

msooseth commented Feb 12, 2025 • edited Loading

Description

Checklist

blishko left a comment

Choose a reason for hiding this comment

blishko Feb 24, 2025

Choose a reason for hiding this comment

blishko Feb 24, 2025

Choose a reason for hiding this comment

blishko Feb 24, 2025

Choose a reason for hiding this comment

blishko Feb 24, 2025

Choose a reason for hiding this comment

blishko Feb 24, 2025

Choose a reason for hiding this comment

blishko Feb 24, 2025

Choose a reason for hiding this comment

msooseth commented Feb 12, 2025 •

edited

Loading