Code

Audit Draft PR for Code Review#3

Code

Draft

derek-certora wants to merge 19 commits intomainCertora/safe-smart-account:mainfrom derek/audit-new-commitCertora/safe-smart-account:derek/audit-new-commitCopy head branch name to clipboard

+1,006-22

Commits

Commits on Dec 16, 2024

• apply a patch to the harness so the rule about hash collisions passes

  

  Derek Sorensen

  authored and

  Derek Sorensen

  committed
  c73b5bc

• a new specification for guards, including transaction guards and module guards; this commit ports a rule from Safe.spec so that rules on guards are in the same spec, adds some functionality to the …

  Show description for 7b7fab2
  

  Derek Sorensen

  authored and

  Derek Sorensen

  committed
  7b7fab2

• a specification for execute, executionTxn, executeTxnFromModule, etc. and all its expected functionality

  

  Derek Sorensen

  authored and

  Derek Sorensen

  committed
  4f7e6c6

• fix execTxnModulePermissions so that it checks whether the caller was an enabled module before making the successful call, and adds documentation that refers to an added function to the Safe Harness

  

  Derek Sorensen

  authored and

  Derek Sorensen

  committed
  5730c06

• clean up two rule statements from bool == true to just bool

  

  Derek Sorensen

  authored and

  Derek Sorensen

  committed
  658bdae

• duplicate new rules for execTransactionFromModule to identical rules but for execTransactionFromModuleReturnData

  

  Derek Sorensen

  authored and

  Derek Sorensen

  committed
  654d3fe

• adding a spec file for rules about the setup, which contains two rules both of which are passing

  

  Derek Sorensen

  authored and

  Derek Sorensen

  committed
  f46fd96

Commits on Dec 17, 2024

• first draft of a fallback spec, with some TODOs including resolving sanity on the invariant fallbackHanlderNeverSelf, adding the static Dummy to the spec, and strengthening from satisfy to assert

  

  Derek Sorensen

  authored and

  Derek Sorensen

  committed
  f2ed3c9

Commits on Dec 18, 2024

• remove unnecessary args in conf files

  

  Derek Sorensen

  authored and

  Derek Sorensen

  committed
  8f011da

• small style adjustment

  

  Derek Sorensen

  authored and

  Derek Sorensen

  committed
  a8561df

• combine the two setup rules into one more concise rules

  

  Derek Sorensen

  authored and

  Derek Sorensen

  committed
  c97107a

• reintroduce prover args to guards conf because moduleGuardCalledReturn and txnGuardCalled are vioalted otherwise

  

  Derek Sorensen

  authored and

  Derek Sorensen

  committed
  019aef5

• extend some rules, deprecate/remove fixes used because I couldn't resolve some CVL issues, filter the invariant fallbackHanlderNeverSelf for sanity, etc. overall improvement of rules for fallback

  

  Derek Sorensen

  authored and

  Derek Sorensen

  committed
  206a82b

Commits on Dec 19, 2024

• add rules on hashing

  

  Derek Sorensen

  authored and

  Derek Sorensen

  committed
  e15d1a2

• change Safe spec to Hash spec for more accurate naming

  

  Derek Sorensen

  authored and

  Derek Sorensen

  committed
  43f4cb1

• committing the hash spec, there was some confusion with renaming this from before

  

  Derek Sorensen

  authored and

  Derek Sorensen

  committed
  9743c13

• update fallback to most current version. all but one passes (annotated) and it's our problem. will update if we can resolve it

  

  Derek Sorensen

  authored and

  Derek Sorensen

  committed
  00349d6

• execute_summary() improvement so it's more general

  

  Derek Sorensen

  authored and

  Derek Sorensen

  committed
  f2f39c5

Commits on Dec 20, 2024

• debugging handlerCalledIfSet rule, included an invariant that handler is never self nor the zero address, and now the Prover is misbehaving. Committing here and opening a ticket

  

  Derek Sorensen

  authored and

  Derek Sorensen

  committed
  d8b3e02