Secure by Design

DeFi Security Summit 2022 · 27 Aug 2022 · 19:15

At DeFi Security Summit 2022, Jared Flatow of Compound Labs lays out his approach to security through design, drawing on the launch of Compound III. He walks through a spec, code, test and ship process, stresses writing down invariants such as supply plus reserves equaling cash plus borrows, and covers testing, formal verification and planning for how deployed code evolves through governance.

Speakers

Topics

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

Transcript

all right I'm back next up we have uh Jared from compound labs hi uh hello thanks everybody uh for having me I'm Jared from compound um I guess that was a great talk by Kurt I'm actually going to talk about a lot of the same things um but you know I think I had too much content so it's great that I can just focus on some of the um some of the differences here but yeah I want to talk about more like um compounds approach my approach to thinking about protocols I've been at compound for um almost four years um worked on the design and shipping V2 and all the things we've done since that uh V2 is the current compound protocol

on ethereum it's um yeah I mean it's a little over over three years old as well um and uh we just we just actually like two days ago um released or launched V3 went live we actually depleted a few weeks ago but the governance proposal to make it active um just went live a couple days ago so I'll talk a little bit about um that as well but really wanted to just talk about um kind of our approach to um to like security through design and the design process and um yeah I mean really picking up where Kurt left off about how the practice is in the process that you have can lead to you know it's not about doing one specific thing it's about

defense in depth and having uh you know just good principles good guiding principles that um you know make sure that you have a safe protocol um so how should I do this scroll down okay is this uh area okay um so yeah so uh it can be um pretty daunting to ship code domain yet um or any blockchain uh you know it's it's more like shipping Hardware or launching a satellite there's less that you can do once um you know your code is out there to to mitigate any issues you things just take

more time especially have a dow or a time lock or something that prevents you from making upgrades immediately uh it's just you have to think you have to put more uh effort and investment in upfront to prevent issues um you know a lot of what we was just talked about so uh you know the way I personally like to think about the process is really like four steps um so it's like the specking specking step the code step the test step and the ship step um the these aren't necessarily sequential so I think you know really it's like a diamond almost you the first thing is the spec um which I'll get into detail on all these things um and then you can do coding and actually these kind of coding and testing in parallel and then you

know and then ship thing is when you're you're finally done with everything um but yeah I think at compound and something that I'm a big uh believer in is the specking process and how important it is to to write a good spec up front and get all of your kind of um design considerations and really have like a complete protocol on paper at a high level first um before you start to to rewrite that at a lower level um and you know it so the things that you should be thinking about when you're writing a spec in my opinion are um you know what are your goals uh what are your use cases what are not your use cases um something we'll talk more about later uh but like what invariance must hold for

compound it's always safety first so the fundamental accounting equation assets equals liabilities always has to hold in the case of compound this is generally like Supply Plus reserves equals Cash Plus borrows it's a high level invariant that should just always be true and you can you can test this with uh you know formal verification and other methods um but it's it's kind of it it's non-negotiable um and then you know there's other attributes that are desirable that help you make decisions when um when you're not sure what else to do in the spec because I think the spec writing process is also uh just the process of uh you know making lots and lots of decisions exploring a huge decision decision space in this uh in

this design space that you're in and um and trying to figure out what to do um so so yeah what attributes are desirable for compound three for example uh we had you know there were some things that we wanted to do uh differently from V2 one uh was you know focused on efficiency so Capital both Capital efficiency and gas efficiency so this helps when you're writing a specter really I can try so how's that okay great um yeah so efficiency um you know another another Focus for for compound three was the ability to make it more portable and Deployable on other chains um so we tried to really

fit a lot into a single contract um did away with our um like Hub and spoke model for for v2 where there was um there's like a a market a contract for each token and then a central risk management to uh uh contract uh really tried to pack every like a whole Market into a single contract um and this you know that that guides a lot of decisions as well um and you know always the uh the tie breaker for making decisions is like what's going to be simple better for users um uh the simpler the protocol is the easier it is for people to understand and um interact with and just the better overall so yeah as I kind of alluded to the spec

writing process is kind of um it's just it's a decision making process um it's just an enormous design space for for a protocol that you know without even specifying what type of protocol you're writing it's it's um it's a it's a huge uh space to explore and usually you shouldn't be working alone you should be doing this with um you know a group of people and um and you want to do that so you want to explore this place collectively and you want to do it as exhaustively as possible and you want to write down all these decisions um that you're that you're making and um and hopefully some some rationale as well for for why you're making those decisions um but you only have you know limited information when you're trying to do

