MakerDAO Smart Contract Safety: When Billions are at Stake

DeFi Security Summit 2022 · 27 Aug 2022 · 17:22

Kurt Barry, a protocol engineer at MakerDAO, lays out the layered, defense in depth approach Maker uses to protect billions in collateral and DAI, built on the Swiss cheese idea that no single technique is enough. He covers safety over security, two sign-offs and post-mortems, fuzzing and fork tests, and formal verification, noting that the formally verified multi-collateral Dai system still had bugs. He also describes late audits, pre-launch bug bounties, instant access modules and the dark spell mechanism for handling live incidents.

Speakers

Topics

From DeFi Security Summit 2022, hosted by DeFi Security Summit.

Transcript

My name's Kurt Berry. I'm a protocol engineer at MakerDAO, and today I'll be telling you about some of the safety and security practices that we use at Maker to secure billions of dollars in value of collateral and outstanding DAI. All right, how are we doing? All right, okay. Well, I'll just keep going from memory here. So, to state the obvious, to start us out, shipping code and DeFi can be very scary because a lot of things can go wrong. You can just straight up ship a bug, but, you know, you can also have unexpected interaction. Straight up ship a bug, but you know, you can also have unexpected interactions between old code and new code You your code you might think it's immutable But your semantics are mutable because the EVM can hard fork out from under you at any moment You can have economic

exploits even if you implemented your protocol as designed and You know there can be more exotic things like network congestion or the chain can go down and so You know the safest thing would be just not ship any code at all right, but codes at all right, but that's not enough So so what can we do and that's not an option You know the safest thing would be just not ship any what you really need is a defense in depth approach? When we get the slides up there will be this nice picture of layers of Swiss cheese And so each layer of Swiss cheese represents, you know some defensive technique And each piece of cheese has some holes in it, right? No technique is perfect or a silver bullet But you line up enough of them and hopefully the holes don't line up or only

very few of them and so you can filter out almost everything before you And so you can filter out almost everything know it gets to production although you always have to be ready to remediate production issues and so in the talk I'll be taking you through how MakerDAO combines a bunch of different practices into sort of a holistic you know engineering method you know to do Muli's opening point about you know the process and the method you know we love to talk about yeah fancy little techniques all right oh here we go this is perfect we're getting there But, you know, how do you put those together and actually use them when you're a DeFi engineering team? All right. I think I can just scroll through them here.

It doesn't have to be perfect. Can everybody, is this good enough for everybody to see here? Maybe just zoom. All right. Let me, I'll just zoom in here and scroll through them. All right. Good enough. All right. So the first thing I want to talk about is principles. This is where it all starts for us. You know, before you say anything about, you know, how you do things or what tools you're using, how do you approach, you know, security in a principle -based way? So the first one is actually it's not about security, it's about safety. Because security means that, you know, some malicious attacker can't cause harm or loss. But a smart contract can be unsafe yet secure if, for example, it just locks funds that are sent to it, or if for

example just locks funds that are sent to it right that's unsafe users care about losing right? That's unsafe. Users care about money in that way just as much as they care about it if there's a hacker and so you know we say safety first another principle we hold to is the intent design implementation hierarchy for organizing levels of abstraction to make that concrete intent your intent say is to enable permissionless trustless asset swaps your design is constant product amm on a blockchain chain and your implementation would be the Uniswap v2 contracts and this is useful because the problems come with usually the boundaries between those layers so you have some design and you might implement it incorrectly right so you can have a design implementation mismatch but you can also have an intent design mismatch where your mechanism just doesn't have the right game theory to satisfy your goal so no matter how perfect your

smart contracts are you know you're broken at the mechanism design and so we always want to remind ourselves to think about both some of the more self -explanatory ones you know, every detail matters, you know, fanatical attention to detail is a big part of our processes. you know every detail matters you know But you always have to respect constraints, namely cost and speed, right? Remember, I said we have to ship code at the end of the day. You know, we then hold that residual risk is always going to exist, so we never completely trust any piece of code or infrastructure. And we believe in having best practices and following them. And if we have time, I'll talk maybe about a few of those towards the end. but let's go ahead and go through to the engineering processes. But let's go ahead and go through to...

