Formal verification: No message can be signed through the core contra…

…ct (#583) * Add a rule for no signed messages * Add a rule for no signed messages
safe-global · Jun 16, 2023 · bf943f8 · bf943f8
1 parent eec5ebc
commit bf943f8
Showing 1 changed file with 5 additions and 1 deletion.
diff --git a/certora/specs/Safe.spec b/certora/specs/Safe.spec
@@ -3,6 +3,7 @@ methods {
     function getThreshold() external returns (uint256) envfree;
     function disableModule(address,address) external;
     function nonce() external returns (uint256) envfree;
+    function signedMessages(bytes32) external returns (uint256) envfree;
 
     // harnessed
     function getModule(address) external returns (address) envfree;
@@ -158,6 +159,9 @@ rule guardAddressChange(method f) filtered {
         f.selector == sig:setGuard(address).selector;
 }
 
+invariant noSignedMessages(bytes32 message)
+    signedMessages(message) == 0
+    filtered { f -> reachableOnly(f) }
 
 rule nativeTokenBalanceSpending(method f) filtered {
     f -> reachableOnly(f)
@@ -233,4 +237,4 @@ rule nativeTokenBalanceSpendingExecTransactionFromModuleReturnData(
 
     assert balanceAfter < balanceBefore => 
         to_mathint(balanceBefore - value) <= to_mathint(balanceAfter);
-}
+}