diff --git a/.github/workflows/formal-verification.yml b/.github/workflows/formal-verification.yml index 86acca7f32b..64c67e3bfe8 100644 --- a/.github/workflows/formal-verification.yml +++ b/.github/workflows/formal-verification.yml @@ -12,7 +12,7 @@ on: env: PIP_VERSION: '3.11' JAVA_VERSION: '11' - SOLC_VERSION: '0.8.20' + SOLC_VERSION: '0.8.27' concurrency: ${{ github.workflow }}-${{ github.ref }} @@ -64,7 +64,7 @@ jobs: - name: Verify specification run: | make -C certora apply - node certora/run.js ${{ steps.arguments.outputs.result }} >> "$GITHUB_STEP_SUMMARY" + node certora/run.js ${{ steps.arguments.outputs.result }} -p 1 -v >> "$GITHUB_STEP_SUMMARY" env: CERTORAKEY: ${{ secrets.CERTORAKEY }} diff --git a/certora/harnesses/ERC20WrapperHarness.sol b/certora/harnesses/ERC20WrapperHarness.sol index ca183ad928c..d98b703ac19 100644 --- a/certora/harnesses/ERC20WrapperHarness.sol +++ b/certora/harnesses/ERC20WrapperHarness.sol @@ -12,18 +12,6 @@ contract ERC20WrapperHarness is ERC20Permit, ERC20Wrapper { string memory _symbol ) ERC20(_name, _symbol) ERC20Permit(_name) ERC20Wrapper(_underlying) {} - function underlyingTotalSupply() public view returns (uint256) { - return underlying().totalSupply(); - } - - function underlyingBalanceOf(address account) public view returns (uint256) { - return underlying().balanceOf(account); - } - - function underlyingAllowanceToThis(address account) public view returns (uint256) { - return underlying().allowance(account, address(this)); - } - function recover(address account) public returns (uint256) { return _recover(account); } diff --git a/certora/run.js b/certora/run.js index 91f4a6aece1..3d3d1dcd359 100755 --- a/certora/run.js +++ b/certora/run.js @@ -1,33 +1,25 @@ #!/usr/bin/env node // USAGE: -// node certora/run.js [[CONTRACT_NAME:]SPEC_NAME]* [--all] [--options OPTIONS...] [--specs PATH] +// node certora/run.js [CONFIG]* [--all] // EXAMPLES: // node certora/run.js --all -// node certora/run.js AccessControl -// node certora/run.js AccessControlHarness:AccessControl +// node certora/run.js ERC721 +// node certora/run.js certora/specs/ERC721.conf -import { spawn } from 'child_process'; -import { PassThrough } from 'stream'; -import { once } from 'events'; -import path from 'path'; -import yargs from 'yargs'; -import { hideBin } from 'yargs/helpers'; -import pLimit from 'p-limit'; -import fs from 'fs/promises'; +const glob = require('glob'); +const fs = require('fs'); +const pLimit = require('p-limit').default; +const { hideBin } = require('yargs/helpers'); +const yargs = require('yargs/yargs'); +const { exec } = require('child_process'); -const argv = yargs(hideBin(process.argv)) +const { argv } = yargs(hideBin(process.argv)) .env('') .options({ all: { - alias: 'a', type: 'boolean', }, - spec: { - alias: 's', - type: 'string', - default: path.resolve(import.meta.dirname, 'specs.json'), - }, parallel: { alias: 'p', type: 'number', @@ -38,131 +30,39 @@ const argv = yargs(hideBin(process.argv)) type: 'count', default: 0, }, - options: { - alias: 'o', - type: 'array', - default: [], - }, - }) - .parse(); - -function match(entry, request) { - const [reqSpec, reqContract] = request.split(':').reverse(); - return entry.spec == reqSpec && (!reqContract || entry.contract == reqContract); -} - -const specs = JSON.parse(fs.readFileSync(argv.spec, 'utf8')).filter(s => argv.all || argv._.some(r => match(s, r))); + }); +const pattern = 'certora/specs/*.conf'; const limit = pLimit(argv.parallel); if (argv._.length == 0 && !argv.all) { console.error(`Warning: No specs requested. Did you forget to toggle '--all'?`); -} - -for (const r of argv._) { - if (!specs.some(s => match(s, r))) { - console.error(`Error: Requested spec '${r}' not found in ${argv.spec}`); - process.exitCode = 1; - } -} - -if (process.exitCode) { - process.exit(process.exitCode); -} - -for (const { spec, contract, files, options = [] } of specs) { - limit(() => - runCertora( - spec, - contract, - files, - [...options, ...argv.options].flatMap(opt => opt.split(' ')), - ), - ); -} - -// Run certora, aggregate the output and print it at the end -async function runCertora(spec, contract, files, options = []) { - const args = [...files, '--verify', `${contract}:certora/specs/${spec}.spec`, ...options]; - if (argv.verbose) { - console.log('Running:', args.join(' ')); - } - const child = spawn('certoraRun', args); - - const stream = new PassThrough(); - const output = collect(stream); - - child.stdout.pipe(stream, { end: false }); - child.stderr.pipe(stream, { end: false }); - - // as soon as we have a job id, print the output link - stream.on('data', function logStatusUrl(data) { - const { '-DjobId': jobId, '-DuserId': userId } = Object.fromEntries( - data - .toString('utf8') - .match(/-D\S+=\S+/g) - ?.map(s => s.split('=')) || [], - ); - - if (jobId && userId) { - console.error(`[${spec}] https://prover.certora.com/output/${userId}/${jobId}/`); - stream.off('data', logStatusUrl); - } - }); - - // wait for process end - const [code, signal] = await once(child, 'exit'); - - // error - if (code || signal) { - console.error(`[${spec}] Exited with code ${code || signal}`); - process.exitCode = 1; - } - - // get all output - stream.end(); - - // write results in markdown format - writeEntry(spec, contract, code || signal, (await output).match(/https:\/\/prover.certora.com\/output\/\S*/)?.[0]); - - // write all details - console.error(`+ certoraRun ${args.join(' ')}\n` + (await output)); -} - -// Collects stream data into a string -async function collect(stream) { - const buffers = []; - for await (const data of stream) { - const buf = Buffer.isBuffer(data) ? data : Buffer.from(data); - buffers.push(buf); - } - return Buffer.concat(buffers).toString('utf8'); -} - -// Formatting -let hasHeader = false; - -function formatRow(...array) { - return ['', ...array, ''].join(' | '); -} - -function writeHeader() { - console.log(formatRow('spec', 'contract', 'result', 'status', 'output')); - console.log(formatRow('-', '-', '-', '-', '-')); -} - -function writeEntry(spec, contract, success, url) { - if (!hasHeader) { - hasHeader = true; - writeHeader(); - } - console.log( - formatRow( - spec, - contract, - success ? ':heavy_check_mark:' : ':x:', - url ? `[link](${url?.replace('/output/', '/jobStatus/')})` : 'error', - url ? `[link](${url})` : 'error', + process.exitCode = 1; +} else { + Promise.all( + (argv.all ? glob.sync(pattern) : argv._.map(name => (fs.existsSync(name) ? name : pattern.replace('*', name)))).map( + (conf, i, { length }) => + limit( + () => + new Promise(resolve => { + if (argv.verbose) console.log(`[${i + 1}/${length}] Running ${conf}`); + exec(`certoraRun ${conf}`, (error, stdout, stderr) => { + const match = stdout.match( + 'https://prover.certora.com/output/[a-z0-9]+/[a-z0-9]+[?]anonymousKey=[a-z0-9]+', + ); + if (error) { + console.error(`[ERR] ${conf} failed with:\n${stderr || stdout}`); + process.exitCode = 1; + } else if (match) { + console.log(`${conf} - ${match[0]}`); + } else { + console.error(`[ERR] Could not parse stdout for ${conf}:\n${stdout}`); + process.exitCode = 1; + } + resolve(); + }); + }), + ), ), ); } diff --git a/certora/specs.json b/certora/specs.json deleted file mode 100644 index a894190924f..00000000000 --- a/certora/specs.json +++ /dev/null @@ -1,110 +0,0 @@ -[ - { - "spec": "Pausable", - "contract": "PausableHarness", - "files": ["certora/harnesses/PausableHarness.sol"] - }, - { - "spec": "AccessControl", - "contract": "AccessControlHarness", - "files": ["certora/harnesses/AccessControlHarness.sol"] - }, - { - "spec": "AccessControlDefaultAdminRules", - "contract": "AccessControlDefaultAdminRulesHarness", - "files": ["certora/harnesses/AccessControlDefaultAdminRulesHarness.sol"] - }, - { - "spec": "AccessManager", - "contract": "AccessManagerHarness", - "files": ["certora/harnesses/AccessManagerHarness.sol"], - "options": ["--optimistic_hashing", "--optimistic_loop"] - }, - { - "spec": "AccessManaged", - "contract": "AccessManagedHarness", - "files": [ - "certora/harnesses/AccessManagedHarness.sol", - "certora/harnesses/AccessManagerHarness.sol" - ], - "options": [ - "--optimistic_hashing", - "--optimistic_loop", - "--link AccessManagedHarness:_authority=AccessManagerHarness" - ] - }, - { - "spec": "DoubleEndedQueue", - "contract": "DoubleEndedQueueHarness", - "files": ["certora/harnesses/DoubleEndedQueueHarness.sol"] - }, - { - "spec": "Ownable", - "contract": "OwnableHarness", - "files": ["certora/harnesses/OwnableHarness.sol"] - }, - { - "spec": "Ownable2Step", - "contract": "Ownable2StepHarness", - "files": ["certora/harnesses/Ownable2StepHarness.sol"] - }, - { - "spec": "ERC20", - "contract": "ERC20PermitHarness", - "files": ["certora/harnesses/ERC20PermitHarness.sol"], - "options": ["--optimistic_loop"] - }, - { - "spec": "ERC20FlashMint", - "contract": "ERC20FlashMintHarness", - "files": [ - "certora/harnesses/ERC20FlashMintHarness.sol", - "certora/harnesses/ERC3156FlashBorrowerHarness.sol" - ], - "options": ["--optimistic_loop"] - }, - { - "spec": "ERC20Wrapper", - "contract": "ERC20WrapperHarness", - "files": [ - "certora/harnesses/ERC20PermitHarness.sol", - "certora/harnesses/ERC20WrapperHarness.sol" - ], - "options": [ - "--link ERC20WrapperHarness:_underlying=ERC20PermitHarness", - "--optimistic_loop" - ] - }, - { - "spec": "ERC721", - "contract": "ERC721Harness", - "files": ["certora/harnesses/ERC721Harness.sol", "certora/harnesses/ERC721ReceiverHarness.sol"], - "options": ["--optimistic_loop"] - }, - { - "spec": "Initializable", - "contract": "InitializableHarness", - "files": ["certora/harnesses/InitializableHarness.sol"] - }, - { - "spec": "EnumerableSet", - "contract": "EnumerableSetHarness", - "files": ["certora/harnesses/EnumerableSetHarness.sol"] - }, - { - "spec": "EnumerableMap", - "contract": "EnumerableMapHarness", - "files": ["certora/harnesses/EnumerableMapHarness.sol"] - }, - { - "spec": "TimelockController", - "contract": "TimelockControllerHarness", - "files": ["certora/harnesses/TimelockControllerHarness.sol"], - "options": ["--optimistic_hashing", "--optimistic_loop"] - }, - { - "spec": "Nonces", - "contract": "NoncesHarness", - "files": ["certora/harnesses/NoncesHarness.sol"] - } -] diff --git a/certora/specs/AccessControl.conf b/certora/specs/AccessControl.conf new file mode 100644 index 00000000000..d27bfb8f220 --- /dev/null +++ b/certora/specs/AccessControl.conf @@ -0,0 +1,7 @@ +{ + "files": [ + "certora/harnesses/AccessControlHarness.sol" + ], + "process": "emv", + "verify": "AccessControlHarness:certora/specs/AccessControl.spec" +} \ No newline at end of file diff --git a/certora/specs/AccessControlDefaultAdminRules.conf b/certora/specs/AccessControlDefaultAdminRules.conf new file mode 100644 index 00000000000..3697f4a3f09 --- /dev/null +++ b/certora/specs/AccessControlDefaultAdminRules.conf @@ -0,0 +1,7 @@ +{ + "files": [ + "certora/harnesses/AccessControlDefaultAdminRulesHarness.sol" + ], + "process": "emv", + "verify": "AccessControlDefaultAdminRulesHarness:certora/specs/AccessControlDefaultAdminRules.spec" +} \ No newline at end of file diff --git a/certora/specs/AccessManaged.conf b/certora/specs/AccessManaged.conf new file mode 100644 index 00000000000..8177aff3c33 --- /dev/null +++ b/certora/specs/AccessManaged.conf @@ -0,0 +1,13 @@ +{ + "files": [ + "certora/harnesses/AccessManagedHarness.sol", + "certora/harnesses/AccessManagerHarness.sol" + ], + "link": [ + "AccessManagedHarness:_authority=AccessManagerHarness" + ], + "optimistic_hashing": true, + "optimistic_loop": true, + "process": "emv", + "verify": "AccessManagedHarness:certora/specs/AccessManaged.spec" +} \ No newline at end of file diff --git a/certora/specs/AccessManager.conf b/certora/specs/AccessManager.conf new file mode 100644 index 00000000000..eeb54186ebb --- /dev/null +++ b/certora/specs/AccessManager.conf @@ -0,0 +1,9 @@ +{ + "files": [ + "certora/harnesses/AccessManagerHarness.sol" + ], + "optimistic_hashing": true, + "optimistic_loop": true, + "process": "emv", + "verify": "AccessManagerHarness:certora/specs/AccessManager.spec" +} \ No newline at end of file diff --git a/certora/specs/AccessManager.spec b/certora/specs/AccessManager.spec index cc4b0132a39..79f74f74cef 100644 --- a/certora/specs/AccessManager.spec +++ b/certora/specs/AccessManager.spec @@ -130,24 +130,35 @@ rule getAdminRestrictions(env e, bytes data) { assert restricted == false; assert roleId == 0; assert delay == 0; + } else if ( + selector == to_bytes4(sig:labelRole(uint64,string).selector) || + selector == to_bytes4(sig:setRoleAdmin(uint64,uint64).selector) || + selector == to_bytes4(sig:setRoleGuardian(uint64,uint64).selector) || + selector == to_bytes4(sig:setGrantDelay(uint64,uint32).selector) || + selector == to_bytes4(sig:setTargetAdminDelay(address,uint32).selector) + ) { + assert restricted == true; + assert roleId == ADMIN_ROLE(); + assert delay == 0; + } else if ( + selector == to_bytes4(sig:updateAuthority(address,address).selector) || + selector == to_bytes4(sig:setTargetClosed(address,bool).selector) || + selector == to_bytes4(sig:setTargetFunctionRole(address,bytes4[],uint64).selector) + ) { + assert restricted == true; + assert roleId == ADMIN_ROLE(); + assert delay == getTargetAdminDelay(e, getFirstArgumentAsAddress(data)); + } else if ( + selector == to_bytes4(sig:grantRole(uint64,address,uint32).selector) || + selector == to_bytes4(sig:revokeRole(uint64,address).selector) + ) { + assert restricted == true; + assert roleId == getRoleAdmin(getFirstArgumentAsUint64(data)); + assert delay == 0; } else { - assert restricted == - isOnlyAuthorized(selector); - - assert roleId == ( - (restricted && selector == to_bytes4(sig:grantRole(uint64,address,uint32).selector)) || - (restricted && selector == to_bytes4(sig:revokeRole(uint64,address).selector )) - ? getRoleAdmin(getFirstArgumentAsUint64(data)) - : ADMIN_ROLE() - ); - - assert delay == ( - (restricted && selector == to_bytes4(sig:updateAuthority(address,address).selector )) || - (restricted && selector == to_bytes4(sig:setTargetClosed(address,bool).selector )) || - (restricted && selector == to_bytes4(sig:setTargetFunctionRole(address,bytes4[],uint64).selector)) - ? getTargetAdminDelay(e, getFirstArgumentAsAddress(data)) - : 0 - ); + assert restricted == false; + assert roleId == getTargetFunctionRole(currentContract, selector); + assert delay == 0; } } @@ -213,29 +224,31 @@ rule canCallExtended(env e) { bool immediate = canCallExtended_immediate(e, caller, target, data); uint32 delay = canCallExtended_delay(e, caller, target, data); - bool enabled = getAdminRestrictions_restricted(e, data); + bool restricted = getAdminRestrictions_restricted(e, data); + bool closed = isTargetClosed(target); uint64 roleId = getAdminRestrictions_roleAdminId(e, data); uint32 operationDelay = getAdminRestrictions_executionDelay(e, data); bool inRole = hasRole_isMember(e, roleId, caller); uint32 executionDelay = hasRole_executionDelay(e, roleId, caller); - if (target == currentContract) { + if (data.length < 4) { + assert immediate == false; + assert delay == 0; + } else if (target == currentContract) { // Can only execute without delay in the specific cases: // - caller is the AccessManager and the executionId is set // or - // - data matches an admin restricted function // - caller has the necessary role // - operation delay is not set // - execution delay is not set assert immediate <=> ( ( caller == currentContract && - data.length >= 4 && executionId() == hashExecutionId(target, selector) ) || ( caller != currentContract && - enabled && - inRole && + inRole == true && + (restricted || !closed) && operationDelay == 0 && executionDelay == 0 ) @@ -247,21 +260,17 @@ rule canCallExtended(env e) { // Can only execute with delay in specific cases: // - caller is a third party - // - data matches an admin restricted function // - caller has the necessary role // -operation delay or execution delay is set assert delay > 0 <=> ( caller != currentContract && - enabled && - inRole && + inRole == true && + (restricted || !closed) && (operationDelay > 0 || executionDelay > 0) ); // If there is a delay, then it must be the maximum of caller's execution delay and the operation delay assert delay > 0 => to_mathint(delay) == max(operationDelay, executionDelay); - } else if (data.length < 4) { - assert immediate == false; - assert delay == 0; } else { // results are equivalent when targeting third party contracts assert immediate == canCall_immediate(e, caller, target, selector); diff --git a/certora/specs/Account.conf b/certora/specs/Account.conf new file mode 100644 index 00000000000..492dc5168b8 --- /dev/null +++ b/certora/specs/Account.conf @@ -0,0 +1,8 @@ +{ + "files": [ + "certora/harnesses/AccountHarness.sol" + ], + "optimistic_loop": true, + "process": "emv", + "verify": "AccountHarness:certora/specs/Account.spec" +} \ No newline at end of file diff --git a/certora/specs/DoubleEndedQueue.conf b/certora/specs/DoubleEndedQueue.conf new file mode 100644 index 00000000000..6669a9ebea8 --- /dev/null +++ b/certora/specs/DoubleEndedQueue.conf @@ -0,0 +1,7 @@ +{ + "files": [ + "certora/harnesses/DoubleEndedQueueHarness.sol" + ], + "process": "emv", + "verify": "DoubleEndedQueueHarness:certora/specs/DoubleEndedQueue.spec" +} \ No newline at end of file diff --git a/certora/specs/ERC20.conf b/certora/specs/ERC20.conf new file mode 100644 index 00000000000..b26b017b73d --- /dev/null +++ b/certora/specs/ERC20.conf @@ -0,0 +1,8 @@ +{ + "files": [ + "certora/harnesses/ERC20PermitHarness.sol" + ], + "optimistic_loop": true, + "process": "emv", + "verify": "ERC20PermitHarness:certora/specs/ERC20.spec" +} \ No newline at end of file diff --git a/certora/specs/ERC20.spec b/certora/specs/ERC20.spec index 21a03358508..1b402359f68 100644 --- a/certora/specs/ERC20.spec +++ b/certora/specs/ERC20.spec @@ -19,15 +19,15 @@ ghost mathint sumOfBalances { // Because `balance` has a uint256 type, any balance addition in CVL1 behaved as a `require_uint256()` casting, // leaving out the possibility of overflow. This is not the case in CVL2 where casting became more explicit. -// A counterexample in CVL2 is having an initial state where Alice initial balance is larger than totalSupply, which -// overflows Alice's balance when receiving a transfer. This is not possible unless the contract is deployed into an +// A counterexample in CVL2 is having an initial state where Alice initial balance is larger than totalSupply, which +// overflows Alice's balance when receiving a transfer. This is not possible unless the contract is deployed into an // already used address (or upgraded from corrupted state). // We restrict such behavior by making sure no balance is greater than the sum of balances. -hook Sload uint256 balance _balances[KEY address addr] STORAGE { +hook Sload uint256 balance _balances[KEY address addr] { require sumOfBalances >= to_mathint(balance); } -hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) STORAGE { +hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) { sumOfBalances = sumOfBalances - oldValue + newValue; } diff --git a/certora/specs/ERC20FlashMint.conf b/certora/specs/ERC20FlashMint.conf new file mode 100644 index 00000000000..927fe232a9f --- /dev/null +++ b/certora/specs/ERC20FlashMint.conf @@ -0,0 +1,9 @@ +{ + "files": [ + "certora/harnesses/ERC20FlashMintHarness.sol", + "certora/harnesses/ERC3156FlashBorrowerHarness.sol" + ], + "optimistic_loop": true, + "process": "emv", + "verify": "ERC20FlashMintHarness:certora/specs/ERC20FlashMint.spec" +} \ No newline at end of file diff --git a/certora/specs/ERC20Wrapper.conf b/certora/specs/ERC20Wrapper.conf new file mode 100644 index 00000000000..0c211d80073 --- /dev/null +++ b/certora/specs/ERC20Wrapper.conf @@ -0,0 +1,12 @@ +{ + "files": [ + "certora/harnesses/ERC20PermitHarness.sol", + "certora/harnesses/ERC20WrapperHarness.sol" + ], + "link": [ + "ERC20WrapperHarness:_underlying=ERC20PermitHarness" + ], + "optimistic_loop": true, + "process": "emv", + "verify": "ERC20WrapperHarness:certora/specs/ERC20Wrapper.spec" +} \ No newline at end of file diff --git a/certora/specs/ERC20Wrapper.spec b/certora/specs/ERC20Wrapper.spec index 04e67042a35..6b2ce958ffb 100644 --- a/certora/specs/ERC20Wrapper.spec +++ b/certora/specs/ERC20Wrapper.spec @@ -1,15 +1,17 @@ import "helpers/helpers.spec"; import "ERC20.spec"; +using ERC20PermitHarness as underlying; + methods { - function underlying() external returns(address) envfree; - function underlyingTotalSupply() external returns(uint256) envfree; - function underlyingBalanceOf(address) external returns(uint256) envfree; - function underlyingAllowanceToThis(address) external returns(uint256) envfree; - - function depositFor(address, uint256) external returns(bool); - function withdrawTo(address, uint256) external returns(bool); - function recover(address) external returns(uint256); + function underlying() external returns(address) envfree; + function depositFor(address, uint256) external returns(bool); + function withdrawTo(address, uint256) external returns(bool); + function recover(address) external returns(uint256); + + function underlying.totalSupply() external returns (uint256) envfree; + function underlying.balanceOf(address) external returns (uint256) envfree; + function underlying.allowance(address,address) external returns (uint256) envfree; } use invariant totalSupplyIsSumOfBalances; @@ -19,11 +21,24 @@ use invariant totalSupplyIsSumOfBalances; │ Helper: consequence of `totalSupplyIsSumOfBalances` applied to underlying │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -definition underlyingBalancesLowerThanUnderlyingSupply(address a) returns bool = - underlyingBalanceOf(a) <= underlyingTotalSupply(); - definition sumOfUnderlyingBalancesLowerThanUnderlyingSupply(address a, address b) returns bool = - a != b => underlyingBalanceOf(a) + underlyingBalanceOf(b) <= to_mathint(underlyingTotalSupply()); + a != b => underlying.balanceOf(a) + underlying.balanceOf(b) <= to_mathint(underlying.totalSupply()); + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Invariant: wrapped token should not allow any third party to spend its tokens │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +invariant noAllowance(address user) + underlying.allowance(currentContract, user) == 0 + { + preserved ERC20PermitHarness.approve(address spender, uint256 value) with (env e) { + require e.msg.sender != currentContract; + } + preserved ERC20PermitHarness.permit(address owner, address spender, uint256 value, uint256 deadline, uint8 v, bytes32 r, bytes32 s) with (env e) { + require owner != currentContract; + } + } /* ┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ @@ -31,17 +46,24 @@ definition sumOfUnderlyingBalancesLowerThanUnderlyingSupply(address a, address b └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ invariant totalSupplyIsSmallerThanUnderlyingBalance() - totalSupply() <= underlyingBalanceOf(currentContract) && - underlyingBalanceOf(currentContract) <= underlyingTotalSupply() && - underlyingTotalSupply() <= max_uint256 + totalSupply() <= underlying.balanceOf(currentContract) && + underlying.balanceOf(currentContract) <= underlying.totalSupply() && + underlying.totalSupply() <= max_uint256 { - preserved { + preserved with (env e) { requireInvariant totalSupplyIsSumOfBalances; - require underlyingBalancesLowerThanUnderlyingSupply(currentContract); - } - preserved depositFor(address account, uint256 amount) with (env e) { + require e.msg.sender != currentContract; require sumOfUnderlyingBalancesLowerThanUnderlyingSupply(e.msg.sender, currentContract); } + preserved ERC20PermitHarness.transferFrom(address from, address to, uint256 amount) with (env e) { + requireInvariant noAllowance(e.msg.sender); + require sumOfUnderlyingBalancesLowerThanUnderlyingSupply(from, to); + } + preserved ERC20PermitHarness.burn(address from, uint256 amount) with (env e) { + // If someone can burn from the wrapper, than the invariant obviously doesn't hold. + require from != currentContract; + require sumOfUnderlyingBalancesLowerThanUnderlyingSupply(from, currentContract); + } } invariant noSelfWrap() @@ -68,13 +90,13 @@ rule depositFor(env e) { uint256 balanceBefore = balanceOf(receiver); uint256 supplyBefore = totalSupply(); - uint256 senderUnderlyingBalanceBefore = underlyingBalanceOf(sender); - uint256 senderUnderlyingAllowanceBefore = underlyingAllowanceToThis(sender); - uint256 wrapperUnderlyingBalanceBefore = underlyingBalanceOf(currentContract); - uint256 underlyingSupplyBefore = underlyingTotalSupply(); + uint256 senderUnderlyingBalanceBefore = underlying.balanceOf(sender); + uint256 senderUnderlyingAllowanceBefore = underlying.allowance(sender, currentContract); + uint256 wrapperUnderlyingBalanceBefore = underlying.balanceOf(currentContract); + uint256 underlyingSupplyBefore = underlying.totalSupply(); uint256 otherBalanceBefore = balanceOf(other); - uint256 otherUnderlyingBalanceBefore = underlyingBalanceOf(other); + uint256 otherUnderlyingBalanceBefore = underlying.balanceOf(other); depositFor@withrevert(e, receiver, amount); bool success = !lastReverted; @@ -93,14 +115,14 @@ rule depositFor(env e) { assert success => ( to_mathint(balanceOf(receiver)) == balanceBefore + amount && to_mathint(totalSupply()) == supplyBefore + amount && - to_mathint(underlyingBalanceOf(currentContract)) == wrapperUnderlyingBalanceBefore + amount && - to_mathint(underlyingBalanceOf(sender)) == senderUnderlyingBalanceBefore - amount + to_mathint(underlying.balanceOf(currentContract)) == wrapperUnderlyingBalanceBefore + amount && + to_mathint(underlying.balanceOf(sender)) == senderUnderlyingBalanceBefore - amount ); // no side effect - assert underlyingTotalSupply() == underlyingSupplyBefore; + assert underlying.totalSupply() == underlyingSupplyBefore; assert balanceOf(other) != otherBalanceBefore => other == receiver; - assert underlyingBalanceOf(other) != otherUnderlyingBalanceBefore => (other == sender || other == currentContract); + assert underlying.balanceOf(other) != otherUnderlyingBalanceBefore => (other == sender || other == currentContract); } /* @@ -124,12 +146,12 @@ rule withdrawTo(env e) { uint256 balanceBefore = balanceOf(sender); uint256 supplyBefore = totalSupply(); - uint256 receiverUnderlyingBalanceBefore = underlyingBalanceOf(receiver); - uint256 wrapperUnderlyingBalanceBefore = underlyingBalanceOf(currentContract); - uint256 underlyingSupplyBefore = underlyingTotalSupply(); + uint256 receiverUnderlyingBalanceBefore = underlying.balanceOf(receiver); + uint256 wrapperUnderlyingBalanceBefore = underlying.balanceOf(currentContract); + uint256 underlyingSupplyBefore = underlying.totalSupply(); uint256 otherBalanceBefore = balanceOf(other); - uint256 otherUnderlyingBalanceBefore = underlyingBalanceOf(other); + uint256 otherUnderlyingBalanceBefore = underlying.balanceOf(other); withdrawTo@withrevert(e, receiver, amount); bool success = !lastReverted; @@ -146,14 +168,14 @@ rule withdrawTo(env e) { assert success => ( to_mathint(balanceOf(sender)) == balanceBefore - amount && to_mathint(totalSupply()) == supplyBefore - amount && - to_mathint(underlyingBalanceOf(currentContract)) == wrapperUnderlyingBalanceBefore - (currentContract != receiver ? amount : 0) && - to_mathint(underlyingBalanceOf(receiver)) == receiverUnderlyingBalanceBefore + (currentContract != receiver ? amount : 0) + to_mathint(underlying.balanceOf(currentContract)) == wrapperUnderlyingBalanceBefore - (currentContract != receiver ? amount : 0) && + to_mathint(underlying.balanceOf(receiver)) == receiverUnderlyingBalanceBefore + (currentContract != receiver ? amount : 0) ); // no side effect - assert underlyingTotalSupply() == underlyingSupplyBefore; + assert underlying.totalSupply() == underlyingSupplyBefore; assert balanceOf(other) != otherBalanceBefore => other == sender; - assert underlyingBalanceOf(other) != otherUnderlyingBalanceBefore => (other == receiver || other == currentContract); + assert underlying.balanceOf(other) != otherUnderlyingBalanceBefore => (other == receiver || other == currentContract); } /* @@ -172,12 +194,12 @@ rule recover(env e) { requireInvariant totalSupplyIsSumOfBalances; requireInvariant totalSupplyIsSmallerThanUnderlyingBalance; - mathint value = underlyingBalanceOf(currentContract) - totalSupply(); + mathint value = underlying.balanceOf(currentContract) - totalSupply(); uint256 supplyBefore = totalSupply(); uint256 balanceBefore = balanceOf(receiver); uint256 otherBalanceBefore = balanceOf(other); - uint256 otherUnderlyingBalanceBefore = underlyingBalanceOf(other); + uint256 otherUnderlyingBalanceBefore = underlying.balanceOf(other); recover@withrevert(e, receiver); bool success = !lastReverted; @@ -189,10 +211,10 @@ rule recover(env e) { assert success => ( to_mathint(balanceOf(receiver)) == balanceBefore + value && to_mathint(totalSupply()) == supplyBefore + value && - totalSupply() == underlyingBalanceOf(currentContract) + totalSupply() == underlying.balanceOf(currentContract) ); // no side effect - assert underlyingBalanceOf(other) == otherUnderlyingBalanceBefore; + assert underlying.balanceOf(other) == otherUnderlyingBalanceBefore; assert balanceOf(other) != otherBalanceBefore => other == receiver; } diff --git a/certora/specs/ERC721.conf b/certora/specs/ERC721.conf new file mode 100644 index 00000000000..e2369b851e6 --- /dev/null +++ b/certora/specs/ERC721.conf @@ -0,0 +1,9 @@ +{ + "files": [ + "certora/harnesses/ERC721Harness.sol", + "certora/harnesses/ERC721ReceiverHarness.sol" + ], + "optimistic_loop": true, + "process": "emv", + "verify": "ERC721Harness:certora/specs/ERC721.spec" +} \ No newline at end of file diff --git a/certora/specs/ERC721.spec b/certora/specs/ERC721.spec index bad4c473772..e5d5546f2e9 100644 --- a/certora/specs/ERC721.spec +++ b/certora/specs/ERC721.spec @@ -113,7 +113,7 @@ ghost mapping(address => mathint) _ownedByUser { init_state axiom forall address a. _ownedByUser[a] == 0; } -hook Sstore _owners[KEY uint256 tokenId] address newOwner (address oldOwner) STORAGE { +hook Sstore _owners[KEY uint256 tokenId] address newOwner (address oldOwner) { _ownedByUser[newOwner] = _ownedByUser[newOwner] + to_mathint(newOwner != 0 ? 1 : 0); _ownedByUser[oldOwner] = _ownedByUser[oldOwner] - to_mathint(oldOwner != 0 ? 1 : 0); _ownedTotal = _ownedTotal + to_mathint(newOwner != 0 ? 1 : 0) - to_mathint(oldOwner != 0 ? 1 : 0); @@ -132,13 +132,13 @@ ghost mapping(address => mathint) _balances { init_state axiom forall address a. _balances[a] == 0; } -hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) STORAGE { +hook Sstore _balances[KEY address addr] uint256 newValue (uint256 oldValue) { _supply = _supply - oldValue + newValue; } // TODO: This used to not be necessary. We should try to remove it. In order to do so, we will probably need to add // many "preserved" directive that require the "balanceOfConsistency" invariant on the accounts involved. -hook Sload uint256 value _balances[KEY address user] STORAGE { +hook Sload uint256 value _balances[KEY address user] { require _balances[user] == to_mathint(value); } diff --git a/certora/specs/EnumerableMap.conf b/certora/specs/EnumerableMap.conf new file mode 100644 index 00000000000..dfa85e40a9c --- /dev/null +++ b/certora/specs/EnumerableMap.conf @@ -0,0 +1,7 @@ +{ + "files": [ + "certora/harnesses/EnumerableMapHarness.sol" + ], + "process": "emv", + "verify": "EnumerableMapHarness:certora/specs/EnumerableMap.spec" +} \ No newline at end of file diff --git a/certora/specs/EnumerableMap.spec b/certora/specs/EnumerableMap.spec index 1801d99f74f..389e41e0a49 100644 --- a/certora/specs/EnumerableMap.spec +++ b/certora/specs/EnumerableMap.spec @@ -21,7 +21,7 @@ methods { │ Helpers │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -definition sanity() returns bool = +definition lengthSanity() returns bool = length() < max_uint256; /* @@ -33,7 +33,7 @@ invariant noValueIfNotContained(bytes32 key) !contains(key) => tryGet_value(key) == to_bytes32(0) { preserved set(bytes32 otherKey, bytes32 someValue) { - require sanity(); + require lengthSanity(); } } @@ -104,7 +104,7 @@ invariant consistencyKey(bytes32 key) └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ rule stateChange(env e, bytes32 key) { - require sanity(); + require lengthSanity(); requireInvariant consistencyKey(key); uint256 lengthBefore = length(); @@ -200,7 +200,7 @@ rule getAndTryGet(bytes32 key) { └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ rule set(bytes32 key, bytes32 value, bytes32 otherKey) { - require sanity(); + require lengthSanity(); uint256 lengthBefore = length(); bool containsBefore = contains(key); @@ -268,7 +268,7 @@ rule remove(bytes32 key, bytes32 otherKey) { └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ rule setEnumerability(bytes32 key, bytes32 value, uint256 index) { - require sanity(); + require lengthSanity(); bytes32 atKeyBefore = key_at(index); bytes32 atValueBefore = value_at(index); diff --git a/certora/specs/EnumerableSet.conf b/certora/specs/EnumerableSet.conf new file mode 100644 index 00000000000..b8f681fffe6 --- /dev/null +++ b/certora/specs/EnumerableSet.conf @@ -0,0 +1,7 @@ +{ + "files": [ + "certora/harnesses/EnumerableSetHarness.sol" + ], + "process": "emv", + "verify": "EnumerableSetHarness:certora/specs/EnumerableSet.spec" +} \ No newline at end of file diff --git a/certora/specs/EnumerableSet.spec b/certora/specs/EnumerableSet.spec index 94d0a918c7f..c96352feb72 100644 --- a/certora/specs/EnumerableSet.spec +++ b/certora/specs/EnumerableSet.spec @@ -17,7 +17,7 @@ methods { │ Helpers │ └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ -definition sanity() returns bool = +definition lengthSanity() returns bool = length() < max_uint256; /* @@ -87,7 +87,7 @@ invariant consistencyKey(bytes32 key) └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ rule stateChange(env e, bytes32 key) { - require sanity(); + require lengthSanity(); requireInvariant consistencyKey(key); uint256 lengthBefore = length(); @@ -142,7 +142,7 @@ rule liveness_2(uint256 index) { └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ rule add(bytes32 key, bytes32 otherKey) { - require sanity(); + require lengthSanity(); uint256 lengthBefore = length(); bool containsBefore = contains(key); @@ -202,7 +202,7 @@ rule remove(bytes32 key, bytes32 otherKey) { └─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ */ rule addEnumerability(bytes32 key, uint256 index) { - require sanity(); + require lengthSanity(); bytes32 atBefore = at_(index); add(key); diff --git a/certora/specs/Initializable.conf b/certora/specs/Initializable.conf new file mode 100644 index 00000000000..3ab0c97ea0d --- /dev/null +++ b/certora/specs/Initializable.conf @@ -0,0 +1,7 @@ +{ + "files": [ + "certora/harnesses/InitializableHarness.sol" + ], + "process": "emv", + "verify": "InitializableHarness:certora/specs/Initializable.spec" +} \ No newline at end of file diff --git a/certora/specs/Nonces.conf b/certora/specs/Nonces.conf new file mode 100644 index 00000000000..98c00078ce7 --- /dev/null +++ b/certora/specs/Nonces.conf @@ -0,0 +1,7 @@ +{ + "files": [ + "certora/harnesses/NoncesHarness.sol" + ], + "process": "emv", + "verify": "NoncesHarness:certora/specs/Nonces.spec" +} \ No newline at end of file diff --git a/certora/specs/Ownable.conf b/certora/specs/Ownable.conf new file mode 100644 index 00000000000..38ce364f0b4 --- /dev/null +++ b/certora/specs/Ownable.conf @@ -0,0 +1,7 @@ +{ + "files": [ + "certora/harnesses/OwnableHarness.sol" + ], + "process": "emv", + "verify": "OwnableHarness:certora/specs/Ownable.spec" +} \ No newline at end of file diff --git a/certora/specs/Ownable2Step.conf b/certora/specs/Ownable2Step.conf new file mode 100644 index 00000000000..ee887f1f5d6 --- /dev/null +++ b/certora/specs/Ownable2Step.conf @@ -0,0 +1,7 @@ +{ + "files": [ + "certora/harnesses/Ownable2StepHarness.sol" + ], + "process": "emv", + "verify": "Ownable2StepHarness:certora/specs/Ownable2Step.spec" +} \ No newline at end of file diff --git a/certora/specs/Pausable.conf b/certora/specs/Pausable.conf new file mode 100644 index 00000000000..90e34a6a91a --- /dev/null +++ b/certora/specs/Pausable.conf @@ -0,0 +1,7 @@ +{ + "files": [ + "certora/harnesses/PausableHarness.sol" + ], + "process": "emv", + "verify": "PausableHarness:certora/specs/Pausable.spec" +} \ No newline at end of file diff --git a/certora/specs/TimelockController.conf b/certora/specs/TimelockController.conf new file mode 100644 index 00000000000..e87617e36a2 --- /dev/null +++ b/certora/specs/TimelockController.conf @@ -0,0 +1,9 @@ +{ + "files": [ + "certora/harnesses/TimelockControllerHarness.sol" + ], + "optimistic_hashing": true, + "optimistic_loop": true, + "process": "emv", + "verify": "TimelockControllerHarness:certora/specs/TimelockController.spec" +} \ No newline at end of file diff --git a/fv-requirements.txt b/fv-requirements.txt index 788adf384a1..27ef60a5f2b 100644 --- a/fv-requirements.txt +++ b/fv-requirements.txt @@ -1,4 +1,4 @@ -certora-cli==4.13.1 +certora-cli==7.31.0 # File uses a custom name (fv-requirements.txt) so that it isn't picked by Netlify's build # whose latest Python version is 0.3.8, incompatible with most recent versions of Halmos halmos==0.3.0