All right, I'll just kind of run through these quickly. Two sign -offs on any code change, that's where it starts. We'll usually hold line -by -line review meetings for complicated pieces of code, you know, usually with kind of a red team or adversarial mindset where you take some engineers who didn't work on that code and say, okay, now go and try to break it. Anytime we have a standardized process, like our weekly governance actions, we make a checklist for that you know checklists are widely... used in other safety critical fields they can work in defy too and the last and maybe most important one is that we always do post -mortems anytime you know there was a problem so this sets up a continuous improvement feedback loop because you know your your people are never perfect no matter how good they are and you've got

to improve your processes next thing up testing you know probably preaching to the choir here when I say it's you know, important and you should do it, you know, full unit test coverage is sort of table stakes, I think, know full unit test coverage is sort of It's because it's, you know, it's easy to do. know important you should do it you relatively cheap compared to, you know, a billion dollar loss, you know, RPC or simulation tests where you're running against a forked version of mainnet is critical whenever you're integrating with some sort of code that's already on chain, you know, and also to access that, you know, those mainnet state values. We're big fans of fuzzing, especially for numerical methods where you can often have tricky rounding cases that are tough to spot just by staring at it. And, you know, we still think there's value in testnet deployments,

not only for ourselves, but also for integration partners who might want to just try it out on something that actually has a live consensus layer underlying it. And one principle we hold to with testing is that you should try to think about and define properties of your contracts or your system, as well as just testing each function's behavior in isolation. You know, the mere exercise of trying to come up with properties can often to come up with. make you think of things that you would have missed otherwise, and having those properties are very useful for the next thing I want to talk about, which is formal verification. So Muli mentioned this a little bit in the openings, the use of formal methods like symbolic execution or others to prove properties of your code. It's often costly in terms of time and maybe sometimes

money, depending on what solution you're using. So we tend to prioritize it for you for, you know, more critical contracts, those that have high risk. upgrade or ones that know more critical contracts those that have high risk those that are hard to it we want to gas optimize why the gas optimization well that's a process that can also introduce bugs you know for example the solce optimizer not to pick on it but you know it has had a few bugs in it and so whenever we're turning that on we view that as that's a little extra risk we should do some bytecode level formal verification if we can um you know you can do this at a lot of different levels you know i said you can do it by code level you can also have a higher A code level, you can also have

a higher level model, you can look at function behavior contra behavior, contract, multi -contract system. You know, we've had an evolution of tools over time. The early days we used a stack based on K -framework, KVM, and the ACT language, which ACT was actually created by the very early maker devs. Now we're using Sertura for a lot of day -to -day formal verification. It's easier for engineers to learn and it's also, you know, very fast, which we like and the Sertura team is great. And we're also researching foundry integrations of various open source tools to improve accessibility because, you know, our philosophy is that it should be as easy to use as possible. Because that's often the barrier is that it's, you know, it's not something you use every day, but it does have value. Now, that said, formal verification is often a bit of

a buzzword. So I want to just put a spicy meme up here for you. So MCD, that's multi -collateral dye. It's a current version of the MakerDAO system. It was sort of famously fully formally verified. and so you might say well there were no bugs right well And so you might say, well, there were no. you know you all understand what this meme is telling you so there were indeed bugs the most the largest class were ones that were interactions between different functions or contracts because the formal verification that was applied to the original version of the system just verified sort of the behavior of each function you know it was perfectly specified okay what we expect but when those contracts or functions combined together you know interesting behaviors extra functions combined together you know interesting behaviors arose so we had like you know maybe five that fell in that category there was also a bug that was mirrored

