Aave-Certora-Secureum: A DeFi Security Collaboration

Part 1

Introduction

“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 amongst 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.

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 focussing 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 of Ethereum smart contract security.

Part 1 of this series on “Aave-Certora-Secureum: A DeFi Security Collaboration'' motivates the role of formal verification in smart contract security. It introduces Certora Prover as one of the leading formal verification tools for Ethereum smart contracts, provides a brief overview of Aave's security initiatives until now and concludes with a description of the Certora-Aave Continuous Verification project while highlighting the role of Secureum in this collaboration.

Smart Contract Security

Smart contracts for Ethereum are typically written in the Solidity language targeting the Ethereum Virtual Machine (EVM) bytecode. Smart contract insecurities stem from aspects such as intricacies of the Solidity language, misunderstanding of EVM internals, dependency on external contracts/libraries/oracles, lack of input validation under Byzantine threat model, access control failures, reentrancy, DoS and specific application-logic related vulnerabilities. Many of the recent significant vulnerabilities have involved application-specific logic which require understanding, specifying and checking application-specific properties. 

Secure Software Development Lifecycle (SSDLC) processes for Web2 products have evolved over several decades to a point where they are expected to meet some minimum requirements of a combination of internal validation, external assessments (e.g. product/process audits, penetration testing) and certifications depending on the value of managed assets, anticipated risk, threat model, and the market domain of products (e.g. financial sector has stricter regulatory compliance requirements). In contrast, Web3 projects predominantly rely on security audits, which given the immutable nature of blockchains, irreversible transactions and substantial values captured in smart contract applications, have become the de facto requirement in the Web3 space.

Security Audits

An audit is an external security assessment of a project codebase, typically requested and paid-for by the project team. It aims to detect and describe (in a report) security issues with underlying vulnerabilities, severity/difficulty, potential exploit scenarios and recommended fixes. It also provides subjective insights into code quality, documentation and testing.

The goal of audits is to assess project code (with any associated specification/documentation) and alert the project team, typically before launch, of potential security-related issues that need to be addressed to improve security posture, decrease attack surface and mitigate risk.

An audit is not a security guarantee of “bug-free” code but a best-effort endeavor by trained security experts operating within reasonable constraints of time, understanding and expertise.

Audit techniques involve a combination of different methods that are applied to the project codebase with accompanying specification and documentation. These include: specification analysis, documentation analysis, testing, static analysis, fuzzing, symbolic checking, manual analysis and formal verification.

Automated analysis using tools is cheap, fast, deterministic and scalable. Manual analysis with humans is expensive, slow, non-deterministic and not scalable because smart contract security expertise is a rare/expensive skill set today and humans are relatively slower, more prone to error and inconsistent. Nevertheless, manual analysis is a critical part of security audits today because tools cannot yet infer application logic for detecting logic-specific vulnerabilities. Audits driven by manual analysis with assistance from tools for increased efficiency and effectiveness is therefore the norm.

While security-minded projects may have detailed documentation, they rarely have a specification describing in detail (even in English) the expected behavior/properties/invariants of different components and flows. Formal verification forces a change in this mindset.

Formal Verification

Formal verification is the act of proving or disproving the correctness of intended algorithms underlying a system with respect to a certain formal specification or property, using formal methods of mathematics. 

Formal verification is effective at detecting complex vulnerabilities which are hard to detect manually or by using simpler automated tools. Formal verification needs a specification of the program being verified and techniques to translate/compare the specification with the actual implementation. Certora’s Prover is a leading example of a formal verification tool for smart contracts. We note that formal specifications have benefits beyond formal verification — they are good conceptual tools and also make testing and fuzzing more automatic.

Certora Prover

The Certora Prover is a verification tool that takes a low-level EVM bytecode program and a specification written in CVL (Certora Verification Language) and analyzes the code together with the spec to identify scenarios where the code deviates from the specification. It automatically locates critical vulnerabilities that even the best auditors may miss and increases confidence in code security by proving that certain key properties are satisfied.

Key features of the Certora Prover include: 1) Fully Automated Verification, 2) Generation of Counter-Example Scenarios, 3) Rich Specification Language, 4) Powerful Interactive Support, and 5) Specification Checking.

Manual audits and automated testing, while essential, have technical limitations such as those related to scalability, path/state explosion and coverage. Certora’s technology complements them in many ways:

1. Collaborative Specification: Auditing is usually performed by external security personnel who have extensive general experience but may lack a deep prior understanding of the specific contract at hand. Certora’s property-based approach lets developers and auditors work together to formulate properties that specify security-relevant aspects of the contract, allowing more application-specific and deeper logical flaws to be detected.

