We determined that the best strategy to maximize security would be to combine our formal verification efforts with more traditional security audits paired with higher-level formal modeling. Therefore, we partnered with three leading independent security auditors to protect against logical errors and/or potential failure modes in the contract logic.
The following industry experts focused on:
Runtime Verification, an Illinois-based software analysis company, uses runtime verification-based techniques to improve the safety, reliability, and technical “correctness” of software systems. The modelling and review components of Runtime Verification’s engagement have been delivered. The code repository can be found in the MakerDAO’s Github.
The project involved a review of the DSS source code, the development of a K specification that described the high-level behaviors of MCD core and the overall state-updates that each operation in the system should have. It also included reproducing the issues found through our other review and the bug bounty program and adding those tests to the specification. Lastly, it included a random tester and bounded model checker that run on both concrete and symbolic back-ends to ensure the properties hold.
While this engagement has been focused more on designing and building the specification than a traditional audit of the code, it did identify several improvements that could be made in the code and integrated known/previous bugs to give us reasonable confidence in the model's ability to identify similar bugs. Going forward this specification and the resulting model can be used to check that changes to the protocol do not violate the specified system behaviors. We are continuing this work by focusing on applying and directing the tester over random and real world events and continuing to add to the high-level properties of the specification.
The random tester can generate arbitrary sequences of transactions for testing and test them against the known properties of the system. These properties document the intended behavior of the system and act as checks against the traces that the random tester generates. Future governance updates to system parameters and changes to the MCD system itself can be tested against the high-level model and random tester before deploying to mainnet to ensure they do not unintentionally violate the desired system properties. If it is desirable to change the properties, the model and testing can be used to show how the proposed change alters the overall behavior of the system.
Trail of Bits (ToB), a world leader in security, has audited our MCD smart contracts. ToB reviews a broad variety of software, creates security tooling, and consults on the modifications necessary for secure system deployment. Its audit consisted of manual review, automated analysis, and bespoke tool development.
Summary of Findings
PeckShield, a security services organization based in China, had previously and independently verified the Maker DSChief vulnerability that was patched in May. Therefore, we contracted them to do a formal audit.
Summary
In addition to the audit results provided by the three contracted organizations noted above, we were contacted by a third-party security firm, Certora, who presented findings after reviewing the MCD code on their own and with their own tools. We want to thank Certora for independently verifying two important vulnerabilities.
Overall, security audits have covered the following areas within MCD:
Our efforts from all four security tracks have resulted in the discovery of a number of bugs, including some high- and critical-severity issues. We’ve taken steps to evaluate and mitigate these issues, and we will continue to work with auditors to verify that we have completely addressed them pre-MCD launch.