Can Code Be Trusted?
DeFi Security Summit 2023 · 14 Jul 2023 · 25:41
At DeFi Security 101 2023, Kurt Barry, an independent security researcher and former core developer at MakerDAO, asks whether code can be trusted and answers with five layers across the software lifecycle: philosophy, processes, testing, verification and operation. He opens with Ken Thompson's Reflections on Trusting Trust, then covers threat modelling, specifications before implementation, fuzzing, formal verification, audits, bug bounties and incident response.
Speakers
Topics
From DeFi Security Summit 2023, hosted by DeFi Security Summit.
Transcript
all right so here we are um I guess I'll briefly introduce myself um I'm Kurt Barry currently just an independent security researcher doing Audits and such um I did spend four years as a core protocol devit maker Dow where I led most things related to security um so I I guess that's that's why I'm here to talk at you today I'll talk to you yeah feel if you have a question yeah feel free to put your hand up even during the talk but we'll have time at the end too and so I'm going to start a bit philosophically so can code be trusted and first let's motivate you know why is that an interesting question so the whole crypto space is founded on you know not trusting things that aren't
code right like this is the headline that's referenced in the Genesis block of Bitcoin um you know alluding to you know the kind of un fairness of the existing Financial system where arbitrary decisions are are made by people that you know many people who are affected by them you know don't have really a lot of input too and so you know if these things like trust code not Central Bankers code is law I mean we we all know how that one's been going of course but you know the web 3 is really founded on the idea of you're going to trust the code and not something else um and the question is broader than that too because you know software is beginning to underpin all aspects of Our
Lives you know like when you fly on an airplane that that airplane is actually mostly flowing by software these days um the pilots have very little they have to do manually and in fact you know in the military they'll often just fly planes you know just completely automated but you know regulations prevent that for uh consumer things but but can we trust all that code right it's it's everywhere around us and as you might imagine this question has been asked before and I'm assuming most people have probably read this essay at some point um so this was uh Ken Thompson inventor of Unix and did many other computer science things and he has this great essay well it's actually a his Turing Award acceptance
talk Reflections on trusting trust and let me just remind you or describe to you for the first time uh the sort of very tricky things he described about why it's hard to trust code um I I won't go through the whole thing because that would take too long but the the core idea is this is that compilers are often written in the language that they compile um you know for example like the C compiler will be written in C um and so you can insert this undetectable back door um into the compiler binary as follows um you have basically two if statements one that's going to be you know inserting a back door into some Target program you know think like the Unix login shell or something
uh and then you'll also have an if statement that's inserting this back door into the compiler and you know this is a little tricky to do but it turns out it's possible right because basically because you can write programs that output themselves that that's a possible thing to do um and so if you have the this version of the compiler you feed it into a non-malicious compiler binary it's going to spit out a different compiler binary that will always insert the back door even when you take the back doors out of the source code right so it's just got this you know really pernicious property that unless you're like actually disassembling the compiler bite code and figuring out that it's you know doing this backdoor thing in special cases you know this is just sort of propagate and
even if it's compiling non-malicious source code um you know it's producing malicious things and you say well is this even relevant like to like defy you know like solidity uh you know uh the solidity compiler is not written in solidity yet you know maybe someday but let me just give another thing to think about the go compiler is actually written in go right and you know go ethereum is the most common execution environment so right what if you're what if your target like you know is gu and then you know you can imagine it's like well when a very particular address uh interacts with like some smart contract system just give them all the funds or
meant that address infinite eth and this can be sitting out there living on the nodes and even if you've you know tested formally verified audited etc etc your uh smart contract you know the nodes could be compromised and you can have problems in any number of other layers of the stack right um so I and actually just as a fun trivia Ken Thompson actually was hired by Google and and worked on go so like maybe he's decided to to do his trick I should mention that original his original essay kind of concludes by like well it's really really hard to trust
code so maybe you still have to trust people um and he actually had a lot of things like calling for like prosecution of hackers in there and anyway it's an interesting historical thing to read um if if you haven't but the Inconvenient Truth is that you don't really even need fancy Trojan Horse compiler binary supply chain attacks to have difficulty trusting code because we programmers just write bugs all the time right it's it happens right so so can you trust code and the problem you face is you know you want to produce a reliable system from unreliable components um nothing has a 0% failure rate um programmers compilers blockchain
clients the software the physical infrastructure right it can all fail um and so what you need to mitigate all these different different hazards you need multiple orthogonal techniques um where it's like these layers of Swiss cheese each one is imperfect but if you get enough of them lined up you can get the risk you know as low as you want um and so for example if we were really truly worried about a go ethereum Trojan Horse there there are a bunch of things that you know can get in the way of that one is just the compiler supply chain if you think about this would be pretty hard to actually pull off in practice um you know especially like in an open source environment um you know you you
basically have to find a way to start Distributing your your compiler binary like you could probably do it but it would take some effort right and then we have redundancy of like there are multiple client implementations and not all of them are written and go right so now you have to attack all the clients like really you know durably you know break the network assuming not everyone is is running the same one um you know you can actually do fuzz testing even symbolic execution of the go ethereum client and see like oh is it correct right like you know this is redundancy right you're using something that's you know written in some other language or at least not back doored um and you can see that you can use that to get some more confidence and then ultimately there's like the social layer fallback that will deter an attempt to execute
this attack because you know there'd be a very concerted effort to find and punish the malicious actor and you know okay it's it's not code but it is a thing that contributes to safety like you can't ignore the social layer because ultimately like the code even if we're trusting the code we're all agreeing to trust the code right you know you can't escape that at at the end of the day so you know my personal take on this is while you can never trust code completely you can get close enough in most practical situations and depending obviously on the criticality of the application you need more and more um effort to get close enough so the the really interesting question though is like how and this is the part where I'll get a little defi specific
um I I realize I'll probably say a lot of things that were said earlier today but I'm going to try to say it all like at once um and hopefully that's beneficial because a big challenge I observe in this space is you know developers come in um and they don't have like experience with critical software components they're used to like web services or something um and where you you know make a mistake find some 500s reserved uh just ship a new version and and everything's good but here it's like you know once you deploy your code is in some cases completely immutable in other cases very hard to change and you know it only takes one hack to have an irreversible you know multi-billion dollar loss uh and so you know it's really all in like the mindset and the
processes and putting it all together into a complete package right there's there is no like Silver Bullet right like you've heard about formal verification today and that's great but it's not the only thing you need right uh so forgive me a little bit for being a little bit playing with words a bit and abusing terminology to make this pyramid but I I wanted to have a pyramid um because I think it helps kind of conceptualize what's the most important part and at the very bottom I'm putting like philosophy which is by which I mean your mindset towards the code above that comes processes um then I've put testing as its own thing although you could argue testing is a a process too but testing is you know it's
such a big topic it deserves its own place above that I'm putting what I call verification which I'm going to basically that's where some of the abuse of of words language comes in here um some of some of the things in verification some people might argue are really testing but for me it's like kind of the testing that I'm referring to with testing is testing that happens during development and this is verification of like the code is basically done we think we've tested it and now we're going to make sure you know it really does what we think it should do and then finally there's this operational step because once code is deployed you know it's not risk-free um even though you've hopefully reduced the risk and you need to be monitoring it and responding to issues so let's go through these a little bit all right so
the philosophy is you know how are you approaching software development right what's your mindset um you know how are you thinking about the problem so for one thing you need to know your tradeoffs right web 3 it's hard to upgrade hard to recover from incidents and so that means you know you need to have that in mind from the start um you need to be modeling your threats you know what what's in scope like if you're a smart contract developer maybe you're like it's not my job to defend against the you know compiler uh gu Trojan Horse right like I'm just going to assume that the other things that we talked about are going to take care of that you know like like what do you want to prevent um you know you want to prevent funds from being stolen you want to be preventing
funds from being locked Etc uh I like to emphasize a safety first mindset um I say safety not security because safety is a superet of security right like security means there's a malicious hacker you know doing something bad but smart contracts can have bugs that just make funds get locked no hacker needed right and users care just as much you know no matter how they lose the money right and that's what really matters I'd like to emphasize here every d project should have at least someone focused on Safety and Security right if if there's one founder that's you if there's like a non-technical and Technical founder it's the technical co-founder right if there's one engineer that engineer is also so that you know the person who owns security right it's
it's not a separate function it's part of the job and all right you know another phosy I've kind of touched on already is like the risk never goes to zero although it can get lower with time and usage right if you have a contract that's not changing and it's got a lot of tvl the more it's longer it sits there and doesn't get hacked you know that increases your confidence in it that's nice but confidence never really goes to 100% you know alific is a goal I think in web 3 you know like we did just said at the end of his talk every time you upgrade something that's a risk uh and you want to not do that and ideally you eventually stop although you know different applications have different needs and you know a big one that is kind of very specific to code is
preferring locality and minimizing dependencies because every dependency you have is something else that can go wrong um every non-locality by which I mean like you have to go to some other function in some other file and from then from there you have to go to some other function some other file makes it harder to understand the code and so having code that's easy to understand maybe that's the real principle that's how I should have phrased is like make the code as easy to understand as possible because you know ultimately that's going to make it easier for you to find bugs or not write them in the first place all right so moving up the pyramid you know now you have your processes and so how do you actually do the development that now that you know how you're approaching it right so you should really start with kind of a
specification of the system prior to implementation and you you know depending on what it is maybe this is just a natural language paragraph maybe it's a full formal spec that you can use later to do formal verification um but but either way you want to have some some level of intent and know what you're trying to achieve um before you start because otherwise you may make some mistakes and have to go back and do it all again um code review is obviously a critical process you know at maker we use kind of like the four eyes principle of you know two people have to sign off on every PR you can do something different but you know you should as a metric probably be spending more time reviewing code than writing code in in web 3 uh checklists are are great I know they're very boring but they're great
and you should use them um so post-mortems right when something goes wrong doing an analysis of it deciding what you know how you can improve your process so you have a process Improvement feedback loop right that's critical um red teaming where you take someone from your team or even outside to really try to adversarially think about the code is a great process to have um and then like phased or gradual rollouts are are another good process to practice you know like how do you deployed you just like let things ramp up to Max tvl immediately or do you know 100,000 a million you know Etc all right so then moving up to testing all right so first of all like full unit test code coverage is
basically table Stakes right you should know your code paths you know list them out make a finite Machine model or control flow graph whatever you have to do and just make sure you're testing every code path right like you wouldn't believe how easy it is to miss them if you aren't like attentive to it if you're integrating with deployed contracts which is very common um you know all uh good development Frameworks support RPC tests where you can actually test the integration with the Live code and even live state of the blockchain and you know do that too uh and and then a good thing with testing is to Define and test has system level properties not just individual function behaviors um you know this connects to what I
mentioned earlier about having a specification right so the specification is good it might already spit out some properties for you to test and then those properties can feed through into later stages of say formal verification um I'm including fuzzing here with testing um if if you do it correctly it's extremely powerful um and it's the nice thing about it is like it's it's tractable for pretty much anything you know some sometimes if you have very very complicated code it be hard to formally verify you know the tools might have timeouts or something but you know fuzzing um you know you have to be smart about shaping the inputs for example uh to to get good results from it sometimes but you know I I think it's really an underutilized tool actually um especially for like
mathematical routines um respond very well to fuzzing and there are a lot of those in dii another thing with testing is you should just always mutate your code maybe manually you're using automation if you can and just make sure the tests actually fail like you know even someone like me who's been writing code for you know quite a while an embarrassing length of time you know I'll write a test and then I'll go change the code and well the test still passes right um you know if it can happen to me it can happen to you um so and if you can have automated mutation testing like that's even better but you know this is just a basic you know hygiene thing make sure your test actually test things which
relatedly you know you should have code when when you have code review code reviewers should look at the tests too like don't just assume that someone wrote complete coverage um you know look at the test see if you can think of any gaps right because you know sometimes it might be easier to spot a gap in the tests than to actually see a mistake in the code all right so then moving up so my my my slight abuse of of language here I apologize for so verification I I'm begin I'm thinking things that act sort of on the system as a whole or when you're basically done with the development process um which formal methods you can actually apply as you go along although that can be a little expensive if you end up changing the code a lot but you know formal verification you know I think you've
heard at least one talk about that today maybe several so I won't beat on it too much but you know it's it's very powerful you know I can find bugs that say are very hard for fuzzing to find if it requires like a very specific input you know like the classic example of something that formal verification is a good use for and just the process of thinking through formally verifying your code is is very valuable economic modeling so this would be like doing numerical simulations of how your system performs um you know under various say path conditions in financial markets um there you can do that yourself in like a spreadsheet um or you could get a company like Gauntlet to do it um you know depends on your needs you don't
some of these you know when you get up here to the higher levels of the pyramids you don't necessarily need every one of them for every project so like you don't necessarily need to do economic modeling all the time but it can be really useful um all right finally we come to audits which I'm trying to contribute to changing some terminology uh in the ecosystem is that we should really be calling these reviews or assessments like in fact when I do an audit like and I write a report I actually it like says you know assessment not audit because audit is like a specific thing in other contexts where it's really like a checklist and this is more more qualitative thing that doesn't make guarantees um but you know you notice audits you know come after all the other stuff which a lot of times audits are
the first thing people think of in web 3 or Security reviews it's like no you really should have done a lot before that um and if you have really really good code you shouldn't need five audits you know you should need one or two unless you have a really complex system and then maybe it's Justified or or if you have a really big budget as well then just get all the audits why not um so then test net deployments are great obviously do them you know get users there to to try them I I mentioned phased roll outs is like I think a process as well but this is part of this I think verification process of making sure the system works once you've created it so you know Whit listed Alphas gradual usage limit increases Etc all right and now like the very highest
level um which actually this one is a central sorry so that's maybe an inconsistency in the pyramid but you've got to mitigate the risk of the code once you've got it deployed so that means having a bug Bounty program so that people are incentivized to tell you about your bugs and not hack you um you should be monitoring things um if you have parameters that need to be set you know you need to maybe have controls and procedures around that um good documentation um be aware of execution environment changes right on ethereum we have a mutable code but mutable semantics uh always fun when like the gas schedule changes and now your hard-coded gas limit doesn't work anymore and potentially more fun things like they're they're nerfing self struck pretty soon um you know sad face and
then have a plan for incident response you know you know know how you're going to run the incident I'm not going to go into how you would do that here but you can like look up standard incident response procedures and just use them you know practice them and particularly like know what your upgrade paths are if you have any and if you have the time and bandwidth you know drills and simulations uh can be good um now I'm going to give you a little bonus here of my like my favorite anti pattern you know while I have a soap box stand on uh which is that like using raw ether is it's just like unnecessary in most contexts and and generally worse from a safety perspective um first of all you know there's no re-entrancy that you have to worry about with wrapped ether um and if you're also supporting like
ERC 20s anyway if everything is an erc20 you can eliminate an extra code path which is just fewer places for bugs to hide right lower your overall complexity and you also have more composability with wrapped ether there's no such thing as you know improve or transfer from for normal ether which you do have with wrapped ether and everything is erc20 compatible these days now what's the concern okay maybe there's a bug in the we contract but that's that's super super unlikely I think the we contract is the contract I would probably trust the most one main net ethereum right now um and yeah okay there is gas overhead but I I think the the Ben the security and safety benefits of using we outweigh the gas costs for most applications maybe the one exception is if you have a
thing that's truly ethal only um and then you say okay well I'm just going to put effort into getting this right uh so anyway I I think that's the end um and yeah if you have questions or whatever Now's the [Applause] Time um do you know of any uh Dev tools that could help with the automated mutation to check faing yes not off the top of my head although someone was mentioning one recently does anyone in the audience know a mutation tool for solidity some back
there sorry I can't hear you Gambit Gambit from Cur okay perfect all right I haven't tried that out yet so I'll have to have to take a test of it Al also Som s how do you spell it oh Sumo suo Sumo apparently it's another tool you can look up all right good crowdsourcing there uh what's a particular upgrades a particular upgrades last slide uh what did I a particular UPG oh like what do I mean by this is maybe
just a poor choice of words um like I just mean like you might need to upgrade different things in your system differently so like maybe in some cases you'd want to deploy a new contract other cases you have like an upgradeable proxy pattern um maybe other things are just not upgradeable at all and you've got to like shut down or migrate your protocol um yeah not maybe not the best choice of words there but hopefully the the context helps uh no question I just wanted to say there's also a universal mutator and necessist for mutation testing so awesome more more options than I ever
imagined uh so what about code that is generated for example like you want to do like a CK proof or something right that is outputed by a tool it's not like readable right so what do you think about those kind of because I you would see a lot more of that going forward what are your thoughts yeah that's a great thing to bring up especially in the context of ZK because there are a lot of interesting things that happen there so with generated code like often you're generating it because it would be too hard to write by hand or it would take too long um and so then it comes to be a about like trusting the tool and you know I think that means you need the same level of like effort to go into creating those tools that goes into
creating you know smart contracts you know maybe even more right like you need mathematicians to like check that the papers match up with the math implementation um and also that the papers were correct but just as a side there was one time a bug in zcash where the programmer had perfectly implemented what was in the math paper but there was just a typo in one of the equations right so you've got to be checking that and then you've got to you know you you know like there should be a huge test suite for whatever your you know circuit generator is right and you know maybe that should be fuzzed I don't know if it' be feasible to formally verify that but you know if it's going to be create if it's going to be producing critical components and those components themselves are like too hard to verify
although you should verify them to the extent that you can you know it means that those tools also have to be basically space grade yeah great question all right yeah if there there are no more questions I'll stop standing between you and your evening plans thank you very much thank you very much good