Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

certora updates #17

Merged
merged 47 commits into from
Jun 27, 2024
Merged

certora updates #17

Show file tree
Hide file tree
Changes from 12 commits
Commits
Show all changes
47 commits
Select commit Hold shift + click to select a range
719007c
certora updates
aazhou1 Jun 20, 2024
8acea29
ignore solidity warnings in servicer
aazhou1 Jun 20, 2024
23c8fea
ignore solidity warnings rollover manager
aazhou1 Jun 20, 2024
d1832fd
replace newSplitParallel certora config proverarg
aazhou1 Jun 21, 2024
0bdb54d
get rid of branch versions of certora
aazhou1 Jun 21, 2024
15871d7
replace newSplitParallel certora config proverarg
aazhou1 Jun 21, 2024
3e15dce
update access roles test for servicer with new controller function fo…
aazhou1 Jun 21, 2024
793cd2b
remove extra semicolon
aazhou1 Jun 21, 2024
cd55e0f
remove specialist role from servicer specs certora
aazhou1 Jun 21, 2024
d148d86
link controller to servicer in servicer spec for certora
aazhou1 Jun 21, 2024
fa90c26
prevent previous term locker from conflicting with controller treasur…
aazhou1 Jun 21, 2024
4621474
add envfree declaration of get treasury address to rollover exposure …
aazhou1 Jun 21, 2024
42a611e
no zero address msg sender in exposure opening on new rollover certora
aazhou1 Jun 21, 2024
4faeef2
treasuery cannot be borrow address
aazhou1 Jun 21, 2024
9bb3594
treasuery cannot be borrow address
aazhou1 Jun 21, 2024
4838471
treasuery address always 100
aazhou1 Jun 22, 2024
8468755
treasuery address always 100
aazhou1 Jun 22, 2024
7da828e
100 address for treasury imported from rules for servicer
aazhou1 Jun 22, 2024
3a42c44
100 address for treasury imported from rules for servicer
aazhou1 Jun 22, 2024
a7943dd
100 address for treasury imported from rules for servicer
aazhou1 Jun 22, 2024
d1e24e1
controller harness for certora
aazhou1 Jun 23, 2024
38073be
controller harness for certora
aazhou1 Jun 23, 2024
8937188
fix acccess roles for servicer certora spec
aazhou1 Jun 23, 2024
36af4cb
100 address for treasury imported from rules for servicer
aazhou1 Jun 23, 2024
3488644
100 address for treasury imported from rules for servicer
aazhou1 Jun 24, 2024
d9e997a
further split tests
aazhou1 Jun 24, 2024
7950d57
undo servicer update
aazhou1 Jun 24, 2024
726543b
minting changes certora spec
aazhou1 Jun 25, 2024
00723b0
minting changes certora spec
aazhou1 Jun 25, 2024
d9ba8a5
beta cli runs for errors in certora prod
aazhou1 Jun 25, 2024
5cce3b4
add 2 new reverts for repayments in certora
aazhou1 Jun 25, 2024
aa7ce02
NONDET summary for access roles controller call for mint open exposur…
aazhou1 Jun 25, 2024
78040d3
split repay and redemption revert certora specs
aazhou1 Jun 25, 2024
47592d6
add semicolon to end of summary in access roles servicer certora
aazhou1 Jun 26, 2024
a08d26e
ignore solidity warnings certora
aazhou1 Jun 26, 2024
c38a54d
split repay and redemption revert certora specs
aazhou1 Jun 26, 2024
04460ac
verify mint exposure access methods certora
aazhou1 Jun 26, 2024
246506f
add env to verifyMintExposureAccess calls
aazhou1 Jun 26, 2024
c2e66c6
DISPATCHER true verifyMintExposureAccess
aazhou1 Jun 26, 2024
660f315
trying to get linking to work
aazhou1 Jun 26, 2024
0bdb6ab
trying to get linking to work
aazhou1 Jun 26, 2024
5df7c54
trying to get linking to work
aazhou1 Jun 26, 2024
46741e8
trying to get linking to work
aazhou1 Jun 26, 2024
743973f
redemption reverts branch version removed
aazhou1 Jun 26, 2024
7a5b2d3
redemption reverts branch version removed
aazhou1 Jun 26, 2024
335b4f3
redemption reverts branch version removed
aazhou1 Jun 26, 2024
ccb2ae4
get mint integrity to stop timing out
aazhou1 Jun 27, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion certora/confs/termAuctionBidLocker-locking.conf
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,6 @@
],
"server": "production",
"rule_sanity": "basic",
"contract_compiler_skip_severe_warning_as_error": true,
"ignore_solidity_warnings": true,
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Consider the implications of ignoring all Solidity warnings.

