A key component of our strategy to maximize security testing by approaching it from different angles and multiple layers to ensure the security of the MCD smart contracts

Formal Verification


# Formal Verification

Overall, the MCD system's core contracts have been fully formally verified, and the verification of peripheral and helper contracts is ongoing. We are now currently working on the formal verification of the tokens that may be voted in as new collateral types, focusing on formally verifying the secondary contracts as well as the governance contracts in the system, and have incorporated formal verification into our continuous testing and release processes. In terms of our in-house efforts, we are leveraging klab, KEVM, and the K Framework for our Formal verification processes.

**Small-step semantics:**

- DSS Core - executable specification
- Exhaustive reachability claims
- EVM bytecode performs as we expect
- Function-level correctness
- Transaction-level correctness

**Big-step semantics:**

- Maker DSL / State Machine
- High-level system model (K)
- System-level invariants
- Exhaustive behaviour checking
- Executable system documentation

**Update - Formal Verification that has been completed thus far:**

- Core system
- Dai token contract
- Auction contracts
- Dai Savings Rate (DSR)
- Emergency shutdown module (ESM)
- The Oracle security module (OSM) has been largely completed.

Overall, the plan is to continue our formal verification efforts on the road to launching MCD, which includes updating past proofs based on the findings of our audits and bug findings.


Introduction

Audit Reports

Bug Bounty Program

Dedicated to providing transparency to our community with respect to the results of our MCD Audits, our Bug Bounty Program, and Formal Verification

Multi-Collateral DAI (MCD) Security

# Multi-Collateral DAI (MCD) Security

These resources are dedicated to providing transparency to our community with respect to the results of our MCD Audits, our Bug Bounty Program, and Formal Verification. It is important to note that this release is the first version and we will continue to add information as it becomes available.

1. Updates On MCD Security Roadmap

    * [MCD Bug Bounty Announcement and Security Roadmap Update](https://blog.makerdao.com/mcd-bug-bounty-announcement-and-security-roadmap-update/) _July 24, 2019_
    * [MCD Security Roadmap Update](https://blog.makerdao.com/mcd-security-roadmap-update-october-2019/) _October 23, 2019_
    * [Publication of the Runtime Verification Audit](https://forum.makerdao.com/t/publication-of-the-runtime-verification-audit/976) _December 19, 2019_

2. [Audit Reports](mcd-security-audits)

3. [Bug Bounty Program](bug-bounty-program)

4. [Formal Verification](formal-verification)




To protect against logical errors and/or potential failure modes in the contract logic

MCD Security Audits


# MCD Security Audits

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:**

- **[Trail of Bits](https://www.trailofbits.com/)** - security reviews of our smart contracts.
- **[PeckShield](https://peckshield.com/)** - traditional audit.
- **[Runtime Verification](https://runtimeverification.com/smartcontract/)** - high-level formal model that can be used to further verify the logic of the system.

# Updates and Results

### [Runtime Verification Specification](https://github.com/makerdao/mkr-mcd-spec)

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](https://github.com/makerdao/mkr-mcd-spec).

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 Final Audit Report](https://github.com/makerdao/developer-portal/blob/master/public/images/security/audit-reports/TOB_MakerDAO_Final_Report.pdf)

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**

- The Trail of Bits team identified two medium-severity issues, four low-severity issues, and eight informational security issues.
- In its audit report, the ToB team noted that our use of formal verification eliminated much of the “low-hanging fruit” in terms of vulnerabilities, and recommended continued use.
- The ToB team also developed several security analysis tools specialized to the MCD codebase. These tools were used throughout the course of the audit to discover bugs, and then delivered to the MCD team once the audit was completed.
- ToB had one specific finding concerning the DSR that we want to address here ([source](https://github.com/makerdao/developer-portal/blob/master/public/images/security/audit-reports/TOB_MakerDAO_Final_Report.pdf), pp. 22). We understand the perceived issue and are exploring the possibilities of how we could apply the DSR to Dai throughout the system. In the meantime, we agree with the risks of users' non-standard ERC-20 proxies for the DSR and have begun R&D on a proof-of-concept implementation. As always, we recommend users practice caution when using third-party smart contracts to interact with the MCD system.
- [Final Audit Report](https://github.com/makerdao/developer-portal/blob/master/public/images/security/audit-reports/TOB_MakerDAO_Final_Report.pdf)

### [PeckShield Final Audit Report](https://github.com/makerdao/developer-portal/blob/master/public/images/security/audit-reports/PeckShield_Final_Audit_Report.pdf)

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**

- The PeckShield team identified one high-severity issue (previously discovered through the bug bounty program), one medium-severity issue, four low-severity issues, and 10 informational security issues.
- In its audit report, the team recognized our independent security efforts: “We always recommend proceeding with several independent audits and a public bug bounty program to ensure the security of smart contract(s).”
- Zero bugs noted in PeckShield’s “17 Typical Smart Contract Coding Bugs” list were found.
- [Final Audit Report](https://github.com/makerdao/developer-portal/blob/master/public/images/security/audit-reports/PeckShield_Final_Audit_Report.pdf)

### Third-Party Audit Results

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.

## In Summary

**Overall, security audits have covered the following areas within MCD:**

- The core Maker Protocol
- Incentive reasoning
- DoS, Replay, Front-running, System/Blockchain-level attacks
- Governance Attacks
- Governance (general)
- Front-end contracts and collateral adapters
- Oracles
- Off-chain price-feed infrastructure
- On-chain oracle contracts
- System deployment and Permissions correctness
- Auctions
- K-dss

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.



# Program Summary

The [Bug Bounty Program](https://hackerone.com/makerdao_bbp/hacktivity?order_direction=DESC&order_field=popular&filter=type%3Abounty-awarded) is a key component of our strategy to maximize security testing by approaching it from different angles and multiple layers to ensure the security of the MCD smart contracts.

### Timeline

- Initiated the Bug Bounty program privately for selected researchers (Private testnet on June 3rd).
- Launched our public bug bounty program on [Hackerone](https://hackerone.com/makerdao_bbp) (July 24th).
- Bug Bounty Program to continue indefinitely.

### Program Scope

The bug bounty program currently contains two separate scopes, which share the same rules with a few exceptions as noted below:

- Smart contracts for Multi-Collateral Dai.
- Infrastructure for select public facing domains (please see the "Ineligible Bugs" section in the **Policy** section on HackerOne, especially regarding third party software, before submitting a report).

**Note:** The program may be expanded in the future to include more asset types such as frontends and apps.

## Updates and Results

Since the launch of the program, three high-severity bugs and one critical-severity bug have been discovered, resulting in bounty reward payments totalling \$90,000. The vulnerabilities consisted of unwanted interactions between the Dai Savings Rate (DSR) module and the Maker Protocol in one case, and the emergency shutdown module and the auctions in another case. The discoveries were in line with our expectations, as these modules either required additional scrutiny or were the most recent ones to be integrated with the system. Given that the security of the system remains our highest priority, we will continue the bug bounty program indefinitely.


Formal Verification

Was this document helpful?

Edit this page

Make the community proud with your contributions