diff --git a/.github/workflows/certora.yml b/.github/workflows/certora.yml new file mode 100644 index 000000000..402149e56 --- /dev/null +++ b/.github/workflows/certora.yml @@ -0,0 +1,51 @@ +name: Certora + +on: + push: + branches: + - main + pull_request: + workflow_dispatch: + +jobs: + verify: + runs-on: ubuntu-latest + + strategy: + fail-fast: false + + matrix: + conf: + - AccrueInterest + - ConsistentState + - ExactMath + - ExitLiquidity + - Health + - LibSummary + - Liveness + - RatioMath + - Reentrancy + - Reverts + - Transfer + + steps: + - uses: actions/checkout@v3 + with: + submodules: recursive + + - name: Install python + uses: actions/setup-python@v4 + + - name: Install certora + run: pip install certora-cli + + - name: Install solc + run: | + wget https://github.com/ethereum/solidity/releases/download/v0.8.19/solc-static-linux + chmod +x solc-static-linux + sudo mv solc-static-linux /usr/local/bin/solc + + - name: Verify ${{ matrix.conf }} + run: certoraRun certora/confs/${{ matrix.conf }}.conf + env: + CERTORAKEY: ${{ secrets.CERTORAKEY }} diff --git a/.gitignore b/.gitignore index 6f198470a..84536674b 100644 --- a/.gitignore +++ b/.gitignore @@ -16,6 +16,10 @@ docs/ # Node modules /node_modules +# Certora +.certora** +emv-*-certora* + # Hardhat /types /cache_hardhat diff --git a/README.md b/README.md index 978c43a60..3164e4533 100644 --- a/README.md +++ b/README.md @@ -40,4 +40,4 @@ All audits are stored in the [audits](./audits/)' folder. ## Licences The primary license for Morpho Blue is the Business Source License 1.1 (`BUSL-1.1`), see [`LICENSE`](./LICENSE). -However, all files in the following folders can also be licensed under `GPL-2.0-or-later` (as indicated in their SPDX headers): [`src/interfaces`](./src/interfaces), [`src/libraries`](./src/libraries), [`src/mocks`](./src/mocks), [`test`](./test). +However, all files in the following folders can also be licensed under `GPL-2.0-or-later` (as indicated in their SPDX headers): [`src/interfaces`](./src/interfaces), [`src/libraries`](./src/libraries), [`src/mocks`](./src/mocks), [`test`](./test), [`certora`](./certora). diff --git a/certora/LICENSE b/certora/LICENSE new file mode 100644 index 000000000..aec4e2aca --- /dev/null +++ b/certora/LICENSE @@ -0,0 +1,389 @@ +This software is available under your choice of the GNU General Public +License, version 2 or later, or the Business Source License, as set +forth below. + + GNU GENERAL PUBLIC LICENSE + Version 2, June 1991 + + Copyright (C) 1989, 1991 Free Software Foundation, Inc., + 51 Franklin Street, Fifth Floor, Boston, MA 02110-1301 USA + Everyone is permitted to copy and distribute verbatim copies + of this license document, but changing it is not allowed. + + Preamble + + The licenses for most software are designed to take away your +freedom to share and change it. By contrast, the GNU General Public +License is intended to guarantee your freedom to share and change free +software--to make sure the software is free for all its users. This +General Public License applies to most of the Free Software +Foundation's software and to any other program whose authors commit to +using it. (Some other Free Software Foundation software is covered by +the GNU Lesser General Public License instead.) You can apply it to +your programs, too. + + When we speak of free software, we are referring to freedom, not +price. Our General Public Licenses are designed to make sure that you +have the freedom to distribute copies of free software (and charge for +this service if you wish), that you receive source code or can get it +if you want it, that you can change the software or use pieces of it +in new free programs; and that you know you can do these things. + + To protect your rights, we need to make restrictions that forbid +anyone to deny you these rights or to ask you to surrender the rights. +These restrictions translate to certain responsibilities for you if you +distribute copies of the software, or if you modify it. + + For example, if you distribute copies of such a program, whether +gratis or for a fee, you must give the recipients all the rights that +you have. You must make sure that they, too, receive or can get the +source code. And you must show them these terms so they know their +rights. + + We protect your rights with two steps: (1) copyright the software, and +(2) offer you this license which gives you legal permission to copy, +distribute and/or modify the software. + + Also, for each author's protection and ours, we want to make certain +that everyone understands that there is no warranty for this free +software. If the software is modified by someone else and passed on, we +want its recipients to know that what they have is not the original, so +that any problems introduced by others will not reflect on the original +authors' reputations. + + Finally, any free program is threatened constantly by software +patents. We wish to avoid the danger that redistributors of a free +program will individually obtain patent licenses, in effect making the +program proprietary. To prevent this, we have made it clear that any +patent must be licensed for everyone's free use or not licensed at all. + + The precise terms and conditions for copying, distribution and +modification follow. + + GNU GENERAL PUBLIC LICENSE + TERMS AND CONDITIONS FOR COPYING, DISTRIBUTION AND MODIFICATION + + 0. This License applies to any program or other work which contains +a notice placed by the copyright holder saying it may be distributed +under the terms of this General Public License. The "Program", below, +refers to any such program or work, and a "work based on the Program" +means either the Program or any derivative work under copyright law: +that is to say, a work containing the Program or a portion of it, +either verbatim or with modifications and/or translated into another +language. (Hereinafter, translation is included without limitation in +the term "modification".) Each licensee is addressed as "you". + +Activities other than copying, distribution and modification are not +covered by this License; they are outside its scope. The act of +running the Program is not restricted, and the output from the Program +is covered only if its contents constitute a work based on the +Program (independent of having been made by running the Program). +Whether that is true depends on what the Program does. + + 1. You may copy and distribute verbatim copies of the Program's +source code as you receive it, in any medium, provided that you +conspicuously and appropriately publish on each copy an appropriate +copyright notice and disclaimer of warranty; keep intact all the +notices that refer to this License and to the absence of any warranty; +and give any other recipients of the Program a copy of this License +along with the Program. + +You may charge a fee for the physical act of transferring a copy, and +you may at your option offer warranty protection in exchange for a fee. + + 2. You may modify your copy or copies of the Program or any portion +of it, thus forming a work based on the Program, and copy and +distribute such modifications or work under the terms of Section 1 +above, provided that you also meet all of these conditions: + + a) You must cause the modified files to carry prominent notices + stating that you changed the files and the date of any change. + + b) You must cause any work that you distribute or publish, that in + whole or in part contains or is derived from the Program or any + part thereof, to be licensed as a whole at no charge to all third + parties under the terms of this License. + + c) If the modified program normally reads commands interactively + when run, you must cause it, when started running for such + interactive use in the most ordinary way, to print or display an + announcement including an appropriate copyright notice and a + notice that there is no warranty (or else, saying that you provide + a warranty) and that users may redistribute the program under + these conditions, and telling the user how to view a copy of this + License. (Exception: if the Program itself is interactive but + does not normally print such an announcement, your work based on + the Program is not required to print an announcement.) + +These requirements apply to the modified work as a whole. If +identifiable sections of that work are not derived from the Program, +and can be reasonably considered independent and separate works in +themselves, then this License, and its terms, do not apply to those +sections when you distribute them as separate works. But when you +distribute the same sections as part of a whole which is a work based +on the Program, the distribution of the whole must be on the terms of +this License, whose permissions for other licensees extend to the +entire whole, and thus to each and every part regardless of who wrote it. + +Thus, it is not the intent of this section to claim rights or contest +your rights to work written entirely by you; rather, the intent is to +exercise the right to control the distribution of derivative or +collective works based on the Program. + +In addition, mere aggregation of another work not based on the Program +with the Program (or with a work based on the Program) on a volume of +a storage or distribution medium does not bring the other work under +the scope of this License. + + 3. You may copy and distribute the Program (or a work based on it, +under Section 2) in object code or executable form under the terms of +Sections 1 and 2 above provided that you also do one of the following: + + a) Accompany it with the complete corresponding machine-readable + source code, which must be distributed under the terms of Sections + 1 and 2 above on a medium customarily used for software interchange; or, + + b) Accompany it with a written offer, valid for at least three + years, to give any third party, for a charge no more than your + cost of physically performing source distribution, a complete + machine-readable copy of the corresponding source code, to be + distributed under the terms of Sections 1 and 2 above on a medium + customarily used for software interchange; or, + + c) Accompany it with the information you received as to the offer + to distribute corresponding source code. (This alternative is + allowed only for noncommercial distribution and only if you + received the program in object code or executable form with such + an offer, in accord with Subsection b above.) + +The source code for a work means the preferred form of the work for +making modifications to it. For an executable work, complete source +code means all the source code for all modules it contains, plus any +associated interface definition files, plus the scripts used to +control compilation and installation of the executable. However, as a +special exception, the source code distributed need not include +anything that is normally distributed (in either source or binary +form) with the major components (compiler, kernel, and so on) of the +operating system on which the executable runs, unless that component +itself accompanies the executable. + +If distribution of executable or object code is made by offering +access to copy from a designated place, then offering equivalent +access to copy the source code from the same place counts as +distribution of the source code, even though third parties are not +compelled to copy the source along with the object code. + + 4. You may not copy, modify, sublicense, or distribute the Program +except as expressly provided under this License. Any attempt +otherwise to copy, modify, sublicense or distribute the Program is +void, and will automatically terminate your rights under this License. +However, parties who have received copies, or rights, from you under +this License will not have their licenses terminated so long as such +parties remain in full compliance. + + 5. You are not required to accept this License, since you have not +signed it. However, nothing else grants you permission to modify or +distribute the Program or its derivative works. These actions are +prohibited by law if you do not accept this License. Therefore, by +modifying or distributing the Program (or any work based on the +Program), you indicate your acceptance of this License to do so, and +all its terms and conditions for copying, distributing or modifying +the Program or works based on it. + + 6. Each time you redistribute the Program (or any work based on the +Program), the recipient automatically receives a license from the +original licensor to copy, distribute or modify the Program subject to +these terms and conditions. You may not impose any further +restrictions on the recipients' exercise of the rights granted herein. +You are not responsible for enforcing compliance by third parties to +this License. + + 7. If, as a consequence of a court judgment or allegation of patent +infringement or for any other reason (not limited to patent issues), +conditions are imposed on you (whether by court order, agreement or +otherwise) that contradict the conditions of this License, they do not +excuse you from the conditions of this License. If you cannot +distribute so as to satisfy simultaneously your obligations under this +License and any other pertinent obligations, then as a consequence you +may not distribute the Program at all. For example, if a patent +license would not permit royalty-free redistribution of the Program by +all those who receive copies directly or indirectly through you, then +the only way you could satisfy both it and this License would be to +refrain entirely from distribution of the Program. + +If any portion of this section is held invalid or unenforceable under +any particular circumstance, the balance of the section is intended to +apply and the section as a whole is intended to apply in other +circumstances. + +It is not the purpose of this section to induce you to infringe any +patents or other property right claims or to contest validity of any +such claims; this section has the sole purpose of protecting the +integrity of the free software distribution system, which is +implemented by public license practices. Many people have made +generous contributions to the wide range of software distributed +through that system in reliance on consistent application of that +system; it is up to the author/donor to decide if he or she is willing +to distribute software through any other system and a licensee cannot +impose that choice. + +This section is intended to make thoroughly clear what is believed to +be a consequence of the rest of this License. + + 8. If the distribution and/or use of the Program is restricted in +certain countries either by patents or by copyrighted interfaces, the +original copyright holder who places the Program under this License +may add an explicit geographical distribution limitation excluding +those countries, so that distribution is permitted only in or among +countries not thus excluded. In such case, this License incorporates +the limitation as if written in the body of this License. + + 9. The Free Software Foundation may publish revised and/or new versions +of the General Public License from time to time. Such new versions will +be similar in spirit to the present version, but may differ in detail to +address new problems or concerns. + +Each version is given a distinguishing version number. If the Program +specifies a version number of this License which applies to it and "any +later version", you have the option of following the terms and conditions +either of that version or of any later version published by the Free +Software Foundation. If the Program does not specify a version number of +this License, you may choose any version ever published by the Free Software +Foundation. + + 10. If you wish to incorporate parts of the Program into other free +programs whose distribution conditions are different, write to the author +to ask for permission. For software which is copyrighted by the Free +Software Foundation, write to the Free Software Foundation; we sometimes +make exceptions for this. Our decision will be guided by the two goals +of preserving the free status of all derivatives of our free software and +of promoting the sharing and reuse of software generally. + + NO WARRANTY + + 11. BECAUSE THE PROGRAM IS LICENSED FREE OF CHARGE, THERE IS NO WARRANTY +FOR THE PROGRAM, TO THE EXTENT PERMITTED BY APPLICABLE LAW. EXCEPT WHEN +OTHERWISE STATED IN WRITING THE COPYRIGHT HOLDERS AND/OR OTHER PARTIES +PROVIDE THE PROGRAM "AS IS" WITHOUT WARRANTY OF ANY KIND, EITHER EXPRESSED +OR IMPLIED, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF +MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE. THE ENTIRE RISK AS +TO THE QUALITY AND PERFORMANCE OF THE PROGRAM IS WITH YOU. SHOULD THE +PROGRAM PROVE DEFECTIVE, YOU ASSUME THE COST OF ALL NECESSARY SERVICING, +REPAIR OR CORRECTION. + + 12. IN NO EVENT UNLESS REQUIRED BY APPLICABLE LAW OR AGREED TO IN WRITING +WILL ANY COPYRIGHT HOLDER, OR ANY OTHER PARTY WHO MAY MODIFY AND/OR +REDISTRIBUTE THE PROGRAM AS PERMITTED ABOVE, BE LIABLE TO YOU FOR DAMAGES, +INCLUDING ANY GENERAL, SPECIAL, INCIDENTAL OR CONSEQUENTIAL DAMAGES ARISING +OUT OF THE USE OR INABILITY TO USE THE PROGRAM (INCLUDING BUT NOT LIMITED +TO LOSS OF DATA OR DATA BEING RENDERED INACCURATE OR LOSSES SUSTAINED BY +YOU OR THIRD PARTIES OR A FAILURE OF THE PROGRAM TO OPERATE WITH ANY OTHER +PROGRAMS), EVEN IF SUCH HOLDER OR OTHER PARTY HAS BEEN ADVISED OF THE +POSSIBILITY OF SUCH DAMAGES. + + END OF TERMS AND CONDITIONS + + +Business Source License 1.1 + +License text copyright (c) 2017 MariaDB Corporation Ab, All Rights Reserved. +"Business Source License" is a trademark of MariaDB Corporation Ab. + +----------------------------------------------------------------------------- + +Parameters + +Licensor: Morpho Association + +Licensed Work: Morpho Blue Core + The Licensed Work is (c) 2023 Morpho Association + +Additional Use Grant: Any uses listed and defined at + morpho-blue-core-license-grants.morpho.eth + +Change Date: The earlier of (i) 2026-01-01, or (ii) a date specified + at morpho-blue-core-license-date.morpho.eth, or (iii) + upon the activation of the setFee function of the + Licensed Work’s applicable protocol smart contracts + deployed for production use. + +Change License: GNU General Public License v2.0 or later + +----------------------------------------------------------------------------- + +Terms + +The Licensor hereby grants you the right to copy, modify, create derivative +works, redistribute, and make non-production use of the Licensed Work. The +Licensor may make an Additional Use Grant, above, permitting limited +production use. + +Effective on the Change Date, or the fourth anniversary of the first publicly +available distribution of a specific version of the Licensed Work under this +License, whichever comes first, the Licensor hereby grants you rights under +the terms of the Change License, and the rights granted in the paragraph +above terminate. + +If your use of the Licensed Work does not comply with the requirements +currently in effect as described in this License, you must purchase a +commercial license from the Licensor, its affiliated entities, or authorized +resellers, or you must refrain from using the Licensed Work. + +All copies of the original and modified Licensed Work, and derivative works +of the Licensed Work, are subject to this License. This License applies +separately for each version of the Licensed Work and the Change Date may vary +for each version of the Licensed Work released by Licensor. + +You must conspicuously display this License on each original or modified copy +of the Licensed Work. If you receive the Licensed Work in original or +modified form from a third party, the terms and conditions set forth in this +License apply to your use of that work. + +Any use of the Licensed Work in violation of this License will automatically +terminate your rights under this License for the current and all other +versions of the Licensed Work. + +This License does not grant you any right in any trademark or logo of +Licensor or its affiliates (provided that you may use a trademark or logo of +Licensor as expressly required by this License). + +TO THE EXTENT PERMITTED BY APPLICABLE LAW, THE LICENSED WORK IS PROVIDED ON +AN "AS IS" BASIS. LICENSOR HEREBY DISCLAIMS ALL WARRANTIES AND CONDITIONS, +EXPRESS OR IMPLIED, INCLUDING (WITHOUT LIMITATION) WARRANTIES OF +MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE, NON-INFRINGEMENT, AND +TITLE. + +MariaDB hereby grants you permission to use this License’s text to license +your works, and to refer to it using the trademark "Business Source License", +as long as you comply with the Covenants of Licensor below. + +----------------------------------------------------------------------------- + +Covenants of Licensor + +In consideration of the right to use this License’s text and the "Business +Source License" name and trademark, Licensor covenants to MariaDB, and to all +other recipients of the licensed work to be provided by Licensor: + +1. To specify as the Change License the GPL Version 2.0 or any later version, + or a license that is compatible with GPL Version 2.0 or a later version, + where "compatible" means that software provided under the Change License can + be included in a program with software provided under GPL Version 2.0 or a + later version. Licensor may specify additional Change Licenses without + limitation. + +2. To either: (a) specify an additional grant of rights to use that does not + impose any additional restriction on the right granted in this License, as + the Additional Use Grant; or (b) insert the text "None". + +3. To specify a Change Date. + +4. Not to modify this License in any other way. + +----------------------------------------------------------------------------- + +Notice + +The Business Source License (this document, or the "License") is not an Open +Source license. However, the Licensed Work will eventually be made available +under an Open Source License, as stated in this License. diff --git a/certora/README.md b/certora/README.md new file mode 100644 index 000000000..29f44afbb --- /dev/null +++ b/certora/README.md @@ -0,0 +1,286 @@ +This folder contains the verification of the Morpho Blue protocol using CVL, Certora's Verification Language. + +The core concepts of the the Morpho Blue protocol are described in the [Whitepaper](../morpho-blue-whitepaper.pdf). +These concepts have been verified using CVL. +We first give a [high-level description](#high-level-description) of the verification and then describe the [folder and file structure](#folder-and-file-structure) of the specification files. + +# High-level description + +The Morpho Blue protocol allows users to take out collateralized loans on ERC20 tokens. + +## ERC20 tokens and transfers + +For a given market, Morpho Blue relies on the fact that the tokens involved respect the ERC20 standard. +In particular, in case of a transfer, it is assumed that the balance of Morpho Blue increases or decreases (depending if its the recipient or the sender) of the amount transferred. + +The file [Transfer.spec](specs/Transfer.spec) defines a summary of the transfer functions. +This summary is taken as the reference implementation to check that the balance of the Morpho Blue contract changes as expected. + +```solidity +function summarySafeTransferFrom(address token, address from, address to, uint256 amount) { + if (from == currentContract) { + balance[token] = require_uint256(balance[token] - amount); + } + if (to == currentContract) { + balance[token] = require_uint256(balance[token] + amount); + } +} +``` + +where `balance` is the ERC20 balance of the Morpho Blue contract. + +The verification is done for the most common implementations of the ERC20 standard, for which we distinguish three different implementations: + +- [ERC20Standard](dispatch/ERC20Standard.sol) which respects the standard and reverts in case of insufficient funds or in case of insufficient allowance. +- [ERC20NoRevert](dispatch/ERC20NoRevert.sol) which respects the standard but does not revert (and returns false instead). +- [ERC20USDT](dispatch/ERC20USDT.sol) which does not strictly respects the standard because it omits the return value of the `transfer` and `transferFrom` functions. + +Additionally, Morpho Blue always goes through a custom transfer library to handle ERC20 tokens, notably in all the above cases. +This library reverts when the transfer is not successful, and this is checked for the case of insufficient funds or insufficient allowance. +The use of the library can make it difficult for the provers, so the summary is sometimes used in other specification files to ease the verification of rules that rely on the transfer of tokens. + +## Markets + +The Morpho Blue contract is a singleton contract that defines different markets. +Markets on Morpho Blue depend on a pair of assets, the loan token that is supplied and borrowed, and the collateral token. +Taking out a loan requires to deposit some collateral, which stays idle in the contract. +Additionally, every loan token that is not borrowed also stays idle in the contract. +This is verified by the following property: + +```solidity +invariant idleAmountLessThanBalance(address token) + idleAmount[token] <= balance[token] +``` + +where `idleAmount` is the sum over all the markets of: the collateral amounts plus the supplied amounts minus the borrowed amounts. +In effect, this means that funds can only leave the contract through borrows and withdrawals. + +Additionally, it is checked that on a given market the borrowed amounts cannot exceed the supplied amounts. + +```solidity +invariant borrowLessThanSupply(MorphoHarness.Id id) + totalBorrowAssets(id) <= totalSupplyAssets(id); +``` + +This property, along with the previous one ensures that other markets can only impact the balance positively. +Said otherwise, markets are independent: tokens from a given market cannot be impacted by operations done in another market. + +## Shares + +When supplying on Morpho Blue, interest is earned over time, and the distribution is implemented through a shares mechanism. +Shares increase in value as interest is accrued. +The share mechanism is implemented symetrically for the borrow side: a share of borrow increasing in value over time represents additional owed interest. +The rule `accrueInterestIncreasesSupplyRatio` checks this property for the supply side with the following statement. + +```soldidity + // Check that the ratio increases: assetsBefore/sharesBefore <= assetsAfter/sharesAfter. + assert assetsBefore * sharesAfter <= assetsAfter * sharesBefore; +``` + +where `assetsBefore` and `sharesBefore` represents respectively the supplied assets and the supplied shares before accruing the interest. Similarly, `assetsAfter` and `sharesAfter` represent the supplied assets and shares after an interest accrual. + +The accounting of the shares mechanism relies on another variable to store the total number of shares, in order to compute what is the relative part of each user. +This variable needs to be kept up to date at each corresponding interaction, and it is checked that this accounting is done properly. +For example, for the supply side, this is done by the following invariant. + +```solidity +invariant sumSupplySharesCorrect(MorphoHarness.Id id) + to_mathint(totalSupplyShares(id)) == sumSupplyShares[id]; +``` + +where `sumSupplyShares` only exists in the specification, and is defined to be automatically updated whenever any of the shares of the users are modified. + +## Positions health and liquidations + +To ensure proper collateralization, a liquidation system is put in place, where unhealthy positions can be liquidated. +A position is said to be healthy if the ratio of the borrowed value over collateral value is smaller than the liquidation loan-to-value (LLTV) of that market. +This leaves a safety buffer before the position can be insolvent, where the aforementioned ratio is above 1. +To ensure that liquidators have the time to interact with unhealthy positions, it is formally verified that this buffer is respected. +Notably, it is verified that in the absence of accrued interest, which is the case when creating a new position or when interacting multiple times in the same block, a position cannot be made unhealthy. + +Let's define bad debt of a position as the amount borrowed when it is backed by no collateral. +Morpho Blue automatically realizes the bad debt when liquidating a position, by transferring it to the lenders. +In effect, this means that there is no bad debt on Morpho Blue, which is verified by the following invariant. + +```solidity +invariant alwaysCollateralized(MorphoHarness.Id id, address borrower) + borrowShares(id, borrower) != 0 => collateral(id, borrower) != 0; +``` + +More generally, this means that the result of liquidating a position multiple times eventually lead to a healthy position (possibly empty). + +## Authorization + +Morpho Blue also defines primitive authorization system, where users can authorize an account to fully manage their position. +This allows to rebuild more granular control of the position on top by authorizing an immutable contract with limited capabilities. +The authorization is verified to be sound in the sense that no user can modify the position of another user without proper authorization (except when liquidating). + +Let's detail the rule that makes sure that the supply side stays consistent. + +```solidity +rule userCannotLoseSupplyShares(env e, method f, calldataarg data) +filtered { f -> !f.isView } +{ + MorphoHarness.Id id; + address user; + + // Assume that the e.msg.sender is not authorized. + require !isAuthorized(user, e.msg.sender); + require user != e.msg.sender; + + mathint sharesBefore = supplyShares(id, user); + + f(e, data); + + mathint sharesAfter = supplyShares(id, user); + + assert sharesAfter >= sharesBefore; +} +``` + +In the previous rule, an arbitrary function of Morpho Blue `f` is called with arbitrary `data`. +Shares of `user` on the market identified by `id` are recorded before and after this call. +In this way, it is checked that the supply shares are increasing when the caller of the function is neither the owner of those shares (`user != e.msg.sender`) nor authorized (`!isAuthorized(user, e.msg.sender)`). + +## Other safety properties + +### Enabled LLTV and IRM + +Creating a market is permissionless on Morpho Blue, but some parameters should fall into the range of admitted values. +Notably, the LLTV value should be enabled beforehand. +The following rule checks that no market can ever exist with a LLTV that had not been previously approved. + +```solidity +invariant onlyEnabledLltv(MorphoHarness.MarketParams marketParams) + isCreated(libId(marketParams)) => isLltvEnabled(marketParams.lltv); +``` + +Similarly, the interest rate model (IRM) used for the market must have been previously whitelisted. + +### Range of the fee + +The governance can choose to set a fee to a given market. +Fees are guaranteed to never exceed 25% of the interest accrued, and this is verified by the following rule. + +```solidity +invariant feeInRange(MorphoHarness.Id id) + fee(id) <= maxFee(); +``` + +### Sanity checks and input validation + +The formal verification is also taking care of other sanity checks, some of which are needed properties to verify other rules. +For example, the following rule checks that the variable storing the last update time is no more than the current time. +This is a sanity check, but it is also useful to ensure that there will be no underflow when computing the time elapsed since the last update. + +```solidity +rule noTimeTravel(method f, env e, calldataarg args) +filtered { f -> !f.isView } +{ + MorphoHarness.Id id; + // Assume the property before the interaction. + require lastUpdate(id) <= e.block.timestamp; + f(e, args); + assert lastUpdate(id) <= e.block.timestamp; +} +``` + +Additional rules are verified to ensure that the sanitization of inputs is done correctly. + +```solidity +rule supplyInputValidation(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) { + supply@withrevert(e, marketParams, assets, shares, onBehalf, data); + assert !exactlyOneZero(assets, shares) || onBehalf == 0 => lastReverted; +} +``` + +The previous rule checks that the `supply` function reverts whenever the `onBehalf` parameter is the address zero, or when either both `assets` and `shares` are zero or both are non-zero. + +## Liveness properties + +On top of verifying that the protocol is secured, the verification also proves that it is usable. +Such properties are called liveness properties, and it is notably checked that the accounting is done when an interaction goes through. +As an example, the `withdrawChangesTokensAndShares` rule checks that calling the `withdraw` function successfully will decrease the shares of the concerned account and increase the balance of the receiver. + +Other liveness properties are verified as well. +Notably, it's also verified that it is always possible to exit a position without concern for the oracle. +This is done through the verification of two rules: the `canRepayAll` rule and the `canWithdrawCollateralAll` rule. +The `canRepayAll` rule ensures that it is always possible to repay the full debt of a position, leaving the account without any oustanding debt. +The `canWithdrawCollateralAll` rule ensures that in the case where the account has no outstanding debt, then it is possible to withdraw the full collateral. + +## Protection against common attack vectors + +Other common and known attack vectors are verified to not be possible on the Morpho Blue protocol. + +### Reentrancy + +Reentrancy is a common attack vector that happen when a call to a contract allows, when in a temporary state, to call the same contract again. +The state of the contract usually refers to the storage variables, which can typically hold values that are meant to be used only after the full execution of the current function. +The Morpho Blue contract is verified to not be vulnerable to this kind of reentrancy attack thanks to the rule `reentrancySafe`. + +### Extraction of value + +The Morpho Blue protocol uses a conservative approach to handle arithmetic operations. +Rounding is done such that potential (small) errors are in favor of the protocol, which ensures that it is not possible to extract value from other users. + +The rule `supplyWithdraw` handles the simple scenario of a supply followed by a withdraw, and has the following check. + +```solidity +assert withdrawnAssets <= suppliedAssets; +``` + +The rule `withdrawLiquidity` is more general and defines `owedAssets` as the assets that are owed to the user, rounding in favor of the protocol. +This rule has the following check to ensure that no more than the owed assets can be withdrawn. + +```solidity +assert withdrawnAssets <= owedAssets; +``` + +# Folder and file structure + +The [`certora/specs`](specs) folder contains the following files: + +- [`AccrueInterest.spec`](specs/AccrueInterest.spec) checks that the main functions accrue interest at the start of the interaction. + This is done by ensuring that accruing interest before calling the function does not change the outcome compared to just calling the function. + View functions do not necessarily respect this property (for example, `totalSupplyShares`), and are filtered out. +- [`ConsistentState.spec`](specs/ConsistentState.spec) checks that the state (storage) of the Morpho contract is consistent. + This includes checking that the accounting of the total amount and shares is correct, that markets are independent from each other, that only enabled IRMs and LLTVs can be used, and that users cannot have their position made worse by an unauthorized account. +- [`ExactMath.spec`](specs/ExactMath.spec) checks precise properties when taking into account exact multiplication and division. + Notably, this file specifies that using supply and withdraw in the same block cannot yield more funds than at the start. +- [`ExitLiquidity.spec`](specs/ExitLiquidity.spec) checks that when exiting a position with withdraw, withdrawCollateral, or repay, the user cannot get more than what was owed. +- [`Health.spec`](specs/Health.spec) checks properties about the health of the positions. + Notably, functions cannot render an account unhealthy, and debt positions always have some collateral (thanks to the bad debt realization mechanism). +- [`LibSummary.spec`](specs/LibSummary.spec) checks the summarization of the library functions that are used in other specification files. +- [`Liveness.spec`](specs/Liveness.spec) checks that main functions change the owner of funds and the amount of shares as expected, and that it's always possible to exit a position. +- [`RatioMath.spec`](specs/RatioMath.spec) checks that the ratio between shares and assets evolves predictably over time. +- [`Reentrancy.spec`](specs/Reentrancy.spec) checks that the contract is immune to a particular class of reentrancy issues. +- [`Reverts.spec`](specs/Reverts.spec) checks the condition for reverts and that inputs are correctly validated. +- [`Transfer.spec`](specs/Transfer.spec) checks the summarization of the safe transfer library functions that are used in other specification files. + +The [`certora/confs`](confs) folder contains a configuration file for each corresponding specification file. + +The [`certora/harness`](harness) folder contains contracts that enable the verification of Morpho Blue. +Notably, this allows handling the fact that library functions should be called from a contract to be verified independently, and it allows defining needed getters. + +The [`certora/dispatch`](dispatch) folder contains different contracts similar to the ones that are expected to be called from Morpho Blue. + +# Getting started + +Install `certora-cli` package with `pip install certora-cli`. +To verify specification files, pass to `certoraRun` the corresponding configuration file in the [`certora/confs`](confs) folder. +It requires having set the `CERTORAKEY` environment variable to a valid Certora key. +You can also pass additional arguments, notably to verify a specific rule. +For example, at the root of the repository: + +``` +certoraRun certora/confs/ConsistentState.conf --rule borrowLessThanSupply +``` + +The `certora-cli` package also includes a `certoraMutate` binary. +The file [`gambit.conf`](gambit.conf) provides a default configuration of the mutations. +You can test to mutate the code and check it against a particular specification. +For example, at the root of the repository: + +``` +certoraMutate --prover_conf certora/confs/ConsistentState.conf --mutation_conf certora/gambit.conf +``` diff --git a/certora/confs/AccrueInterest.conf b/certora/confs/AccrueInterest.conf new file mode 100644 index 000000000..a923c628e --- /dev/null +++ b/certora/confs/AccrueInterest.conf @@ -0,0 +1,12 @@ +{ + "files": [ + "certora/harness/MorphoHarness.sol" + ], + "verify": "MorphoHarness:certora/specs/AccrueInterest.spec", + "prover_args": [ + "-smt_hashingScheme plaininjectivity", + "-mediumTimeout 30" + ], + "rule_sanity": "basic", + "msg": "Morpho Blue Accrue Interest" +} diff --git a/certora/confs/ConsistentState.conf b/certora/confs/ConsistentState.conf new file mode 100644 index 000000000..9691cfcb1 --- /dev/null +++ b/certora/confs/ConsistentState.conf @@ -0,0 +1,8 @@ +{ + "files": [ + "certora/harness/MorphoHarness.sol" + ], + "verify": "MorphoHarness:certora/specs/ConsistentState.spec", + "rule_sanity": "basic", + "msg": "Morpho Blue Consistent State" +} diff --git a/certora/confs/ExactMath.conf b/certora/confs/ExactMath.conf new file mode 100644 index 000000000..26a0d6d2b --- /dev/null +++ b/certora/confs/ExactMath.conf @@ -0,0 +1,12 @@ +{ + "files": [ + "certora/harness/MorphoHarness.sol" + ], + "verify": "MorphoHarness:certora/specs/ExactMath.spec", + "rule_sanity": "basic", + "prover_args": [ + "-smt_hashingScheme plaininjectivity", + "-mediumTimeout 30" + ], + "msg": "Morpho Blue Exact Math" +} diff --git a/certora/confs/ExitLiquidity.conf b/certora/confs/ExitLiquidity.conf new file mode 100644 index 000000000..336359251 --- /dev/null +++ b/certora/confs/ExitLiquidity.conf @@ -0,0 +1,8 @@ +{ + "files": [ + "certora/harness/MorphoHarness.sol" + ], + "verify": "MorphoHarness:certora/specs/ExitLiquidity.spec", + "rule_sanity": "basic", + "msg": "Morpho Blue Exit Liquidity" +} diff --git a/certora/confs/Health.conf b/certora/confs/Health.conf new file mode 100644 index 000000000..a75fa1bb6 --- /dev/null +++ b/certora/confs/Health.conf @@ -0,0 +1,12 @@ +{ + "files": [ + "certora/harness/MorphoHarness.sol", + "src/mocks/OracleMock.sol" + ], + "verify": "MorphoHarness:certora/specs/Health.spec", + "rule_sanity": "basic", + "prover_args": [ + "-smt_hashingScheme plaininjectivity" + ], + "msg": "Morpho Blue Health" +} diff --git a/certora/confs/LibSummary.conf b/certora/confs/LibSummary.conf new file mode 100644 index 000000000..4aebed846 --- /dev/null +++ b/certora/confs/LibSummary.conf @@ -0,0 +1,8 @@ +{ + "files": [ + "certora/harness/MorphoHarness.sol" + ], + "verify": "MorphoHarness:certora/specs/LibSummary.spec", + "rule_sanity": "basic", + "msg": "Morpho Blue Lib Summary" +} diff --git a/certora/confs/Liveness.conf b/certora/confs/Liveness.conf new file mode 100644 index 000000000..2659b17b1 --- /dev/null +++ b/certora/confs/Liveness.conf @@ -0,0 +1,8 @@ +{ + "files": [ + "certora/harness/MorphoInternalAccess.sol" + ], + "verify": "MorphoInternalAccess:certora/specs/Liveness.spec", + "rule_sanity": "basic", + "msg": "Morpho Blue Liveness" +} diff --git a/certora/confs/RatioMath.conf b/certora/confs/RatioMath.conf new file mode 100644 index 000000000..700c436e2 --- /dev/null +++ b/certora/confs/RatioMath.conf @@ -0,0 +1,13 @@ +{ + "files": [ + "certora/harness/MorphoHarness.sol" + ], + "verify": "MorphoHarness:certora/specs/RatioMath.spec", + "rule_sanity": "basic", + "prover_args": [ + "-smt_hashingScheme plaininjectivity", + "-mediumTimeout 30", + "-timeout 3600" + ], + "msg": "Morpho Blue Ratio Math" +} diff --git a/certora/confs/Reentrancy.conf b/certora/confs/Reentrancy.conf new file mode 100644 index 000000000..0fe902cfb --- /dev/null +++ b/certora/confs/Reentrancy.conf @@ -0,0 +1,11 @@ +{ + "files": [ + "certora/harness/MorphoHarness.sol" + ], + "verify": "MorphoHarness:certora/specs/Reentrancy.spec", + "rule_sanity": "basic", + "prover_args": [ + "-enableStorageSplitting false" + ], + "msg": "Morpho Blue Reentrancy" +} diff --git a/certora/confs/Reverts.conf b/certora/confs/Reverts.conf new file mode 100644 index 000000000..92ce70bff --- /dev/null +++ b/certora/confs/Reverts.conf @@ -0,0 +1,8 @@ +{ + "files": [ + "certora/harness/MorphoHarness.sol" + ], + "verify": "MorphoHarness:certora/specs/Reverts.spec", + "rule_sanity": "basic", + "msg": "Morpho Blue Reverts" +} diff --git a/certora/confs/Transfer.conf b/certora/confs/Transfer.conf new file mode 100644 index 000000000..ac1bdeee1 --- /dev/null +++ b/certora/confs/Transfer.conf @@ -0,0 +1,11 @@ +{ + "files": [ + "certora/harness/TransferHarness.sol", + "certora/dispatch/ERC20Standard.sol", + "certora/dispatch/ERC20USDT.sol", + "certora/dispatch/ERC20NoRevert.sol" + ], + "verify": "TransferHarness:certora/specs/Transfer.spec", + "rule_sanity": "basic", + "msg": "Morpho Blue Transfer" +} diff --git a/certora/dispatch/ERC20NoRevert.sol b/certora/dispatch/ERC20NoRevert.sol new file mode 100644 index 000000000..b8dfccd1e --- /dev/null +++ b/certora/dispatch/ERC20NoRevert.sol @@ -0,0 +1,48 @@ +// SPDX-License-Identifier: GPL-2.0-or-later +pragma solidity ^0.8.0; + +contract ERC20NoRevert { + address public owner; + uint256 public totalSupply; + mapping(address => uint256) public balanceOf; + mapping(address => mapping(address => uint256)) public allowance; + + constructor() { + owner = msg.sender; + } + + modifier onlyOwner() { + require(msg.sender == owner); + _; + } + + function _transfer(address _from, address _to, uint256 _amount) internal returns (bool) { + if (balanceOf[_from] < _amount) { + return false; + } + balanceOf[_from] -= _amount; + balanceOf[_to] += _amount; + return true; + } + + function transfer(address _to, uint256 _amount) public returns (bool) { + return _transfer(msg.sender, _to, _amount); + } + + function transferFrom(address _from, address _to, uint256 _amount) public returns (bool) { + if (allowance[_from][msg.sender] < _amount) { + return false; + } + allowance[_from][msg.sender] -= _amount; + return _transfer(_from, _to, _amount); + } + + function approve(address _spender, uint256 _amount) public { + allowance[msg.sender][_spender] = _amount; + } + + function mint(address _receiver, uint256 _amount) public onlyOwner { + balanceOf[_receiver] += _amount; + totalSupply += _amount; + } +} diff --git a/certora/dispatch/ERC20Standard.sol b/certora/dispatch/ERC20Standard.sol new file mode 100644 index 000000000..71af6d9ca --- /dev/null +++ b/certora/dispatch/ERC20Standard.sol @@ -0,0 +1,42 @@ +// SPDX-License-Identifier: GPL-2.0-or-later +pragma solidity ^0.8.0; + +contract ERC20Standard { + address public owner; + uint256 public totalSupply; + mapping(address => uint256) public balanceOf; + mapping(address => mapping(address => uint256)) public allowance; + + constructor() { + owner = msg.sender; + } + + modifier onlyOwner() { + require(msg.sender == owner); + _; + } + + function _transfer(address _from, address _to, uint256 _amount) internal returns (bool) { + balanceOf[_from] -= _amount; + balanceOf[_to] += _amount; + return true; + } + + function transfer(address _to, uint256 _amount) public returns (bool) { + return _transfer(msg.sender, _to, _amount); + } + + function transferFrom(address _from, address _to, uint256 _amount) public returns (bool) { + allowance[_from][msg.sender] -= _amount; + return _transfer(_from, _to, _amount); + } + + function approve(address _spender, uint256 _amount) public { + allowance[msg.sender][_spender] = _amount; + } + + function mint(address _receiver, uint256 _amount) public onlyOwner { + balanceOf[_receiver] += _amount; + totalSupply += _amount; + } +} diff --git a/certora/dispatch/ERC20USDT.sol b/certora/dispatch/ERC20USDT.sol new file mode 100644 index 000000000..cce99353a --- /dev/null +++ b/certora/dispatch/ERC20USDT.sol @@ -0,0 +1,45 @@ +// SPDX-License-Identifier: GPL-2.0-or-later +pragma solidity ^0.8.0; + +contract ERC20USDT { + address public owner; + uint256 public totalSupply; + mapping(address => uint256) public balanceOf; + mapping(address => mapping(address => uint256)) public allowance; + + constructor() { + owner = msg.sender; + } + + modifier onlyOwner() { + require(msg.sender == owner); + _; + } + + function _transfer(address _from, address _to, uint256 _amount) internal { + balanceOf[_from] -= _amount; + balanceOf[_to] += _amount; + } + + function transfer(address _to, uint256 _amount) public { + _transfer(msg.sender, _to, _amount); + } + + function transferFrom(address _from, address _to, uint256 _amount) public { + if (allowance[_from][msg.sender] < type(uint256).max) { + allowance[_from][msg.sender] -= _amount; + } + _transfer(_from, _to, _amount); + } + + function approve(address _spender, uint256 _amount) public { + require(!((_amount != 0) && (allowance[msg.sender][_spender] != 0))); + + allowance[msg.sender][_spender] = _amount; + } + + function mint(address _receiver, uint256 _amount) public onlyOwner { + balanceOf[_receiver] += _amount; + totalSupply += _amount; + } +} diff --git a/certora/gambit.conf b/certora/gambit.conf new file mode 100644 index 000000000..0dcba742c --- /dev/null +++ b/certora/gambit.conf @@ -0,0 +1,6 @@ + { + "filename" : "../src/Morpho.sol", + "sourceroot": "..", + "num_mutants": 15, + "solc_remappings": [] +} diff --git a/certora/harness/MorphoHarness.sol b/certora/harness/MorphoHarness.sol new file mode 100644 index 000000000..1a1912aeb --- /dev/null +++ b/certora/harness/MorphoHarness.sol @@ -0,0 +1,92 @@ +// SPDX-License-Identifier: GPL-2.0-or-later +pragma solidity 0.8.19; + +import "../../src/Morpho.sol"; +import "../../src/libraries/SharesMathLib.sol"; +import "../../src/libraries/MarketParamsLib.sol"; + +contract MorphoHarness is Morpho { + using MarketParamsLib for MarketParams; + + constructor(address newOwner) Morpho(newOwner) {} + + function wad() external pure returns (uint256) { + return WAD; + } + + function maxFee() external pure returns (uint256) { + return MAX_FEE; + } + + function totalSupplyAssets(Id id) external view returns (uint256) { + return market[id].totalSupplyAssets; + } + + function totalSupplyShares(Id id) external view returns (uint256) { + return market[id].totalSupplyShares; + } + + function totalBorrowAssets(Id id) external view returns (uint256) { + return market[id].totalBorrowAssets; + } + + function totalBorrowShares(Id id) external view returns (uint256) { + return market[id].totalBorrowShares; + } + + function supplyShares(Id id, address account) external view returns (uint256) { + return position[id][account].supplyShares; + } + + function borrowShares(Id id, address account) external view returns (uint256) { + return position[id][account].borrowShares; + } + + function collateral(Id id, address account) external view returns (uint256) { + return position[id][account].collateral; + } + + function lastUpdate(Id id) external view returns (uint256) { + return market[id].lastUpdate; + } + + function fee(Id id) external view returns (uint256) { + return market[id].fee; + } + + function virtualTotalSupplyAssets(Id id) external view returns (uint256) { + return market[id].totalSupplyAssets + SharesMathLib.VIRTUAL_ASSETS; + } + + function virtualTotalSupplyShares(Id id) external view returns (uint256) { + return market[id].totalSupplyShares + SharesMathLib.VIRTUAL_SHARES; + } + + function virtualTotalBorrowAssets(Id id) external view returns (uint256) { + return market[id].totalBorrowAssets + SharesMathLib.VIRTUAL_ASSETS; + } + + function virtualTotalBorrowShares(Id id) external view returns (uint256) { + return market[id].totalBorrowShares + SharesMathLib.VIRTUAL_SHARES; + } + + function libId(MarketParams memory marketParams) external pure returns (Id) { + return marketParams.id(); + } + + function refId(MarketParams memory marketParams) external pure returns (Id marketParamsId) { + marketParamsId = Id.wrap(keccak256(abi.encode(marketParams))); + } + + function libMulDivUp(uint256 x, uint256 y, uint256 d) external pure returns (uint256) { + return MathLib.mulDivUp(x, y, d); + } + + function libMulDivDown(uint256 x, uint256 y, uint256 d) external pure returns (uint256) { + return MathLib.mulDivDown(x, y, d); + } + + function isHealthy(MarketParams memory marketParams, address user) external view returns (bool) { + return _isHealthy(marketParams, marketParams.id(), user); + } +} diff --git a/certora/harness/MorphoInternalAccess.sol b/certora/harness/MorphoInternalAccess.sol new file mode 100644 index 000000000..a4f7ecfa1 --- /dev/null +++ b/certora/harness/MorphoInternalAccess.sol @@ -0,0 +1,17 @@ +// SPDX-License-Identifier: GPL-2.0-or-later +pragma solidity 0.8.19; + +import "./MorphoHarness.sol"; + +contract MorphoInternalAccess is MorphoHarness { + constructor(address newOwner) MorphoHarness(newOwner) {} + + function update(Id id, uint256 timestamp) external { + market[id].lastUpdate = uint128(timestamp); + } + + function increaseInterest(Id id, uint128 interest) external { + market[id].totalBorrowAssets += interest; + market[id].totalSupplyAssets += interest; + } +} diff --git a/certora/harness/TransferHarness.sol b/certora/harness/TransferHarness.sol new file mode 100644 index 000000000..67a6d88c8 --- /dev/null +++ b/certora/harness/TransferHarness.sol @@ -0,0 +1,35 @@ +// SPDX-License-Identifier: GPL-2.0-or-later +pragma solidity ^0.8.12; + +import "../../src/libraries/SafeTransferLib.sol"; +import "../../src/interfaces/IERC20.sol"; + +interface IERC20Extended is IERC20 { + function balanceOf(address) external view returns (uint256); + function allowance(address, address) external view returns (uint256); + function totalSupply() external view returns (uint256); +} + +contract TransferHarness { + using SafeTransferLib for IERC20; + + function libSafeTransferFrom(address token, address from, address to, uint256 value) external { + IERC20(token).safeTransferFrom(from, to, value); + } + + function libSafeTransfer(address token, address to, uint256 value) external { + IERC20(token).safeTransfer(to, value); + } + + function balanceOf(address token, address user) external view returns (uint256) { + return IERC20Extended(token).balanceOf(user); + } + + function allowance(address token, address owner, address spender) external view returns (uint256) { + return IERC20Extended(token).allowance(owner, spender); + } + + function totalSupply(address token) external view returns (uint256) { + return IERC20Extended(token).totalSupply(); + } +} diff --git a/certora/specs/AccrueInterest.spec b/certora/specs/AccrueInterest.spec new file mode 100644 index 000000000..7babf38de --- /dev/null +++ b/certora/specs/AccrueInterest.spec @@ -0,0 +1,138 @@ +// SPDX-License-Identifier: GPL-2.0-or-later +methods { + function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE; + + function maxFee() external returns uint256 envfree; + + function MathLib.mulDivDown(uint256 a, uint256 b, uint256 c) internal returns uint256 => ghostMulDivDown(a,b,c); + function MathLib.mulDivUp(uint256 a, uint256 b, uint256 c) internal returns uint256 => ghostMulDivUp(a,b,c); + function MathLib.wTaylorCompounded(uint256 a, uint256 b) internal returns uint256 => ghostTaylorCompounded(a, b); + // We assume here that all external functions will not access storage, since we cannot show commutativity otherwise. + // We also need to assume that the price and borrow rate return always the same value (and do not depend on msg.origin), so we use ghost functions for them. + function _.borrowRate(MorphoHarness.MarketParams marketParams, MorphoHarness.Market market) external with (env e) => ghostBorrowRate(marketParams.irm, e.block.timestamp) expect uint256; + function _.price() external with (env e) => ghostOraclePrice(e.block.timestamp) expect uint256; + function _.transfer(address to, uint256 amount) external => ghostTransfer(to, amount) expect bool; + function _.transferFrom(address from, address to, uint256 amount) external => ghostTransferFrom(from, to, amount) expect bool; + function _.onMorphoLiquidate(uint256, bytes) external => NONDET; + function _.onMorphoRepay(uint256, bytes) external => NONDET; + function _.onMorphoSupply(uint256, bytes) external => NONDET; + function _.onMorphoSupplyCollateral(uint256, bytes) external => NONDET; + function _.onMorphoFlashLoan(uint256, bytes) external => NONDET; +} + +ghost ghostMulDivUp(uint256, uint256, uint256) returns uint256; +ghost ghostMulDivDown(uint256, uint256, uint256) returns uint256; +ghost ghostTaylorCompounded(uint256, uint256) returns uint256; +ghost ghostBorrowRate(address, uint256) returns uint256; +ghost ghostOraclePrice(uint256) returns uint256; +ghost ghostTransfer(address, uint256) returns bool; +ghost ghostTransferFrom(address, address, uint256) returns bool; + + +// Check that calling accrueInterest first has no effect. +// This is because supply should call accrueInterest itself. +rule supplyAccruesInterest(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) { + // Safe require because timestamps cannot realistically be that large. + require e.block.timestamp < 2^128; + + storage init = lastStorage; + + accrueInterest(e, marketParams); + supply(e, marketParams, assets, shares, onBehalf, data); + storage afterBoth = lastStorage; + + supply(e, marketParams, assets, shares, onBehalf, data) at init; + storage afterOne = lastStorage; + + assert afterBoth == afterOne; +} + +// Check that calling accrueInterest first has no effect. +// This is because withdraw should call accrueInterest itself. +rule withdrawAccruesInterest(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) { + // Safe require because timestamps cannot realistically be that large. + require e.block.timestamp < 2^128; + + storage init = lastStorage; + + accrueInterest(e, marketParams); + withdraw(e, marketParams, assets, shares, onBehalf, receiver); + storage afterBoth = lastStorage; + + withdraw(e, marketParams, assets, shares, onBehalf, receiver) at init; + storage afterOne = lastStorage; + + assert afterBoth == afterOne; +} + +// Check that calling accrueInterest first has no effect. +// This is because borrow should call accrueInterest itself. +rule borrowAccruesInterest(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) { + // Safe require because timestamps cannot realistically be that large. + require e.block.timestamp < 2^128; + + storage init = lastStorage; + + accrueInterest(e, marketParams); + borrow(e, marketParams, assets, shares, onBehalf, receiver); + storage afterBoth = lastStorage; + + borrow(e, marketParams, assets, shares, onBehalf, receiver) at init; + storage afterOne = lastStorage; + + assert afterBoth == afterOne; +} + +// Check that calling accrueInterest first has no effect. +// This is because repay should call accrueInterest itself. +rule repayAccruesInterest(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) { + // Safe require because timestamps cannot realistically be that large. + require e.block.timestamp < 2^128; + + storage init = lastStorage; + + accrueInterest(e, marketParams); + repay(e, marketParams, assets, shares, onBehalf, data); + storage afterBoth = lastStorage; + + repay(e, marketParams, assets, shares, onBehalf, data) at init; + storage afterOne = lastStorage; + + assert afterBoth == afterOne; +} + +// Show that accrueInterest commutes with other state changing rules. +// We exclude view functions, because: +// (a) we cannot check the return value and for storage commutativity is trivial, and +// (b) most view functions, e.g. totalSupplyShares, are not commutative, i.e. they return a different value if called before accrueInterest is called. +// We also exclude setFeeRecipient, as it is known to be not commutative. +rule accrueInterestCommutesExceptForSetFeeRecipient(method f, calldataarg args) +filtered { + f -> !f.isView && f.selector != sig:setFeeRecipient(address).selector +} +{ + env e1; + env e2; + MorphoHarness.MarketParams marketParams; + + // Assume interactions to happen at the same block. + require e1.block.timestamp == e2.block.timestamp; + // Safe require because timestamps cannot realistically be that large. + require e1.block.timestamp < 2^128; + + storage init = lastStorage; + + accrueInterest(e1, marketParams); + f@withrevert(e2, args); + bool revert1 = lastReverted; + storage store1 = lastStorage; + + + f@withrevert(e2, args) at init; + bool revert2 = lastReverted; + accrueInterest(e1, marketParams); + storage store2 = lastStorage; + + assert revert1 <=> revert2; + assert store1 == store2; +} diff --git a/certora/specs/ConsistentState.spec b/certora/specs/ConsistentState.spec new file mode 100644 index 000000000..97083a02d --- /dev/null +++ b/certora/specs/ConsistentState.spec @@ -0,0 +1,294 @@ +// SPDX-License-Identifier: GPL-2.0-or-later +methods { + function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE; + + function supplyShares(MorphoHarness.Id, address) external returns uint256 envfree; + function borrowShares(MorphoHarness.Id, address) external returns uint256 envfree; + function collateral(MorphoHarness.Id, address) external returns uint256 envfree; + function totalSupplyAssets(MorphoHarness.Id) external returns uint256 envfree; + function totalSupplyShares(MorphoHarness.Id) external returns uint256 envfree; + function totalBorrowAssets(MorphoHarness.Id) external returns uint256 envfree; + function totalBorrowShares(MorphoHarness.Id) external returns uint256 envfree; + function fee(MorphoHarness.Id) external returns uint256 envfree; + function lastUpdate(MorphoHarness.Id) external returns uint256 envfree; + function isIrmEnabled(address) external returns bool envfree; + function isLltvEnabled(uint256) external returns bool envfree; + function isAuthorized(address, address) external returns bool envfree; + + function maxFee() external returns uint256 envfree; + function wad() external returns uint256 envfree; + function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; + + function _.borrowRate(MorphoHarness.MarketParams, MorphoHarness.Market) external => HAVOC_ECF; + + function SafeTransferLib.safeTransfer(address token, address to, uint256 value) internal => summarySafeTransferFrom(token, currentContract, to, value); + function SafeTransferLib.safeTransferFrom(address token, address from, address to, uint256 value) internal => summarySafeTransferFrom(token, from, to, value); +} + +ghost mapping(MorphoHarness.Id => mathint) sumSupplyShares { + init_state axiom (forall MorphoHarness.Id id. sumSupplyShares[id] == 0); +} + +ghost mapping(MorphoHarness.Id => mathint) sumBorrowShares { + init_state axiom (forall MorphoHarness.Id id. sumBorrowShares[id] == 0); +} + +ghost mapping(MorphoHarness.Id => mathint) sumCollateral { + init_state axiom (forall MorphoHarness.Id id. sumCollateral[id] == 0); +} + +ghost mapping(address => mathint) balance { + init_state axiom (forall address token. balance[token] == 0); +} + +ghost mapping(address => mathint) idleAmount { + init_state axiom (forall address token. idleAmount[token] == 0); +} + +ghost mapping(MorphoHarness.Id => address) idToBorrowable; + +ghost mapping(MorphoHarness.Id => address) idToCollateral; + +hook Sstore idToMarketParams[KEY MorphoHarness.Id id].loanToken address token STORAGE { + idToBorrowable[id] = token; +} + +hook Sstore idToMarketParams[KEY MorphoHarness.Id id].collateralToken address token STORAGE { + idToCollateral[id] = token; +} + +hook Sstore position[KEY MorphoHarness.Id id][KEY address owner].supplyShares uint256 newShares (uint256 oldShares) STORAGE { + sumSupplyShares[id] = sumSupplyShares[id] - oldShares + newShares; +} + +hook Sstore position[KEY MorphoHarness.Id id][KEY address owner].borrowShares uint128 newShares (uint128 oldShares) STORAGE { + sumBorrowShares[id] = sumBorrowShares[id] - oldShares + newShares; +} + +hook Sstore position[KEY MorphoHarness.Id id][KEY address owner].collateral uint128 newAmount (uint128 oldAmount) STORAGE { + sumCollateral[id] = sumCollateral[id] - oldAmount + newAmount; + idleAmount[idToCollateral[id]] = idleAmount[idToCollateral[id]] - oldAmount + newAmount; +} + +hook Sstore market[KEY MorphoHarness.Id id].totalSupplyAssets uint128 newAmount (uint128 oldAmount) STORAGE { + idleAmount[idToBorrowable[id]] = idleAmount[idToBorrowable[id]] - oldAmount + newAmount; +} + +hook Sstore market[KEY MorphoHarness.Id id].totalBorrowAssets uint128 newAmount (uint128 oldAmount) STORAGE { + idleAmount[idToBorrowable[id]] = idleAmount[idToBorrowable[id]] + oldAmount - newAmount; +} + +function summarySafeTransferFrom(address token, address from, address to, uint256 amount) { + if (from == currentContract) { + // Safe require because the reference implementation would revert. + balance[token] = require_uint256(balance[token] - amount); + } + if (to == currentContract) { + // Safe require because the reference implementation would revert. + balance[token] = require_uint256(balance[token] + amount); + } +} + +definition isCreated(MorphoHarness.Id id) returns bool = + lastUpdate(id) != 0; + +// Check that the fee is always lower than the max fee constant. +invariant feeInRange(MorphoHarness.Id id) + fee(id) <= maxFee(); + +// Check that the accounting of totalSupplyShares is correct. +invariant sumSupplySharesCorrect(MorphoHarness.Id id) + to_mathint(totalSupplyShares(id)) == sumSupplyShares[id]; + +// Check that the accounting of totalBorrowShares is correct. +invariant sumBorrowSharesCorrect(MorphoHarness.Id id) + to_mathint(totalBorrowShares(id)) == sumBorrowShares[id]; + +// Check that a market only allows borrows up to the total supply. +// This invariant shows that markets are independent, tokens from one market cannot be taken by interacting with another market. +invariant borrowLessThanSupply(MorphoHarness.Id id) + totalBorrowAssets(id) <= totalSupplyAssets(id); + +// This invariant is useful in the following rule, to link an id back to a market. +invariant marketInvariant(MorphoHarness.MarketParams marketParams) + isCreated(libId(marketParams)) => + idToBorrowable[libId(marketParams)] == marketParams.loanToken && + idToCollateral[libId(marketParams)] == marketParams.collateralToken; + +// Check that the idle amount on the singleton is greater to the sum amount, that is the sum over all the markets of the total supply plus the total collateral minus the total borrow. +invariant idleAmountLessThanBalance(address token) + idleAmount[token] <= balance[token] +{ + // Safe requires on the sender because the contract cannot call the function itself. + preserved supply(MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) with (env e) { + requireInvariant marketInvariant(marketParams); + require e.msg.sender != currentContract; + } + preserved withdraw(MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) with (env e) { + requireInvariant marketInvariant(marketParams); + require e.msg.sender != currentContract; + } + preserved borrow(MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) with (env e) { + requireInvariant marketInvariant(marketParams); + require e.msg.sender != currentContract; + } + preserved repay(MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) with (env e) { + requireInvariant marketInvariant(marketParams); + require e.msg.sender != currentContract; + } + preserved supplyCollateral(MorphoHarness.MarketParams marketParams, uint256 assets, address onBehalf, bytes data) with (env e) { + requireInvariant marketInvariant(marketParams); + require e.msg.sender != currentContract; + } + preserved withdrawCollateral(MorphoHarness.MarketParams marketParams, uint256 assets, address onBehalf, address receiver) with (env e) { + requireInvariant marketInvariant(marketParams); + require e.msg.sender != currentContract; + } + preserved liquidate(MorphoHarness.MarketParams marketParams, address _b, uint256 shares, uint256 receiver, bytes data) with (env e) { + requireInvariant marketInvariant(marketParams); + require e.msg.sender != currentContract; + } +} + +// Check that a market can only exist if its LLTV is enabled. +invariant onlyEnabledLltv(MorphoHarness.MarketParams marketParams) + isCreated(libId(marketParams)) => isLltvEnabled(marketParams.lltv); + +invariant lltvSmallerThanWad(uint256 lltv) + isLltvEnabled(lltv) => lltv < wad(); + +// Check that a market can only exist if its IRM is enabled. +invariant onlyEnabledIrm(MorphoHarness.MarketParams marketParams) + isCreated(libId(marketParams)) => isIrmEnabled(marketParams.irm); + +// Check the pseudo-injectivity of the hashing function id(). +rule libIdUnique() { + MorphoHarness.MarketParams marketParams1; + MorphoHarness.MarketParams marketParams2; + + // Assume that arguments are the same. + require libId(marketParams1) == libId(marketParams2); + + assert marketParams1.loanToken == marketParams2.loanToken; + assert marketParams1.collateralToken == marketParams2.collateralToken; + assert marketParams1.oracle == marketParams2.oracle; + assert marketParams1.irm == marketParams2.irm; + assert marketParams1.lltv == marketParams2.lltv; +} + +// Check that only the user is able to change who is authorized to manage his position. +rule onlyUserCanAuthorizeWithoutSig(env e, method f, calldataarg data) +filtered { + f -> !f.isView && f.selector != sig:setAuthorizationWithSig(MorphoHarness.Authorization memory, MorphoHarness.Signature calldata).selector +} +{ + address user; + address someone; + + // Assume that it is another user that is interacting with Morpho. + require user != e.msg.sender; + + bool authorizedBefore = isAuthorized(user, someone); + + f(e, data); + + bool authorizedAfter = isAuthorized(user, someone); + + assert authorizedAfter == authorizedBefore; +} + +// Check that only authorized users are able to decrease supply shares of a position. +rule userCannotLoseSupplyShares(env e, method f, calldataarg data) +filtered { f -> !f.isView } +{ + MorphoHarness.Id id; + address user; + + // Assume that the e.msg.sender is not authorized. + require !isAuthorized(user, e.msg.sender); + require user != e.msg.sender; + + mathint sharesBefore = supplyShares(id, user); + + f(e, data); + + mathint sharesAfter = supplyShares(id, user); + + assert sharesAfter >= sharesBefore; +} + +// Check that only authorized users are able to increase the borrow shares of a position. +rule userCannotGainBorrowShares(env e, method f, calldataarg args) +filtered { f -> !f.isView } +{ + MorphoHarness.Id id; + address user; + + // Assume that the e.msg.sender is not authorized. + require !isAuthorized(user, e.msg.sender); + require user != e.msg.sender; + + mathint sharesBefore = borrowShares(id, user); + + f(e, args); + + mathint sharesAfter = borrowShares(id, user); + + assert sharesAfter <= sharesBefore; +} + +// Check that users cannot lose collateral by unauthorized parties except in case of a liquidation. +rule userCannotLoseCollateralExceptLiquidate(env e, method f, calldataarg args) +filtered { + f -> !f.isView && + f.selector != sig:liquidate(MorphoHarness.MarketParams, address, uint256, uint256, bytes).selector +} +{ + MorphoHarness.Id id; + address user; + + // Assume that the e.msg.sender is not authorized. + require !isAuthorized(user, e.msg.sender); + require user != e.msg.sender; + + mathint collateralBefore = collateral(id, user); + + f(e, args); + + mathint collateralAfter = collateral(id, user); + + assert collateralAfter >= collateralBefore; +} + +// Check that users cannot lose collateral by unauthorized parties if they have no outstanding debt. +rule userWithoutBorrowCannotLoseCollateral(env e, method f, calldataarg args) +filtered { f -> !f.isView } +{ + MorphoHarness.Id id; + address user; + + // Assume that the e.msg.sender is not authorized. + require !isAuthorized(user, e.msg.sender); + require user != e.msg.sender; + // Assume that the user has no outstanding debt. + require borrowShares(id, user) == 0; + + mathint collateralBefore = collateral(id, user); + + f(e, args); + + mathint collateralAfter = collateral(id, user); + + assert collateralAfter >= collateralBefore; +} + +// Invariant checking that the last updated time is never greater than the current time. +rule noTimeTravel(method f, env e, calldataarg args) +filtered { f -> !f.isView } +{ + MorphoHarness.Id id; + // Assume the property before the interaction. + require lastUpdate(id) <= e.block.timestamp; + f(e, args); + assert lastUpdate(id) <= e.block.timestamp; +} diff --git a/certora/specs/ExactMath.spec b/certora/specs/ExactMath.spec new file mode 100644 index 000000000..d25465c25 --- /dev/null +++ b/certora/specs/ExactMath.spec @@ -0,0 +1,123 @@ +// SPDX-License-Identifier: GPL-2.0-or-later +methods { + function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE; + + function feeRecipient() external returns address envfree; + function supplyShares(MorphoHarness.Id, address) external returns uint256 envfree; + function borrowShares(MorphoHarness.Id, address) external returns uint256 envfree; + function virtualTotalSupplyAssets(MorphoHarness.Id) external returns uint256 envfree; + function virtualTotalSupplyShares(MorphoHarness.Id) external returns uint256 envfree; + function virtualTotalBorrowAssets(MorphoHarness.Id) external returns uint256 envfree; + function virtualTotalBorrowShares(MorphoHarness.Id) external returns uint256 envfree; + function lastUpdate(MorphoHarness.Id) external returns uint256 envfree; + function fee(MorphoHarness.Id) external returns uint256 envfree; + + function maxFee() external returns uint256 envfree; + function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; + + function MathLib.mulDivDown(uint256 a, uint256 b, uint256 c) internal returns uint256 => summaryMulDivDown(a,b,c); + function MathLib.mulDivUp(uint256 a, uint256 b, uint256 c) internal returns uint256 => summaryMulDivUp(a,b,c); + function SafeTransferLib.safeTransfer(address token, address to, uint256 value) internal => NONDET; + function SafeTransferLib.safeTransferFrom(address token, address from, address to, uint256 value) internal => NONDET; + function _.onMorphoSupply(uint256 assets, bytes data) external => HAVOC_ECF; +} + +function summaryMulDivUp(uint256 x, uint256 y, uint256 d) returns uint256 { + // Safe require because the reference implementation would revert. + return require_uint256((x * y + (d - 1)) / d); +} + +function summaryMulDivDown(uint256 x, uint256 y, uint256 d) returns uint256 { + // Safe require because the reference implementation would revert. + return require_uint256((x * y) / d); +} + +// Check that when not accruing interest, and when repaying all, the borrow ratio is at least reset to the initial ratio. +// More details on the purpose of this rule in RatioMath.spec. +rule repayAllResetsBorrowRatio(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) { + MorphoHarness.Id id = libId(marketParams); + // Safe require because this invariant is checked in ConsistentState.spec + require fee(id) <= maxFee(); + + mathint assetsBefore = virtualTotalBorrowAssets(id); + mathint sharesBefore = virtualTotalBorrowShares(id); + + // Assume no interest as it would increase the borrowed assets. + require lastUpdate(id) == e.block.timestamp; + + mathint repaidAssets; + repaidAssets, _ = repay(e, marketParams, assets, shares, onBehalf, data); + + // Check the case where the market is fully repaid. + require repaidAssets >= assetsBefore; + + mathint assetsAfter = virtualTotalBorrowAssets(id); + mathint sharesAfter = virtualTotalBorrowShares(id); + + assert assetsAfter == 1; + // There are at least as many shares as virtual shares. +} + +// There should be no profit from supply followed immediately by withdraw. +rule supplyWithdraw() { + MorphoHarness.MarketParams marketParams; + MorphoHarness.Id id = libId(marketParams); + env e1; + env e2; + address onBehalf; + + // Assume that interactions happen at the same block. + require e1.block.timestamp == e2.block.timestamp; + // Assume that the user starts without any supply position. + require supplyShares(id, onBehalf) == 0; + // Assume that the user is not the fee recipient, otherwise the gain can come from the fee. + require onBehalf != feeRecipient(); + // Safe require because timestamps cannot realistically be that large. + require e1.block.timestamp < 2^128; + + uint256 supplyAssets; uint256 supplyShares; bytes data; + uint256 suppliedAssets; + uint256 suppliedShares; + suppliedAssets, suppliedShares = supply(e1, marketParams, supplyAssets, supplyShares, onBehalf, data); + + // Hints for the prover. + assert suppliedAssets * (virtualTotalSupplyShares(id) - suppliedShares) >= suppliedShares * (virtualTotalSupplyAssets(id) - suppliedAssets); + assert suppliedAssets * virtualTotalSupplyShares(id) >= suppliedShares * virtualTotalSupplyAssets(id); + + uint256 withdrawAssets; uint256 withdrawShares; address receiver; + uint256 withdrawnAssets; + withdrawnAssets, _ = withdraw(e2, marketParams, withdrawAssets, withdrawShares, onBehalf, receiver); + + assert withdrawnAssets <= suppliedAssets; +} + +// There should be no profit from borrow followed immediately by repaying all. +rule borrowRepay() { + MorphoHarness.MarketParams marketParams; + MorphoHarness.Id id = libId(marketParams); + address onBehalf; + env e1; + env e2; + + // Assume interactions happen at the same block. + require e1.block.timestamp == e2.block.timestamp; + // Assume that the user starts without any borrow position. + require borrowShares(id, onBehalf) == 0; + // Safe require because timestamps cannot realistically be that large. + require e1.block.timestamp < 2^128; + + uint256 borrowAssets; uint256 borrowShares; address receiver; + uint256 borrowedAssets; + uint256 borrowedShares; + borrowedAssets, borrowedShares = borrow(e2, marketParams, borrowAssets, borrowShares, onBehalf, receiver); + + // Hints for the prover. + assert borrowedAssets * (virtualTotalBorrowShares(id) - borrowedShares) <= borrowedShares * (virtualTotalBorrowAssets(id) - borrowedAssets); + assert borrowedAssets * virtualTotalBorrowShares(id) <= borrowedShares * virtualTotalBorrowAssets(id); + + bytes data; + uint256 repaidAssets; + repaidAssets, _ = repay(e1, marketParams, 0, borrowedShares, onBehalf, data); + + assert borrowedAssets <= repaidAssets; +} diff --git a/certora/specs/ExitLiquidity.spec b/certora/specs/ExitLiquidity.spec new file mode 100644 index 000000000..73c5af58c --- /dev/null +++ b/certora/specs/ExitLiquidity.spec @@ -0,0 +1,70 @@ +// SPDX-License-Identifier: GPL-2.0-or-later +methods { + function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE; + + function supplyShares(MorphoHarness.Id, address) external returns uint256 envfree; + function borrowShares(MorphoHarness.Id, address) external returns uint256 envfree; + function collateral(MorphoHarness.Id, address) external returns uint256 envfree; + function virtualTotalSupplyAssets(MorphoHarness.Id) external returns uint256 envfree; + function virtualTotalSupplyShares(MorphoHarness.Id) external returns uint256 envfree; + function virtualTotalBorrowAssets(MorphoHarness.Id) external returns uint256 envfree; + function virtualTotalBorrowShares(MorphoHarness.Id) external returns uint256 envfree; + function lastUpdate(MorphoHarness.Id) external returns uint256 envfree; + + function libMulDivDown(uint256, uint256, uint256) external returns uint256 envfree; + function libMulDivUp(uint256, uint256, uint256) external returns uint256 envfree; + function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; +} + +// Check that it's not possible to withdraw more assets than what the user owns. +rule withdrawLiquidity(MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) { + env e; + MorphoHarness.Id id = libId(marketParams); + + // Assume no interest as it would increase the total supply assets. + require lastUpdate(id) == e.block.timestamp; + + uint256 initialShares = supplyShares(id, onBehalf); + uint256 initialTotalSupply = virtualTotalSupplyAssets(id); + uint256 initialTotalSupplyShares = virtualTotalSupplyShares(id); + uint256 ownedAssets = libMulDivDown(initialShares, initialTotalSupply, initialTotalSupplyShares); + + uint256 withdrawnAssets; + withdrawnAssets, _ = withdraw(e, marketParams, assets, shares, onBehalf, receiver); + + assert withdrawnAssets <= ownedAssets; +} + +// Check that it's not possible to withdraw more collateral than what the user owns. +rule withdrawCollateralLiquidity(MorphoHarness.MarketParams marketParams, uint256 withdrawnAssets, address onBehalf, address receiver) { + env e; + MorphoHarness.Id id = libId(marketParams); + + uint256 ownedAssets = collateral(id, onBehalf); + + withdrawCollateral(e, marketParams, withdrawnAssets, onBehalf, receiver); + + assert withdrawnAssets <= ownedAssets; +} + +// Check than when repaying the full outstanding debt requires more assets than what the user owes. +rule repayLiquidity(MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) { + env e; + MorphoHarness.Id id = libId(marketParams); + + // Assume no interest as it would increase the total borrowed assets. + require lastUpdate(id) == e.block.timestamp; + + uint256 initialShares = borrowShares(id, onBehalf); + uint256 initialTotalBorrow = virtualTotalBorrowAssets(id); + uint256 initialTotalBorrowShares = virtualTotalBorrowShares(id); + uint256 owedAssets = libMulDivUp(initialShares, initialTotalBorrow, initialTotalBorrowShares); + + uint256 repaidAssets; + repaidAssets, _ = repay(e, marketParams, assets, shares, onBehalf, data); + + // Assume a full repay. + require borrowShares(id, onBehalf) == 0; + + assert repaidAssets >= owedAssets; +} diff --git a/certora/specs/Health.spec b/certora/specs/Health.spec new file mode 100644 index 000000000..dc565b909 --- /dev/null +++ b/certora/specs/Health.spec @@ -0,0 +1,108 @@ +// SPDX-License-Identifier: GPL-2.0-or-later +methods { + function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE; + + function totalBorrowShares(MorphoHarness.Id) external returns uint256 envfree; + function lastUpdate(MorphoHarness.Id) external returns uint256 envfree; + function borrowShares(MorphoHarness.Id, address) external returns uint256 envfree; + function collateral(MorphoHarness.Id, address) external returns uint256 envfree; + function isAuthorized(address, address user) external returns bool envfree; + + function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; + function isHealthy(MorphoHarness.MarketParams, address user) external returns bool envfree; + + function _.price() external => mockPrice() expect uint256; + function MathLib.mulDivDown(uint256 a, uint256 b, uint256 c) internal returns uint256 => summaryMulDivDown(a,b,c); + function MathLib.mulDivUp(uint256 a, uint256 b, uint256 c) internal returns uint256 => summaryMulDivUp(a,b,c); + function UtilsLib.min(uint256 a, uint256 b) internal returns uint256 => summaryMin(a,b); +} + +ghost uint256 lastPrice; +ghost bool priceChanged; + +function mockPrice() returns uint256 { + uint256 somePrice; + if (somePrice != lastPrice) { + priceChanged = true; + lastPrice = somePrice; + } + return somePrice; +} + +function summaryMulDivUp(uint256 x, uint256 y, uint256 d) returns uint256 { + // Safe require because the reference implementation would revert. + require d != 0; + return require_uint256((x * y + (d - 1)) / d); +} + +function summaryMulDivDown(uint256 x, uint256 y, uint256 d) returns uint256 { + // Safe require because the reference implementation would revert. + require d != 0; + return require_uint256((x * y) / d); +} + +function summaryMin(uint256 a, uint256 b) returns uint256 { + return a < b ? a : b; +} + +// Check that without accruing interest, no interaction can put an healthy account into an unhealthy one. +// This rule times out for liquidate, repay and borrow. +rule stayHealthy(env e, method f, calldataarg data) +filtered { + f -> !f.isView && + f.selector != sig:liquidate(MorphoHarness.MarketParams, address, uint256, uint256, bytes).selector && + f.selector != sig:repay(MorphoHarness.MarketParams, uint256, uint256, address, bytes).selector && + f.selector != sig:borrow(MorphoHarness.MarketParams, uint256, uint256, address, address).selector +} +{ + MorphoHarness.MarketParams marketParams; + MorphoHarness.Id id = libId(marketParams); + address user; + + // Assume that the position is healthy before the interaction. + require isHealthy(marketParams, user); + // Safe require because of the invariants onlyEnabledLltv and lltvSmallerThanWad in ConsistentState.spec. + require marketParams.lltv < 10^18; + // Assumption to ensure that no interest is accumulated. + require lastUpdate(id) == e.block.timestamp; + + priceChanged = false; + f(e, data); + + // Safe require because of the invariant sumBorrowSharesCorrect. + require borrowShares(id, user) <= totalBorrowShares(id); + + bool stillHealthy = isHealthy(marketParams, user); + assert !priceChanged => stillHealthy; +} + +// Check that users cannot lose collateral by unauthorized parties except in case of an unhealthy position. +rule healthyUserCannotLoseCollateral(env e, method f, calldataarg data) +filtered { f -> !f.isView } +{ + MorphoHarness.MarketParams marketParams; + MorphoHarness.Id id = libId(marketParams); + address user; + + // Assume that the e.msg.sender is not authorized. + require !isAuthorized(user, e.msg.sender); + require user != e.msg.sender; + // Assumption to ensure that no interest is accumulated. + require lastUpdate(id) == e.block.timestamp; + // Assume that the user is healthy. + require isHealthy(marketParams, user); + + mathint collateralBefore = collateral(id, user); + + priceChanged = false; + f(e, data); + + mathint collateralAfter = collateral(id, user); + + assert !priceChanged => collateralAfter >= collateralBefore; +} + +// Check that users without collateral also have no debt. +// This invariant ensures that bad debt realization cannot be bypassed. +invariant alwaysCollateralized(MorphoHarness.Id id, address borrower) + borrowShares(id, borrower) != 0 => collateral(id, borrower) != 0; diff --git a/certora/specs/LibSummary.spec b/certora/specs/LibSummary.spec new file mode 100644 index 000000000..030e89140 --- /dev/null +++ b/certora/specs/LibSummary.spec @@ -0,0 +1,26 @@ +// SPDX-License-Identifier: GPL-2.0-or-later +methods { + function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE; + + function libMulDivUp(uint256, uint256, uint256) external returns uint256 envfree; + function libMulDivDown(uint256, uint256, uint256) external returns uint256 envfree; + function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; + function refId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; +} + +// Check the summary of MathLib.mulDivUp required by RatioMath.spec +rule checkSummaryMulDivUp(uint256 x, uint256 y, uint256 d) { + uint256 result = libMulDivUp(x, y, d); + assert result * d >= x * y; +} + +// Check the summary of MathLib.mulDivDown required by RatioMath.spec +rule checkSummaryMulDivDown(uint256 x, uint256 y, uint256 d) { + uint256 result = libMulDivDown(x, y, d); + assert result * d <= x * y; +} + +// Check the summary of MarketParamsLib.id required by Liveness.spec +rule checkSummaryId(MorphoHarness.MarketParams marketParams) { + assert libId(marketParams) == refId(marketParams); +} diff --git a/certora/specs/Liveness.spec b/certora/specs/Liveness.spec new file mode 100644 index 000000000..0c621ac77 --- /dev/null +++ b/certora/specs/Liveness.spec @@ -0,0 +1,386 @@ +// SPDX-License-Identifier: GPL-2.0-or-later +methods { + function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE; + function supplyShares(MorphoInternalAccess.Id, address) external returns uint256 envfree; + function borrowShares(MorphoInternalAccess.Id, address) external returns uint256 envfree; + function collateral(MorphoInternalAccess.Id, address) external returns uint256 envfree; + function totalSupplyAssets(MorphoInternalAccess.Id) external returns uint256 envfree; + function totalSupplyShares(MorphoInternalAccess.Id) external returns uint256 envfree; + function totalBorrowAssets(MorphoInternalAccess.Id) external returns uint256 envfree; + function totalBorrowShares(MorphoInternalAccess.Id) external returns uint256 envfree; + function fee(MorphoInternalAccess.Id) external returns uint256 envfree; + function lastUpdate(MorphoInternalAccess.Id) external returns uint256 envfree; + function nonce(address) external returns uint256 envfree; + function isAuthorized(address, address) external returns bool envfree; + + function libId(MorphoInternalAccess.MarketParams) external returns MorphoInternalAccess.Id envfree; + function refId(MorphoInternalAccess.MarketParams) external returns MorphoInternalAccess.Id envfree; + + function _._accrueInterest(MorphoInternalAccess.MarketParams memory marketParams, MorphoInternalAccess.Id id) internal with (env e) => summaryAccrueInterest(e, marketParams, id) expect void; + + function MarketParamsLib.id(MorphoInternalAccess.MarketParams memory marketParams) internal returns MorphoInternalAccess.Id => summaryId(marketParams); + function SafeTransferLib.safeTransfer(address token, address to, uint256 value) internal => summarySafeTransferFrom(token, currentContract, to, value); + function SafeTransferLib.safeTransferFrom(address token, address from, address to, uint256 value) internal => summarySafeTransferFrom(token, from, to, value); +} + +ghost mapping(address => mathint) myBalances { + init_state axiom (forall address token. myBalances[token] == 0); +} + +function summaryId(MorphoInternalAccess.MarketParams marketParams) returns MorphoInternalAccess.Id { + return refId(marketParams); +} + +function summarySafeTransferFrom(address token, address from, address to, uint256 amount) { + if (from == currentContract) { + // Safe require because the reference implementation would revert. + myBalances[token] = require_uint256(myBalances[token] - amount); + } + if (to == currentContract) { + // Safe require because the reference implementation would revert. + myBalances[token] = require_uint256(myBalances[token] + amount); + } +} + +function min(mathint a, mathint b) returns mathint { + return a < b ? a : b; +} + +// Assume no fee. +// Summarize the accrue interest to avoid having to deal with reverts with absurdly high borrow rates. +function summaryAccrueInterest(env e, MorphoInternalAccess.MarketParams marketParams, MorphoInternalAccess.Id id) { + // Safe require because timestamps cannot realistically be that large. + require e.block.timestamp < 2^128; + if (e.block.timestamp != lastUpdate(id) && totalBorrowAssets(id) != 0) { + uint128 interest; + uint256 supply = totalSupplyAssets(id); + // Safe require because the reference implementation would revert. + require interest + supply < 2^256; + increaseInterest(e, id, interest); + } + + update(e, id, e.block.timestamp); +} + +definition isCreated(MorphoInternalAccess.Id id) returns bool = + lastUpdate(id) != 0; + +// Check that tokens and shares are properly accounted following a supply. +rule supplyChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) { + MorphoInternalAccess.Id id = libId(marketParams); + + // Safe require because Morpho cannot call such functions by itself. + require currentContract != e.msg.sender; + // Assumption to ensure that no interest is accumulated. + require lastUpdate(id) == e.block.timestamp; + + mathint sharesBefore = supplyShares(id, onBehalf); + mathint balanceBefore = myBalances[marketParams.loanToken]; + mathint liquidityBefore = totalSupplyAssets(id) - totalBorrowAssets(id); + + uint256 suppliedAssets; + uint256 suppliedShares; + suppliedAssets, suppliedShares = supply(e, marketParams, assets, shares, onBehalf, data); + + mathint sharesAfter = supplyShares(id, onBehalf); + mathint balanceAfter = myBalances[marketParams.loanToken]; + mathint liquidityAfter = totalSupplyAssets(id) - totalBorrowAssets(id); + + assert assets != 0 => suppliedAssets == assets; + assert shares != 0 => suppliedShares == shares; + assert sharesAfter == sharesBefore + suppliedShares; + assert balanceAfter == balanceBefore + suppliedAssets; + assert liquidityAfter == liquidityBefore + suppliedAssets; +} + +// Check that you can supply non-zero tokens by passing shares. +rule canSupplyByPassingShares(env e, MorphoInternalAccess.MarketParams marketParams, uint256 shares, address onBehalf, bytes data) { + uint256 suppliedAssets; + suppliedAssets, _ = supply(e, marketParams, 0, shares, onBehalf, data); + + satisfy suppliedAssets != 0; +} + +// Check that tokens and shares are properly accounted following a withdraw. +rule withdrawChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) { + MorphoInternalAccess.Id id = libId(marketParams); + + // Assume that Morpho is not the receiver. + require currentContract != receiver; + // Assumption to ensure that no interest is accumulated. + require lastUpdate(id) == e.block.timestamp; + + mathint sharesBefore = supplyShares(id, onBehalf); + mathint balanceBefore = myBalances[marketParams.loanToken]; + mathint liquidityBefore = totalSupplyAssets(id) - totalBorrowAssets(id); + + uint256 withdrawnAssets; + uint256 withdrawnShares; + withdrawnAssets, withdrawnShares = withdraw(e, marketParams, assets, shares, onBehalf, receiver); + + mathint sharesAfter = supplyShares(id, onBehalf); + mathint balanceAfter = myBalances[marketParams.loanToken]; + mathint liquidityAfter = totalSupplyAssets(id) - totalBorrowAssets(id); + + assert assets != 0 => withdrawnAssets == assets; + assert shares != 0 => withdrawnShares == shares; + assert sharesAfter == sharesBefore - withdrawnShares; + assert balanceAfter == balanceBefore - withdrawnAssets; + assert liquidityAfter == liquidityBefore - withdrawnAssets; +} + +// Check that you can withdraw non-zero tokens by passing shares. +rule canWithdrawByPassingShares(env e, MorphoInternalAccess.MarketParams marketParams, uint256 shares, address onBehalf, address receiver) { + uint256 withdrawnAssets; + withdrawnAssets, _ = withdraw(e, marketParams, 0, shares, onBehalf, receiver); + + satisfy withdrawnAssets != 0; +} + +// Check that tokens and shares are properly accounted following a borrow. +rule borrowChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) { + MorphoInternalAccess.Id id = libId(marketParams); + + // Assume that Morpho is not the receiver. + require currentContract != receiver; + // Assumption to ensure that no interest is accumulated. + require lastUpdate(id) == e.block.timestamp; + + mathint sharesBefore = borrowShares(id, onBehalf); + mathint balanceBefore = myBalances[marketParams.loanToken]; + mathint liquidityBefore = totalSupplyAssets(id) - totalBorrowAssets(id); + + uint256 borrowedAssets; + uint256 borrowedShares; + borrowedAssets, borrowedShares = borrow(e, marketParams, assets, shares, onBehalf, receiver); + + mathint sharesAfter = borrowShares(id, onBehalf); + mathint balanceAfter = myBalances[marketParams.loanToken]; + mathint liquidityAfter = totalSupplyAssets(id) - totalBorrowAssets(id); + + assert assets != 0 => borrowedAssets == assets; + assert shares != 0 => borrowedShares == shares; + assert sharesAfter == sharesBefore + borrowedShares; + assert balanceAfter == balanceBefore - borrowedAssets; + assert liquidityAfter == liquidityBefore - borrowedAssets; +} + +// Check that you can borrow non-zero tokens by passing shares. +rule canBorrowByPassingShares(env e, MorphoInternalAccess.MarketParams marketParams, uint256 shares, address onBehalf, address receiver) { + uint256 borrowedAssets; + borrowedAssets, _ = borrow(e, marketParams, 0, shares, onBehalf, receiver); + + satisfy borrowedAssets != 0; +} + +// Check that tokens and shares are properly accounted following a repay. +rule repayChangesTokensAndShares(env e, MorphoInternalAccess.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) { + MorphoInternalAccess.Id id = libId(marketParams); + + // Safe require because Morpho cannot call such functions by itself. + require currentContract != e.msg.sender; + // Assumption to ensure that no interest is accumulated. + require lastUpdate(id) == e.block.timestamp; + + mathint sharesBefore = borrowShares(id, onBehalf); + mathint balanceBefore = myBalances[marketParams.loanToken]; + mathint liquidityBefore = totalSupplyAssets(id) - totalBorrowAssets(id); + + mathint borrowAssetsBefore = totalBorrowAssets(id); + + uint256 repaidAssets; + uint256 repaidShares; + repaidAssets, repaidShares = repay(e, marketParams, assets, shares, onBehalf, data); + + mathint sharesAfter = borrowShares(id, onBehalf); + mathint balanceAfter = myBalances[marketParams.loanToken]; + mathint liquidityAfter = totalSupplyAssets(id) - totalBorrowAssets(id); + + assert assets != 0 => repaidAssets == assets; + assert shares != 0 => repaidShares == shares; + assert sharesAfter == sharesBefore - repaidShares; + assert balanceAfter == balanceBefore + repaidAssets; + // Taking the min to handle the zeroFloorSub in the code. + assert liquidityAfter == liquidityBefore + min(repaidAssets, borrowAssetsBefore); +} + +// Check that you can repay non-zero tokens by passing shares. +rule canRepayByPassingShares(env e, MorphoInternalAccess.MarketParams marketParams, uint256 shares, address onBehalf, bytes data) { + uint256 repaidAssets; + repaidAssets, _ = repay(e, marketParams, 0, shares, onBehalf, data); + + satisfy repaidAssets != 0; +} + +// Check that tokens and balances are properly accounted following a supplyCollateral. +rule supplyCollateralChangesTokensAndBalance(env e, MorphoInternalAccess.MarketParams marketParams, uint256 assets, address onBehalf, bytes data) { + MorphoInternalAccess.Id id = libId(marketParams); + + // Safe require because Morpho cannot call such functions by itself. + require currentContract != e.msg.sender; + + mathint collateralBefore = collateral(id, onBehalf); + mathint balanceBefore = myBalances[marketParams.collateralToken]; + + supplyCollateral(e, marketParams, assets, onBehalf, data); + + mathint collateralAfter = collateral(id, onBehalf); + mathint balanceAfter = myBalances[marketParams.collateralToken]; + + assert collateralAfter == collateralBefore + assets; + assert balanceAfter == balanceBefore + assets; +} + +// Check that tokens and balances are properly accounted following a withdrawCollateral. +rule withdrawCollateralChangesTokensAndBalance(env e, MorphoInternalAccess.MarketParams marketParams, uint256 assets, address onBehalf, address receiver) { + MorphoInternalAccess.Id id = libId(marketParams); + + // Assume that Morpho is not the receiver. + require currentContract != receiver; + // Assumption to ensure that no interest is accumulated. + require lastUpdate(id) == e.block.timestamp; + + mathint collateralBefore = collateral(id, onBehalf); + mathint balanceBefore = myBalances[marketParams.collateralToken]; + + withdrawCollateral(e, marketParams, assets, onBehalf, receiver); + + mathint collateralAfter = collateral(id, onBehalf); + mathint balanceAfter = myBalances[marketParams.collateralToken]; + + assert collateralAfter == collateralBefore - assets; + assert balanceAfter == balanceBefore - assets; +} + +// Check that tokens are properly accounted following a liquidate. +rule liquidateChangesTokens(env e, MorphoInternalAccess.MarketParams marketParams, address borrower, uint256 seized, uint256 repaidShares, bytes data) { + MorphoInternalAccess.Id id = libId(marketParams); + + // Safe require because Morpho cannot call such functions by itself. + require currentContract != e.msg.sender; + // Assumption to simplify the balance specification in the rest of this rule. + require marketParams.loanToken != marketParams.collateralToken; + // Assumption to ensure that no interest is accumulated. + require lastUpdate(id) == e.block.timestamp; + + mathint collateralBefore = collateral(id, borrower); + mathint balanceLoanBefore = myBalances[marketParams.loanToken]; + mathint balanceCollateralBefore = myBalances[marketParams.collateralToken]; + mathint liquidityBefore = totalSupplyAssets(id) - totalBorrowAssets(id); + + mathint borrowLoanAssetsBefore = totalBorrowAssets(id); + + uint256 seizedAssets; + uint256 repaidAssets; + seizedAssets, repaidAssets = liquidate(e, marketParams, borrower, seized, repaidShares, data); + + mathint collateralAfter = collateral(id, borrower); + mathint balanceLoanAfter = myBalances[marketParams.loanToken]; + mathint balanceCollateralAfter = myBalances[marketParams.collateralToken]; + mathint liquidityAfter = totalSupplyAssets(id) - totalBorrowAssets(id); + + assert seized != 0 => seizedAssets == seized; + assert collateralBefore > to_mathint(seizedAssets) => collateralAfter == collateralBefore - seizedAssets; + assert balanceLoanAfter == balanceLoanBefore + repaidAssets; + assert balanceCollateralAfter == balanceCollateralBefore - seizedAssets; + // Taking the min to handle the zeroFloorSub in the code. + assert liquidityAfter == liquidityBefore + min(repaidAssets, borrowLoanAssetsBefore); +} + +// Check that you can liquidate non-zero tokens by passing shares. +rule canLiquidateByPassingShares(env e, MorphoInternalAccess.MarketParams marketParams, address borrower, uint256 repaidShares, bytes data) { + uint256 seizedAssets; + uint256 repaidAssets; + seizedAssets, repaidAssets = liquidate(e, marketParams, borrower, 0, repaidShares, data); + + satisfy seizedAssets != 0 && repaidAssets != 0; +} + +// Check that nonce and authorization are properly updated with calling setAuthorizationWithSig. +rule setAuthorizationWithSigChangesNonceAndAuthorizes(env e, MorphoInternalAccess.Authorization authorization, MorphoInternalAccess.Signature signature) { + mathint nonceBefore = nonce(authorization.authorizer); + + setAuthorizationWithSig(e, authorization, signature); + + mathint nonceAfter = nonce(authorization.authorizer); + + assert nonceAfter == nonceBefore + 1; + assert isAuthorized(authorization.authorizer, authorization.authorized) == authorization.isAuthorized; +} + +// Check that one can always repay the debt in full. +rule canRepayAll(env e, MorphoInternalAccess.MarketParams marketParams, uint256 shares, bytes data) { + MorphoInternalAccess.Id id = libId(marketParams); + + // Assume no callback, which still allows to repay all. + require data.length == 0; + + // Assume a full repay. + require shares == borrowShares(id, e.msg.sender); + // Omit sanity checks. + require isCreated(id); + require e.msg.sender != 0; + require e.msg.value == 0; + require shares > 0; + // Safe require because of the noTimeTravel rule. + require lastUpdate(id) <= e.block.timestamp; + // Safe require because of the sumBorrowSharesCorrect invariant. + require shares <= totalBorrowShares(id); + + // Accrue interest first to ensure that the accrued interest is reasonable (next require). + // Safe because of the AccrueInterest.repayAccruesInterest rule + summaryAccrueInterest(e, marketParams, id); + + // Assume that the invariant about tokens total supply is respected. + require totalBorrowAssets(id) < 10^35; + + repay@withrevert(e, marketParams, 0, shares, e.msg.sender, data); + + assert !lastReverted; +} + +// Check the one can always withdraw all, under the condition that there are no outstanding debt on the market. +rule canWithdrawAll(env e, MorphoInternalAccess.MarketParams marketParams, uint256 shares, address receiver) { + MorphoInternalAccess.Id id = libId(marketParams); + + // Assume a full withdraw. + require shares == supplyShares(id, e.msg.sender); + // Omit sanity checks. + require isCreated(id); + require e.msg.sender != 0; + require receiver != 0; + require e.msg.value == 0; + require shares > 0; + // Assume no outstanding debt on the market. + require totalBorrowAssets(id) == 0; + // Safe require because of the noTimeTravel rule. + require lastUpdate(id) <= e.block.timestamp; + // Safe require because of the sumSupplySharesCorrect invariant. + require shares <= totalSupplyShares(id); + + withdraw@withrevert(e, marketParams, 0, shares, e.msg.sender, receiver); + + assert !lastReverted; +} + +// Check that a user can always withdraw all, under the condition that this user does not have an outstanding debt. +// Combined with the canRepayAll rule, this ensures that a borrower can always fully exit a market. +rule canWithdrawCollateralAll(env e, MorphoInternalAccess.MarketParams marketParams, uint256 assets, address receiver) { + MorphoInternalAccess.Id id = libId(marketParams); + + // Ensure a full withdrawCollateral. + require assets == collateral(id, e.msg.sender); + // Omit sanity checks. + require isCreated(id); + require receiver != 0; + require e.msg.value == 0; + require assets > 0; + // Safe require because of the noTimeTravel rule. + require lastUpdate(id) <= e.block.timestamp; + // Assume that the user does not have an outstanding debt. + require borrowShares(id, e.msg.sender) == 0; + + withdrawCollateral@withrevert(e, marketParams, assets, e.msg.sender, receiver); + + assert !lastReverted; +} diff --git a/certora/specs/RatioMath.spec b/certora/specs/RatioMath.spec new file mode 100644 index 000000000..2ae82a8bc --- /dev/null +++ b/certora/specs/RatioMath.spec @@ -0,0 +1,157 @@ +// SPDX-License-Identifier: GPL-2.0-or-later +methods { + function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE; + function virtualTotalSupplyAssets(MorphoHarness.Id) external returns uint256 envfree; + function virtualTotalSupplyShares(MorphoHarness.Id) external returns uint256 envfree; + function virtualTotalBorrowAssets(MorphoHarness.Id) external returns uint256 envfree; + function virtualTotalBorrowShares(MorphoHarness.Id) external returns uint256 envfree; + function fee(MorphoHarness.Id) external returns uint256 envfree; + function lastUpdate(MorphoHarness.Id) external returns uint256 envfree; + + function maxFee() external returns uint256 envfree; + function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; + + function MathLib.mulDivDown(uint256 a, uint256 b, uint256 c) internal returns uint256 => summaryMulDivDown(a,b,c); + function MathLib.mulDivUp(uint256 a, uint256 b, uint256 c) internal returns uint256 => summaryMulDivUp(a,b,c); + function MathLib.wTaylorCompounded(uint256, uint256) internal returns uint256 => NONDET; + + function _.borrowRate(MorphoHarness.MarketParams, MorphoHarness.Market) external => HAVOC_ECF; + +} + +invariant feeInRange(MorphoHarness.Id id) + fee(id) <= maxFee(); + +// This is a simple overapproximative summary, stating that it rounds in the right direction. +function summaryMulDivUp(uint256 x, uint256 y, uint256 d) returns uint256 { + uint256 result; + // Safe require that is checked by the specification in LibSummary.spec. + require result * d >= x * y; + return result; +} + +// This is a simple overapproximative summary, stating that it rounds in the right direction. +function summaryMulDivDown(uint256 x, uint256 y, uint256 d) returns uint256 { + uint256 result; + // Safe require that is checked by the specification in LibSummary.spec. + require result * d <= x * y; + return result; +} + +// Check that accrueInterest increases the value of supply shares. +rule accrueInterestIncreasesSupplyRatio(env e, MorphoHarness.MarketParams marketParams) { + MorphoHarness.Id id; + requireInvariant feeInRange(id); + + mathint assetsBefore = virtualTotalSupplyAssets(id); + mathint sharesBefore = virtualTotalSupplyShares(id); + + // The check is done for every market, not just for id. + accrueInterest(e, marketParams); + + mathint assetsAfter = virtualTotalSupplyAssets(id); + mathint sharesAfter = virtualTotalSupplyShares(id); + + // Check that the ratio increases: assetsBefore/sharesBefore <= assetsAfter / sharesAfter. + assert assetsBefore * sharesAfter <= assetsAfter * sharesBefore; +} + +// Check that accrueInterest increases the value of borrow shares. +rule accrueInterestIncreasesBorrowRatio(env e, MorphoHarness.MarketParams marketParams) { + MorphoHarness.Id id; + requireInvariant feeInRange(id); + + mathint assetsBefore = virtualTotalBorrowAssets(id); + mathint sharesBefore = virtualTotalBorrowShares(id); + + // The check is done for every marketParams, not just for id. + accrueInterest(e, marketParams); + + mathint assetsAfter = virtualTotalBorrowAssets(id); + mathint sharesAfter = virtualTotalBorrowShares(id); + + // Check that the ratio increases: assetsBefore/sharesBefore <= assetsAfter / sharesAfter. + assert assetsBefore * sharesAfter <= assetsAfter * sharesBefore; +} + + +// Check that except when not accruing interest and except for liquidate, every function increases the value of supply shares. +rule onlyLiquidateCanDecreaseSupplyRatio(env e, method f, calldataarg args) +filtered { + f -> !f.isView && f.selector != sig:liquidate(MorphoHarness.MarketParams, address, uint256, uint256, bytes).selector +} +{ + MorphoHarness.Id id; + requireInvariant feeInRange(id); + + mathint assetsBefore = virtualTotalSupplyAssets(id); + mathint sharesBefore = virtualTotalSupplyShares(id); + + // Interest is checked separately by the rules above. + // Here we assume interest has already been accumulated for this block. + require lastUpdate(id) == e.block.timestamp; + + f(e,args); + + mathint assetsAfter = virtualTotalSupplyAssets(id); + mathint sharesAfter = virtualTotalSupplyShares(id); + + // Check that the ratio increases: assetsBefore/sharesBefore <= assetsAfter / sharesAfter + assert assetsBefore * sharesAfter <= assetsAfter * sharesBefore; +} + +// Check that except when not accruing interest, every function is decreasing the value of borrow shares. +// The repay function is checked separately, see below. +// The liquidate function is not checked. +rule onlyAccrueInterestCanIncreaseBorrowRatio(env e, method f, calldataarg args) +filtered { + f -> !f.isView && + f.selector != sig:repay(MorphoHarness.MarketParams, uint256, uint256, address, bytes).selector && + f.selector != sig:liquidate(MorphoHarness.MarketParams, address, uint256, uint256, bytes).selector +} +{ + MorphoHarness.Id id; + requireInvariant feeInRange(id); + + // Interest would increase borrow ratio, so we need to assume that no time passes. + require lastUpdate(id) == e.block.timestamp; + + mathint assetsBefore = virtualTotalBorrowAssets(id); + mathint sharesBefore = virtualTotalBorrowShares(id); + + f(e,args); + + mathint assetsAfter = virtualTotalBorrowAssets(id); + mathint sharesAfter = virtualTotalBorrowShares(id); + + // Check that the ratio decreases: assetsBefore/sharesBefore >= assetsAfter / sharesAfter + assert assetsBefore * sharesAfter >= assetsAfter * sharesBefore; +} + +// Check that when not accruing interest, repay is decreasing the value of borrow shares. +// Check the case where the market is not repaid fully. +// The other case requires exact math (ie not over-approximating mulDivUp and mulDivDown), so it is checked separately in ExactMath.spec. +rule repayDecreasesBorrowRatio(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) +{ + MorphoHarness.Id id = libId(marketParams); + requireInvariant feeInRange(id); + + mathint assetsBefore = virtualTotalBorrowAssets(id); + mathint sharesBefore = virtualTotalBorrowShares(id); + + // Interest would increase borrow ratio, so we need to assume that no time passes. + require lastUpdate(id) == e.block.timestamp; + + mathint repaidAssets; + repaidAssets, _ = repay(e, marketParams, assets, shares, onBehalf, data); + + // Check the case where the market is not repaid fully. + require repaidAssets < assetsBefore; + + mathint assetsAfter = virtualTotalBorrowAssets(id); + mathint sharesAfter = virtualTotalBorrowShares(id); + + assert assetsAfter == assetsBefore - repaidAssets; + // Check that the ratio decreases: assetsBefore/sharesBefore >= assetsAfter / sharesAfter + assert assetsBefore * sharesAfter >= assetsAfter * sharesBefore; +} diff --git a/certora/specs/Reentrancy.spec b/certora/specs/Reentrancy.spec new file mode 100644 index 000000000..6ec26dc4e --- /dev/null +++ b/certora/specs/Reentrancy.spec @@ -0,0 +1,61 @@ +// SPDX-License-Identifier: GPL-2.0-or-later +methods { + function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE; + + function _.borrowRate(MorphoHarness.MarketParams marketParams, MorphoHarness.Market) external => summaryBorrowRate() expect uint256; +} + +ghost bool delegateCall; +ghost bool callIsBorrowRate; +// True when storage has been accessed with either a SSTORE or a SLOAD. +ghost bool hasAccessedStorage; +// True when a CALL has been done after storage has been accessed. +ghost bool hasCallAfterAccessingStorage; +// True when storage has been accessed, after which an external call is made, followed by accessing storage again. +ghost bool hasReentrancyUnsafeCall; + +function summaryBorrowRate() returns uint256 { + uint256 result; + callIsBorrowRate = true; + return result; +} + +hook ALL_SSTORE(uint loc, uint v) { + hasAccessedStorage = true; + hasReentrancyUnsafeCall = hasCallAfterAccessingStorage; +} + +hook ALL_SLOAD(uint loc) uint v { + hasAccessedStorage = true; + hasReentrancyUnsafeCall = hasCallAfterAccessingStorage; +} + +hook CALL(uint g, address addr, uint value, uint argsOffset, uint argsLength, uint retOffset, uint retLength) uint rc { + if (callIsBorrowRate) { + // The calls to borrow rate are trusted and don't count. + callIsBorrowRate = false; + } else { + hasCallAfterAccessingStorage = hasAccessedStorage; + } +} + +hook DELEGATECALL(uint g, address addr, uint argsOffset, uint argsLength, uint retOffset, uint retLength) uint rc { + delegateCall = true; +} + +// Check that no function is accessing storage, then making an external CALL other than to the IRM, and accessing storage again. +rule reentrancySafe(method f, env e, calldataarg data) { + // Set up the initial state. + require !callIsBorrowRate; + require !hasAccessedStorage && !hasCallAfterAccessingStorage && !hasReentrancyUnsafeCall; + f(e,data); + assert !hasReentrancyUnsafeCall; +} + +// Check that the contract is truly immutable. +rule noDelegateCalls(method f, env e, calldataarg data) { + // Set up the initial state. + require !delegateCall; + f(e,data); + assert !delegateCall; +} diff --git a/certora/specs/Reverts.spec b/certora/specs/Reverts.spec new file mode 100644 index 000000000..9ae422c51 --- /dev/null +++ b/certora/specs/Reverts.spec @@ -0,0 +1,179 @@ +// SPDX-License-Identifier: GPL-2.0-or-later +methods { + function extSloads(bytes32[]) external returns bytes32[] => NONDET DELETE; + + function owner() external returns address envfree; + function feeRecipient() external returns address envfree; + function totalSupplyAssets(MorphoHarness.Id) external returns uint256 envfree; + function totalBorrowAssets(MorphoHarness.Id) external returns uint256 envfree; + function totalSupplyShares(MorphoHarness.Id) external returns uint256 envfree; + function totalBorrowShares(MorphoHarness.Id) external returns uint256 envfree; + function lastUpdate(MorphoHarness.Id) external returns uint256 envfree; + function isIrmEnabled(address) external returns bool envfree; + function isLltvEnabled(uint256) external returns bool envfree; + function isAuthorized(address, address) external returns bool envfree; + function nonce(address) external returns uint256 envfree; + + function libId(MorphoHarness.MarketParams) external returns MorphoHarness.Id envfree; + + function maxFee() external returns uint256 envfree; + function wad() external returns uint256 envfree; +} + +definition isCreated(MorphoHarness.Id id) returns bool = + (lastUpdate(id) != 0); + +ghost mapping(MorphoHarness.Id => mathint) sumCollateral +{ + init_state axiom (forall MorphoHarness.Id id. sumCollateral[id] == 0); +} +hook Sstore position[KEY MorphoHarness.Id id][KEY address owner].collateral uint128 newAmount (uint128 oldAmount) STORAGE { + sumCollateral[id] = sumCollateral[id] - oldAmount + newAmount; +} + +definition emptyMarket(MorphoHarness.Id id) returns bool = + totalSupplyAssets(id) == 0 && + totalSupplyShares(id) == 0 && + totalBorrowAssets(id) == 0 && + totalBorrowShares(id) == 0 && + sumCollateral[id] == 0; + +definition exactlyOneZero(uint256 assets, uint256 shares) returns bool = + (assets == 0 && shares != 0) || (assets != 0 && shares == 0); + +// This invariant catches bugs when not checking that the market is created with lastUpdate. +invariant notCreatedIsEmpty(MorphoHarness.Id id) + !isCreated(id) => emptyMarket(id) +{ + preserved with (env e) { + // Safe require because timestamps cannot realistically be that large. + require e.block.timestamp < 2^128; + } +} + +// Useful to ensure that authorized parties are not the zero address and so we can omit the sanity check in this case. +invariant zeroDoesNotAuthorize(address authorized) + !isAuthorized(0, authorized) +{ + preserved setAuthorization(address _authorized, bool _newAuthorization) with (env e) { + // Safe require because no one controls the zero address. + require e.msg.sender != 0; + } +} + +// Check the revert condition for the setOwner function. +rule setOwnerRevertCondition(env e, address newOwner) { + address oldOwner = owner(); + setOwner@withrevert(e, newOwner); + assert lastReverted <=> e.msg.value != 0 || e.msg.sender != oldOwner || newOwner == oldOwner; +} + +// Check the revert condition for the setOwner function. +rule enableIrmRevertCondition(env e, address irm) { + address oldOwner = owner(); + bool oldIsIrmEnabled = isIrmEnabled(irm); + enableIrm@withrevert(e, irm); + assert lastReverted <=> e.msg.value != 0 || e.msg.sender != oldOwner || oldIsIrmEnabled; +} + +// Check the revert condition for the enableLltv function. +rule enableLltvRevertCondition(env e, uint256 lltv) { + address oldOwner = owner(); + bool oldIsLltvEnabled = isLltvEnabled(lltv); + enableLltv@withrevert(e, lltv); + assert lastReverted <=> e.msg.value != 0 || e.msg.sender != oldOwner || lltv >= wad() || oldIsLltvEnabled; +} + +// Check that setFee reverts when its inputs are not validated. +// setFee can also revert if the accrueInterest reverts. +rule setFeeInputValidation(env e, MorphoHarness.MarketParams marketParams, uint256 newFee) { + MorphoHarness.Id id = libId(marketParams); + address oldOwner = owner(); + bool wasCreated = isCreated(id); + setFee@withrevert(e, marketParams, newFee); + bool hasReverted = lastReverted; + assert e.msg.value != 0 || e.msg.sender != oldOwner || !wasCreated || newFee > maxFee() => hasReverted; +} + +// Check the revert condition for the setFeeRecipient function. +rule setFeeRecipientRevertCondition(env e, address newFeeRecipient) { + address oldOwner = owner(); + address oldFeeRecipient = feeRecipient(); + setFeeRecipient@withrevert(e, newFeeRecipient); + assert lastReverted <=> e.msg.value != 0 || e.msg.sender != oldOwner || newFeeRecipient == oldFeeRecipient; +} + +// Check the revert condition for the createMarket function. +rule createMarketRevertCondition(env e, MorphoHarness.MarketParams marketParams) { + MorphoHarness.Id id = libId(marketParams); + bool irmEnabled = isIrmEnabled(marketParams.irm); + bool lltvEnabled = isLltvEnabled(marketParams.lltv); + bool wasCreated = isCreated(id); + createMarket@withrevert(e, marketParams); + assert lastReverted <=> e.msg.value != 0 || !irmEnabled || !lltvEnabled || wasCreated; +} + +// Check that supply reverts when its input are not validated. +rule supplyInputValidation(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) { + supply@withrevert(e, marketParams, assets, shares, onBehalf, data); + assert !exactlyOneZero(assets, shares) || onBehalf == 0 => lastReverted; +} + +// Check that withdraw reverts when its inputs are not validated. +rule withdrawInputValidation(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) { + // Safe require because no one controls the zero address. + require e.msg.sender != 0; + requireInvariant zeroDoesNotAuthorize(e.msg.sender); + withdraw@withrevert(e, marketParams, assets, shares, onBehalf, receiver); + assert !exactlyOneZero(assets, shares) || onBehalf == 0 || receiver == 0 => lastReverted; +} + +// Check that borrow reverts when its inputs are not validated. +rule borrowInputValidation(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, address receiver) { + // Safe require because no one controls the zero address. + require e.msg.sender != 0; + requireInvariant zeroDoesNotAuthorize(e.msg.sender); + borrow@withrevert(e, marketParams, assets, shares, onBehalf, receiver); + assert !exactlyOneZero(assets, shares) || onBehalf == 0 || receiver == 0 => lastReverted; +} + +// Check that repay reverts when its inputs are not validated. +rule repayInputValidation(env e, MorphoHarness.MarketParams marketParams, uint256 assets, uint256 shares, address onBehalf, bytes data) { + repay@withrevert(e, marketParams, assets, shares, onBehalf, data); + assert !exactlyOneZero(assets, shares) || onBehalf == 0 => lastReverted; +} + +// Check that supplyCollateral reverts when its inputs are not validated. +rule supplyCollateralInputValidation(env e, MorphoHarness.MarketParams marketParams, uint256 assets, address onBehalf, bytes data) { + supplyCollateral@withrevert(e, marketParams, assets, onBehalf, data); + assert assets == 0 || onBehalf == 0 => lastReverted; +} + +// Check that withdrawCollateral reverts when its inputs are not validated. +rule withdrawCollateralInputValidation(env e, MorphoHarness.MarketParams marketParams, uint256 assets, address onBehalf, address receiver) { + // Safe require because no one controls the zero address. + require e.msg.sender != 0; + requireInvariant zeroDoesNotAuthorize(e.msg.sender); + withdrawCollateral@withrevert(e, marketParams, assets, onBehalf, receiver); + assert assets == 0 || onBehalf == 0 || receiver == 0 => lastReverted; +} + +// Check that liquidate reverts when its inputs are not validated. +rule liquidateInputValidation(env e, MorphoHarness.MarketParams marketParams, address borrower, uint256 seizedAssets, uint256 repaidShares, bytes data) { + liquidate@withrevert(e, marketParams, borrower, seizedAssets, repaidShares, data); + assert !exactlyOneZero(seizedAssets, repaidShares) => lastReverted; +} + +// Check that setAuthorizationWithSig reverts when its inputs are not validated. +rule setAuthorizationWithSigInputValidation(env e, MorphoHarness.Authorization authorization, MorphoHarness.Signature signature) { + uint256 nonceBefore = nonce(authorization.authorizer); + setAuthorizationWithSig@withrevert(e, authorization, signature); + assert e.block.timestamp > authorization.deadline || authorization.nonce != nonceBefore => lastReverted; +} + +// Check that accrueInterest reverts when its inputs are not validated. +rule accrueInterestInputValidation(env e, MorphoHarness.MarketParams marketParams) { + bool wasCreated = isCreated(libId(marketParams)); + accrueInterest@withrevert(e, marketParams); + assert !wasCreated => lastReverted; +} diff --git a/certora/specs/Transfer.spec b/certora/specs/Transfer.spec new file mode 100644 index 000000000..a560f0658 --- /dev/null +++ b/certora/specs/Transfer.spec @@ -0,0 +1,83 @@ +// SPDX-License-Identifier: GPL-2.0-or-later +methods { + function libSafeTransfer(address, address, uint256) external envfree; + function libSafeTransferFrom(address, address, address, uint256) external envfree; + function balanceOf(address, address) external returns (uint256) envfree; + function allowance(address, address, address) external returns (uint256) envfree; + function totalSupply(address) external returns (uint256) envfree; + + function _.transfer(address, uint256) external => DISPATCHER(true); + function _.transferFrom(address, address, uint256) external => DISPATCHER(true); + function _.balanceOf(address) external => DISPATCHER(true); + function _.allowance(address, address) external => DISPATCHER(true); + function _.totalSupply() external => DISPATCHER(true); +} + +ghost mapping(address => mathint) myBalances +{ + init_state axiom (forall address token. myBalances[token] == 0); +} + +function summarySafeTransferFrom(address token, address from, address to, uint256 amount) { + if (from == currentContract) { + // Safe require because the reference implementation would revert. + myBalances[token] = require_uint256(myBalances[token] - amount); + } + if (to == currentContract) { + // Safe require because the reference implementation would revert. + myBalances[token] = require_uint256(myBalances[token] + amount); + } +} + +// Check the functional correctness of the summary of safeTransfer. +rule checkTransferSummary(address token, address to, uint256 amount) { + mathint initialBalance = balanceOf(token, currentContract); + // Safe require because the total supply is greater than the sum of the balance of any two accounts. + require to != currentContract => initialBalance + balanceOf(token, to) <= to_mathint(totalSupply(token)); + + libSafeTransfer(token, to, amount); + mathint finalBalance = balanceOf(token, currentContract); + + require myBalances[token] == initialBalance; + summarySafeTransferFrom(token, currentContract, to, amount); + assert myBalances[token] == finalBalance; +} + +// Check the functional correctness of the summary of safeTransferFrom. +rule checkTransferFromSummary(address token, address from, uint256 amount) { + mathint initialBalance = balanceOf(token, currentContract); + // Safe require because the total supply is greater than the sum of the balance of any two accounts. + require from != currentContract => initialBalance + balanceOf(token, from) <= to_mathint(totalSupply(token)); + + libSafeTransferFrom(token, from, currentContract, amount); + mathint finalBalance = balanceOf(token, currentContract); + + require myBalances[token] == initialBalance; + summarySafeTransferFrom(token, from, currentContract, amount); + assert myBalances[token] == finalBalance; +} + +// Check the revert condition of the summary of safeTransfer. +rule transferRevertCondition(address token, address to, uint256 amount) { + uint256 initialBalance = balanceOf(token, currentContract); + uint256 toInitialBalance = balanceOf(token, to); + // Safe require because the total supply is greater than the sum of the balance of any two accounts. + require to != currentContract => initialBalance + toInitialBalance <= to_mathint(totalSupply(token)); + + libSafeTransfer@withrevert(token, to, amount); + + assert lastReverted <=> initialBalance < amount; +} + +// Check the revert condition of the summary of safeTransferFrom. +rule transferFromRevertCondition(address token, address from, address to, uint256 amount) { + uint256 initialBalance = balanceOf(token, from); + uint256 toInitialBalance = balanceOf(token, to); + uint256 allowance = allowance(token, from, currentContract); + // Safe require because the total supply is greater than the sum of the balance of any two accounts. + require to != from => initialBalance + toInitialBalance <= to_mathint(totalSupply(token)); + + libSafeTransferFrom@withrevert(token, from, to, amount); + + assert lastReverted <=> initialBalance < amount || allowance < amount; +}