Hardening Blockchain Security with Formal Methods

Transcript

Hi everyone. Uh my name is Ishel Dillik. I am the president of a startup called Veradise and I'm also a computer science professor at the University of Texas at Austin. And today I'd like to tell you about a research area called formal methods and in particular how this field of formal methods can help us improve blockchain security. So first of all, let me start by stating the obvious which is that bugs in blockchain software as we all know tend to be extremely costly, right? And when I talk about blockchain software, of course, this includes DeFi applications and smart contracts and web 3 applications, but it also includes the underlying blockchain implementation, for example, consensus protocols as well

as zero knowledge proof circuits. And if you have a logical bug or a security vulnerability in any of those layers, they can have catastrophic consequences if and when they're exploited. So let me give you a few examples to illustrate the impact of these bugs. So as an example, there was recently a flash loan vulnerability in a smart contract uh in the uh Beantock DeFi protocol. And when that flash loan vulnerability was exploited, that resulted in uh in a loss of $182 million worth of cryptocurrency.

Now you can also have serious security vulnerabilities in the underlying blockchain implementation. As an example, there was recently a denial of service vulnerability in the consensus protocol of Salana. And when that vulnerability was exploited, that resulted in network outage and caused the Salana prices to plunge and lose uh more than 12% of their value overnight. And last but not least, you can also have serious security vulnerabilities in zero knowledge proofs. And to illustrate that, there was actually a bug in an arithmetic circuit implementing a ZK snark in the Zcash protocol. And if that vulnerability had been exploited, this

would have allowed attackers to create a very large number of fake Zcash coins, which is obviously problematic. Now, you're probably thinking, well, that's pretty depressing, but it's something I see in the news every day. Well, the good news is that what I'm here to tell you is that these kinds of bugs and security vulnerabilities are actually maybe not as inevitable as that they might seem. And in fact, this research area called formal methods can help us eradicate uh these bugs. So, in the remainder of the talk, I want to tell you kind of give you an overview of what formal methods is all about and how we can leverage it to improve blockchain security.

So for those of you who may not have heard the term, basically formal methods refers to a set of mathematically rigorous techniques that can be used to automatically find bugs in software and also to automatically construct proofs about program correctness. Now when you hear the term formal methods, you shouldn't think of it as one specific technique, but you should rather think of it as basically a spectrum of uh different techniques that have different tradeoffs. And these techniques include things like automated testing, static analysis, and formal verification. And generally speaking, the further to the right you go on the spectrum, the stronger the guarantees that you get. But as we all

know, there's typically no free lunch. So if you want to get very strong guarantees about your software, you also need to be willing to invest more human effort into the process. Now at a very high level, you can classify formal methods techniques as either being dynamic or static depending on whether they execute your program or not. So in particular, dynamic techniques basically generate in a systematic way a set of interesting inputs and they execute the program on those inputs and they monitor what happens and see if some key property is violated or not.

On the other hand, static techniques don't actually run the program. They kind of literally stare at the source code of your program and they try to reason about all executions at the same time by performing some kind of approximations as we will see shortly. And as you can imagine, static and dynamic techniques have complimentary strengths. They have different pros and cons. So specifically the big advantage of static analysis is that they can be used to reason about all executions of the program possibly infinite space of executions.

And in addition to being useful as a bug finding technique, they can also be used to construct proofs of program correctness precisely because they're of their ability to reason about all executions at the same time. In contrast, uh, dynamic techniques rely on executing a fixed set of, uh, inputs. So therefore, they're primarily useful as a bug finding tool, but you cannot give guarantees using dynamic techniques. On the other hand, the big advantage of dynamic analysis over static analysis is that they don't report false positives.

When a dynamic analysis tool says there is a bug or security vulnerability in your code, you can rest assured that there is actually a problem. Whereas with static analysis, as I mentioned earlier, they rely on uh performing some sort of approximate reasoning. So they may as a result report false positive. So when they report a bug that may or may not correspond to an actual bug in the program. So now whenever I talk about static and dynamic analysis, most people have the reaction, well dynamic analysis that makes sense. It sort of sounds like automated testing, but what the heck is static analysis, right? Like what does it mean to reason about all executions?

Everyone has this reaction that it sounds really mysterious. So um to kind of demystify static analysis, let's just um take a look and understand how it works at a very high level. So basically the key idea underlying static analysis is essentially to emulate all possible executions of the program by symbolically executing uh the different paths. Okay. So what what do I mean by that? So basically the idea is that whenever you have a branching point in the code, whenever you could take this branch or that branch, you conservatively assume that either path could be taken, you symbolically execute both of those branches. You collect some

