When developing projects for the Ethereum network, writing the smart contracts’ code is only a fraction of the work. Most of the development time is spent on requirements analysis and quality assurance, in particular, to guarantee the safety of the system.

The Maker Foundation has always been committed to the highest security standards and, of course, that won’t change with the release of Multi-Collateral Dai (MCD). This blog post provides an overview of the security roadmap that our teams are working on in the run-up to launch.

Security Roadmap Tracks

The MCD security roadmap consists of four parallel tracks: 

1. An extensive Bug Bounty Program hosted in collaboration with HackerOne. The program will run for an indefinite period, continuing after MCD launch. 
2. Formal Verification of the smart contracts to the fullest extent possible with today’s technology.
3. Independent third-party Security Audits by leading auditors in the industry. 
4. An Integration Partner Program to test MCD in collaboration with our closest partners in a realistic environment. 

Each track is detailed below.

Bug Bounty Program

In June, we invited select researchers to a private version of the bug bounty program. Today, we announce the public version, which will progress in iterations as we near the launch of MCD:

• The scope of assets will increase, and assets already in scope may also receive minor updates.
• Bug bounty amounts will increase.

The initial scope is a selection of MCD smart contracts as deployed on Ethereum Kovan testnet; more assets will be added toward MCD launch. The scope may also expand to include web applications, tools, etc.

For this iteration of the program, we will award $50,000 for discovery of a bug classified as Critical, in addition to smaller rewards for High-, Medium-, and Low-severity bugs.

The program is planned to continue indefinitely after the launch of MCD.

To learn more and participate as a researcher, please visit the HackerOne program page.

Formal Verification

Formal verification of programming code is typically done for software that is most critical in engineering systems. It is, for example, applied in aerospace engineering to guarantee accuracy of safety-critical functions. More specifically, formal verification guarantees that the low-level bytecode, which is executed by the computer, correctly reflects the intentions of the software developer and has no unintended side effects.

Due to the high stakes and immutable nature of the blockchain, which prevents easy patching of software bugs after the initial deployment, the practice of formally verifying smart contracts has become somewhat standard in the Ethereum ecosystem. Maker has always been at the forefront of this practice and was one of the first to apply the methodology to a major dapp. 

Since the formal verification of the MCD core contracts, a lot more ground has been covered. It is our goal to formally verify not only those core contracts, but also as many MCD system contracts as is technically feasible.

Formal verification of the core system, the Dai token contract, the auction contracts, the Dai Savings Rate (DSR), the emergency shutdown module, and the oracle security module (OSM) has been largely completed. 

The team is still working to formally verify the secondary contracts and governance contracts in the system. Most notably, these are the vote proxy contracts, the CDP manager contract, and the so-called join/exit path of collateral adapter contracts, which handles the locking and freeing of collateral in the system.

Security Audits

While formal verification of the contracts guarantees that the low-level bytecode accurately reflects the intention of the software developer, it also comes with a number of limitations. For example, it does not protect against logical errors in the contracts, nor can it look beyond the scope of a single transaction.

For this reason, formal verification of the contracts should always be combined with more traditional security audits and, if possible, higher-level formal modeling. 

This is exactly what the Maker Foundation is doing. We are procuring not one but three independent security audits by leading industry experts:

1. A collaboration with Runtime Verification, an Illinois-based company that will create a high-level formal model that can be used to further verify the logic of the system. If formal verification of the contracts can be compared to a unit test, then this would be the equivalent of formal integration testing.
   
   
2. An audit by Trail of Bits, our long-term partner for security reviews of our smart contracts. Trail of Bits will specifically focus on areas that are not well covered by formal verification.
   
   
3. A more traditional audit by PeckShield, a relative newcomer in the industry based in China and founded in early 2018 by industry veterans. PeckShield independently verified the Maker DSChief vulnerability that was patched in May of this year.

Integration Partner Program

Bug bounty programs, formal verification, and external auditing are great tools to guarantee the safety of the MCD system as a stand-alone unit. But, while the system holds a great deal of promise, it is only with partner integrations that the ecosystem will truly thrive.

The Maker Foundation is working closely with a select group of integration and business partners to test MCD in a realistic setting, further decreasing the odds of any vulnerabilities slipping through the cracks. 

If you’d like to join the integration partner program, contact our integrations team at [email protected].

Next Steps

As we near the launch of MCD, our teams are working hard to complete the roadmap described above. We look forward to working with the community and our partners to deliver a system with the top-notch security that our users expect. 

Beyond security and behind the scenes, our teams are working on additional infrastructure that will assist our integration partners and our own QA engineers with the rigorous testing that this project requires. 

To that point, be on the lookout for the next security update, which will discuss our Staxx platform for end-to-end testing and QA.
For more on MCD, read Introduction to Auctions and Keepers in Multi-Collateral Dai and Collateral Onboarding Guide: How to Nominate Tokens for MCD