@jared thanks for joining the discussion!
I have tried to break out each of your questions with answers below:
What about Formal Verification (FV)?
As you may be aware we are trying to use formal verification on critical components of the OpenZeppelin Contracts Library. We see FV as helping to lower the overall risk footprint but FV also has its clear limitations. Therefore, we see FV as a component of an overall holistic security process that must include coding best practices, manual auditing, education, threat monitoring and bug bounties (our internal process encompasses all of these). Formal verification is only as good as the initial description of the desired properties of critical elements of the protocol, which is why manual auditing is still a critical step in the overall program. We have relationship with Certora and are fans of the progress their technology is making but would be happy to work with whichever formal verification vendor Compound chooses and implements. Security as you indicated is not about looking for a “silver bullet” but layering in services, processes, and technologies to lower overall risk exposure. We would be happy to include additional work and cooperation with Compound’s desired FV vendor as part of this existing proposal. Our PSO and auditors can aid in ensuring that the desired properties of the protocol are described properly from a security perspective, so the FV vendor can write the rules effectively for implementation.
Would this include all new contracts developed by the community and adopted by governance?
Yes, that's the expectation. Any substantial changes to the Compound protocol would be covered by an OpenZeppelin audit. Audit times would be set aside in advance for upcoming proposals and protocol changes. We would commit to auditing all community-supported proposals on a timely basis. That said, not all proposals are created equal; some will be high priority for the protocol and some will be low priority. We expect to work with the community on helping us separate the signal from the noise
Logistically speaking, when can a proposal be submitted for audit? If we are truly just monitoring proposals that have been made on-chain, that seems not nearly enough time for an audit and a response to the audit. In that case, what would the actual process of scheduling an audit look like? What sort of lead times should the community expect?
As part of the Advisory Solution, the first task of the OpenZeppelin Protocol Security Officer (PSO) is to propose to the community a clear approach and process as to how security audits and security related issues would be incorporated into the proposal lifecycle. From our perspective, security audits should be a prerequisite for submitting a governance proposal that makes changes to the protocol.
Once a potential community proposal has initial support and begins development, the submitter will work with the PSO and dedicated OpenZeppelin auditors to ensure the agreed defined process is followed, and everything is ready for code completion in the most efficient way possible.
The initial proposal is considered code complete with a frozen commit, it would then be submitted to the OpenZeppelin Audit team for audit.
Based on similar audits (e.g. Celo governance upgrades) our initial estimates suggest 2 weeks for auditing minor protocol proposals although exact time required depends on the lines of code and complexity. This includes 1 week for the audit and another week for reviewing fixes although this timing also depends on how quickly the proposal submitter responds with fixes. Once the final report is finalized and shared with the Community, the proposal will be able to move forward with the governance process starting with the two day review. Good communication between the OpenZeppelin team, the submitter, and the community will be critical and will be managed by the PSO. Please note that we have been conservative in these estimates, it's our assumption that we can improve the timeliness based on improved processes, developer education and good community communication.
Before auditing new proposals it's our expectation that we will do a full protocol audit, starting out with existing critical components of the Compound protocol which should include the governance contract, Comptroller, and other components typically involved in governance proposals. This initial audit will ensure that OpenZeppelin can take full ownership for the security for the entire protocol and give our auditors the necessary context to review new protocol changes.This would take approximately 7-9 weeks based on our knowledge of the existing Compound code base, we would begin this audit as soon as possible upon acceptance of this proposal.
I have attached an example to illustrate the process:
Proposal 62 would have consisted of the following steps:
- Late July - Forum post responding to RFP16 is made and development begins on the proposal changes. The PSO is made aware of the proposal in progress and works with the submitter to prepare for an audit in accordance with community guidelines.
- September 13th - Proposal code is completed as a Pull Request with a frozen commit one week prior to audit start
- September 20th - Audit begins the week of Sep 20th and ends that week on Sep 24th. An audit report is delivered to the submitter no later than Sep 27th.
- September 27th - Submitter addresses bugs found and submits fixes to the audit team to review. The audit team reviews the fixes and updates the report.
- October 4th - The report is finalized and shared with the Community. The proposal is able to move forward with the governance process starting with the two day review.
I hope this clarifies our willingness to support FV as a component of an overall holistic security process, and the way we are thinking about integrating our offering into the Compound Community governance process.
Steve Gant
OpenZeppelin