From 76866f30a0b8eace4887124463dbef37c25be006 Mon Sep 17 00:00:00 2001 From: miguelmtz <36620902+miguelmtzinf@users.noreply.github.com> Date: Mon, 29 Jan 2024 12:57:38 +0100 Subject: [PATCH] docs: Add Certora report to README (#384) * docs: Add Certora report for GSM * fix: Fix format --- .github/workflows/certora-gsm.yml | 5 ++--- README.md | 1 + certora/GSM/harness/OracleSwapFreezerHarness.sol | 2 +- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/.github/workflows/certora-gsm.yml b/.github/workflows/certora-gsm.yml index 9b8eb83b..028b1ceb 100644 --- a/.github/workflows/certora-gsm.yml +++ b/.github/workflows/certora-gsm.yml @@ -38,11 +38,11 @@ jobs: wget https://github.com/ethereum/solidity/releases/download/v0.8.10/solc-static-linux chmod +x solc-static-linux sudo mv solc-static-linux /usr/local/bin/solc8.10 - + - name: Install node dependencies run: | npm i - + - name: Verify rule ${{ matrix.rule }} run: | echo "key length" ${#CERTORAKEY} @@ -69,4 +69,3 @@ jobs: - non-4626/otakar-getAmount_properties.conf --rule getAssetAmountForBuyAsset_funcProperty_LR getAssetAmountForBuyAsset_funcProperty_RL - non-4626/otakar-finishedRules.conf --rule whoCanChangeExposure whoCanChangeAccruedFees sellingDoesntExceedExposureCap cantBuyOrSellWhenSeized giftingGhoDoesntAffectStorageSIMPLE giftingUnderlyingDoesntAffectStorageSIMPLE collectedBuyFeePlus1IsAtLeastAsRequired sellAssetSameAsGetGhoAmountForSellAsset collectedSellFeeIsAtLeastAsRequired collectedBuyFeeIsAtLeastAsRequired correctnessOfBuyAsset collectedBuyFeePlus2IsAtLeastAsRequired getAssetAmountForSellAsset_correctness cantBuyOrSellWhenFrozen whoCanChangeExposureCap cantSellIfExposureTooHigh sellAssetIncreasesExposure buyAssetDecreasesExposure rescuingGhoKeepsAccruedFees rescuingAssetKeepsAccruedFees - non-4626/otakar-OracleSwapFreezer.conf - diff --git a/README.md b/README.md index 64bbe1dd..0dc83f4f 100644 --- a/README.md +++ b/README.md @@ -45,6 +45,7 @@ You can find all audit reports under the [audits](./audits/) folder - [2023-06-13 - Sigma Prime (GhoSteward)](./audits/2023-06-13_GhoSteward_SigmaPrime.pdf) - [2023-09-20 - Emanuele Ricci @Stermi (GHO Stability Module)](./audits/2023-09-20_GSM_Stermi.pdf) - [2023-10-23 - Sigma Prime (GHO Stability Module)](./audits/2023-10-23_GSM_SigmaPrime.pdf) +- [2023-12-07 - Certora Formal Verification (GHO Stability Module)](./certora/reports/Formal_Verification_Report_of_GHO_Stability_Module.pdf) ## Getting Started diff --git a/certora/GSM/harness/OracleSwapFreezerHarness.sol b/certora/GSM/harness/OracleSwapFreezerHarness.sol index f0bee2f1..6a4de982 100644 --- a/certora/GSM/harness/OracleSwapFreezerHarness.sol +++ b/certora/GSM/harness/OracleSwapFreezerHarness.sol @@ -78,7 +78,7 @@ contract OracleSwapFreezerHarness is OracleSwapFreezer { return IPriceOracle(ADDRESS_PROVIDER.getPriceOracle()).getAssetPrice(UNDERLYING_ASSET); } - function hasRole() external view returns(bool) { + function hasRole() external view returns (bool) { return GSM.hasRole(GSM.SWAP_FREEZER_ROLE(), address(this)); } }