Protocol Engineering & The Road to DeFi Safety

Maker’s holistic Safety and Security Strategy

The Protocol Engineering Core Unit would like to present our thoughts for a holistic strategy and roadmap to promote and improve Maker Protocol safety. Our proposal puts forth new paradigms, processes and tools to ensure the long term robustness of the system while accommodating short term innovation and delivering continuous value.

Building upon this strategy will allow us to innovate, evolve and ship quickly without sacrificing safety and security. We will be better prepared to move fast and not break things.

By adopting a safety-engineering mindset, we have broken our strategy into three key pillars:

1. Decision Support, includes tooling to provide more effective ways for reasoning about the protocol and understanding whether the effects of a protocol change matches our expectations. One large effort is the goal of computer-aided governance through the use of a digital twin of the Maker protocol. Such a digital twin would be a running simulation of Maker’s system dynamics, customizable and presented with a clean, intuitive interface. This would usher in a new era of scientific governance wherein protocol-changes (“policies”) could be added to the model to understand its emergent effects. Another example is a mapping of contract and system-wide dependencies to understand the potentially unanticipated effects of some code change. This will significantly improve visibility and auditability as we grow further decentralized.

Decision Support will become a publicly accessible, real time, and modifiable simulation of the protocol that integrates with live feeds of data from the deployed Maker system. Tools such as this will allow individuals to input their proposal into a digital twin model to better understand its effects in the real world.

2. Verification, involves efforts to better integrate formal verification practices into our workflow as well as develop more comprehensive verification techniques & tooling. We aim to formally verify not just properties about bytecode, but properties about multi-contract systems over time and their game theoretic properties. As automated tooling becomes more advanced & the smart contract ecosystem matures, it is becoming easier to address low hanging fruit such as known code anti-patterns. This is, so far, where automated tooling has proven to really shine. Yet, high-impact problems in complex systems tend to be emergent and are not detectable using methodologies focused at code-level analysis.

3. Education, including the development of educational material and training programs focused on formal methods, systems & safety engineering. This will serve to lower the barrier of entry into these disciplines for engineers, to enable more effective onboarding of engineers into the Protocol Engineering team, and, hopefully, to increase adoption of these methods across the industry.

More detailed information about these pillars, our philosophy and approach, can be found in a more in-depth document referenced below.

Why is this strategy critical to the Maker protocol?

The potential harm caused by a mistake in the code or design is extremely high. This is especially true to Maker as a critical component within the ecosystem of DeFi legos which continues to experience rapid innovation. In such an environment it is imperative that we keep up with innovation while at least maintaining, and hopefully improving, our level of safety and security. These are oft-used terms and it is important to clarify and distinguish between them to reinforce the importance of this overall initiative, namely:

Security, which concerns itself with the mitigation of threats by minimizing vulnerabilities that allow unauthorized access. These must be remedied because they undermine confidentiality, privacy, authenticity, integrity, and/or permissions of the system.

Safety, which is the absence of negative outcomes for entities interacting with or having a stake in the contract or protocol. Poor safety controls could result in locked funds or improperly operating smart contracts.

These risks, require us to have a methodology and toolchain that enables us to better grasp, test, and verify at the systemic level. While in-depth manual review, advanced testing techniques, and auditor engagements are standard practice at Maker, these often focus on the granular details of the system on a per-contract level. Higher level systemic interactions between contracts, as well as social level incentive dynamics and externalities, are often only roughly captured through discussions and integration testing. It is therefore important that we capture and understand undesirable behaviors that escape both automated detection and manual review. This highlights the need for further research & development of assurance methods as described in our above 3 pillars.

How will this strategy be achieved?

The following roadmap is subject to change as we dive deeper into various aspects of this initiative with the community and our fellow neighbouring core units. We have already seen that certain activities have taken far less time than expected, while others have taken longer to complete. This roadmap is a first attempt at providing more concrete structure for ourselves and the rest of the community to lay the groundwork for communication and assessment of progress.

Thank you for taking the time to read our forum post and we look forward to discussion and dialogue to help us focus on delivering continuous value while simultaneously working towards a higher level, long term vision of DeFi safety engineering for all Maker Core Unit teams. As mentioned above, further detail of our strategy can be found here.

23 Likes

Nice! Such a well written document–I think every DeFi Dev that decides to build and add to the Money Lego ecosystem should give this paper, “Making Maker Safe” a read. Highly recommended.

" Minimizing catastrophe at the cost of stagnation will not allow Maker to thrive in the rapidly evolving DeFi ecosystem"

Feels like pension funds should one day consider putting MKR into their portfolios (not financial advice) :wink:

Good stuff–TY Sir!

3 Likes

One concept that I don’t see, maybe it’s obvious, is the notion of adversarial teams working “against” each other. For example, you have one development team trying to make forward progress and another somewhat separate team thinking like an adversary trying to find bugs in the code base. I guess you’d probably need to do this at more than one level. For example, a team building a simulation of the Maker system could also benefit from an adversarial team trying to find discrepancies between the simulation and mainnet Maker.

Anyway, you are smart people. You have probably thought of this already.

1 Like

Yeah, great point! That adversarial style thinking is a regular part of our daily code review practices and because we are so close to the code, we will certainly apply the same thinking as we build increasingly abstract models of the system.

As the saying goes, “all models are wrong, but some are useful” and a crucial part of these endeavors is determining where to put those boundaries; what to exclude and what to include for a particular model. This decision is really based on the types of questions we are asking of the models we build. That decision-making processes is done by adding or excluding certain assumptions, and those will be explicit in the models and hopefully serve as grounds for useful discussion when evaluating potential additions or changes to the protocol.

2 Likes

Wow this is very impressive and necessary to the long-term sustainability of the protocol. It is without a doubt the most essential of the core units since without it the whole ecosystem can fall apart.

1 Like