in the formal spec so wrote the code wrote the spec the spec in the code just had the same bug you know there should have been a unit test that was ultimately caught by an integration test on a testnet so you know example of defense in depth coming through we had issues with phantom overflows there are some calculations that would just revert when you gave them reasonable values and you know that was a problem in practice but again the specs were and you know that was a problem in practice but again the just saying oh you know we revert if there's an overflow okay but you know maybe you should check that you don't revert if the values are in some ranges which you can also do with formal verification you know we just didn't do it a very recent discovery is that we thought

we had a particular invariant in the core accounting logic that it was not invariant i actually sort of sat down just to try to prove that for fun because we were getting to ready to deploy multi -collateral die on We were getting ready to deploy multi -collateral DAI on L2s. is true. Maybe I should try to prove it. turned out it was false. Fortunately, not an issue in production, one of those cases where it could never really be exploited, but interesting discovery. And finally, there was cases where the design failed to satisfy the intent. I mentioned that intent design implementation hierarchy earlier, and I think the best example of that was the Black Thursday auction losses, where we had auctions that just weren't well -suited We had auctions that just weren't well suited for a blockchain environment and, you know, liquidity and network congestion constraints. for a blockchain environment. And so we rewrote those auctions and, you know,

addressing those intent design mismatches brings me to the next thing I want to touch on, which is economic modeling, meaning agent -based simulations or other financial calculations, where you look for emergent properties of your system under various, you know, financial conditions. Think, you know, big price crash. This is best suited for large and complex upgrades that significantly alter fly. This is best suited for large and complex upgrades that significantly alter your underlying mechanics and incentives. We worked with Gauntlet for our liquidation system upgrade. That was a great experience. And Maker also has a RISC core unit. The different teams in Maker are called core units if you're not familiar with the decentralized governance. And they do some in -house financial modeling. And the important thing to remember with this is all models are wrong. Some models are useful. So make sure you're testing the scenarios that you need to. Make sure the agent Seeing the scenarios that you

need to make sure the agent logic has the right sort of incentives, you know, built into it so that you get something useful out that will actually tell you about the real world. All right. Now I want to get to audits. So this is usually the first thing you talk about in Web3 security. We think it should be one of the last things. We're not believers in ADD, which is audit driven development. I think I stole that joke from Marillion on Twitter, not mine. So credit where credit is due. But, you know, these are just most productive when the code is. well polished. We find a lot of value in having a retainer agreement with an auditing firm because then you get auditor continuity, which means they have a deeper understanding of protocol and they're more likely to catch subtle interaction issues, you know, which

is one of our big bug bears at Maker. I'll give a shout out to Chain Security. They're our current auditors. They do fantastic work. Now, bug bounties. Ideally, you want to expose your code to bounties prior to launch so that the bugs can get caught before they're in production, but, you know, you should have production bug bounties too. You know, the pre -launch bug bounty for multi -collateral die turned up four critical and high severity issues that were actually missed in the audits. Well, that's not entirely fair. One of the audits identified one of the preconditions for the issues, but it didn't, you know, find the full severity of it. And that's not that the audits were bad, it's just that there is no silver bullet, right?

Everything is a piece of Swiss cheese, and you know you just want as many pieces of Swiss cheese as you can get because it increases your safety and it's delicious all right and maker currently works with Immunify to manage its bug bounty program all right looks like I've still got some time here so I wanted to talk briefly about handling production issues which is something that as much as you try to avoid it is inevitably going to happen and there's There are some unique challenges of a decentralized environment for this. and I just listed three of them here. Time locks, immutability, transparency. You know, the first is that to protect against governance attacks, most protocols have some sort of delay before an action can take effect. But if your protocol is being actively exploited, maybe you don't want that delay, right? That's a challenge. You

know, immutability, you know, sometimes you just can't upgrade something. And immutability can be a good thing because it's what allows people to really trust code. It allows people to really trust code, like, this can't change out from under me, you know, This can't change out from under me. that should be a goal long term, is to have an immutable financial system that, you know, the rules can't change on people. But when you're in the early stages of working out the bugs, maybe immutability is a problem if something has a bug and you can't replace it. And of course, transparency, you know, most DAOs are very open, the governance processes, you know, on forums that are publicly accessible. But if you just go out and say, oh, hey, there's a bug, maybe we should fix it that means bad actors can see it and fix it.

