With the launch of Multi-Collateral Dai (MCD), the Maker Foundation worked with the community to deliver a major milestone for the DeFi ecosystem. Rather than the end point, the initial deployment of the MCD system is the start of a continuous process of extending and improving the protocol.
Not only will the Maker protocol be extended with new functionality, the quality and security of the system are also reviewed on an on-going basis. This was already illustrated by the publication of our permanent security overview site, as well as the bug bounty program which is still on-going without end date.
On October 23rd, the Maker Foundation posted the latest update of the MCD security roadmap discussing the details of multiple audits. At the time, we published and discussed the findings of the Trail of Bits and Peckshield audits that were done on the MCD code base.
Runtime Verification Audit
A third team, Runtime Verification, had already completed their high-level model of the core MCD system and just begun building models of the other modules. In the meantime, the remaining models for MCD have been completed and we’re happy to publish these results today.
Read the update below, have a look at our updated security overview site, or visit the github repository for more technical details. Any questions and comments can be posted in this forum thread and the Foundation smart contracts team will be happy to reply.
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.