<h1>
<a name="executive-summary-1" href="#executive-summary-1"></a>Executive Summary</h1>
<p>This is a continuation of proposal <a href="https://governance.aave.com/t/continuous-formal-verification/6308">6308 <span>19</span></a> to improve the security of smart contracts built on top of Aave using a combination of formal verification and manual code review. In the last six months, Certora has improved the security of the Aave protocol and played a significant role in increasing the security community’s involvement in Aave’s development. We want to continue to improve Aave’s security and enable agile development of new products. This proposal will give a brief overview of Certora and formal verification, outline what we’ve accomplished in the last six months, and discuss our goals for ensuring Aave’s security.</p>
<h1>
<a name="overview-2" href="#overview-2"></a>Overview</h1>
<p>Certora is a security company focused on delivering tools that enable developers to mathematically prove the correctness of DeFi protocols. In the last six months, Certora worked closely with the Aave community, Aave developers, BGD labs, and external communities, including <a href="https://www.secureum.xyz/">The Secureum <span>1</span></a>, to guarantee the security of the Aave protocol and enable massive innovation.</p>
<p>We engaged twenty external security researchers who, along with our team of security engineers and researchers, helped Aave safely develop 16 new products and list 12 new tokens. A total of 51 smart contracts were reviewed which contained over 25,000 lines of Solidity code. One critical and two high-severity bugs were prevented using the hundreds of correctness rules written by the community and the Certora team.</p>
<p>As we continue our collaboration, we plan to improve on the current proposal in five significant ways: (1) allocate more resources, (2) improve the Certora Prover, (3) develop new open source technology for automatically checking rules written by the community, (4) drastically improve the collaboration with auditors and the security research community, and (5) develop a monitoring framework for checking the CVL rules before every transaction.</p>
<h2>
<a name="about-certora-3" href="#about-certora-3"></a>About Certora</h2>
<p>Our technical team of over 80 people consists of formal verification experts, compiler experts, static analysis experts, research and development engineers, security engineers, and security researchers. Many have PhDs in their fields, decades of security experience, and a strong history of significantly increasing the security of the most significant protocols in DeFi [<a href="https://www.certora.com/wp-content/uploads/2022/02/AaveV3Jan2022-1.pdf">Aave</a>, <a href="https://www.certora.com/wp-content/uploads/2022/02/OpenZeppelinGovernance7Dec2021.pdf">OpenZeppelin <span>2</span></a>, <a href="https://hackmd.io/@SaferMaker/DAICertoraSurprise">MakerDAO</a>, <a href="https://www.certora.com/wp-content/uploads/2022/02/EulerNov2021.pdf">Euler <span>1</span></a>, <a href="https://www.certora.com/wp-content/uploads/2022/06/CometReport-1.pdf">Compound <span>2</span></a>, <a href="https://medium.com/truefieng/preventing-billion-dollar-hacks-403d7bffac75">TrueFi</a>].</p>
<h1>
<a name="project-highlights-march-13-2022-september-12-2022-4" href="#project-highlights-march-13-2022-september-12-2022-4"></a>Project Highlights: March 13, 2022 - September 12, 2022</h1>
<p>The Aave protocol is leading DeFi in innovation and security, supported by Certora’s technology and the security research community. The Certora team worked closely with BGD labs and the Aave protocol team to ensure code security using funding from the previous continuous verification proposal. We outline the main highlights of Certora’s contributions during the six months of the project:</p>
<ul>
<li>Certora allocated six R&amp;D personnel and engaged twenty external community security researchers to review protocol contracts, most new to the Aave community. Secureum was very helpful in developing this community.</li>
<li>16 new Aave products were developed under our security review, and 12 new tokens were listed, all checked by the Certora Prover for bugs and nonstandard behavior.</li>
<li>51 smart contracts were reviewed, totaling 25,000 Solidity lines of checked code (the Certora Prover checks the generated EVM byte code, which is much larger).</li>
<li>A total of 380 correctness rules were selected out of 600 submitted rules by the Certora team and the Aave community. Unlike traditional security audits, these specifications continue to be useful as protocols continue to evolve.</li>
<li>Certora provided three workshops to familiarize the community with our tools.</li>
<li>$283,500 were awarded in grants to the community. $151,000 of these awards came from the grants allocated by Aave in the original proposal; Certora provided the additional $132,500. As of September, twenty security researchers composed over 550 security rules for Aave and won 35 grants.</li>
<li>One critical, Two high-severity, One medium-severity and Ten low-severity bugs were prevented before the code was deployed.</li>
<li>No major bugs were identified in manual audits by Chain Security and Sigma Prime after formal verification and in the deployed code.</li>
<li>A dedicated dashboard for verified smart contracts is maintained <a href="https://www.certora.com/dashboards/aave-dashboard/">here <span>5</span></a>.</li>
<li>A dedicated dashboard for checked listed tokens is maintained <a href="https://www.certora.com/erc20s/aave-listings/">here <span>2</span></a>.</li>
<li>Three complementary papers are being written by The Secureum, BGD Labs, and Certora which describe the main lessons learned from the three-way collaboration. The first article is titled <a href="https://secureum.substack.com/p/aave-certora-secureum-collaboration?r=15ftav&amp;utm_campaign=post&amp;utm_medium=web">“Aave-Certora-Secureum: A DeFi Security Collaboration” <span>4</span></a>.</li>
</ul>
<h1>
<a name="the-new-proposal-keeping-aave-agile-and-safe-5" href="#the-new-proposal-keeping-aave-agile-and-safe-5"></a>The New Proposal: Keeping Aave Agile and Safe</h1>
<p>We propose to continue the current engagement. Below are the highlights of what we will accomplish:</p>
<ul>
<li>Allocate six R&amp;D personnel to lead the community in specification development for the Aave protocol.</li>
<li>Write specifications and verify new Aave products and listed tokens.</li>
<li>Provide free access to our SaaS tooling (Certora Prover) to members of the Aave community.</li>
<li>Develop and improve our technology to address needs raised by the Aave verification efforts. We will continue to provide new tools to the Aave community as they are developed.</li>
<li>Develop our education materials and be available to the community to help them learn to use our tools.</li>
<li>Continue to grow Aave’s security community and incentivize the best of this community to engage with Aave more closely. We propose to award several fellowships to the best security researchers to work closely with Aave and Certora. We have identified leading candidates who contributed to this year’s program.</li>
<li>Certora will collaborate with Sigma Prime to help them use the Certora Prover as part of their <a href="https://app.aave.com/governance/proposal/?proposalId=88">ongoing security review <span>1</span></a>. We will also collaborate with other third parties such as Secureum, who are working to ensure the security of Aave and building the Aave community. Additionally, <a href="https://code4rena.com/">Code4rena</a> and <a href="https://spearbit.com/">Spearbit</a> security researchers are proficient in rule writing. For example, Kurt Barry, who works as an independent security researcher through Spearbit, was able to find a <a href="https://hackmd.io/@SaferMaker/DAICertoraSurprise">4 year old bug in the MakeDao tool using the Certora Prover.</a> Therefore, for major code revisions, we will conduct Code4rena competitions for finding bugs and writing correctness rules.</li>
</ul>
<h1>
<a name="pricing-6" href="#pricing-6"></a>Pricing</h1>
<p>The previous proposal cost $1.7M per 6 months. A 20% discount is given for an annual contract ($3.4M), bringing the total to $2,700,000 for a year while maintaining the level of service provided by Certora. In addition, Aave will provide 400,000 USDC for fellowships and community grants. The total cost to AAVE will be $3,100,000.</p>
<p>This community grant will be partially used to support designated fellowships to security engineers who are engaging with the Aave DAO on a part-time basis and potentially long-term collaborations with the DAO. We have identified several candidates who participated in the previous grant program and contributed significant rules throughout the project and expressed interest in participating in the fellowship program.</p>
<p>The price for the project is per annum, and vested linearly over one year. 30-day termination is possible with a vote. $1,890,000 is paid in USDC and $810,000 is paid in Aave tokens. 400,000 USDC are awarded to security researchers from the Aave community for reviewing code and writing security rules, as well as the fellowships. The receivers of the fellowship will be selected by a community with two people from Aave BGD, one person from the Aave team, and two people from Certora. Unutilized grants will be returned to Aave.</p>
<hr />
<p><strong>UPDATE 30 October 2022:</strong></p>
<p>Following the community’s feedback, Certora decided to fund the grant program in the original sum of $400K per year. No fellowships will be awarded as part of the grant.</p>
<p>This reduces the total cost of this proposal to the Aave community to $2.7M.</p>

