From 688a8ed9294e66bae34011cc02f8518d3c8a242a Mon Sep 17 00:00:00 2001 From: r4bbit <445106+0x-r4bbit@users.noreply.github.com> Date: Wed, 24 Jul 2024 18:50:18 +0200 Subject: [PATCH] Set up certora and implement first rules (#122) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Co-authored-by: 0xb337r007 <0xe4e5@proton.me> Co-authored-by: Adam Uhlíř --- .github/workflows/ci.yml | 43 +++++++++++++++++++++++++ .gitignore | 1 + Readme.md | 17 ++++++++++ certora/confs/Marketplace.conf | 21 ++++++++++++ certora/helpers/ERC20A.sol | 9 ++++++ certora/specs/Marketplace.spec | 58 ++++++++++++++++++++++++++++++++++ contracts/FuzzMarketplace.sol | 2 +- contracts/TestEndian.sol | 2 +- contracts/TestMarketplace.sol | 2 +- contracts/TestProofs.sol | 2 +- contracts/TestToken.sol | 2 +- package.json | 4 ++- 12 files changed, 157 insertions(+), 6 deletions(-) create mode 100644 certora/confs/Marketplace.conf create mode 100644 certora/helpers/ERC20A.sol create mode 100644 certora/specs/Marketplace.spec diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index 81f9820..9ce3d90 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -26,3 +26,46 @@ jobs: path: fuzzing/corpus key: fuzzing - run: npm run fuzz + + verify: + runs-on: ubuntu-latest + + steps: + - uses: actions/checkout@v4 + with: + submodules: recursive + + - name: Install Python + uses: actions/setup-python@v2 + with: { python-version: 3.9 } + + - name: Install Java + uses: actions/setup-java@v1 + with: { java-version: "11", java-package: jre } + + - name: Install Certora CLI + run: pip3 install certora-cli==7.6.3 + + - name: Install Solidity + run: | + wget https://github.com/ethereum/solidity/releases/download/v0.8.23/solc-static-linux + chmod +x solc-static-linux + sudo mv solc-static-linux /usr/local/bin/solc + + - name: "Install Node.js" + uses: "actions/setup-node@v3" + with: + cache: "npm" + node-version: "lts/*" + + - name: "Install the Node.js dependencies" + run: "npm install" + + - name: Verify rules + run: "npm run verify" + env: + CERTORAKEY: ${{ secrets.CERTORAKEY }} + + strategy: + fail-fast: false + max-parallel: 16 diff --git a/.gitignore b/.gitignore index c15ea20..f267262 100644 --- a/.gitignore +++ b/.gitignore @@ -3,3 +3,4 @@ cache artifacts deployment-localhost.json crytic-export +.certora_internal diff --git a/Readme.md b/Readme.md index 9e57bba..c5e8872 100644 --- a/Readme.md +++ b/Readme.md @@ -25,6 +25,23 @@ To start a local Ethereum node with the contracts deployed, execute: This will create a `deployment-localhost.json` file containing the addresses of the deployed contracts. + +Running the prover +------------------ + +To run the formal verification rules using Certora, first, make sure you have Java (JDK >= 11.0) installed on your machine, and then install the Certora CLI + +``` +$ pip install certora-cli +``` + +Once that is done the `certoraRun` command can be used to send CVL specs to the prover. + +You can run Certora's specs with the provided `npm` script: + + npm run verify + + Overview -------- diff --git a/certora/confs/Marketplace.conf b/certora/confs/Marketplace.conf new file mode 100644 index 0000000..5caa384 --- /dev/null +++ b/certora/confs/Marketplace.conf @@ -0,0 +1,21 @@ +{ + "files": [ + "contracts/Marketplace.sol", + "contracts/Groth16Verifier.sol", + "certora/helpers/ERC20A.sol", + ], + "parametric_contracts": ["Marketplace"], + "link" : [ + "Marketplace:_token=ERC20A", + "Marketplace:_verifier=Groth16Verifier" + ], + "msg": "Verifying Marketplace", + "rule_sanity": "basic", + "verify": "Marketplace:certora/specs/Marketplace.spec", + "optimistic_loop": true, + "loop_iter": "3", + "optimistic_hashing": true, + "hashing_length_bound": "512", +} + + diff --git a/certora/helpers/ERC20A.sol b/certora/helpers/ERC20A.sol new file mode 100644 index 0000000..cb42bf1 --- /dev/null +++ b/certora/helpers/ERC20A.sol @@ -0,0 +1,9 @@ +// SPDX-License-Identifier: MIT + +pragma solidity ^0.8.23; + +import {ERC20} from "@openzeppelin/contracts/token/ERC20/ERC20.sol"; + +contract ERC20A is ERC20 { + constructor(string memory name_, string memory symbol_) ERC20(name_, symbol_) {} +} diff --git a/certora/specs/Marketplace.spec b/certora/specs/Marketplace.spec new file mode 100644 index 0000000..af013bc --- /dev/null +++ b/certora/specs/Marketplace.spec @@ -0,0 +1,58 @@ +using ERC20A as Token; + +/*-------------------------------------------- +| Ghosts and hooks | +--------------------------------------------*/ + +ghost mathint totalReceived; + +hook Sload uint256 defaultValue currentContract._marketplaceTotals.received { + require totalReceived >= to_mathint(defaultValue); +} + +hook Sstore currentContract._marketplaceTotals.received uint256 defaultValue (uint256 defaultValue_old) { + totalReceived = totalReceived + defaultValue - defaultValue_old; +} + +ghost mathint totalSent; + +hook Sload uint256 defaultValue currentContract._marketplaceTotals.sent { + require totalSent >= to_mathint(defaultValue); +} + +hook Sstore currentContract._marketplaceTotals.sent uint256 defaultValue (uint256 defaultValue_old) { + totalSent = totalSent + defaultValue - defaultValue_old; +} + +/*-------------------------------------------- +| Properties | +--------------------------------------------*/ + +rule sanity(env e, method f) { + calldataarg args; + f(e, args); + assert true; + satisfy true; +} + +rule totalReceivedCannotDecrease(env e, method f) { + mathint total_before = totalReceived; + + calldataarg args; + f(e, args); + + mathint total_after = totalReceived; + + assert total_after >= total_before; +} + +rule totalSentCannotDecrease(env e, method f) { + mathint total_before = totalSent; + + calldataarg args; + f(e, args); + + mathint total_after = totalSent; + + assert total_after >= total_before; +} diff --git a/contracts/FuzzMarketplace.sol b/contracts/FuzzMarketplace.sol index d8f8f9a..9fe5c7d 100644 --- a/contracts/FuzzMarketplace.sol +++ b/contracts/FuzzMarketplace.sol @@ -1,5 +1,5 @@ // SPDX-License-Identifier: MIT -pragma solidity ^0.8.0; +pragma solidity ^0.8.23; import "./TestToken.sol"; import "./Marketplace.sol"; diff --git a/contracts/TestEndian.sol b/contracts/TestEndian.sol index 7ee7df9..5d1d33f 100644 --- a/contracts/TestEndian.sol +++ b/contracts/TestEndian.sol @@ -1,5 +1,5 @@ // SPDX-License-Identifier: MIT -pragma solidity ^0.8.0; +pragma solidity ^0.8.23; import "./Endian.sol"; diff --git a/contracts/TestMarketplace.sol b/contracts/TestMarketplace.sol index f67fa07..81b090a 100644 --- a/contracts/TestMarketplace.sol +++ b/contracts/TestMarketplace.sol @@ -1,5 +1,5 @@ // SPDX-License-Identifier: MIT -pragma solidity ^0.8.0; +pragma solidity ^0.8.23; import "./Marketplace.sol"; diff --git a/contracts/TestProofs.sol b/contracts/TestProofs.sol index a90e00f..ae34b24 100644 --- a/contracts/TestProofs.sol +++ b/contracts/TestProofs.sol @@ -1,5 +1,5 @@ // SPDX-License-Identifier: MIT -pragma solidity ^0.8.0; +pragma solidity ^0.8.23; import "./Proofs.sol"; diff --git a/contracts/TestToken.sol b/contracts/TestToken.sol index b7df313..5d3c6dd 100644 --- a/contracts/TestToken.sol +++ b/contracts/TestToken.sol @@ -1,5 +1,5 @@ // SPDX-License-Identifier: MIT -pragma solidity ^0.8.0; +pragma solidity ^0.8.23; import "@openzeppelin/contracts/token/ERC20/ERC20.sol"; diff --git a/package.json b/package.json index 062f110..cee7974 100644 --- a/package.json +++ b/package.json @@ -9,7 +9,9 @@ "format": "prettier --write contracts/**/*.sol test/**/*.js", "format:check": "prettier --check contracts/**/*.sol test/**/*.js", "lint": "solhint contracts/**.sol", - "deploy": "hardhat deploy" + "deploy": "hardhat deploy", + "verify": "npm run verify:marketplace", + "verify:marketplace": "certoraRun certora/confs/Marketplace.conf" }, "devDependencies": { "@nomiclabs/hardhat-ethers": "^2.2.1",