Ignoring all Solidity warnings (ignore_solidity_warnings: true) may lead to overlooking significant issues in smart contracts, especially in a production environment. It's crucial to weigh the benefits against potential risks. If this setting is necessary for certain builds or testing scenarios, consider enabling it conditionally or ensuring that all warnings are reviewed manually or through additional automated checks before deployment.

"verify": "TermAuctionBidLockerHarness:certora/specs/termAuctionBidLocker/rulesLocking.spec"
}
2 changes: 1 addition & 1 deletion certora/confs/termAuctionBidLocker-lockingReverts.conf
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,6 @@
],
"server": "production",
"rule_sanity": "basic",
"contract_compiler_skip_severe_warning_as_error": true,
"ignore_solidity_warnings": true,
"verify": "TermAuctionBidLockerHarness:certora/specs/termAuctionBidLocker/rulesLockingReverts.spec"
}
2 changes: 1 addition & 1 deletion certora/confs/termAuctionBidLocker-stateVariables.conf
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,6 @@
],
"server": "production",
"rule_sanity": "basic",
"contract_compiler_skip_severe_warning_as_error": true,
"ignore_solidity_warnings": true,
"verify": "TermAuctionBidLockerHarness:certora/specs/termAuctionBidLocker/rulesStateVariables.spec"
}
2 changes: 1 addition & 1 deletion certora/confs/termAuctionBidLocker.conf
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,6 @@
],
"server": "production",
"rule_sanity": "basic",
"contract_compiler_skip_severe_warning_as_error": true,
"ignore_solidity_warnings": true,
"verify": "TermAuctionBidLockerHarness:certora/specs/termAuctionBidLocker/rules.spec"
}
2 changes: 1 addition & 1 deletion certora/confs/termRepoCollateralManager-batchDefault.conf
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@
"solc_optimize": "50",
"loop_iter": "2",
"optimistic_loop": true,
"contract_compiler_skip_severe_warning_as_error": true,
"ignore_solidity_warnings": true,
"prover_args": [
"-smt_initialSplitDepth 3",
"-depth 10"
Expand Down
2 changes: 1 addition & 1 deletion certora/confs/termRepoCollateralManager-batchLiquidation.conf
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@
"solc_optimize": "50",
"loop_iter": "2",
"optimistic_loop": true,
"contract_compiler_skip_severe_warning_as_error": true,
"ignore_solidity_warnings": true,
"prover_args": [
"-smt_initialSplitDepth 3",
"-depth 10"
Expand Down
2 changes: 1 addition & 1 deletion certora/confs/termRepoCollateralManager-batchLiquidationWithRepoToken.conf
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@
"solc_optimize": "50",
"loop_iter": "2",
"optimistic_loop": true,
"contract_compiler_skip_severe_warning_as_error": true,
"ignore_solidity_warnings": true,
"prover_args": [
"-smt_initialSplitDepth 4",
"-depth 20",
Expand Down
2 changes: 1 addition & 1 deletion certora/confs/termRepoCollateralManager-stateVariables.conf
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@
"solc_optimize": "50",
"loop_iter": "3",
"optimistic_loop": true,
"contract_compiler_skip_severe_warning_as_error": true,
"ignore_solidity_warnings": true,
"prover_args": [
"-depth 15",
"-splitParallel true"
Expand Down
2 changes: 1 addition & 1 deletion certora/confs/termRepoCollateralManager.conf
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,7 +21,7 @@
"solc_optimize": "50",
"loop_iter": "3",
"optimistic_loop": true,
"contract_compiler_skip_severe_warning_as_error": true,
"ignore_solidity_warnings": true,
"prover_args": [
"-depth 15",
"-splitParallel true"
Expand Down
2 changes: 1 addition & 1 deletion certora/confs/termRepoRolloverManager.conf
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@
"solc_optimize": "50",
"loop_iter": "3",
"optimistic_loop": true,
"contract_compiler_skip_severe_warning_as_error": true,
"ignore_solidity_warnings": true,
"parametric_contracts": [
"TermRepoRolloverManagerHarness"
],
Expand Down
4 changes: 2 additions & 2 deletions certora/confs/termRepoServicer-lockFulfill.conf
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,14 +20,14 @@
"-smt_initialSplitDepth 5",
"-depth 15",
"-mediumTimeout 20",
"-newSplitParallel true",
"-splitParallel true",
"-splitParallelTimelimit 7200",
"-splitParallelInitialDepth 10"
],
"solc_optimize": "50",
"loop_iter": "2",
"optimistic_loop": true,
"contract_compiler_skip_severe_warning_as_error": true,
"ignore_solidity_warnings": true,

"smt_timeout": "7200",
"parametric_contracts": [
Expand Down
2 changes: 1 addition & 1 deletion certora/confs/termRepoServicer-lockFulfillReverts.conf
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -27,7 +27,7 @@
"solc_optimize": "50",
"loop_iter": "2",
"optimistic_loop": true,
"contract_compiler_skip_severe_warning_as_error": true,
"ignore_solidity_warnings": true,

"smt_timeout": "7200",
"parametric_contracts": [
Expand Down
4 changes: 2 additions & 2 deletions certora/confs/termRepoServicer-mintCollapse.conf
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,14 +20,14 @@
"-smt_initialSplitDepth 5",
"-depth 15",
"-mediumTimeout 2",
"-newSplitParallel true",
"-splitParallel true",
"-splitParallelTimelimit 7200",
"-splitParallelInitialDepth 5"
],
"solc_optimize": "50",
"loop_iter": "2",
"optimistic_loop": true,
"contract_compiler_skip_severe_warning_as_error": true,
"ignore_solidity_warnings": true,
"smt_timeout": "7200",
"parametric_contracts": [
"TermRepoServicerHarness"
Expand Down
2 changes: 1 addition & 1 deletion certora/confs/termRepoServicer-mintCollapseReverts.conf
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@
"solc_optimize": "50",
"loop_iter": "2",
"optimistic_loop": true,
"contract_compiler_skip_severe_warning_as_error": true,
"ignore_solidity_warnings": true,
"smt_timeout": "7200",
"parametric_contracts": [
"TermRepoServicerHarness"
Expand Down
5 changes: 2 additions & 3 deletions certora/confs/termRepoServicer-repaymentsRedemptions.conf
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,12 +20,12 @@
"-smt_initialSplitDepth 5",
"-depth 15",
"-mediumTimeout 20",
"-newSplitParallel true",
"-splitParallel true",
"-splitParallelTimelimit 7200",
"-splitParallelInitialDepth 5"
],
"solc_optimize": "50",
"contract_compiler_skip_severe_warning_as_error": true,
"ignore_solidity_warnings": true,
"loop_iter": "2",
"optimistic_loop": true,
"smt_timeout": "7200",
Expand All @@ -37,6 +37,5 @@
"@chainlink=node_modules/@chainlink",
"@openzeppelin=node_modules/@openzeppelin"
],
"prover_version": "jtoman/finder-fixes-will-it-ever-end",
"verify": "TermRepoServicerHarness:certora/specs/termRepoServicer/rulesRepaymentsRedemptions.spec"
}
3 changes: 1 addition & 2 deletions certora/confs/termRepoServicer-repaymentsRedemptionsReverts.conf
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,7 +25,7 @@
"-splitParallelInitialDepth 5"
],
"solc_optimize": "50",
"contract_compiler_skip_severe_warning_as_error": true,
"ignore_solidity_warnings": true,
"loop_iter": "2",
"optimistic_loop": true,
"smt_timeout": "7200",
Expand All @@ -37,6 +37,5 @@
"@chainlink=node_modules/@chainlink",
"@openzeppelin=node_modules/@openzeppelin"
],
"prover_version": "jtoman/finder-fixes-will-it-ever-end",
"verify": "TermRepoServicerHarness:certora/specs/termRepoServicer/rulesRepaymentsRedemptionsReverts.spec"
}
4 changes: 2 additions & 2 deletions certora/confs/termRepoServicer-stateVariables.conf
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -20,12 +20,12 @@
"-smt_initialSplitDepth 10",
"-depth 20",
"-mediumTimeout 2",
"-newSplitParallel true",
"-splitParallel true",
"-splitParallelTimelimit 7200",
"-splitParallelInitialDepth 10"
],
"solc_optimize": "50",
"contract_compiler_skip_severe_warning_as_error": true,
"ignore_solidity_warnings": true,
"loop_iter": "2",
"optimistic_loop": true,
"smt_timeout": "7200",
Expand Down
5 changes: 3 additions & 2 deletions certora/confs/termRepoServicer.conf
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,21 +13,22 @@
"TermRepoServicerHarness:termRepoToken=TermRepoToken",
"TermRepoServicerHarness:termRepoLocker=TermRepoLocker",
"TermRepoServicerHarness:termRepoCollateralManager=TermRepoCollateralManagerHarness",
"TermRepoServicerHarness:termController=TermController",
"TermRepoServicerHarness:termRepoRolloverManager=TermRepoRolloverManager",
"TermRepoCollateralManagerHarness:termRepoLocker=TermRepoLocker"
],
"prover_args": [
"-smt_initialSplitDepth 10",
"-depth 20",
"-mediumTimeout 2",
"-newSplitParallel true",
"-splitParallel true",
"-splitParallelTimelimit 7200",
"-splitParallelInitialDepth 10"
],
"solc_optimize": "50",
"loop_iter": "2",
"optimistic_loop": true,
"contract_compiler_skip_severe_warning_as_error": true,
"ignore_solidity_warnings": true,
"smt_timeout": "7200",
"parametric_contracts": [
"TermRepoServicerHarness"
Expand Down
14 changes: 9 additions & 5 deletions certora/specs/termRepoServicer/accessRoles.spec
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,9 @@
import "../methods/erc20Methods.spec";
import "../methods/emitMethods.spec";

using TermController as servicerAccessController;
Copy link

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Tip

Codebase Verification

Inconsistent usage of alias servicerAccessController detected.

The alias servicerAccessController should be used consistently throughout the file. However, there is a direct usage of TermController in the function definition:

  • function TermController.verifyMintExposureAccess(address) external returns(bool)

Please replace TermController with servicerAccessController in this instance to maintain consistency.

Analysis chain

Validate the use of alias for TermController.

The line using TermController as servicerAccessController; introduces an alias for TermController. Ensure that this alias is used consistently throughout the file to avoid confusion.

Scripts executed

The following scripts were executed for the analysis:

Script:

#!/bin/bash
# Description: Verify consistent usage of the alias `servicerAccessController`.

# Test: Search for inconsistent usage of the alias. Expect: No occurrences of direct `TermController` usage where the alias should be used.
rg --type spec $'TermController' certora/specs/termRepoServicer/accessRoles.spec

Length of output: 226



methods {
function hasRole(bytes32, address) external returns (bool) envfree;
function ADMIN_ROLE() external returns (bytes32) envfree;
Expand All @@ -9,9 +12,10 @@ methods {
function COLLATERAL_MANAGER() external returns (bytes32) envfree;
function DEVOPS_ROLE() external returns (bytes32) envfree;
function INITIALIZER_ROLE() external returns (bytes32) envfree;
function SPECIALIST_ROLE() external returns (bytes32) envfree;
function ROLLOVER_MANAGER() external returns (bytes32) envfree;
function ROLLOVER_TARGET_AUCTIONEER_ROLE() external returns (bytes32) envfree;

function TermController.verifyMintExposureAccess(address) external returns(bool) envfree;
}


Expand All @@ -36,10 +40,10 @@ rule onlyRoleCanCallRevert(method f, calldataarg args, env e) filtered {
|| hasRole(AUCTIONEER(),e.msg.sender)
|| hasRole(COLLATERAL_MANAGER(),e.msg.sender)
|| hasRole(DEVOPS_ROLE(),e.msg.sender)
|| hasRole(SPECIALIST_ROLE(),e.msg.sender)
|| hasRole(ROLLOVER_MANAGER(),e.msg.sender)
|| hasRole(ROLLOVER_TARGET_AUCTIONEER_ROLE(),e.msg.sender)
|| hasRole(INITIALIZER_ROLE(),e.msg.sender);
|| hasRole(INITIALIZER_ROLE(),e.msg.sender)
|| servicerAccessController.verifyMintExposureAccess(e.msg.sender);
}

rule onlyRoleCanCallStorage(method f, calldataarg args, env e) filtered {
Expand All @@ -64,8 +68,8 @@ rule onlyRoleCanCallStorage(method f, calldataarg args, env e) filtered {
|| hasRole(AUCTIONEER(),e.msg.sender)
|| hasRole(COLLATERAL_MANAGER(),e.msg.sender)
|| hasRole(DEVOPS_ROLE(),e.msg.sender)
|| hasRole(SPECIALIST_ROLE(),e.msg.sender)
|| hasRole(ROLLOVER_MANAGER(),e.msg.sender)
|| hasRole(ROLLOVER_TARGET_AUCTIONEER_ROLE(),e.msg.sender)
|| hasRole(INITIALIZER_ROLE(),e.msg.sender);
|| hasRole(INITIALIZER_ROLE(),e.msg.sender)
|| servicerAccessController.verifyMintExposureAccess(e.msg.sender);
}
6 changes: 6 additions & 0 deletions certora/specs/termRepoServicer/rolloverExposure.spec
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,3 +1,4 @@
using TermController as rolloverExposureController;
using TermRepoLocker as rolloverExposureLocker;
using TermRepoRolloverManager as rolloverExposureRolloverManager;
using TermRepoCollateralManagerHarness as rolloverExposureRepaymentCollateralManager;
Expand Down Expand Up @@ -34,6 +35,8 @@ methods {
function DummyERC20A.allowance(address,address) external returns(uint256) envfree;
function DummyERC20A.balanceOf(address) external returns(uint256) envfree;
function DummyERC20A.totalSupply() external returns(uint256) envfree;

function TermController.getTreasuryAddress() external returns (address) envfree;
}

rule openExposureOnRolloverNewIntegrity(env e) {
Expand All @@ -50,6 +53,9 @@ rule openExposureOnRolloverNewIntegrity(env e) {
require(rolloverExposureLocker != previousTermRepoLocker);
require(rolloverExposureLocker != 100); // Protecting locker from using treasury address;
require(previousTermRepoLocker != 100); // Protecting previous locker from using treasury address;
require(rolloverExposureController.getTreasuryAddress() != e.msg.sender); // Protecting treasury from calling this function
require(rolloverExposureController.getTreasuryAddress() != rolloverExposureLocker); // Protecting locker from using treasury address;
require(rolloverExposureController.getTreasuryAddress() != previousTermRepoLocker); // Protecting previous locker from using treasury address;

mathint balanceBefore = getBorrowerRepurchaseObligation(borrower);
mathint tokenBalanceTermRepoLockerBefore = rolloverExposureToken.balanceOf(rolloverExposureLocker);
Expand Down
Loading