this so um so that this is kind of one of the hard Parts about this exercise is like what how do you make decisions when you don't necessarily know uh what what's what's going to be better for users or or how things are gonna play out or evolve um and so you know for so my advice here is to do what it takes to move the Discord forward discourse forward when uh now um so I think uh Kurt talked about it but modeling simulations are a good uh a really good exercise to help you gain insight into certain problems um for instance uh in compound three we weren't we knew that we wanted to change the liquidation mechanisms from from V2 but uh we didn't know exactly what you

know what we should what was the best alternative um so we we did a lot of Monte Carlo simulations and modeling of the liquidation Dynamics to try to figure out what um what would sort of be a better uh system that that that might um you know not that wouldn't lose lots of funds for the protocol um you know it has as as mentioned you know this is a very there's a lot of caveats when you're when you're modeling things like this but it does help you to to make um decisions earlier on when you don't when you can't when it's kind of the best tool that you have available um again when it comes to specing the more you do it like anything else the better you get at it um you know with V3 of compound there's

there's a lot of learnings and regrets from previous versions that we could we were able to incorporate into our uh our respect um so that that's always helpful and um just remember that this is the spec is like a high level design document and it's the cheat so therefore it should be also the cheapest um version of your protocol to iterate on it should also be the easiest to collaborate on um if it's not then you should use a different platform for for writing it um we tend to use uh just like Google Google Docs and uh where you know people can comment and um you know collaborate in that way but whatever your favorite collaboration tool for writing documents I think that's what that's what you should use um but if it really you know it is like

a higher level version of your whatever protocol you're trying to write and you'll you know the next step will be to compile this down to to code and a lower level code um and so yeah almost by definition it should be just cheaper to to iterate on so and if you've done it well then the code and the test should pretty much fall directly out of it um and so um you know this is kind of the hard part of of building a protocol in my opinion is is is doing the specking and doing it well um but yeah once once you get to the the code step um there's kind of you know there's not there shouldn't be too much to think about you've already made all the hard decisions um you if you haven't if you find that they're you're debating what to do in

the code then you should probably go back in and fix your spec um you know you should it should just be an exercise in really just like compiling your your English or high level language into solidity or whatever you're you're writing your your protocol in in your contracts um so yeah it's kind of like coding is probably the easiest step I also consider um unit testing as part of the coding uh phase or step um you know as as curtain also mentioned you know unit test is kind of just like table Stakes you should have 100 unit test coverage or anything in your your contracts um the best way to do that is to always keep your your main development Branch like completely covered and you should only merge branches or pull requests once um once things are covered and that

means that unit tests are you're writing them together with with the code that you're implementing from your spec uh you know brand all your branches that are in your code should be reflected in your spec so you know there should be at least one test for Every branch in your code that should be that should map to a a unit test that should map to coverage of your spec and the easiest way the best way to do this in my opinion is to to um write these together and do them one for one and um you know that's very straightforward it's kind of like the boring most boring part of of uh writing a protocol probably is you know the spec is kind of like interesting and fun and design challenge um now you're just like compiling in the coding phase

um and then there's this other step of testing which is the more like interesting thoughtful kind of testing um uh just keep going moving along here so you know I guess what I want to do kind of uh communicate or focus on here was that um you know first of all think in terms of invariance uh kind of brought up one and very earlier the fundamental accounting equation um these invariants that you should have thought about during your your spec process um you should try to write these down um so for for compound just some examples this is the fundamental Cloud equation I mentioned uh there's exchange rate should always increase so for v2

um we had C tokens and they're in C tokens there's an exchange rate between the token and the underlying asset and this should never go down basically and um you know that's that's example of variant um another type of invariant might be like if you supply an acid an asset Supply should always be able to be withdrawn by the user that supplied it or an account that goes underwater should be liquidatable for example um so these are these are just like statements about the about the protocol about the the state um that should always just that are just true um the the thing that trying to avoid here is writing more imperative steps

that you would have been writing in in like unit tests where you say like okay user user a uh initiates a supply um of whatever x amount of some asset and then withdraws it and that tests a very specific situation but uh doesn't tell you like what the higher level property of of your uh protocol should be um you know another example about creating a borrower and the prices move against them and then they liquidate them that's like one specific thing that you're testing but it's not it's not a general property that that lets you generate lots of um test cases or uh prove in a formal way so focus on invariance start with the

