Skip to content

Commit

Permalink
Add rule for checking non corresponding storage keeps unchanged
Browse files Browse the repository at this point in the history
  • Loading branch information
@sunbreak1211
sunbreak1211 committed Oct 31, 2023
1 parent 7e15bd8 commit 9b3940d
Show file tree
Hide file tree
Showing 10 changed files with 324 additions and 585 deletions.
20 changes: 10 additions & 10 deletions Makefile
View file
Original file line number Diff line number Diff line change
@@ -1,10 +1,10 @@
certora-buffer :; PATH=~/.solc-select/artifacts/solc-0.8.16:~/.solc-select/artifacts:${PATH} certoraRun --solc_map AllocatorBuffer=solc-0.8.16,GemMock=solc-0.8.16 --solc_optimize_map AllocatorBuffer=200,GemMock=0 --rule_sanity basic src/AllocatorBuffer.sol test/mocks/GemMock.sol --verify AllocatorBuffer:certora/AllocatorBuffer.spec$(if $(short), --short_output,)$(if $(rule), --rule $(rule),) --wait_for_results
certora-vault :; PATH=~/.solc-select/artifacts/solc-0.8.16:~/.solc-select/artifacts:${PATH} certoraRun --solc_map AllocatorVault=solc-0.8.16,AllocatorRoles=solc-0.8.16,VatMock=solc-0.8.16,JugMock=solc-0.8.16,NstJoinMock=solc-0.8.16,NstMock=solc-0.8.16 --solc_optimize_map AllocatorVault=200,AllocatorRoles=200,VatMock=0,JugMock=0,NstJoinMock=0,NstMock=0 --rule_sanity basic src/AllocatorVault.sol src/AllocatorRoles.sol test/mocks/VatMock.sol test/mocks/JugMock.sol test/mocks/NstJoinMock.sol test/mocks/NstMock.sol --link AllocatorVault:roles=AllocatorRoles AllocatorVault:vat=VatMock AllocatorVault:jug=JugMock AllocatorVault:nstJoin=NstJoinMock AllocatorVault:nst=NstMock JugMock:vat=VatMock NstJoinMock:vat=VatMock NstJoinMock:nst=NstMock --verify AllocatorVault:certora/AllocatorVault.spec$(if $(short), --short_output,)$(if $(rule), --rule $(rule),) --wait_for_results --multi_assert_check
certora-roles :; PATH=~/.solc-select/artifacts/solc-0.8.16:~/.solc-select/artifacts:${PATH} certoraRun --solc_map AllocatorRoles=solc-0.8.16 --solc_optimize_map AllocatorRoles=200 --rule_sanity basic src/AllocatorRoles.sol --verify AllocatorRoles:certora/AllocatorRoles.spec$(if $(short), --short_output,)$(if $(rule), --rule $(rule),) --wait_for_results
certora-oracle :; PATH=~/.solc-select/artifacts/solc-0.8.16:~/.solc-select/artifacts:${PATH} certoraRun --solc_map AllocatorOracle=solc-0.8.16 --solc_optimize_map AllocatorOracle=200 --rule_sanity basic src/AllocatorOracle.sol --verify AllocatorOracle:certora/AllocatorOracle.spec$(if $(short), --short_output,)$(if $(rule), --rule $(rule),) --wait_for_results
certora-registry :; PATH=~/.solc-select/artifacts/solc-0.8.16:~/.solc-select/artifacts:${PATH} certoraRun --solc_map AllocatorRegistry=solc-0.8.16 --solc_optimize_map AllocatorRegistry=200 --rule_sanity basic src/AllocatorRegistry.sol --verify AllocatorRegistry:certora/AllocatorRegistry.spec$(if $(short), --short_output,)$(if $(rule), --rule $(rule),) --wait_for_results
certora-swapper :; PATH=~/.solc-select/artifacts/solc-0.8.16:~/.solc-select/artifacts:${PATH} certoraRun --solc_map Swapper=solc-0.8.16,AllocatorRoles=solc-0.8.16,Gem0Mock=solc-0.8.16,Gem1Mock=solc-0.8.16,CalleeMock=solc-0.8.16 --solc_optimize_map Swapper=200,AllocatorRoles=200,Gem0Mock=0,Gem1Mock=0,CalleeMock=0 --rule_sanity basic src/funnels/Swapper.sol src/AllocatorRoles.sol test/mocks/Gem0Mock.sol test/mocks/Gem1Mock.sol test/mocks/CalleeMock.sol --link Swapper:roles=AllocatorRoles --verify Swapper:certora/funnels/Swapper.spec$(if $(short), --short_output,)$(if $(rule), --rule $(rule),) --wait_for_results
certora-depositoruniv3 :; PATH=~/.solc-select/artifacts/solc-0.8.16:~/.solc-select/artifacts:${PATH} certoraRun --solc_map DepositorUniV3=solc-0.8.16,AllocatorRoles=solc-0.8.16,PoolUniV3Mock=solc-0.8.16,Gem0Mock=solc-0.8.16,Gem1Mock=solc-0.8.16,Auxiliar=solc-0.8.16 --solc_optimize_map DepositorUniV3=200,AllocatorRoles=200,PoolUniV3Mock=0,Gem0Mock=0,Gem1Mock=0,Auxiliar=0 --rule_sanity basic src/funnels/DepositorUniV3.sol src/AllocatorRoles.sol test/mocks/PoolUniV3Mock.sol test/mocks/Gem0Mock.sol test/mocks/Gem1Mock.sol certora/funnels/Auxiliar.sol --link DepositorUniV3:roles=AllocatorRoles --verify DepositorUniV3:certora/funnels/DepositorUniV3.spec$(if $(short), --short_output,)$(if $(rule), --rule $(rule),) --wait_for_results
certora-stable-swapper :; PATH=~/.solc-select/artifacts/solc-0.8.16:~/.solc-select/artifacts:${PATH} certoraRun --solc_map StableSwapper=solc-0.8.16 --solc_optimize_map StableSwapper=200 --rule_sanity basic src/funnels/automation/StableSwapper.sol --verify StableSwapper:certora/funnels/automation/StableSwapper.spec$(if $(short), --short_output,)$(if $(rule), --rule $(rule),) --wait_for_results
certora-stable-depositoruniv3 :; PATH=~/.solc-select/artifacts/solc-0.8.16:~/.solc-select/artifacts:${PATH} certoraRun --solc_map StableDepositorUniV3=solc-0.8.16 --solc_optimize_map StableDepositorUniV3=200 --rule_sanity basic src/funnels/automation/StableDepositorUniV3.sol --verify StableDepositorUniV3:certora/funnels/automation/StableDepositorUniV3.spec$(if $(short), --short_output,)$(if $(rule), --rule $(rule),) --wait_for_results
certora-conduit-mover :; PATH=~/.solc-select/artifacts/solc-0.8.16:~/.solc-select/artifacts:${PATH} certoraRun --solc_map ConduitMover=solc-0.8.16 --solc_optimize_map ConduitMover=200 --rule_sanity basic src/funnels/automation/ConduitMover.sol --verify ConduitMover:certora/funnels/automation/ConduitMover.spec$(if $(short), --short_output,)$(if $(rule), --rule $(rule),) --wait_for_results
certora-buffer :; PATH=~/.solc-select/artifacts/solc-0.8.16:~/.solc-select/artifacts:${PATH} certoraRun --solc_map AllocatorBuffer=solc-0.8.16,GemMock=solc-0.8.16 --solc_optimize_map AllocatorBuffer=200,GemMock=0 --rule_sanity basic src/AllocatorBuffer.sol test/mocks/GemMock.sol --verify AllocatorBuffer:certora/AllocatorBuffer.spec --wait_for_results$(if $(short), --short_output,)$(if $(rule), --rule $(rule),)
certora-vault :; PATH=~/.solc-select/artifacts/solc-0.8.16:~/.solc-select/artifacts:${PATH} certoraRun --solc_map AllocatorVault=solc-0.8.16,AllocatorRoles=solc-0.8.16,VatMock=solc-0.8.16,JugMock=solc-0.8.16,NstJoinMock=solc-0.8.16,NstMock=solc-0.8.16 --solc_optimize_map AllocatorVault=200,AllocatorRoles=200,VatMock=0,JugMock=0,NstJoinMock=0,NstMock=0 --rule_sanity basic src/AllocatorVault.sol src/AllocatorRoles.sol test/mocks/VatMock.sol test/mocks/JugMock.sol test/mocks/NstJoinMock.sol test/mocks/NstMock.sol --link AllocatorVault:roles=AllocatorRoles AllocatorVault:vat=VatMock AllocatorVault:jug=JugMock AllocatorVault:nstJoin=NstJoinMock AllocatorVault:nst=NstMock JugMock:vat=VatMock NstJoinMock:vat=VatMock NstJoinMock:nst=NstMock --verify AllocatorVault:certora/AllocatorVault.spec --parametric_contracts AllocatorVault --wait_for_results$(if $(short), --short_output,)$(if $(rule), --rule $(rule),) --multi_assert_check
certora-roles :; PATH=~/.solc-select/artifacts/solc-0.8.16:~/.solc-select/artifacts:${PATH} certoraRun --solc_map AllocatorRoles=solc-0.8.16 --solc_optimize_map AllocatorRoles=200 --rule_sanity basic src/AllocatorRoles.sol --verify AllocatorRoles:certora/AllocatorRoles.spec --wait_for_results$(if $(short), --short_output,)$(if $(rule), --rule $(rule),)
certora-oracle :; PATH=~/.solc-select/artifacts/solc-0.8.16:~/.solc-select/artifacts:${PATH} certoraRun --solc_map AllocatorOracle=solc-0.8.16 --solc_optimize_map AllocatorOracle=200 --rule_sanity basic src/AllocatorOracle.sol --verify AllocatorOracle:certora/AllocatorOracle.spec --wait_for_results$(if $(short), --short_output,)$(if $(rule), --rule $(rule),)
certora-registry :; PATH=~/.solc-select/artifacts/solc-0.8.16:~/.solc-select/artifacts:${PATH} certoraRun --solc_map AllocatorRegistry=solc-0.8.16 --solc_optimize_map AllocatorRegistry=200 --rule_sanity basic src/AllocatorRegistry.sol --verify AllocatorRegistry:certora/AllocatorRegistry.spec --wait_for_results$(if $(short), --short_output,)$(if $(rule), --rule $(rule),)
certora-swapper :; PATH=~/.solc-select/artifacts/solc-0.8.16:~/.solc-select/artifacts:${PATH} certoraRun --solc_map Swapper=solc-0.8.16,AllocatorRoles=solc-0.8.16,Gem0Mock=solc-0.8.16,Gem1Mock=solc-0.8.16,CalleeMock=solc-0.8.16 --solc_optimize_map Swapper=200,AllocatorRoles=200,Gem0Mock=0,Gem1Mock=0,CalleeMock=0 --rule_sanity basic src/funnels/Swapper.sol src/AllocatorRoles.sol test/mocks/Gem0Mock.sol test/mocks/Gem1Mock.sol test/mocks/CalleeMock.sol --link Swapper:roles=AllocatorRoles --verify Swapper:certora/funnels/Swapper.spec --parametric_contracts Swapper --wait_for_results$(if $(short), --short_output,)$(if $(rule), --rule $(rule),)
certora-depositoruniv3 :; PATH=~/.solc-select/artifacts/solc-0.8.16:~/.solc-select/artifacts:${PATH} certoraRun --solc_map DepositorUniV3=solc-0.8.16,AllocatorRoles=solc-0.8.16,PoolUniV3Mock=solc-0.8.16,Gem0Mock=solc-0.8.16,Gem1Mock=solc-0.8.16,Auxiliar=solc-0.8.16 --solc_optimize_map DepositorUniV3=200,AllocatorRoles=200,PoolUniV3Mock=0,Gem0Mock=0,Gem1Mock=0,Auxiliar=0 --rule_sanity basic src/funnels/DepositorUniV3.sol src/AllocatorRoles.sol test/mocks/PoolUniV3Mock.sol test/mocks/Gem0Mock.sol test/mocks/Gem1Mock.sol certora/funnels/Auxiliar.sol --link DepositorUniV3:roles=AllocatorRoles --verify DepositorUniV3:certora/funnels/DepositorUniV3.spec --parametric_contracts DepositorUniV3 --wait_for_results$(if $(short), --short_output,)$(if $(rule), --rule $(rule),)
certora-stable-swapper :; PATH=~/.solc-select/artifacts/solc-0.8.16:~/.solc-select/artifacts:${PATH} certoraRun --solc_map StableSwapper=solc-0.8.16 --solc_optimize_map StableSwapper=200 --rule_sanity basic src/funnels/automation/StableSwapper.sol --verify StableSwapper:certora/funnels/automation/StableSwapper.spec --wait_for_results$(if $(short), --short_output,)$(if $(rule), --rule $(rule),)
certora-stable-depositoruniv3 :; PATH=~/.solc-select/artifacts/solc-0.8.16:~/.solc-select/artifacts:${PATH} certoraRun --solc_map StableDepositorUniV3=solc-0.8.16 --solc_optimize_map StableDepositorUniV3=200 --rule_sanity basic src/funnels/automation/StableDepositorUniV3.sol --verify StableDepositorUniV3:certora/funnels/automation/StableDepositorUniV3.spec --wait_for_results$(if $(short), --short_output,)$(if $(rule), --rule $(rule),)
certora-conduit-mover :; PATH=~/.solc-select/artifacts/solc-0.8.16:~/.solc-select/artifacts:${PATH} certoraRun --solc_map ConduitMover=solc-0.8.16 --solc_optimize_map ConduitMover=200 --rule_sanity basic src/funnels/automation/ConduitMover.sol --verify ConduitMover:certora/funnels/automation/ConduitMover.spec --wait_for_results$(if $(short), --short_output,)$(if $(rule), --rule $(rule),)
16 changes: 16 additions & 0 deletions certora/AllocatorBuffer.spec
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,22 @@ methods {
function _.approve(address, uint256) external => DISPATCHER(true) UNRESOLVED;
}

