From ec4e77397f0b4e2be145cc6238ceb5bd3486f94c Mon Sep 17 00:00:00 2001
From: Aleksander Kryukov <firealexkryukov@gmail.com>
Date: Thu, 31 Mar 2022 21:08:14 +0100
Subject: [PATCH] AccessControl verification

---
 certora/scripts/verifyAccessControl.sh |  9 +++
 certora/specs/AccessControl.spec       | 85 ++++++++++++++++++++++++++
 2 files changed, 94 insertions(+)
 create mode 100644 certora/scripts/verifyAccessControl.sh
 create mode 100644 certora/specs/AccessControl.spec

diff --git a/certora/scripts/verifyAccessControl.sh b/certora/scripts/verifyAccessControl.sh
new file mode 100644
index 000000000..6b1a7ba05
--- /dev/null
+++ b/certora/scripts/verifyAccessControl.sh
@@ -0,0 +1,9 @@
+certoraRun \
+    certora/harnesses/AccessControlHarness.sol \
+    --verify AccessControlHarness:certora/specs/AccessControl.spec \
+    --solc solc8.2 \
+    --optimistic_loop \
+    --staging \
+    --rule_sanity \
+    --msg "modifier check"
+    
\ No newline at end of file
diff --git a/certora/specs/AccessControl.spec b/certora/specs/AccessControl.spec
new file mode 100644
index 000000000..83f925d86
--- /dev/null
+++ b/certora/specs/AccessControl.spec
@@ -0,0 +1,85 @@
+methods {
+    grantRole(bytes32, address)
+    revokeRole(bytes32, address)
+    _checkRole(bytes32)
+    safeTransferFrom(address, address, uint256, uint256, bytes)
+    safeBatchTransferFrom(address, address, uint256[], uint256[], bytes)
+
+    getRoleAdmin(bytes32) returns(bytes32) envfree
+    hasRole(bytes32, address) returns(bool) envfree
+} 
+
+
+// STATUS - verified
+// check onlyRole modifier for grantRole()
+rule onlyRoleModifierCheckGrant(env e){
+    bytes32 role; address account;
+
+    _checkRole@withrevert(e, getRoleAdmin(role));
+    bool checkRevert = lastReverted;
+
+    grantRole@withrevert(e, role, account);
+    bool grantRevert = lastReverted;
+
+    assert checkRevert => grantRevert, "modifier goes bananas";
+}
+
+
+// STATUS - verified
+// check onlyRole modifier for revokeRole()
+rule onlyRoleModifierCheckRevoke(env e){
+    bytes32 role; address account;
+
+    _checkRole@withrevert(e, getRoleAdmin(role));
+    bool checkRevert = lastReverted;
+
+    revokeRole@withrevert(e, role, account);
+    bool revokeRevert = lastReverted;
+
+    assert checkRevert => revokeRevert, "modifier goes bananas";
+}
+
+
+// STATUS - verified
+// grantRole() does not affect another accounts 
+rule grantRoleEffect(env e){
+    bytes32 role; address account; 
+    bytes32 anotherRole; address nonEffectedAcc;
+    require account != nonEffectedAcc;
+
+    bool hasRoleBefore = hasRole(anotherRole, nonEffectedAcc);
+
+    grantRole(e, role, account);
+
+    bool hasRoleAfter = hasRole(anotherRole, nonEffectedAcc);
+
+    assert hasRoleBefore == hasRoleAfter, "modifier goes bananas";
+}
+
+
+// STATUS - verified
+// grantRole() does not affect another accounts 
+rule revokeRoleEffect(env e){
+    bytes32 role; address account; 
+    bytes32 anotherRole; address nonEffectedAcc;
+    require account != nonEffectedAcc;
+
+    bool hasRoleBefore = hasRole(anotherRole, nonEffectedAcc);
+
+    revokeRole(e, role, account);
+
+    bool hasRoleAfter = hasRole(anotherRole, nonEffectedAcc);
+
+    assert hasRoleBefore == hasRoleAfter, "modifier goes bananas";
+}
+
+
+
+
+
+
+
+
+
+
+