strongest invariance the the most Global absolutely true invariance that you that you can claim um that you'd like to claim doesn't matter if you can uh prove these things or not yet you know the the step after this is to figure out strategies for for proving these things or or getting at them um but first first of all you know think about what they are write them down uncover implicit assumptions that you're making about um about your protocol um preconditions you know make make everything explicit as as best as you can so that's that's uh if I guess if there's one takeaway here I think this is this is it you know really should be thinking about things in terms of invariance when you're when you're writing a protocol um and then if you've done that then you know there's two kind of high level

strategies I think for for getting at these invariants so one is to like you know use formal verification prove what you can write them in something like uh sort of verification language um you know you might be able to prove them exhaustively over your entire space which is awesome um when it works but sometimes uh it doesn't work you need to make approximations in the in those uh to make to make the problem tractable um and so they're you know you have to um to do what you can and then for whatever you can't do uh you know try to come up with other ways of of testing those things um but even you know even if you can't prove certain things it's it's a really uh super beneficial exercise in itself

um also mentioned this but just the act alone of of writing these variants causes you to think differently about your problem in a different way in like a more top-down way instead of a bottom-up way and that is is really valuable um to give you insight into other uh uh yeah sure uh looks like I have five minutes left is that is that true okay uh yeah I mean I've got way too many slides here I'll just jump through the end here um but yeah I mean this is really what I want to focus on actually is is the invariance and um uh you know the strategies for for proving invariance

and uh working through scenarios so yeah so scenarios for everything else um for compound three we built a a new scenario framework which lets you kind of write properties and um I'll just skip to an example here so uh when I talk about scenarios there's like a property there's assumptions that you make and then we have a framework that lets you generate different worlds and context in which um those assumptions that you've written down hold and then you can test this property and all of those in all those different situations so this is kind of like an example output where um you you know you take our scenario suite for compound three and um we run it and it's uh you know it runs on Forks

of deployments on on four different chains that we have and so you're running your scenario Suite against lots of different variations of different forks I can talk more about this this is a lot there's probably a lot a lot to go into here here more than I can um cover so uh I guess I'll move right along um you know mentioned already but you should get more get more eyes on your code hire Auditors triple quadruple check your work share it with the community share your ideas um share your your spec um you know the more people understand your spec and your intention the better feedback you'll get um don't you know another tip is just like don't take feedback personally when you're doing this because um you know you really want to get as

many criticisms of what you're doing and find as many holes and things as you can and this energy discover issues like the better so um you know you know be grateful when people take the time to to help you and look at your code and and your spec and um you know whether they find issues or not just just be glad um that uh that they did that um you know also take the moment to thank uh like the people that helped us do that for for compound three so chain security open Zeppelin um Gauntlet I think people from all those companies are here so thank you for for all your help with compound three um you guys are awesome and then yeah the last step is is kind of shipping your code um there's also kind of a lot of

to say about this probably but um you know I'll just say that for for v2 uh a compound there was um you know we we went from a centralized uh like a company deploying the contracts and having a multi-suit key to control them to a doubt controlling those things in a time lock and taking like a week to at least to upgrade things and um you know the design of V2 didn't really it was kind of uh you know it was just very organic and didn't really think about the the how to best do that with compound three we've kind of um thought a lot about how to make the code maintainable

um by adao um so it's really a more holistic approach um this is our strategy Now is really to have like a deployment script for for each Network or deployment that that the code is on and um there's some relations that that can be kind of crawled automatically so that you always know what the set of contracts for that deployment are um you know I'll talk more about that if you have questions but um you know the other part of this is planning for evolution so how do you change the code once once you've deployed it and um you know the The Simple Story here is for for compound three we've gotten it down to like you open a p a pull request you can see if that are scenario seat and

all our tests run against that pull request and the hypothetical changes that are being made in it um you can see the artifacts being generated you can also um actually do the same deploy from the same script that's being tested in GitHub you can do the real deploy and it makes it easy for governance to review those things and um uh you know once it's executed you can merge the pr so yeah I think I'm out of time but thanks um you know if you have questions I'll be around um also I'm on on Twitter at JM Plato um you can join our compound Discord and also uh you know if you're interested in the stuff we are hiring and um happy to talk to you about that as well but thanks [Applause]