// Verify that each storage layout is only modified in the corresponding functions
rule storageAffected(method f) {
env e;

address anyAddr;

mathint wardsBefore = wards(anyAddr);

calldataarg args;
f(e, args);

mathint wardsAfter = wards(anyAddr);

assert wardsAfter != wardsBefore => f.selector == sig:rely(address).selector || f.selector == sig:deny(address).selector, "wards[x] changed in an unexpected function";
}

// Verify correct storage changes for non reverting rely
rule rely(address usr) {
env e;
Expand Down
32 changes: 20 additions & 12 deletions certora/AllocatorRegistry.spec
View file
Original file line number Diff line number Diff line change
Expand Up @@ -5,26 +5,42 @@ methods {
function buffers(bytes32) external returns (address) envfree;
}

// Verify that each storage layout is only modified in the corresponding functions
rule storageAffected(method f) {
env e;

address anyAddr;
bytes32 anyBytes32;

mathint wardsBefore = wards(anyAddr);
address buffersBefore = buffers(anyBytes32);

calldataarg args;
f(e, args);

mathint wardsAfter = wards(anyAddr);
address buffersAfter = buffers(anyBytes32);

assert wardsAfter != wardsBefore => f.selector == sig:rely(address).selector || f.selector == sig:deny(address).selector, "wards[x] changed in an unexpected function";
assert buffersAfter != buffersBefore => f.selector == sig:file(bytes32,bytes32,address).selector, "buffers[x] changed in an unexpected function";
}

// Verify correct storage changes for non reverting rely
rule rely(address usr) {
env e;

address other;
require other != usr;
bytes32 anyBytes32;

mathint wardsOtherBefore = wards(other);
address buffersBefore = buffers(anyBytes32);

rely(e, usr);

mathint wardsUsrAfter = wards(usr);
mathint wardsOtherAfter = wards(other);
address buffersAfter = buffers(anyBytes32);

assert wardsUsrAfter == 1, "rely did not set the wards";
assert wardsOtherAfter == wardsOtherBefore, "rely did not keep unchanged the rest of wards[x]";
assert buffersAfter == buffersBefore, "rely did not keep unchanged every buffers[x]";
}

// Verify revert rules on rely
Expand All @@ -49,20 +65,16 @@ rule deny(address usr) {

address other;
require other != usr;
bytes32 anyBytes32;

mathint wardsOtherBefore = wards(other);
address buffersBefore = buffers(anyBytes32);

deny(e, usr);

mathint wardsUsrAfter = wards(usr);
mathint wardsOtherAfter = wards(other);
address buffersAfter = buffers(anyBytes32);

assert wardsUsrAfter == 0, "deny did not set the wards";
assert wardsOtherAfter == wardsOtherBefore, "deny did not keep unchanged the rest of wards[x]";
assert buffersAfter == buffersBefore, "deny did not keep unchanged every buffers[x]";
}

// Verify revert rules on deny
Expand All @@ -85,20 +97,16 @@ rule deny_revert(address usr) {
rule file(bytes32 ilk, bytes32 what, address data) {
env e;

address anyAddr;
bytes32 otherBytes32;
require otherBytes32 != ilk;

mathint wardsBefore = wards(anyAddr);
address buffersOtherBefore = buffers(otherBytes32);

file(e, ilk, what, data);

mathint wardsAfter = wards(anyAddr);
address buffersIlkAfter = buffers(ilk);
address buffersOtherAfter = buffers(otherBytes32);

assert wardsAfter == wardsBefore, "file did not keep unchanged every wards[x]";
assert buffersIlkAfter == data, "file did not set buffers[ilk] to data";
assert buffersOtherAfter == buffersOtherBefore, "file did not keep unchanged the rest of buffers[x]";
}
Expand Down
Loading

0 comments on commit 9b3940d

Please sign in to comment.