2. Shift Left: The Secure Software Development Lifecycle in Web3 has unfortunately been reduced to a 3-step “Build-Audit(s)-Launch” linear timeline where there are enormous and unrealistic expectations from the audit phase(s), which is unsustainable. Specifying and checking security properties by developers/experts using Certora tools forces the team to focus on the required/expected behavior of code which in turn facilitates the finding/fixing of mistakes earlier on in the software lifecycle. This will catalyze a “Shift Left” effort where security will be better addressed and significantly improved at initial stages of the application lifecycle.

3. Automatic Rechecking: Every time the code changes, a new audit is needed which requires ideally hiring the same team of external auditors. Scheduling recurring audits or retainers ahead of time at a predetermined cadence can be a significant operational challenge. In contrast, Certora’s approach lets developers specify critical properties early in the development process which can then be automatically rechecked whenever the code changes — Specify Once, Verify Many!

4. Ready Availability: The best auditors are typically booked 6-9 months in advance. Due to the steep learning curve, a lack of structured onboarding resources/initiatives and high expectations combined with low demand for novice auditors, Ethereum may continue to endure a significant shortage of code security professionals in the foreseeable future. Because Certora’s approach leverages automatic verification techniques to reduce the repetitive effort needed, its services are more readily available to developers/experts who can specify properties on their code.

5. Stronger Guarantees: Any small mistake or oversight from an auditor can cause a critical vulnerability to be missed. Even the best auditors make mistakes, so, not surprisingly, the Certora tool suite has found major vulnerabilities even after extensive auditing. In the Certora approach, all attention can be focused on specifying the properties. Since the checking of the properties is fully automated, a successful check guarantees mathematically that the property holds. The prover, unlike a human auditor, never makes reasoning errors. A failed check helps the developer pinpoint a failing case.

The Prover can not only complement manual auditing but also work well together with it. Manual audits can help specify new rules or identify missing rules, while Prover can identify corner cases missed by manual audits especially when code is continuously modified over time. Certora Prover can therefore prove to be an invaluable and indispensable component of the Ethereum application security suite.

Aave Protocol & 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.

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.

Aave has therefore been designed to ensure that the protocol adheres to the highest security standards. It has been audited by some of the leading security firms such as ABDK, OpenZeppelin, Peckshield, Sigma Prime and Trail of Bits, along with formal verification by Certora. Certora has been working with the Aave team since before V2 protocol. They have formally verified the various iterations of the AAVE token, and significant parts of the V2 protocol where they found and prevented 6 high severity issues before deployment, including a solvency vulnerability.

Bored Ghosts Developing (BGD) is an initiative founded by 3 well-known Aave community members (Ernesto Boado, Emilio Frangella and Andrey Kozlov) with deep technical expertise on Aave and DeFi in general. The BGD initiative was approved by Aave governance in May 2022 to provide support on the development of the Aave ecosystem from the community.

One of the key missions of BGD is: Security before Pace — “Aave has moved really fast in the past and should keep doing the same in the future. But it is important to highlight that pace was always secondary versus the security of what was delivered on the ecosystem. As the size and complexity of Aave grow, this order of priority needs to be kept, and that is our mentality.”

Certora-Aave Continuous Verification

Certora received an Aave grant for Continuous Formal Verification and Certora Prover Education focussed on the Aave protocol, and has been executing this in collaboration with Aave community and BGD initiative.

The Continuous Verification grant changed the prior project-based relationship between Aave and Certora to an ongoing relationship, where Certora provides ongoing support and rule-writing for Certora Prover on Aave’s code to ensure that the constantly-evolving Aave code remains secure to protect its users’ assets.

A key focus of this grant is the Certora Prover Education to educate and encourage the community to understand security properties of the Aave ecosystem and write Certora Prover rules for verifying them. Certora has led many education initiatives towards achieving this goal.

Secureum collaborated with Certora and BGD Labs over the last three months (July-September) to further catalyze their unique initiative by inviting 128 top participants from the Secureum community to learn more about Certora’s Prover and Aave protocol. With access to Certora tools, training, team, and an opportunity to dive deep into the Aave protocol, the Secureum community combined their learnings to write Prover rules for the Aave protocol and received significant grant rewards.

With this collaboration, Secureum enhanced its community-focussed mission to “educate and evaluate Ethereum security” and make Aave more secure with formal verification techniques pioneered by Certora with deep Aave insights from BGD Labs. 

The next article in this series will dive deeper into the Continuous Verification projects by highlighting details of the verified smart contracts, education efforts, community participation, rules submitted, evaluation criteria and rewards distributed. This will help showcase the extent of community awareness/participation generated by this initiative and the challenges & opportunities ahead.

Let's Prove-Aave-Secure! 🧐 👻 🔐