Aave-Certora-Secureum: A DeFi Security Collaboration
Part 2
Context
“Don’t Trust, Verify.” is a core tenet of the Crypto space. However, application security in the Ethereum space is dominated today by smart contract security audits where manual analysis — a best-effort approach by human auditor(s) to identify vulnerabilities without necessarily specifying/verifying code properties using formal verification tools — continues to be the trusted technique. The role of tools to assist, enhance and complement manual audits is seeing considerable innovation in recent years, with Certora spearheading this in the formal verification category.
This series of three articles aims to create awareness among readers about the role and advantages of Certora’s technology in the Ethereum smart contract security space, specifically in the context of the Certora-Aave verification grant projects with participation from the Secureum community.
Part 1 of this article series motivated the role of formal verification in smart contract security. It introduced the Certora Prover as one of the leading formal verification tools for Ethereum smart contracts and provided a brief overview of Aave's security initiatives up until now. It concluded with a description of the Certora-Aave Continuous Verification project while underlining the role of Secureum in this collaboration.
Part 2 here dives further into the Continuous Verification project. Highlighting the contracts verified, education efforts, and community participation with rewards, the aim is to showcase the extent to which this initiative has been able to drive awareness. Part 2 concludes by underscoring the challenges & opportunities ahead.
Aave is a decentralized non-custodial liquidity market protocol where users can participate as depositors or borrowers. Depositors provide liquidity to the market to earn a passive income, while borrowers are able to borrow in an over collateralized (perpetually) or undercollateralized (one-block liquidity) fashion. Aave is one of the largest and most popular DeFi protocols having pioneered industry-leading concepts such as flash loans and continuing to innovate on community-led financial, governance, and security initiatives.
Certora is a security firm whose formal verification technology is designed to help developers detect and prevent security vulnerabilities before code is deployed. Certora’s Prover tool is meant to complement/assist manual audits and has been used by industry-leading companies (Aave, Balancer, Benqi, Compound, MakerDAO, OpenZeppelin, Sushi, and more) to prevent more than 100 safety-critical bugs including 20 solvency bugs.
Secureum is a community-centric initiative focusing on the education and evaluation of Ethereum security. It is widely recognized for its smart contract security bootcamps where it collaborates with security partners such as Certora, Trail of Bits, ConsenSys Diligence, Sigma Prime, Sherlock, Spearbit and security-minded protocols such as Aave to raise the bar for Ethereum smart contract security.
Certora-Aave Continuous Verification
In March 2022, Certora received an Aave grant for Continuous Formal Verification and Certora Prover Education focused on the Aave protocol, and has been executing this in collaboration with the Aave community and BGD initiative.
The Continuous Verification grant changed the prior project-based relationship between Aave and Certora to an ongoing relationship for the duration of 6 months (April-September 2022). Certora provided ongoing support and rule-writing for the Certora Prover on Aave’s code, ensuring that the constantly-evolving Aave code remained secure and protecting its users’ assets.
The value proposition was four-fold:
Certora would assign a full time software engineer (with expertise in formal methods and DeFi) to write rules and a security researcher to review each proposed change.
A comprehensive set of rules would be specified for the entire Aave Protocol to assure its continuous security and robustness in the presence of changes coming from governance proposals. Those rules would be checked automatically on changes pushed to the code repository, even for external contributions.
An open source path coverage tool would be developed to continuously scan code paths for more complex rules.
The community would be taught to write security rules for Aave and contributors of new rules would be rewarded. A dedicated grant of up to USD 200,000 was allocated to reward contributions from the Aave community for formal verification using the Certora Prover.
Community Education Grant
A significant focus of the Continuous Verification grant was the Certora Prover Education. The goal was to help the community understand the Aave ecosystem’s security properties and encourage community members to write Certora Prover rules for verifying them. To support this initiative, Certora conducted several workshops and office-hour sessions.
Grant rewards were given to participants who met the following criteria:
Each participant that contributed at least 3 good rules received USD 2,000. Rules were counted only if they were verified or uncovered an issue in the code.
For every additional rule/invariant or issue found in the process, an additional USD 500 was rewarded.
Each participant was limited to a max reward of USD 10,000 per project.
Secureum and Certora had collaborated earlier in March on a Certora Prover workshop for the top performing Secureum community participants. Nine of the 16 invited participants received a significant Certora scholarship for writing interesting Prover rules on a real-world protocol.
For this initiative, Secureum collaborated with Certora and BGD over three months from July-September. The 128 top performing participants from the Secureum community were invited to learn more about the Certora Prover and Aave protocol. With access to Certora tools, training, and personnel, as well as an opportunity to dive deep into the Aave protocol, the Secureum community combined their insights to write Prover rules for the Aave protocol and become eligible for rewards.
Community-driven Verification Projects
Four community-driven Aave verification projects were executed during this six-month period:
Project StaticATokenLM: StaticATokenLM was the first community-driven verification project. This was related to aTokens bridge for Starknet and happened over two weeks from May 15-29. One participant was awarded USD 6,000 for writing 11 rules.
Project AStETH: The goal of this second project was to verify the AStETH.sol contract, which is the AToken of StETH on the AAVE platform. The verification of AStETH on AAVE V2 happened over two weeks from June 12-29, with 5 participants contributing to the security of the contract, writing a total of 25 quality rules and winning a combined USD 19,500 in grants.
Project AAVE Token V3: The third verification project happened from July 1-23 to verify the AAVE Token V3 contracts which implement an ERC20 token for the AAVE governance system on Ethereum.
Out of 25 community members reviewing the code, 19 submitted Prover spec files containing formal specifications resulting in 275 properties in total. Out of those 275 rules, 240 passed Certora’s professional review and their authors were credited with grants. The top 10 community correctness rules were added to the final spec in addition to Certora’s 40 rules to increase the coverage of the specification. Participants won a combined sum of USD 125,500, with 4 contributors winning USD 10,000 and 3 more winning USD 9,000 each.
Project Aave-Starknet Bridge: Between August 15 and September 5, the fourth community verification project was conducted to verify the Bridge.sol contract on the Ethereum side of the Aave-Starknet bridge. This contract implements a bridge on the Ethereum side that acts as an intermediary between users and the Aave platform, enabling the transfer of Atokens to Starknet from the Aave platform on the Ethereum mainnet while handling deposits, withdrawals, and reward claims.
In a collective effort, the community detected a low-severity issue where the initialize function of the bridge did not correctly check the validity of all of its input values. Eleven participants submitted their specifications, contributing a total of 175 security rules and winning a total of USD 57,500 in rewards.
Challenges & Opportunities
Security is a continuous process and is best initiated during the earliest stages of software development, an approach popularly called “Shift Left” in security jargon. As such, the Certora-Aave Continuous Verification project incentivizes community participation in order to make formal specification of correctness properties and their formal verification an intrinsic and initial part of the smart contract development lifecycle. This ambitious goal has challenges that must be overcome to realize the tremendous opportunities for a higher standard in smart contract security.
The mission of integrating formal verification into the smart contract development process includes the following four obstacles:
Appreciation: Formal verification is viewed as something daunting that is required after security assessments/audits and only for the most security-minded, well-capitalized and high-risk protocols (such as Aave). In contrast, the decades old discipline of software engineering teaches us that for any software, specification of properties should be done immediately after requirements gathering and well before implementation. While protocols generally have at least some documentation, very few of them have any specification (even in English) to allow for verification. This lack of appreciation for formal specification and verification stems from a combination of the next three factors. Certora’s goal is to have every protocol formally specify and verify their security properties in the earliest phases of its development lifecycle. Formal Verification First, Not Last!
Access: Security tools and techniques in the Ethereum security ecosystem are slowly maturing and becoming more accessible. Certora is spearheading the formal verification category with its Prover tool, which has already been used to verify the leading DeFi protocols in this space and has found many critical vulnerabilities. Licenses to use the tool are available from Certora and free for education/evaluation purposes. An open-source version is also being developed. Greater Access, Fewer Vulnerabilities!
Awareness: Formal verification typically requires a deeper understanding of formal logic and security properties of the code. It is not a turn-key solution that security enthusiasts or developers can immediately use to find and fix vulnerabilities without in-depth knowledge or at least some prior experience/setup. Mastering such tools has a steep learning curve to understand the domain-specific-language (DSL) used to specify properties (e.g. Certora Verification Language or CVL), to craft meaningful rules/invariants, and to analyze any counterexamples detected so as to identify and fix vulnerabilities. Certora’s educational initiatives, such as the Community Education Grant under this project, are critical to increasing awareness and building a talent pool of security professionals and smart contract developers who know how to use formal verification. More Awareness, Less Carelessness!
Affordability: The Secure Software Development Lifecycle (SSDLC) in Web3 has unfortunately been reduced to a 3-step “Build-Audit(s)-Launch” linear timeline where the audit phase is currently dominated by manual analysis. The high cost of manual audits, driven primarily by the lack of skilled auditors and the demand-supply imbalance, forces typical protocols to seek an audit but skip formal verification. Most audit firms do not yet perform formal verification as part of their audit process. Formal verification services are currently more expensive than manual audits because of an even greater shortage of access and talent. Certora’s approach of providing community access will increase the talent base of Certora Prover experts and hopefully bring down the cost over time. More Users, Less Expenses!
If we overcome these challenges, we have an opportunity to shift the industry towards a new SSDLC paradigm. One where developers think about code correctness properties at the very beginning of the development lifecycle and specify them for formal verification, where they integrate formal verification into the CI/CD process and combine it with other static analysis tools for greater coverage, and where they complement it with manual audits and include manual assessments of the specification rules. In short, one which achieves greater overall assurance about the security posture of smart contracts.
With tens of billions of dollars at stake across various protocols and billions of dollars exploited annually in hacks, the benevolent goals of Ethereum applications are at significant risk due to the overbearing reputational damage from exploits and scams. There has been no better time for Certora, and indeed for the entire Ethereum security community, to further accelerate on delivering the motto of “Move Fast and Break Nothing.”
The final article in this series will talk about the future plans of Certora’s initiatives with Aave and other leading DeFi protocols. Let's Prove-Aave-Secure! 🧐 👻 🔐