Security and Agility of Aave Smart Contracts via Continuous Formal Verification 
  Executive Summary 
 This is

Security and Agility of Aave Smart Contracts via Continuous Formal Verification

<h1>
<a name="summary-1" href="#summary-1"></a>Summary</h1>
<p>A proposal for significantly and continuously improving the security of the Aave platform and the dApps built on top of it, by offering our formal verification and path coverage tooling service to the Aave Platform contributors and the Aave Protocol dApp developers. The initial proposal is for 6 months starting January 2022. A discount price is given for an annual contract.</p>
<h1>
<a name="background-2" href="#background-2"></a>Background</h1>
<h2>
<a name="aave-security-3" href="#aave-security-3"></a>Aave Security</h2>
<p>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.</p>
<p>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.</p>
<p>These risks were highlighted by a recent incident in which a bug was introduced in a <a href="https://compound.finance/governance/proposals/62">Compound governance proposal <span>16</span></a>, leading to huge nonrecoverable financial losses. Of course, such bugs are not exclusive to Compound— they have been affecting many DeFi protocols.</p>
<p>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.</p>
<h2>
<a name="about-certora-4" href="#about-certora-4"></a>About Certora</h2>
<p><a href="https://www.certora.com">Our team <span>18</span></a> consists of 31 experts in smart contract security, <a href="https://en.wikipedia.org/wiki/Formal_verification">formal verification <span>11</span></a> methods, and compilation techniques. 9 of our team members have PhD in formal verification. We have built a world-class and unique developer tool that seamlessly integrates into CI/CD, allowing continuous verification of contract correctness.</p>
<p>We enable companies to “move fast and break nothing”, taking months off of the time to market, by decreasing code audit time. Our product, the Certora Prover, allows both pre- and post-deployment code verification: it statically analyzes the code before it is deployed but also runs on the EVM bytecode of the deployed contracts. The product verifies code by checking that it obeys high-level semantic rules. For example, a rule could assert that the sum of token balances remains unchanged by all operations that do not mint new tokens. A free demo of the Certora Prover can be found <a href="https://demo.certora.com/">here <span>13</span></a>.</p>
<p>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 <a href="https://blog.soliditylang.org/category/security-alerts/">critical security bugs <span>3</span></a> in the Solidity compiler itself and in deployed contracts of major DeFi organizations.</p>
<h2>
<a name="certora-and-aave-relationship-5" href="#certora-and-aave-relationship-5"></a>Certora and Aave relationship</h2>
<p>We have been working with the Aave team since before V2 protocol. We’ve formally verified the various iterations of the AAVE token, and significant parts of the V2 protocol. <a href="https://www.certora.com/pubs/AaveV2Dec2020.pdf">We found and prevented 6 high severity issues in V2 before deployment, including a solvency bug. <span>4</span></a> We will soon be working on the next major upgrade to the protocol. Our security rules for Aave are <a href="https://github.com/aave/protocol-v2/tree/master/specs">publicly available <span>3</span></a> and serve as a useful tool for contract upgrades and integrations. Protocols that integrate into Aave could use these rules and run their code against them to make sure the integration process is smooth. Making this service more accessible is part of this proposal.</p>
<h1>
<a name="proposal-6" href="#proposal-6"></a>Proposal</h1>
<p>We propose two approaches to significantly increase the confidence in the platform itself and in the smart contracts built on top of it.</p>
<p>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 who contribute to Aave’s ecosystem: Aave’s in-house developers, community contributors and dApp developers. This will ensure that the constantly-evolving code of Aave’s platform remains secure, protecting its users’ assets.</p>
<p>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.</p>
<p>The two approaches are complementary: Our continuous rule-writing for the Certora Prover will mathematically prove that critical code areas are secure, while the symbolic execution tool will be more comprehensive, running 24/7 to continuously increase the coverage for specifications that are too complex to prove using the Certora Prover.</p>
<p>In the following sections, we will specify the deliverables of our proposal.</p>
<h2>
<a name="continuous-high-level-cvl-rules-specification-for-the-aave-ecosystem-contributors-7" href="#continuous-high-level-cvl-rules-specification-for-the-aave-ecosystem-contributors-7"></a>Continuous High-Level CVL rules specification for the Aave Ecosystem Contributors</h2>
<p>We will write high-level correctness rules in English and in <a href="https://certora.atlassian.net/wiki/spaces/CPD/overview">CVL <span>9</span></a>, Certora’s domain-specific specification language, for DeFi smart contracts built on top of Aave, as well as for the Aave platform itself via its contributors. These rules will be used later for the Certora Prover and the new symbolic execution tool.</p>
<p>In the process of writing the rules, we will perform a code review and identify bugs manually. We will allocate an expert software engineer for the entire period of the contract, dedicated to Aave. Normally, customers wait several months for our services, while here Aave will receive ongoing support. This engineer will update the rules to capture the essential security properties of the Aave Protocol and its derivatives. Also, we will update the rules when bugs are found.</p>
<p>Fitting the DeFi community spirit, we will make the CVL rules open-source, allowing decentralized rule writing and rule auditing. This will allow knowledge-sharing in rule writing between contributors and dApps developers, as different developers could use rules fitting their purposes which were written by others.</p>
<h2>
<a name="formal-verification-of-smart-contracts-during-cicd-8" href="#formal-verification-of-smart-contracts-during-cicd-8"></a>Formal Verification of Smart Contracts during CI/CD</h2>
<p>The above rules will be used by the Certora Prover, which will be available to all Aave platform developers. Rules can be developed using a new VSCode extension, with tooling to integrate CVL specs to the Solidity code project. The extension will also be able to invoke the Certora Prover, and present an ongoing status of the rules: whether they are proven or violated. When a rule is violated, the extension will return a concrete call-trace showing the input for which the rule is violated, in a view similar to a debugger.</p>
<h2>
<a name="code-coverage-for-smart-contracts-9" href="#code-coverage-for-smart-contracts-9"></a>Code Coverage for Smart Contracts</h2>
<p>This project is inspired by the <a href="https://www.youtube.com/watch?v=12oEACM5UEU">Sage Direct Fuzzing Project <span>6</span></a> which prevented million-dollar bugs for Microsoft.</p>
<p>We will develop a new symbolic execution product for increasing code coverage of the Aave smart contracts. For each smart contract, the product will automatically generate inputs, enumerating over time more and more control flow execution paths using SMT solvers, in pre and post-deployment. This complements formal verification when the code is too complex for it or when using it is too labor-intensive.</p>
<p>This is similar to Dynamic Monitoring provided by <a href="https://techcrunch.com/2021/09/30/forta-launches-with-23m-to-bring-better-security-to-smart-contracts/">Forta</a>, however, our tool is different in two aspects: it uses high-level security rules and leverages SMT solvers for triggering rarely executed scenarios. The code developed in this project will be open source to allow contributions from the community. This means that every developer can get access to a security tool for her/his smart contract.</p>
<p>In addition to creating the product, we will create a dashboard that will report the inputs and the paths covered by the different inputs, as well as rule violations that may occur. Also, for each input, we check that every CVL rule holds, which will also be reported.</p>
<h2>
<a name="measures-of-success-10" href="#measures-of-success-10"></a>Measures of Success</h2>
<p>Certora Prover takes as input a contract and a specification and formally proves that the contract satisfies the specification in all scenarios. Importantly, the guarantees of Certora Prover are scoped to the provided specification, and any cases not covered by the specification are not currently checked by Certora Prover.</p>
<p>In general, we note that there is no silver bullet in smart contract security and in formal verification specifically. Still, we plan to measure success according to the following KPI: (1) the number of paths covered by the symbolic execution tool, (2) the number of rules formally proved, (3) the number of bugs identified by the Certora Prover before deployment, (4) the number of bugs identified by the path coverage tool, and (5) the number of missed bugs in code analyzed by Certora found by auditors and other means. The numbers will be available on a daily basis.</p>
<h1>
<a name="certora-services-summary-11" href="#certora-services-summary-11"></a>Certora Services Summary</h1>
<p>We offer the following services by the company:</p>
<ul>
<li>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.</li>
<li>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.</li>
<li>We will develop an open source directed fuzzing engine on top of modern <a href="https://en.wikipedia.org/wiki/Satisfiability_modulo_theories">SMT <span>3</span></a> solvers.</li>
<li>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.</li>
<li>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.</li>
<li>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.</li>
<li>We will create a two-week online course on writing rules. The course will be recorded for availability for all developers.</li>
<li>We will hold 2 weekly support Zoom calls for users of the Certora Prover and the new symbolic execution tool.</li>
</ul>
<h1>
<a name="pricing-12" href="#pricing-12"></a>Pricing</h1>
<ul>
<li>The project price is $1,700,000 for 6 months or $3,400,000 for 1 year. For a 6 months period, $1,000,000 is paid in USD and USDC. $700,000 is paid in Aave tokens vested linearly over a year period. A 20% discount is given for an annual contract bringing the total to $2,720,000 for a year.</li>
<li>An additional sum of $200,000 will be paid to Certora and purposed for paying decentralized community rule writers. This sum will not be used for any other purpose.</li>
<li>The normal price for our services is $70,000 per week for rule writing subject to availability. We are booked 6 months in advance. The SaaS fees are $2000 per month for each user. Here we allow 52 weeks and an unbounded number of users.</li>
</ul>

Security and Agility of Aave Smart Contracts via Continuous Formal Verification

Continuous Formal Verification

Got something to add?