Statically Safe: Proving Security with Semantic Queries

Transcript

Okay, thanks everybody. I'm here to talk to you about how to keep our programs safe uh statically. So, if anyone here has performed an audit or reviewed code for bugs, they may be familiar with the rather draining experience of the increasing cognitive load that happens as you identify more and more potential issues in your code. And what I mean by cognitive load here is that as you think about more and more potential attack vectors and more and more potential problems which might lead to a hack, the number of ways in which these potential problems can manifest and the number of things that you need to check grows much more quickly than the number of problems that you identify. So these are all kind of

example questions we might ask when we are auditing a program. Uh, for example, if we have a lending protocol, we might wonder, is a health check always called before money is withdrawn. Or if we're interacting with some address and some internal function, we want to be sure that we always know that address has been validated at some point to be something in the protocol and not something that could lead to us getting exploited by a re-entry. And this leads to a kind of loop that we wind up having to deal with for each function for each property that we are concerned about for each of those functions for each call site of that function.

Is it possible that the inputs are going to violate this property? This is going to require eventually just meticulous notekeeping, tracking, being very careful that can transform kind of the fun creative aspect of bug finding into something that is stressful and even errorprone. And when we approach meticulous uh problems, we often ask ourselves, can I just have a computer do this for me? And so what we'd like to do is take our bug, our idea for an attack, ask the computer, is this bug in my code? Yes, check mark or no, it's not in my code and I'd like to move on. Now, computer is an increasingly vague term these days. We can be using all kinds of

different tech stacks to try to identify bugs. Uh we might be using AI. We could fuzz and test in various different scenarios. We can work to apply full for formal verification. Uh we can try to apply some static analysis which is you know ideally sound. And I've tried to map these out here across three properties that I think are relevant to cognitive load in auditing whether we can ask custom queries. Right? So lots of static analyzers today the kind of most design common design pattern is we have various detectors built in. So we might not be able to ask uh our specific question. Uh automatic detection is important. We don't want to just insert more work. Instead of notekeeping now you have to do a lot of extra maybe theorem proving. And we also want to be

able to trust our results. We don't want false alerts. Uh which means that if we still have to worry about a potential problem, the tool says, uh, no, that bug isn't present. Can we actually trust that the bug is not present? Can I actually cross that off of my audit to-do list? And I think one notable uh missing point in the design space here and we can argue about my exact placement of AI or static analysis depending on your your favorite tool is when the robot here is telling us no. So if we want to reduce cognitive load, we need to be able to cross something off of our list. We need to take something out of that inner loop as we're going through our audit and say okay I actually don't have to check for this

anymore. I don't have to trace through the call stack and check every time has this address been validated? Yes, great. No, I propagate it to the next call site. So to reduce that, we need something where we can uh perform a query, have it detected automatically, have it tell us no, there is no such instance of this bug and then we can still sleep at night because we can trust that there are no false alerts. And the solution I would pause it is to leverage static analyzers in a way differently than we have today. So this is an example of a a static detector from audit hub where we have a kind of SQL like detection language. And the idea here is that we can be very precise. Uh so I'll very quickly bore

you with a quote from Dystra that [snorts] so-called natural language is wonderful for the purpose it was created for but hopelessly inadequate when we have to deal unambiguously with situations of great intricacy which unavoidably arise in such activities as legislation, arbitration, mathematics or programming. And my point with all of this and what I just want to end on is that being able to precisely and exactly say what we want to find and what we want to not be present in our codebase and then succinctly and automatically have that checked and removed from our code is incredibly important in building trust and reducing the kind of effort and amount of cognitive load that goes into an audit. Thank you.

>> Awesome. Thank you, Benjamin.