That means bad actors. maybe take advantage of it so so what do you do there are a lot of different approaches and I'll just go briefly through some of the things MakerDAO does one thing we have is our so -called instant access modules that allow governance to take very selected very specific immediate actions that aren't through the time lock and but of course very limited so that they can't do too much damage to the system in the case of some sort of governance attack that's Often often combined with maybe ensuring there's a window of time that governance So if you're combined with maybe ensuring there's a window of time that governance is able to act. familiar with Maker, you might know that it uses prices that are one hour delayed, and that's to give governance time to trigger an instant access module that would freeze

the oracles if some sort of attack or just malfunction was occurring. I mentioned this earlier, but we do extra scrutiny on things that can't be upgraded or are very hard to upgrade. We have in our governance process so -called vote delegates that make coordination easier. us so -called vote delegates that make coordination easier so you know this is just the voting token power can be delegated to you know saying a fairly small set of individuals you know not too small obviously or otherwise that's its own risk vector but it's a lot easier to coordinate a few people who are sort of like spending their full time worrying about voting and maker governance as opposed to just some large token holders who might have you know a lot of other things to do and then like the nuclear option for production issues for

us as we have this issues for us as we create to base dark spell mechanism just basically where you'll deploy a contract or well you won't deploy it but you'll make it and you'll pre commit to the deployed address using the you can use this create to opcode in the VM to do it I I don't know everybody's background so Google it later I guess if you don't know what it is but then you have to go to maybe some trusted people like your auditors or prominent community members and get them to a test the test that the fix is that the fix is going to be safe and then you can sort of very going to be safe and then you can sort of very quickly you know vote quick in this this dark spell and then it takes effect as soon as it's

deployed without revealing uh the you know the bug for a period of time to be attacked all right um in the last uh couple minutes here let me try to run through some selected and very opinionated maker dow best practices the first one that we like we believe that wrapped ether is basically strictly better than raw Ether in pretty much every scenario. than than raw ether pretty much every scenario First of all, it's safer. You're not going to ever have a re -entrancy with wrapped Ether. And if you're trying to handle ERC -20s and raw Ether both, you have multiple code paths, more code paths, more possibility for bugs. Wrapped Ether is also more composable. You don't have a proved transfer from with normal Ether, and ERC -20 compatibility is widespread. The counterpoint is, well, what if there's a bug in the WETH

contract? I told you nothing is either fully trusted, but we think that's very, very think that's very very unlikely at this point because it's at least the West nine unlikely at this point. We'll do nothing is other fully trusted, but you know, we Contract has been operating for many years with billions of values locked simple codes No administrative functions no upgrade ability, so unless you really need the gas efficiency of raw ether Just use less you're going to have an easier time of it All right another thing we believe that is it okay to delay right? There's often a lot of pressure to ship and ship quickly and that has its place but usually delaying a week if somebody has a bad gut feeling about something but usually delaying the week if somebody has a bad you know that's usually better than shipping a bug

another principle we have for practice is gradual risk exposure so when we launch new code we try to limit the financial exposure of the system and this is maybe analogous to like you know ab rollouts or phased rollouts in traditional web services but in defy it's more you know it's about how much of how much of your TVL or how much risk are you exposing your protocol and your your tvl or how much risk are you It's more, you know, it's about your users to, and you try to do that in an incremental fashion. So basically just don't upgrade everything at once, don't go to maximum debt ceiling, etc. And finally, we really think you should try to minimize external dependencies and calls in smart contracts. You know, fewer imports, fewer external calls, and that's just code that's easier to read, easier to test and verify. Of course, there's some unavoidable amount of

complexity you have to accept to build certain. There's some unavoidable amount of complexity you have to accept to build certain things. But you should minimize it. All right, and that's the end. I think I'm out of time, too. So thanks, everybody. And please find me and ask questions later.