👻Aave: Continuous Formal Verification
Summary:
This proposal represents a partnership between Certora and Aave. This partnership would provide additional security measures in the form of ‘formal verification and path coverage tooling service to the Aave Platform contributors and the Aave Protocol dApp developers.’.
Aave Security: The Aave Protocol is a fully decentralized system that provides sophisticated tools for accessing liquidity. The protocol’s ongoing management is controlled by a governance protocol that allows external contributions and voting by stakeholders. Such a system opens up the possibility of creating powerful new DeFi protocols built on top of it, without giving up on decentralization.
One of the major risks in managing a complex system of smart contracts is that it is harder to ensure that changes introduced via governance are safe, and that they do not break the behavior of the protocol. While those problems are common to every piece of evolving software, decentralization introduces additional risks.
These risks were highlighted by a recent incident in which a bug was introduced in a Compound governance proposal (https://compound.finance/governance/proposals/62), leading to huge nonrecoverable financial losses. Of course, such bugs are not exclusive to Compound— they have been affecting many DeFi protocols.
Detecting vulnerabilities before they are deployed is difficult because of the lack of good security tools for smart contract development. Smart contract developers often rely on manual auditing to prevent bugs, but audits are difficult to employ in the setting of ongoing, time-controlled governance proposals. Moreover, even the best auditor can miss critical bugs due to the complexity of the code. (taken from Aave’s forum)
About Certora
Certora is a leading smart contract security firm with a team of 30+ professionals focusing on smart contract security, formal verification, and compilation techniques. They provide smart contract monitoring and (https://en.wikipedia.org/wiki/Continuous_integration) developer tools to organizations like Coinbase, Compound, Maker DAO and others.
Certora's developer tool, the Certora Prover, allows for companies to ‘move fast and break nothing’, which takes months off company’s ‘time-to-market’ by decreasing overall auditing time, and also offers post-launch code verification.
Our product is used by the industry’s leading companies (Aave, Balancer, Benqi, Compound, MakerDAO, OpenZeppelin, Sushi and more) and has prevented more than 100 safety-critical bugs, including 20 “solvency” bugs (a bug in which a user can steal money from the contract). Each bug can lead to tens or even hundreds of millions of dollars in losses. The Certora technology has also uncovered critical security bugs https://blog.soliditylang.org/category/security-alerts/ in the Solidity compiler itself and in deployed contracts of major DeFi organizations. (Aave Forum)
Certora x Aave:
Certora has been working with Aave since before the Aave v2 launch, and in that time they have found and prevented 6 ‘high-severity’ issues, including a ‘solvency bug’. (Link to Certora Prover Aave V2 findings:https://www.certora.com/pubs/AaveV2Dec2020.pdf) Certora currently plays a key role within Aave's Risk Framework (https://docs.aave.com/risk) as a regular auditor (along with Consensys and CertiK, each on a project basis). Certora is proposing to formalize their relationship with Aave into a full-time partnership (including development of open-source software and transparency tools for the Aave community).
What Certora proposes:
Certora proposes the following:
“First, we propose to change the project-based relationship of Aave and Certora, to an ongoing relationship, where we will provide ongoing support and rule-writing for Certora Prover on Aave’s code. This service will be provided to all community contributions to core and periphery parts of the Aave ecosystem. This will ensure that the constantly-evolving code of Aave’s platform remains secure, protecting its users’ assets.” (Governance Proposal)
“Second, we will develop a new symbolic execution tool (path coverage) which will significantly increase the coverage of code areas where we look for bugs, complementing the more focused nature of the Certora Prover. This tool’s results will be visible to all via a unique dashboard we will build. In addition, it will be open-source, so the community could contribute to its development.” (Governance Proposal)
Services offered
We will allocate a dedicated expert software engineer for writing rules for the Aave platform contributors and for Aave dApps as needed for the whole period. We will also allocate a full-time security researcher to review all proposed code changes.
We will offer all Aave platform contributors (registered by Aave) access to the Certora Prover SaaS platform to check new and existing rules, as well as provide support for run analysis and creation of new rules.
We will develop an open source directed fuzzing engine on top of modern SMT solvers.
We will create a cloud-based symbolic execution product that will analyze the Aave platform code and the dApps built on top of it in pre and post-deployment.
We will create a dashboard displaying the results of the symbolic execution product, including rule violations and covered paths, visible to all Aave users. Rule violations will be reported automatically to the Aave security team, but not visible to all users to avoid revealing potential exploits.
We will create an open-source database of CVL rules and the code they refer to, to decentralize rule writing and promote decentralized contributions to rules.
We will create a two-week online course on writing rules. The course will be recorded for availability for all developers.
We will hold 2 weekly support Zoom calls for users of the Certora Prover and the new symbolic execution tool. (Aave Forum)
Pricing:
The total price for Certora’s services for a period of 6 months is $1,700,000 with the addition of a one-time payment of $200,000. The one time payment of $200,000 will go to a 3/4 multi-sig wallet controlled by 2 members from Certora, and 2 members from the Aave community. The one-time payment of $200,000 will serve as a fund for paying ‘decentralized community rule writers’. The following transactions will take place upon this proposals passing:
$1,000,000 to be paid in $USDC (vested using Sablier).
$700,000 paid in $Aave (vested using Sablier)
$200,000 transferred to multi-sig wallet with split control between Aave and Certora.
(See implementation section of proposal for full details on transfer:https://app.aave.com/#/governance/66-QmXz9i8zYz2g9XpTP63eKYPZxPftF76hQXr2jzWTMX7zY4)
Proposal:
https://app.aave.com/#/governance/66-QmXz9i8zYz2g9XpTP63eKYPZxPftF76hQXr2jzWTMX7zY4
Links:
Governance discussion: https://governance.aave.com/t/continuous-formal-verification/6308
Sablier: https://docs.sablier.finance/
Certora: https://www.certora.com/
Formal Verification Definition: https://en.wikipedia.org/wiki/Formal_verification
Certora’s Security Rules for Aave: https://github.com/aave/protocol-v2/tree/master/specs
Proposal Payload Contract: https://github.com/Certora/aave-proposal-test
Payload Contract: https://etherscan.io/address/0x879a89d30b04b481bcd54f474533d3d6a27cfd7d
Recommendation:
I recommend that the Rabbithole metagovernance pod vote ‘Yes’ in favor of Aave partnering with with Certora. While the cost may be high, it seems more than worth it in the name of user security. This partnership will be made in an effort to avoid challenges similar to those that Compound has recently faced, resulting in a lot of users losing a lot of funds. Certora has an outstanding reputation, providing critical tooling across countless highly reputable defi protocols. In my opinion, $1,900,000 is a small price to pay when it comes to upholding/securing a stellar reputation such as Aave’s. I believe this proposal is positive sum due to the fact that it adds a much needed extra element of security for not only Aave, but also anybody that deposits their funds with Aave.
Open Questions:
Feedback:
Execution status:
Vote:
Community Vote
31 Y
0 N
Pod Vote
16 Y
0 N
Last updated