Hello everyone,
As Compound’s Security Advisor, I’d like to clarify a few things around how we, at OpenZeppelin, expect Certora’s Formal Verification Proposal to work within our existing partnership and Compund’s overall security.
Past Discussions of Formal Verification
As we mentioned during the Audit Proposal discussions in November, we see Formal Verification (FV) as a component of an overall holistic security process that must include coding best practices, manual auditing, education, threat monitoring, other testing suites and bug bounties. We have an existing relationship with Certora and are fans of the progress their technology is making but we leave the decision of pricing and vendor selection up to the Compound community. We had previously mentioned the possibility of offering FV security services but that never materialized in our existing proposal since there was no active FV vendor at the time.
Audit Scope for FV Rules
Formal verification is only as good as the initial description of the desired properties of critical elements of the protocol, which is why it is important that FV rules are written correctly. However, given the current scope of our security partnership, OpenZeppelin auditors would not be involved in either writing or reviewing FV rules. We’ve learned how important it is to prioritize auditor time to avoid backlogs on important proposals and reviewing FV rules line-by-line in addition to the code would mean potentially doubling the timeline of any audit engagement on protocol changes.
During our audits, we do often look at tests to understand developer intentions in the code but we do not offer security reviews of the tests themselves and FV rules would be no different in this regard. We would assume that any necessary FV-specific supporting services will be performed separately by the Certora team as part of their proposal.
This all being said, we do think that having robust FV rules would enhance the security of governance proposals and would be a good way to prepare for an audit by catching bugs during development. We already recommend that our audit clients build a robust test suite, which can include FV, as part of their Audit Readiness.
Other Clarifications
There are a few other things we wanted to address from the forum discussion:
- Asset Listings - Asset Listing Proposals would certainly be a good use for FV and could cover some of the items in our recent Asset Listing Checklist. However, it’s important to note that not all checks may be possible with FV rules written for Compound on external assets so additional security tooling and manual checks may still be necessary.
- Comparison to Forta - @shelly earlier mentioned that Certora’s Code Coverage tool was similar to the Forta Network being used in our monitoring solution for Compound. It’s important to distinguish that Certora’s tooling here is used for evaluating code prior to deployment while Forta is built to monitor live smart contract events after deployment in either the protocol itself or external contracts such as oracles and ERC20 contracts for CToken markets. We see these two tools as entirely separate to be used for different security needs.
- Security Decision-maker - Certora makes mention of both Compound Labs and a “Compound security team“ that would be involved in deciding new FV rules and handling payments to community rule-writers. When OpenZeppelin has needed the DAO to make security-related decisions, we’ve defaulted to asking the Guardian Multi-sig but we’re happy to go with Labs or a different entity if that’s preferred by the community. Therefore, we’d like to understand if Certora expects Compound Labs to be the decision-maker in all these instances or if they are expected to fall elsewhere. In any case, it’s important that security decision responsibilities are clearly defined to avoid confusion and potential problems in the future.
Summary
Overall, more security tooling is always a good thing and we’re happy to see discussions on additional ways to protect Compound beyond just security audits, advisory and monitoring. OpenZeppelin’s feedback above is intended to be neutral on Certora’s proposal since we believe this needs to be guided by Compound’s vendor selection process. Our goal here is to clarify some assumptions on how OpenZeppelin’s existing partnership would be impacted and where FV could be used in Compound’s proposal lifecycle. We leave it to Certora and the community to decide how they’d like to proceed.