From bf943f80fec5ac647159d26161446ac5d716a294 Mon Sep 17 00:00:00 2001 From: Mikhail Date: Fri, 16 Jun 2023 19:34:05 +0200 Subject: [PATCH] Formal verification: No message can be signed through the core contract (#583) * Add a rule for no signed messages * Add a rule for no signed messages --- certora/specs/Safe.spec | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) diff --git a/certora/specs/Safe.spec b/certora/specs/Safe.spec index bf9876851..f09780902 100644 --- 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); -} \ No newline at end of file +}