information and when there is a merge point in the code, you summarize you uh you combine the information that you gathered along the different branches. So very simple example here. Let's say in this code snippet you're assigning X to either one or minus one depending on whether flag is true. So basically a static analysis tool would separately analyze one branch and then it would analyze the other branch and then it would combine this information. So for instance in this case it might say that X is some value in the range minus one to one even though we don't know exactly what it is. And now you see what I mean by static analysis introducing approximations and you can probably see why you get uh you potentially get false

positives when you do static analysis. Okay, so hopefully that gives everyone some intuition about static analysis. But you're probably asking what can you actually prove using static analysis? Well, the answer to that question is it depends. And in particular, it depends on how much effort you as a user are willing to put uh into uh the verification. And in particular, if you want to get strong guarantees, you as a user need to write something which is called a formal specification.

And in a nutshell, a formal specification is a mathematically precise description of the intended correct behavior of the program. And the key thing here is that a formal specification needs to be mathematically precise. It needs to be something that has very precise semantics. So therefore, formal specifications are typically expressed in some sort of formal logic. For example, it can be first order logic or it can be uh some sort of temporal logic. So as a quick example, let's say you have a DeFi protocol that's implementing an option. And here one of the properties that you might care about an auction is if the auction closes and I'm

not the winner of the auction I should naturally expect to get my bid back. Right? So if you want to get strong guarantees using static analysis you need to formally express this property. And here on this slide you see uh a formalization of this property in a logic called linear temporal logic. So basically this box over here means always. This diamond means eventually and basically it's saying if the auction has closed and I'm not the winner of the auction then eventually I'm going to be sent exactly the amount of money that I initially bid. Okay. So that's a formal specification of this intuitive English property.

Now the cool thing about writing formal specifications is that once you take the trouble of writing a formal specification, we can use automated or at least semi-automated tools to check whether the implementation adheres to the specification or not. And again, the nice thing here is that assuming that you've written a specification that's both correct and complete. And you know, that's a big if there that's not trivial, you can use formal verification tools to find any logical bug in the program or prove the absence of any logical bug, which is a very very strong and very nice guarantee.

But of course, in many cases, it's um you know, not that easy to write these formal specifications. So if you don't want to write these specifications, you can still apply static analysis. For example, you can use techniques like abstract interpretation to look for known types of bugs in your software. For example, uh you can show that there are no arithmetic overflows or you can use a static analyzer to look for re-entrancey or flash loan vulnerabilities and so on. But of course, you don't get as strong guarantees because we're looking for specific classes of bugs, right? So in the case where you verify something, you're saying I verified under certain assumptions that we don't have this

class of bugs in the code. So hopefully that gives you some idea about kind of the landscape of different formal verification techniques. But taking a step back, what I want to emphasize here is that as you can see, there are many different techniques that we can throw at the problem and they all have different trade-offs. They have complimentary strengths. They each have their own pros and cons. And in my opinion as a formal methods researcher uh for many years I think it would be fair to say that there isn't one formal methods technique that's universally the best that's going to be the onesizefits-all solution that's going to cater to uh every one of your needs.

So this brings me to the philosophy of our startup uh Veradise which is basically to embrace the fact that different techniques have complimentary strengths. They have different pros and cons. So rather than trying to apply the same hammer to all the different nails out there, what we try to do is we try to find the right tool to attack the right problem and use different tools in ways that are complimentary. And based on that philosophy, we develop and utilize a wide range of formal methods tools with the goal of being able to uncover defects not just in web 3 applications or smart contracts, but with the goal of uh addressing problems in all layers of the blockchain

ecosystem, ranging from the blockchain implementations to problems with zero knowledge proofs as well as uh DeFi and web3 applications. And based on that philosophy, we've been building a uh range of uh formal methods software that can be used to mostly automatically analyze blockchain applications. So just to give you some idea, we have a tool called Vanguard and some version of this is actually uh available as open source and Vanguard performs static analysis to look for common vulnerabilities in blockchain applications. And what kind of vulnerability we look for depends on what layer you're targeting.

Uh we also have automated testing tools based off fuzzing and property directed checking and these can look for both common vulnerabilities as well as logical bugs assuming that you give us some sort of specification. And we also have a deductive verification tool that takes in addition to your source code some specification written in our specification language called V and it checks whether your implementation adheres to the specification. And last but not least, we've also been building this tool called Urus uh that basically helps us deal with the shortcomings of static analysis and verification tools. So as I mentioned, one of the shortcomings of static

