How to Use AIs to Find Bugs
And by AI, we mean Automatic(ally Generated) Invariants
Hi there! Sorry it’s been more than a week. If you want to see what I’ve been busy with, you may want to check our latest blog post over at Akita. And if you’re wondering why I’m writing about bug-finding and gel manicures in the same post, you may want to read this first post.
A trusty sidekick who knows exactly what you want and helps you do it is the DREAM. The Jeeves to your Wooster. The Rose Tyler to your Doctor Who. The Hermione to your Harry. (There are cool sidekicks who aren’t British too, I promise.)
That’s the allure of AI, the Artificial Intelligence kind. Pretty much any time I hear anybody ask for an AI, what they’re really asking for is some combination of assistant and friend (and maybe lover?) who can anticipate their every need in an epic partnership.
In this post, I’m going to talk about a different kind of AI—Automated Invariants—that lets you live out the programmer’s version of this dream: the dream of automatically finding the bugs you care about, without you having to write tests. In this post, I’ll first introduce what invariants are, then what it means to automatically infer them, and then how this has been used in practice.
🤔 What are invariants and how do they help me?
Even if you don’t know they’re called that, you’ve probably used invariants at some point in programming. An invariant is simply a property that’s always true every time a program runs. Assertions represent invariants, since the program stops immediately with an exception if an assertion is violated. For instance, I just lazily copied an assert example for Python here:
def avg(marks):
assert len(marks) != 0
return sum(marks)/len(marks)In this example, the assertion introduces the invariant that the list being passed in for averaging needs to be non-empty. Dynamic assertions serve two main functions: 1) to force an exception if the assertion gets violated and 2) to let you assume that the assertion is true for the entire rest of the program. (You never have to check the length of marks again as long as it doesn’t change!)
I personally love programming with assertions (or other kinds of invariants, like types) because you can move a lot faster if you don’t have to keep checking for the same bugs throughout your code! But they do have some drawbacks. First, it takes discipline to program with assertions. Also, the assertions that we would think to write only catch a subset of the possible bugs. There are many “normal” program interactions that we wouldn’t think to capture as assertions, that would indicate the presence of bugs if they were no longer true. If it were a couple decades ago, I would have just told you “BEAUTY IS PAIN SO YOU HAVE TO WRITE MORE TESTS.” But I’m about to show you how we can do so much better.
Side note: not necessary for understanding this post, but something that I’ve spent a lot of time working on is statically verified invariants, properties that you can prove about programs before they ever run. To learn more, you may be interested in this talk I gave at Papers We Love a few years ago, about Tony Hoare’s 1969 paper “An Axiomatic Basis for Computer Programming.” (There is a lot of Ryan Gosling in this talk. I should have made the title “Fun with Logic with Ryan Gosling.)
✨ Using automatically generated invariants for fun and profit
Now I’m about to tell you about what I think is one of the most magical technologies in all of programming: automatically generated invariants. The technology behind this watches your programs run and in order to learn what is normal behavior, in order to automatically generate assertions that look like they always hold while the program is running. You can then use these assertions to help with documentation, bug-finding, static program verification, or whatever else it is you like to do with assertions. I don’t know about you, but as a programmer, this is pretty much everything I want in a sidekick/friend/assistant/lover.
At this point, if you’re a security person, you might be wondering what the big deal is, since there have been anomaly detectors in security tooling for a long time. At a high level, here are the two main reasons this is better:
You can see what’s actually getting learned. Because these invariant detectors are learning based on program models, you can go in and examine what they learn in order to understand what’s going on. You can check the automatically inferred assertions in order to see if they’re the right ones—and, sometimes, change them if they’re not. That’s huge, given the alternative is this black-box thing you have no control over.
You get way better accuracy. It’s not surprising that being able to actually model the program—and potentially get hints from the programmer—means that you can get fewer positives than other, less precise solutions.
Now I’ll talk a little about Daikon, a well-known research system for dynamic invariant generation built by UW professor Mike Ernst and his collaborators. (Fun fact: Mike Ernst was supposed to be my PhD co-advisor at MIT, but he ended up deciding to move to UW just before I got there.) Daikon works by tracing variables of interest to learn a set of possible invariants over program values, and then testing those invariants to see what actually sticks. (See this paper for more details.) It turns out that this approach is super powerful! Examples of Daikon output are as follows:
w >= 0
x < 10
y = w + x
z = 0 (mod 4)And you can imagine doing this not just for arithmetic, but also for access policies, data structure invariants, and more! There are two benefits to automatically learning these. First, a programmer doesn’t have to write these by hand anymore!! Second, you can imagine there are many of these kind of invariants that a programmer might not think to write, but that are actually true about a program and helpful to have. (And some the programmer might not think of because they’re actually a result of a bug!)
And what can you do with these? A programmer can look at this raw output to see if anything is out of the ordinary. Daikon is also a great tool to use in other automated tools: it’s been used for anomaly detection, understanding object interfaces, generating specs for static checking, supporting program refactoring, inferring behavior for concurrent systems, and more. There are Daikon frontends for Java, C/C++, .NET, Eiffel, and Simulink/Stateflow. In order to run with Daikon, you simply need to recompile with Daikon instrumentation. To get a sense of all the things you can do with Daikon, you may want to check out these papers.
👷🏻♀️ Finding invariants for fun and profit
Solutions like dynamic invariant generation often sound great in theory, but completely fall down in practice. I’ll talk about a couple of examples that show that dynamic invariant generation probably is one of the most useful ways of finding bugs people aren’t talking about today.
One of the coolest projects that uses the Daikon invariant generator directly is captured in the (unfortunately named) ClearView paper from Martin Rinard’s group at MIT. They use Daikon to generate invariants for normal program behavior, then use the learned invariants to monitor the system for anomalous behavior, and then automatically generate patches for the code. One of the most amazing parts is that they were able to successfully defend against a proper Red Team this way. (Read the paper for more!) Below is a somewhat gratuitous photo containing many of the authors of the papers and ME, at an MIT Programming Languages and Software Engineering Offsite from during my PhD. It’s getting really late so I’m not going to bother labeling the people and leave it as a where’s-Waldo kind of situation. (Hint: I’m Waldo.)
Invariant detection hasn’t been simply an academic exercise! Facebook has been using invariant detection for several years now. Here’s a paper about how they use invariant detector to learn and detect authorization rules. Facebook’s invariant detection uses database queries rather than program state, allowing the analysis to better handle Facebook-scale data. In this paper, they refer to a previous incarnation of the invariant detector that they were using for even longer.
💅 Now for the fashion part: automatically generated gel manicures with ManiMe
If it’s not already clear, I’m a big fan of automation and I don’t like to sit around doing things slowly. I’ve spent hours and hours of my life sitting through gel manicures that I endure because they look good, have no drying time (the reason I don’t do regular polish manicures), and last a long time (another reason I don’t do regular polish manicures). So you can imagine my delight upon discovering ManiMe, a company that is essentially making automated gel manicures: gel stickers laser cut from photos of your nails. Like actual gel manicures, they have no drying time and have that smooth gel look. Like super fancy salon gel manicures, they feature designs from Instagram-famous nail artists alongside classic colors and patterns.
They’re toxin-free, cruelty-free, and—best of all—peel right off without damaging your nails. See the Tweet below to find out the surprising way I learned about them, why I like doing them while on calls, and my referral code (which you can use to get $5 off 😉).
(And for everyone who wonders about the frivolity of manicures: spend some time looking at the hands of women in positions of power. I didn’t make the rules!)
Anyway, it’s bedtime, so that’s all the automation for today. Happy automating!
—
⚡️ Liked what you saw? Subscribe to JeanStack for your weekly dose of runway PL and fast fashion! Tell all of your friends!!
📺 If you’re interested in accessible PL conversations, you might also like my PLTalk Twitch livestream with Hongyi Hu (security @ Figma) Fridays at 3pm PT. Friday 8/7 our special guest will be Edwin Brady, the creator of Idris. 8/14 our special guest is Jeff Bezanson, co-creator of Julia. Tune in to learn about two of the hottest new programming languages!
✨ You may also be interested in checking out what we’re doing with API tools at my company, Akita Software. We’re very much applying techniques like this one—at the API level. If this sounds exciting to you, we’d love to have you try out our beta!