From aaad1f4a4ffdba7da789d93a28030e5c411f0181 Mon Sep 17 00:00:00 2001 From: Hadrien Croubois Date: Wed, 8 Mar 2023 19:30:07 +0100 Subject: [PATCH] Add FV specs for Ownable and Ownable2Steps (#4094) Co-authored-by: Santiago Palladino Co-authored-by: Francisco --- certora/harnesses/Ownable2StepHarness.sol | 9 ++ certora/harnesses/OwnableHarness.sol | 9 ++ certora/run.js | 4 +- certora/specs.json | 10 ++ certora/specs/Ownable.spec | 78 ++++++++++++++++ certora/specs/Ownable2Step.spec | 108 ++++++++++++++++++++++ certora/specs/methods/IOwnable.spec | 5 + certora/specs/methods/IOwnable2Step.spec | 7 ++ 8 files changed, 228 insertions(+), 2 deletions(-) create mode 100644 certora/harnesses/Ownable2StepHarness.sol create mode 100644 certora/harnesses/OwnableHarness.sol create mode 100644 certora/specs/Ownable.spec create mode 100644 certora/specs/Ownable2Step.spec create mode 100644 certora/specs/methods/IOwnable.spec create mode 100644 certora/specs/methods/IOwnable2Step.spec diff --git a/certora/harnesses/Ownable2StepHarness.sol b/certora/harnesses/Ownable2StepHarness.sol new file mode 100644 index 000000000..4d30e5041 --- /dev/null +++ b/certora/harnesses/Ownable2StepHarness.sol @@ -0,0 +1,9 @@ +// SPDX-License-Identifier: MIT + +pragma solidity ^0.8.0; + +import "../patched/access/Ownable2Step.sol"; + +contract Ownable2StepHarness is Ownable2Step { + function restricted() external onlyOwner {} +} diff --git a/certora/harnesses/OwnableHarness.sol b/certora/harnesses/OwnableHarness.sol new file mode 100644 index 000000000..93cbb4770 --- /dev/null +++ b/certora/harnesses/OwnableHarness.sol @@ -0,0 +1,9 @@ +// SPDX-License-Identifier: MIT + +pragma solidity ^0.8.0; + +import "../patched/access/Ownable.sol"; + +contract OwnableHarness is Ownable { + function restricted() external onlyOwner {} +} diff --git a/certora/run.js b/certora/run.js index 1da238d4f..161465258 100644 --- a/certora/run.js +++ b/certora/run.js @@ -64,7 +64,7 @@ async function runCertora(spec, contract, files, options = []) { stream.end(); // write results in markdown format - writeEntry(spec, contract, code || signal, (await output).match(/https:\S*/)[0]); + writeEntry(spec, contract, code || signal, (await output).match(/https:\S*/)?.[0]); // write all details console.error(`+ certoraRun ${args.join(' ')}\n` + (await output)); @@ -103,7 +103,7 @@ function writeEntry(spec, contract, success, url) { contract, success ? ':x:' : ':heavy_check_mark:', `[link](${url})`, - `[link](${url.replace('/jobStatus/', '/output/')})`, + `[link](${url?.replace('/jobStatus/', '/output/')})`, ), ); } diff --git a/certora/specs.json b/certora/specs.json index 4d3e1fb90..c22b1ebba 100644 --- a/certora/specs.json +++ b/certora/specs.json @@ -4,6 +4,16 @@ "contract": "AccessControlHarness", "files": ["certora/harnesses/AccessControlHarness.sol"] }, + { + "spec": "Ownable", + "contract": "OwnableHarness", + "files": ["certora/harnesses/OwnableHarness.sol"] + }, + { + "spec": "Ownable2Step", + "contract": "Ownable2StepHarness", + "files": ["certora/harnesses/Ownable2StepHarness.sol"] + }, { "spec": "ERC20", "contract": "ERC20PermitHarness", diff --git a/certora/specs/Ownable.spec b/certora/specs/Ownable.spec new file mode 100644 index 000000000..48bd84d13 --- /dev/null +++ b/certora/specs/Ownable.spec @@ -0,0 +1,78 @@ +import "helpers.spec" +import "methods/IOwnable.spec" + +methods { + restricted() +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Function correctness: transferOwnership changes ownership │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule transferOwnership(env e) { + require nonpayable(e); + + address newOwner; + address current = owner(); + + transferOwnership@withrevert(e, newOwner); + bool success = !lastReverted; + + assert success <=> (e.msg.sender == current && newOwner != 0), "unauthorized caller or invalid arg"; + assert success => owner() == newOwner, "current owner changed"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Function correctness: renounceOwnership removes the owner │ + +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule renounceOwnership(env e) { + require nonpayable(e); + + address current = owner(); + + renounceOwnership@withrevert(e); + bool success = !lastReverted; + + assert success <=> e.msg.sender == current, "unauthorized caller"; + assert success => owner() == 0, "owner not cleared"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Access control: only current owner can call restricted functions │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule onlyCurrentOwnerCanCallOnlyOwner(env e) { + require nonpayable(e); + + address current = owner(); + + calldataarg args; + restricted@withrevert(e, args); + + assert !lastReverted <=> e.msg.sender == current, "access control failed"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: ownership can only change in specific ways │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule onlyOwnerOrPendingOwnerCanChangeOwnership(env e, method f) { + address oldCurrent = owner(); + + calldataarg args; + f(e, args); + + address newCurrent = owner(); + + // If owner changes, must be either transferOwnership or renounceOwnership + assert oldCurrent != newCurrent => ( + (e.msg.sender == oldCurrent && newCurrent != 0 && f.selector == transferOwnership(address).selector) || + (e.msg.sender == oldCurrent && newCurrent == 0 && f.selector == renounceOwnership().selector) + ); +} diff --git a/certora/specs/Ownable2Step.spec b/certora/specs/Ownable2Step.spec new file mode 100644 index 000000000..70c520a03 --- /dev/null +++ b/certora/specs/Ownable2Step.spec @@ -0,0 +1,108 @@ +import "helpers.spec" +import "methods/IOwnable2Step.spec" + +methods { + restricted() +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Function correctness: transferOwnership sets the pending owner │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule transferOwnership(env e) { + require nonpayable(e); + + address newOwner; + address current = owner(); + + transferOwnership@withrevert(e, newOwner); + bool success = !lastReverted; + + assert success <=> e.msg.sender == current, "unauthorized caller"; + assert success => pendingOwner() == newOwner, "pending owner not set"; + assert success => owner() == current, "current owner changed"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Function correctness: renounceOwnership removes the owner and the pendingOwner │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule renounceOwnership(env e) { + require nonpayable(e); + + address current = owner(); + + renounceOwnership@withrevert(e); + bool success = !lastReverted; + + assert success <=> e.msg.sender == current, "unauthorized caller"; + assert success => pendingOwner() == 0, "pending owner not cleared"; + assert success => owner() == 0, "owner not cleared"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Function correctness: acceptOwnership changes owner and reset pending owner │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule acceptOwnership(env e) { + + require nonpayable(e); + + address current = owner(); + address pending = pendingOwner(); + + acceptOwnership@withrevert(e); + bool success = !lastReverted; + + assert success <=> e.msg.sender == pending, "unauthorized caller"; + assert success => pendingOwner() == 0, "pending owner not cleared"; + assert success => owner() == pending, "owner not transferred"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Access control: only current owner can call restricted functions │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule onlyCurrentOwnerCanCallOnlyOwner(env e) { + require nonpayable(e); + + address current = owner(); + + calldataarg args; + restricted@withrevert(e, args); + + assert !lastReverted <=> e.msg.sender == current, "access control failed"; +} + +/* +┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐ +│ Rule: ownership and pending ownership can only change in specific ways │ +└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘ +*/ +rule ownerOrPendingOwnerChange(env e, method f) { + address oldCurrent = owner(); + address oldPending = pendingOwner(); + + calldataarg args; + f(e, args); + + address newCurrent = owner(); + address newPending = pendingOwner(); + + // If owner changes, must be either acceptOwnership or renounceOwnership + assert oldCurrent != newCurrent => ( + (e.msg.sender == oldPending && newCurrent == oldPending && newPending == 0 && f.selector == acceptOwnership().selector) || + (e.msg.sender == oldCurrent && newCurrent == 0 && newPending == 0 && f.selector == renounceOwnership().selector) + ); + + // If pending changes, must be either acceptance or reset + assert oldPending != newPending => ( + (e.msg.sender == oldCurrent && newCurrent == oldCurrent && f.selector == transferOwnership(address).selector) || + (e.msg.sender == oldPending && newCurrent == oldPending && newPending == 0 && f.selector == acceptOwnership().selector) || + (e.msg.sender == oldCurrent && newCurrent == 0 && newPending == 0 && f.selector == renounceOwnership().selector) + ); +} diff --git a/certora/specs/methods/IOwnable.spec b/certora/specs/methods/IOwnable.spec new file mode 100644 index 000000000..cfa15f95f --- /dev/null +++ b/certora/specs/methods/IOwnable.spec @@ -0,0 +1,5 @@ +methods { + owner() returns (address) envfree + transferOwnership(address) + renounceOwnership() +} diff --git a/certora/specs/methods/IOwnable2Step.spec b/certora/specs/methods/IOwnable2Step.spec new file mode 100644 index 000000000..c8e671d27 --- /dev/null +++ b/certora/specs/methods/IOwnable2Step.spec @@ -0,0 +1,7 @@ +methods { + owner() returns (address) envfree + pendingOwner() returns (address) envfree + transferOwnership(address) + acceptOwnership() + renounceOwnership() +}