Project Information
CATEGORY
Smart Contracts
NETWORK
StarkNet
WEBSITE
https://makerdao.com/
DESCRIPTION
From July 25th 2022 to February 1st 2023, MakerDAO engaged Veridise to review the security of their Multi Collateral Dai Protocol for StarkNet. The review focused on verifying the functional correctness of various operations within the Cairo version of the VAT contract of the DAI Stablecoin. Veridise conducted this assessment over 14 person-months, with two senior research scientists and one research engineer. The auditing strategy involved tool-assisted analysis of the source code performed by Veridise engineers. Specifically, Medjai was used to formally verify the implementation of the protocol based on functional specifications. Some enhancements to Medjai were developed specifically to enable this verification.
Audit Report
SCOPE
During the course of our audit, Medjai identified a bug while verifying V-MCD-PROP-034. The bug was caused by a mismatch of assumptions between the caller and callee of arithmetic operations in safe_math.cairo, and affected operations that used safe math arithmetic such as fold. This section describes the bug in detail, describes the suggested (and implemented) fix. It also outlines Veridise’s recommendations for continued verification of the protocol as a whole.