analysis is that they can report false alarms. So when it reports a a report, you don't know whether that is a real bug or not. So we've built this tool called URS. In the case where one of our tools reports a vulnerability, it tries to automatically construct an exploit that shows how that vulnerability can be taken advantage of. And another thing I want to point out about kind of our philosophy here is uh we recognize that you know there are many different languages out there uh solidity rust and many different blockchains and you know like people want to uh you know use many of them or a combination of them. So we try to build tools that can be applied to

multiple languages by having by doing our analyses at an intermediate representation and a lot of our tools are are also applicable to multiple blockchains not just Ethereum and across all of these tools we can use them to uncover both logical bugs and known types of vulnerabilities. So based on all this tooling that we've built uh during our security audits, we've been able to uncover many zeroday vulnerabilities with the help of all these tools uh which would have been very hard to do if we didn't have these tools. So for example, we've been uh auditing DeFi applications and we found a number of issues obviously like things like flash loan and re-entrance

vulnerabilities but also things like access control problems and locked funds. Uh we've also done security audits for the blockchain implementations themselves. For example, uh we found serious denial of service vulnerabilities in the underlying consensus protocols. And last but not least, we're also in the process of building a bunch of tooling for zero knowledge uh proof circuits specifically targeting circum circuits and Cairo. And some of these tools can uh also find soundness bugs in zero knowledge proofs.

So basically the point that I want to make the more broader point is that the moto here is that tools and humans are much better together in the sense that formal methods tools can really help security auditors perform their audits much more effectively and much more consistently because they can help humans to realize edge cases that they normally wouldn't think about. So they're a really good way to augment human intelligence. So uh in addition to performing security audits that are heavily assisted by formal methods tools uh we are also in the process of uh starting what I call uh verification as a service. And the

idea here is that our clients will be able to upload their source code into our servers and use our formal methods tools to automatic to automatically analyze the code and get results in real time and uh perform continuous integration. So basically as a concluding thought, so the one thing I really would like everyone to take away from this uh talk is that tools and humans are much better together and formal methods can make auditing much more consistent, scalable and cost effective because they can help uncover security vulnerabilities in a more automated fashion than just uh humans alone can. So that's all I have.

Thank you very much. If you have any questions, I'm happy to take them. Uh hi there. I have two quick questions. Sure. Firstly, former methods has been around for a very long time and I've been doing security 20 plus years. I haven't really seen that amount of traction for for methods other than in very specific edge cases which is mostly military certified systems. Haven't we seen I haven't seen formally verified systems for the last 20 plus years. Red book if you look at it is a specification for formally verified techniques.

We haven't seen adoption in the space as in like security general security not even blockchain right number one it implies a uh scarcity of skills b difficulty the logic that you write down and the logic that you build that is a key problem right like if the two are inconsistent there is zero value in actually having form second thing is I want to understand how you would provide soundness proof for circum because I deploy something on circum I use 16 so I'd be curious to know how you do that Okay, so first question I absolutely agree with you that and that's why I said tools are not a substitute for humans because in order to formally verify anything you need to write formal specifications and if you don't have

formal specifications or if they're incorrect or they're incomplete then the formal verification guarantees that you get are going to be only as good as your uh specifications. Right? So uh regarding your question about circum uh that would be probably like a you know a topic for an entirely different talk. I could just talk about it like for so we yeah we have uh for more challenging circum uh proofs we have cockbased techniques for proving their correctness and for uh the not the libraries but the stuff that build on top of those libraries we have more automated ways of proving them but as I said that's like an that would be an entirely different talk in its own right we can have last one question

number two. Um, hi. Uh, I have short question. How long does it take to have a formal verification? Let's say from fist. Oh, that totally depends on how the complexity of what you're trying to analyze and the complexity of your specification. And you know generally speaking when I show that spectrum the lighter weight techniques tend to take less time whereas you know like the you know the more strong guarantees you want to give the longer sorry um so for example if you use a deductive verification tool and you're willing to write like these pre and post conditions

and method contracts then you can make verification modular. So that would basically like um mitigate some of the basically anytime you can make something modular then you can scale pretty much linearly with respect to the number of uh methods that you have timera no we're talking about like you know minutes or tens of minutes right yeah I was wondering um you said that all these four tools are all blockchain agnostic and language agnostic. So I'm wondering how you achieved that. Does that mean that you uh That's a great question. Yeah. So I I tried to hint at it, but the way we do

it, I shouldn't say they're completely language and blockchain agnostic. So what we do is we build our tools at the intermediate representation level at the LLVM bit code level and basically we uh instrument the when we do that translation from uh source code to the intermediate representation we instrument it with blockchain specific assumptions. So that's uh so in order to support a new language and a new blockchain you still need to you know modify that translation step or add that translation step but once you do that of course that's uh much easier than building a tool from scratch that's what I mean by language and blockchain agnostic [Applause]