[00:00.000 --> 00:08.100] Hopefully you guys will see this as a nice talk for setting the stage. [00:08.460 --> 00:15.240] The original idea was to have it as a very in-depth, very long two-panel talk. I think that [00:15.920 --> 00:24.900] was very optimistic. So this will be hopefully a cool talk in kind of the history and the [00:24.900 --> 00:31.280] uh, the field of program analysis. How we got where we got and where we came from. [00:32.940 --> 00:37.640] Let's see, we're almost there. Is it not? Can we have a countdown? [00:39.920 --> 00:46.960] New set? Alright! The stage is mine. Psych! I'm not talking about program analysis. We're [00:46.960 --> 00:54.400] gonna look at cats all day. But in all seriousness, when I saw that it was the 25th anniversary of [00:54.400 --> 01:04.580] DEF CON, I had this thought because just the week before I read the CFP, I was reading some [01:04.580 --> 01:10.600] paper about program analysis that was published in the 90s. And I was thinking that, you know, [01:10.600 --> 01:17.220] wow, these guys had like a lot of the same ideas that we're having now. And they were talking [01:17.220 --> 01:23.740] about this in the 90s. I wonder how much other such history has kind of fallen by the wayside. [01:24.900 --> 01:31.140] And so I started looking a little bit, digging through, and I wrote this proposal for the CFP [01:31.820 --> 01:36.900] to kind of go through the last 25 years of program analysis. And then when I was putting together [01:36.900 --> 01:44.280] the slides, I realized that program analysis goes way farther back. So where does, you know, [01:44.280 --> 01:52.020] the 25 years number come from? And I thought about some more. I realized that 25 years [01:52.020 --> 01:59.180] is actually my involvement with program analysis. 25 years ago, my grandma gifted me a book called [01:59.180 --> 02:04.840] Professor Fortran's Encyclopedia, which had like a cat named X and a professor named Fortran [02:04.840 --> 02:11.420] and a caterpillar named Caterpillar. And it went through their adventures in computer land [02:11.420 --> 02:17.320] and taught kids all about computer. I was crazy about this book. I ditched classes in first grade [02:17.320 --> 02:23.340] to hide in the stairwell and reread this book over and over. And I learned basic from it. And [02:23.340 --> 02:32.800] then later on, moved on to C and so forth. And I realized very early on that if I, you know, [02:32.800 --> 02:37.500] make a standard program that asks me for my name, and my name is too long, my last name, by the way, [02:37.500 --> 02:45.220] is Shorshutashvili. So I actually triggered bugs with this last name, then the program would crash. [02:46.320 --> 02:50.940] That turns out to be a buffer overflow and so forth. And then I started realizing that [02:51.980 --> 02:57.040] it's incredible to look at a computer program, try to understand how it really works. I mean, [02:57.040 --> 03:03.040] that's a whole different world in there, right? A world of ones and zeros and assembly instructions [03:03.040 --> 03:10.340] and logic gates. And somewhere along the line, it becomes alive and it starts behaving in ways [03:10.340 --> 03:16.920] that you don't quite understand ahead of time. And that's manual program analysis, [03:16.920 --> 03:24.100] understanding how this works. But then you can take that and make it automated. You can create [03:24.100 --> 03:31.680] programs that can understand programs. And it's like a whole level of craziness. That's like [03:31.680 --> 03:37.240] creating some sort of intelligence almost. And that's what fascinates me about program analysis. [03:37.240 --> 03:41.960] That's what's kept me going down the path I've been going for the last 25 years. [03:42.300 --> 03:50.300] And so this talk is about, you know, the history of program analysis. And it's about, you know, [03:50.300 --> 03:54.700] why we want to do program analysis in terms of kind of the dry things like we want to, [03:54.700 --> 04:02.180] you know, hack programs, we want to make sure programs are safe. But try to approach this [04:02.690 --> 04:10.120] topic from the sort of kid's perspective of discovering a whole new world of how programs [04:10.120 --> 04:16.380] work, and how programs might understand other programs. Program analysis is useful, [04:16.380 --> 04:25.840] but it's also kind of magical in a way. So with that said, let's move on to technical issues. [04:27.180 --> 04:34.120] Hmm. Hold on. Boom. Success. Let's move on to program analysis. [04:36.320 --> 04:44.780] Program analysis is a field that has basically three parts to it, right? You want to analyze [04:44.940 --> 04:50.740] a program, but you always want to analyze a program to figure something out about it. So [04:50.740 --> 04:56.140] for example, you might want to make sure that a certain specification of the program holds. The [04:56.140 --> 05:02.800] program doesn't crash, the program doesn't allow random people to unlock your smart key for your [05:02.800 --> 05:08.580] house, the program doesn't allow, you know, for your brakes to be remotely controlled, and so on. [05:09.440 --> 05:15.940] And you have a goal that you want to achieve with that specification. So for example, [05:15.940 --> 05:23.200] if your specification is, hey, I don't want this to crash, you could say, I want to make sure that [05:23.200 --> 05:29.620] that specification holds always. Or you might want to say, I want to make sure that that [05:29.620 --> 05:34.420] specification does not hold. I want to find the crash, right? So kind of, are you looking for bugs? [05:34.420 --> 05:38.920] Are you trying to make sure things are safe? And then, of course, once you decide what you want to [05:38.920 --> 05:44.100] do, you need to decide how you want to do it. What is the technique that you're going to use to [05:44.100 --> 05:54.560] reason about a specification on your program? And with these three kind of categories in mind, [05:54.560 --> 06:00.540] I'm going to run you through the history of program analysis and where along the line you [06:00.540 --> 06:09.460] collected different items, kind of different instances of these three categories. And so [06:09.460 --> 06:16.400] we're going to commence on a brief history of computing, starting in the 1830s with Charles [06:16.400 --> 06:23.520] Babbage. Charles Babbage created the analytical engine. It was a mechanical computer, super far [06:23.520 --> 06:29.760] ahead of its time. And he wrote a bunch of programs for it. By all accounts, these programs were [06:29.760 --> 06:33.860] actually really buggy. So that's really interesting. Some of the first computer programs written [06:33.860 --> 06:39.100] were already buggy. We didn't have that term yet. I'll talk about that later. And about a decade [06:39.100 --> 06:49.260] later, Ada Lovelace published a series of notes and more reasoning about this analytical engine, [06:49.260 --> 06:56.780] including the first complex program for one of these machines. So this is Ada Lovelace's [06:57.580 --> 07:06.760] description of the execution trace of this program. And the program computed Bernoulli numbers. [07:06.760 --> 07:13.080] And so she goes through instruction by instruction and says how variables change, [07:13.080 --> 07:23.760] and so forth. And this is in the 1840s, right? And so that's where things started. In 1947, [07:23.760 --> 07:33.620] about 105 years later, we got the term bug. Grace Hopper found, or people working with her, [07:34.440 --> 07:41.120] a actual moth inside a computer causing a computer error. So 100 years roughly after the [07:41.120 --> 07:48.040] first instance of kind of a computer in the semi-modern era, we have kind of this official [07:48.040 --> 07:57.660] term for the word bug. And this very quickly started getting people thinking about how do we [07:57.660 --> 08:02.820] kind of prevent actual software bugs. The moth, I guess, technically was kind of a wetware bug. [08:03.620 --> 08:11.140] But how do we prevent bugs in our software? And one of the kind of early visionaries here was [08:11.140 --> 08:18.680] Alan Turing, who's known for, of course, the Turing machine, but also cracking Enigma and [08:18.680 --> 08:27.340] onwards and onwards. But he also had the first paper that I could find that talked about, [08:27.340 --> 08:36.720] maybe we should try to make sure that the program is correct. And he published this in 1949. So two [08:36.720 --> 08:44.360] years after the kind of invention of the term bug, people start thinking about how do we make sure [08:44.360 --> 08:50.320] that there are no bugs in a program. And this creates the field of program verification. [08:50.360 --> 08:57.020] So program verification says, hey, given a program and the specification, we want to make sure that [08:57.020 --> 09:03.580] there are no bugs in this program, that this program carries out the computation needs to [09:03.580 --> 09:14.300] carry out and so forth, and doesn't go astray. So as an example, here's a simple program that [09:14.300 --> 09:20.940] has a crash, but that crash is not reachable, right? So if you give this program [09:23.800 --> 09:30.800] the somehow three numbers that add up, where a plus b equals c, but then c minus b is not [09:30.800 --> 09:36.900] equal to a, it'll crash. And you want to see if this program is safe. You can run a program [09:36.900 --> 09:45.460] verification on it, which will identify, you know, hopefully that this condition can never [09:45.460 --> 09:50.960] hold, and will produce a proof that tells you that the program is safe according to your [09:50.960 --> 09:58.540] specification. So that's great. And if everything worked like that in the real world, then we might [09:58.540 --> 10:04.500] not have bugs. And in certain cases, it does work like this in the real world. So there is formally [10:04.500 --> 10:08.540] verified hardware, according to a specific specification, of course. So things that [10:08.540 --> 10:13.220] the specification doesn't reason about, you know, maybe still can go wrong with that hardware, [10:13.220 --> 10:20.760] but things that are covered by the specification don't. So there's, you know, hardware that can [10:20.760 --> 10:27.840] provably not contain kind of timing side channel attacks, for example. And there's verified [10:27.840 --> 10:33.460] software. I heard recently that Google, for example, is switching over to a formally verified [10:33.460 --> 10:42.620] crypto system. And so the problems, of course, come when the software kind of gets bigger and [10:42.620 --> 10:47.400] complexity starts getting introduced, and verification stops being able to reason about [10:47.400 --> 10:53.260] things very effectively. So for example, here we have a different type of program, right? And [10:53.260 --> 11:01.400] this program also doesn't crash. That A cubed plus B cubed equals C cubed, that's Fermat's last [11:01.400 --> 11:08.520] theorem, right? That is not solvable. There's no solution. But it took humans hundreds of years [11:08.520 --> 11:15.500] to figure this out. And the computer, you know, verification tools, unless they're special coded [11:15.500 --> 11:23.400] for this, will also be unable to handle it. So it will kind of see this condition, it'll say, okay, [11:23.400 --> 11:30.880] well, if this condition is true, then the program will crash. Can I prove that the condition is [11:30.880 --> 11:34.940] always false? And if it can't prove that the condition is always false, it has no choice [11:34.940 --> 11:46.580] but to alert that the program cannot be verified. So what happens then, right? So then [11:47.110 --> 11:53.760] you have to go in and you have to start looking at the program manually and finding bugs. And [11:53.760 --> 12:01.020] if anyone's used kind of commercially available static analysis tools, you're very well familiar [12:01.020 --> 12:07.680] with the false positive problem, right? You open up a binary or a piece of software and the tool [12:07.680 --> 12:14.520] pops up alerts all over the place. And some of those are actual bugs. But you spend a lot of time [12:14.520 --> 12:23.100] chasing down the alerts. So when we look at, you know, software, open source software, for example, [12:23.840 --> 12:31.860] we often see, you know, a security check done twice, the same check. If A is not null, [12:31.860 --> 12:38.720] if A is not null. Why is that check there twice? Because for whatever reason, a program verification [12:38.720 --> 12:46.600] tool alerted that there could be a bug there and the programmer figured out some hack to make it [12:46.600 --> 12:56.920] shut up. So program verification, while it's a very useful field, like I said, there is verified [12:56.920 --> 13:04.420] software and hardware out there. It's not kind of the final answer on its own. So we also at some [13:04.420 --> 13:10.160] point need to have kind of the flip side. So program verification can say that is safe. But, [13:10.160 --> 13:15.600] you know, after that it says, okay, I can't really reason about it. So the flip side is you have a [13:15.600 --> 13:21.020] technique that says that is not safe. I can prove it. But I can't really prove, you know, if it is [13:21.020 --> 13:28.560] safe. But if it is not safe, I'll give you a counterexample. And the way this works is by, [13:28.560 --> 13:33.880] you know, finding counterexamples to whatever technique. So in this case, with a slightly [13:33.880 --> 13:43.480] different condition, that is A squared plus B squared equals C squared, a technique might find [13:43.480 --> 13:48.640] A, B, and C of three, four, and five as a counterexample that will reproduce a crash. [13:49.320 --> 13:56.840] And so this is, there are many techniques that, you know, we'll mention later that can be used [13:56.840 --> 14:04.500] to do program testing. But one of the very early ones, the first instance of program testing of [14:04.500 --> 14:10.260] this style that I found was in the 1950s, which is about four decades before I thought that this [14:11.700 --> 14:21.600] kind of idea was created. Programmers in the 1950s would program in punch cards. And to test [14:21.600 --> 14:27.880] their code, it was common practice to dig punch cards out of the trash and feed them as input to [14:27.880 --> 14:35.020] your program. This is unexpected input, just random stuff. And of course, by random stuff, [14:35.020 --> 14:42.960] program shouldn't crash. So this is kind of an early example of this sort of [14:43.960 --> 14:51.400] kind of institutionalized testing that we're, you know, only seeing come back recently. [14:52.200 --> 14:58.060] And so, you know, these early developments, verification, testing, the creation of those [14:58.060 --> 15:06.420] two ideas, and then the idea of what you might check for. So the, you know, trash decks check [15:06.420 --> 15:13.020] for crashes. Turing reasoned about ensuring logical properties. But this is all done manually. [15:13.020 --> 15:18.500] So this is kind of our first set of tools in our tool bag, and they're manual tools. We have to [15:18.500 --> 15:25.500] dig them out. Okay, let's get our trash, you know, cards. This one got eaten by something and, [15:25.500 --> 15:31.520] you know, put in the ones that won't jam your machine and try them. But none of this was [15:31.520 --> 15:39.760] automated. And so as computers became more and more ubiquitous, the need for automation started [15:39.760 --> 15:49.800] showing itself. So again, we come on a mention of Grace Hopper here, because she not only found the [15:49.800 --> 15:57.780] first bug, but she also invented the compiler. So Grace Hopper in 1952 published a paper saying, [15:57.780 --> 16:02.120] hey, what if we wrote in kind of higher level languages and it got, you know, squished down to [16:02.120 --> 16:10.660] computer code. And this took a little while to catch on. And the reason it took a while to catch [16:10.660 --> 16:17.880] on, one of the reasons is that the code that was generated by this compiler was very slow. [16:17.880 --> 16:24.920] It couldn't be, you know, optimized as well as handwritten assembly could at the time. [16:25.220 --> 16:31.940] And so this identified another need, another goal of program analysis, transformation of binaries [16:31.940 --> 16:37.480] into something different, something faster in this case. And in the modern era, you know, [16:37.480 --> 16:43.640] you can transform binaries, for example, or transform programs to ensure that they're safe. [16:43.640 --> 16:48.000] Transfer programs to meet any sort of specification around on a different set of hardware. [16:50.000 --> 16:55.420] And so now we needed to optimize code because, you know, people write slow code when they're [16:55.420 --> 17:04.660] writing source for whatever reason. And another thing happened, people started realizing that [17:04.660 --> 17:11.820] we have all of these architectures with all of this data flowing around in them. And if you're [17:11.820 --> 17:18.120] not very, very, very careful, some data could be read from or written to a different location than [17:18.120 --> 17:27.280] intended, and the memory could be corrupted. So I just played, you know, two days of a CTF full of [17:27.280 --> 17:37.280] these errors, of course, memory corruption bugs. And this was first described in 1968. In 1968, [17:37.280 --> 17:43.260] there was a paper saying, hey, you know, we noticed that if the kernel, they called it a [17:43.260 --> 17:50.380] monitor at the time, blindly trusts everything that, you know, the user space sends it, bad [17:50.380 --> 17:55.720] things can start to happen. And so this paper introduced that concept. It's also the paper that, [17:55.720 --> 18:02.280] you know, one of the early works in memory protection and virtual memory and so forth, [18:02.280 --> 18:08.300] which is pretty interesting that immediately they realized this was a problem. And a little while [18:08.300 --> 18:13.780] later, there was, you know, Ken Thompson's reflecting on trusting trust, where he reasoned [18:13.780 --> 18:19.060] that you could build in a backdoor into a compiler that could build in backdoors into sensitive code. [18:19.060 --> 18:26.290] And so suddenly, we have two more things that we need to worry about in terms of specifications, [18:28.070 --> 18:33.170] or even more, but, you know, including memory safety, information disclosure, [18:33.170 --> 18:39.810] and authentication, right? So now you might want to verify that a program doesn't have a backdoor. [18:40.810 --> 18:46.910] Or you might verify that a program will not leak your sensitive private information. That is, [18:46.910 --> 18:52.750] that one is very relevant today with all of our phones having all of our information and [18:52.750 --> 19:00.710] very little control over it. And so the need for automation was pretty well established [19:01.790 --> 19:10.450] by the kind of turn of the century, for sure. But even before that, those papers were like [19:10.450 --> 19:18.690] in the 1960s or something, late 1960s. And very quickly, oops, sorry, very quickly, [19:18.690 --> 19:23.510] people started to meet this need. The research community started pumping out [19:23.510 --> 19:28.670] automated approaches. And so I'm going to introduce a couple of these automated approaches. [19:30.610 --> 19:37.310] And before I do so, I want to make you guys experts in program analysis, so that we can [19:37.310 --> 19:44.330] reason about what's going on here. So we'll talk about a couple of prerequisites, right? [19:44.330 --> 19:50.830] So let's say you have a program. So on the top right, there's like a little Python program [19:52.790 --> 19:59.030] that's already a vulnerable program, by the way. And so you have this program, [19:59.950 --> 20:03.950] and you want to analyze it. So you have to reason about a program in a slightly different way [20:03.950 --> 20:10.710] as a computer than as a human. So for example, a program is viewed by a computer as a set of [20:10.710 --> 20:17.410] basic blocks. A basic block is a piece of code that is executed all together before passing on [20:17.410 --> 20:24.570] control flow somewhere else. So in our case, we'll pretend that input is part of this basic block. So [20:24.570 --> 20:30.250] this X equals input is a single basic block, and then it might branch depending on the input, [20:30.250 --> 20:37.010] right? So if you put in 42, it'll do one thing. If you put in something else, it'll do another. [20:37.010 --> 20:42.350] And so this is the end of the basic block, and then the result of that if statement is two other [20:42.350 --> 20:51.150] basic blocks, the true case and the false case. And each of these has a constraint that has to [20:51.150 --> 20:56.870] be met, right? In order to go down one path, you have to put in 42. In order to go down another, [20:56.870 --> 21:03.110] you have to put in not 42. And so these are called constraints. If you then look at all of the basic [21:03.110 --> 21:08.710] blocks of a program, this is called a control flow graph because that's, you know, these are [21:08.710 --> 21:16.570] basic blocks and control flows between them. And if you look at a path down this graph, now in this [21:16.570 --> 21:22.050] case the graph is nice and simple, but in reality it could have loops, a path might hit the same node [21:22.050 --> 21:29.490] multiple times, and so on. And then you look at the constraints all along this path. These are [21:29.490 --> 21:36.290] the path predicates that uniquely identify this path. So if you collect all of these constraints [21:36.290 --> 21:47.770] and you say that x is not 42 but x is 1337, that input will... any input that matches those [21:47.770 --> 21:54.170] constraints will take the same path through the program. So these are kind of the prerequisites [21:54.170 --> 22:00.150] of our program analysis techniques. So now we'll go through three of them. Actually for time reasons [22:00.150 --> 22:05.670] we'll go through two of them and mention a third. But we'll start with symbolic execution. And [22:05.670 --> 22:11.130] symbolic execution got a lot of hype recently, especially with stuff like the cyber grant [22:11.130 --> 22:21.570] challenge and so on, as a way for machines to reason about program code. And you think that [22:21.570 --> 22:28.430] this is something new, but it turns out that it's not. It's quite old actually. So 40 years ago, [22:28.830 --> 22:33.890] a little bit more, the first symbolic execution paper that I could find was proposed. [22:35.290 --> 22:39.630] And there were several actually, right in one year basically. So this idea [22:40.370 --> 22:46.730] had some prerequisites that were met and then it exploded. And so the symbolic execution engines [22:46.730 --> 22:52.710] were developed that could then symbolically execute Fortran code. Now we have symbolic [22:52.710 --> 22:58.210] execution engines that you can download off GitHub that can execute binaries, Java, [22:58.910 --> 23:08.530] Android, whatever you want. And this is kind of a fairly powerful way of reasoning about programs. [23:08.530 --> 23:13.090] And let's run through an introduction of it with a slightly more complicated [23:14.550 --> 23:19.530] example than what we learned about program analysis with. [23:20.970 --> 23:29.570] Hold on. So here's a program that has several bugs, right? One is it, [23:30.370 --> 23:36.870] well, it definitely has one bug and that is if you enter a username of service [23:36.870 --> 23:43.070] and a command code of seven, it'll crash, right? You can imagine that instead of this crash, [23:43.090 --> 23:47.910] it does some system relevant stuff. So it could be a backdoor instant memory [23:47.910 --> 23:51.910] corruption, but basically we have a program with a bug and we would like to find this bug. [23:51.910 --> 23:56.210] So let's see how we might approach this problem with symbolic execution, right? [23:57.290 --> 24:02.930] So first let's look at the control flow graph of this program, starting from the beginning. Again, [24:02.930 --> 24:08.570] the control flow graph is made up of basic blocks and the control flow transitions between them. [24:08.570 --> 24:14.750] So we start at this input. If the input is service, it branches. If the username is service, [24:14.750 --> 24:23.690] it branches into one side of the equation of the program where it checks for the command code [24:23.690 --> 24:30.950] being seven. And if it is, it crashes. If not, it prints an on command and then it exits. [24:31.750 --> 24:39.970] On the other side of the branch, it asks for a passcode. If the passcode is invalid, [24:39.970 --> 24:44.970] it prints invalid passcode. Otherwise, it calls the authentication function, [24:44.970 --> 24:49.250] then it prints exit and exits. So this is our control flow graph. And how would [24:49.250 --> 24:56.350] we use symbolic execution to try to find that crash, try to find the ability to reach this crash? [24:56.350 --> 25:04.590] So we would start executing the program in an emulator. And in this emulator, instead of ones [25:04.590 --> 25:14.210] and zeros, we are working on X, Y, and other symbols. So, for example, username is a symbol [25:14.210 --> 25:22.010] in this emulator. So when we pull in an input, it will produce an unconstrained variable called [25:22.010 --> 25:27.090] username. And we don't know what username is. Username can be anything. Because, you know, [25:27.090 --> 25:36.670] that is how we implement our emulator. And as we check for values of username, we [25:36.670 --> 25:42.330] create what are called constraints, right? So these are the exact constraints that the basic [25:42.330 --> 25:49.270] block checks when it pushes execution forward. And we collect two constraints in this case. [25:49.270 --> 25:53.630] On the one side, username equals service. On the other side, it does not equal service. These are [25:53.630 --> 26:00.810] constraints. And we continue executing both sides of this statement with symbolic execution. [26:01.530 --> 26:08.090] But then we hit something that is very bad for symbolic execution. We hit, for example, [26:08.090 --> 26:14.870] string processing functions. So a string processing function like A2I might check a [26:14.870 --> 26:20.910] given byte, see if it is a number. If it is a number, it'll do one thing. If it's not, it'll [26:20.910 --> 26:26.390] do another, right? Or if it's a certain number, it might do one. If it's not a certain number, [26:26.390 --> 26:31.950] it'll do another. So it'll keep branching the symbolic emulator at every... [26:33.810 --> 26:42.050] I'm sorry? Oh, awesome. It'll keep branching the symbolic emulator at every if statement, [26:42.050 --> 26:50.390] every check on this number until we get into a situation where there are just too many checks, [26:50.390 --> 26:56.230] right? So it'll try to check for a command code of, you know, [26:57.330 --> 27:04.910] 10 bytes with arbitrary values of 9 bytes and so on. And there's an exponential path explosion [27:04.910 --> 27:11.730] here. And there are some approaches in the symbolic execution world to try to deal with [27:11.730 --> 27:16.730] this sort of path explosion. But in general, these approaches boil down to the requirement [27:16.730 --> 27:23.210] to remove paths, right? And lose this information. And so in the end, the symbolic execution engine [27:23.210 --> 27:31.990] might only find certain paths and not others and miss the bug. Because we have to simplify [27:32.450 --> 27:38.850] to keep things tractable. So that's symbolic execution. It might find the bug if you're lucky, [27:39.090 --> 27:47.190] but if you're not, and it has to simplify its state space essentially as it's executing, [27:47.190 --> 27:53.890] there are certain things that it might miss. Symbolic execution was proposed as you saw in [27:53.890 --> 28:05.590] 1975. But the interesting thing is that in Ada Lovelace's notes from 1942, we can see [28:06.310 --> 28:14.610] that she did a symbolic trace of the execution of her program. So where she has this sort of [28:14.610 --> 28:23.750] program execution log in her notes, she writes down the symbol, the equation for each variable [28:23.750 --> 28:31.470] as the program progresses. And this is the first symbolic trace of a program, done in 1842 before [28:31.470 --> 28:39.290] computers were invented. So that was a pretty interesting thing to find. And kind of a nice [28:39.290 --> 28:49.190] point of history that we can put as the start of program analysis in this sense. 1842, not 1975 or [28:49.190 --> 28:58.570] 1949 or any of those much, much later dates. And so symbolic execution is a kind of tool in our [28:58.570 --> 29:06.430] tool set that we can use to achieve either verification of a specification, the testing of a [29:06.430 --> 29:14.650] specification, or to support the transformation of code. Of course, how you verify a program, for [29:14.650 --> 29:20.910] example, using symbolic execution is a pretty complex thing with the symbolic execution style [29:20.910 --> 29:25.930] that I described for program testing. It generates inputs to find vulnerabilities, but it can't prove [29:25.930 --> 29:35.630] that there aren't any. But that's kind of a, we could go down that route for an entire semester [29:35.630 --> 29:42.590] course, and not just a 45 minute introductory talk. So I'll leave that as future research for [29:42.590 --> 29:50.910] you guys. And we'll go on to static analysis, because static analysis can show that, for example, [29:51.250 --> 30:00.850] a program is immune to a certain class of vulnerabilities or properly implements a certain [30:00.850 --> 30:09.410] specification. Static analysis, or at least one of the very common ways to do static analysis, [30:09.410 --> 30:15.950] which is abstract interpretation, was proposed in 1977, shortly after symbolic execution. [30:15.950 --> 30:30.610] And abstract interpretation looks at the control flow graph, the program as a whole, essentially. [30:30.610 --> 30:40.010] It doesn't have to figure out how to reach a certain basic block to reason about properties [30:40.010 --> 30:45.770] of the program at that basic block, which is the problem that symbolic execution had, and the reason [30:45.770 --> 30:53.010] that symbolic execution could not find the bug in our example. And so static analysis with [30:53.010 --> 30:58.070] abstract interpretation might be able to find that bug, probably will be able to find that bug if it [30:58.070 --> 31:05.610] is a simple bug, or actually, I should say, will be able to find that bug. Because if it cannot [31:05.610 --> 31:12.350] prove that a piece of code is safe, it will raise an alert. The problem is that, as we talked about, [31:12.350 --> 31:17.570] there are false positives. So in our program, it might think that that function has a bug, even if [31:17.570 --> 31:25.350] it doesn't, alert on that, and eat up time for a human to go through and verify all these results. [31:26.670 --> 31:33.350] And so through abstract interpretation, we got a way to perform verification or specification [31:33.350 --> 31:44.150] on a program in 1977, 40 years ago. And then we moved on to fuzzing. And so fuzzing is kind of one [31:44.150 --> 31:50.890] of the biggest ways to find vulnerabilities in modern software. And it's actually surprisingly [31:50.890 --> 31:58.670] simple. Proposed in 1981, initially, in its most basic form, which was, hey, let's throw random [31:58.670 --> 32:04.950] input at a program and see if it crashes. It's evolved quite a bit since then. And so the [32:05.710 --> 32:12.490] specific implementation of fuzzing that I'll describe here is implemented by American Fuzzy [32:12.490 --> 32:20.250] Lab. It's a fuzzer that mutates its inputs when it detects differences in program execution. [32:20.970 --> 32:26.630] And so let's see how it would run on our program here. We'll start with [32:27.470 --> 32:34.850] some randomly generated test case or human-seeded test case. So a human might input a username of [32:34.850 --> 32:44.070] ASDF and a password of 111. And that input will trigger certain basic blocks to be executed, [32:44.070 --> 32:49.770] right? And so we executed the username input, of course. We executed the check for the [32:50.470 --> 32:57.190] kind of service username that could lead to the crash. We did not satisfy it, so we took the else [32:57.190 --> 33:06.690] branch, read in the passcode, and errored out on an invalid passcode and exited. So we triggered [33:06.690 --> 33:13.690] those basic blocks. And so the fuzzer starts mutating this input, right? It might make a [33:13.690 --> 33:26.730] capital D or something. Or it might mutate input in a way that passes another check. So it mutated [33:26.730 --> 33:34.230] the input in a way that passes that passcode check. It actually doesn't, because there's [33:34.230 --> 33:39.070] another bug in the program that I didn't notice before. But let's pretend that it [33:40.790 --> 33:49.630] creates a valid size of a passcode and triggers that authentication function, right? So that [33:49.630 --> 33:56.690] is a new basic block that it triggers. Now with fuzzing, we've triggered a block that symbolic [33:56.690 --> 34:05.470] execution before us wasn't able to trigger just through randomly mutating inputs. But then we get [34:05.470 --> 34:13.610] stuck. Because through randomly mutating inputs, we are unable to satisfy complex checks, right? [34:13.610 --> 34:20.210] We need a username of service, and we have randomly mutated usernames. The chances are [34:20.210 --> 34:25.330] that we'll create the string service are very slim, and we'll keep guessing and guessing and [34:25.330 --> 34:30.770] guessing. Of course, in this specific case, you could seed the fuzzer with the string service, [34:30.770 --> 34:37.370] and you could scan the program for all of its strings and automatically [34:38.050 --> 34:43.350] make the fuzzer pass this check. But string checks aren't the only complex checks [34:43.350 --> 34:52.010] in programs. There are hashes, there are complex input formats, dependencies between [34:52.010 --> 35:00.230] different input bytes. And so in the general case, we cannot guarantee, of course, with a fuzzer [35:00.230 --> 35:08.850] that we will find code that is protected by these complex checks. And so fuzzing [35:09.970 --> 35:17.990] with this random data, of course, is a throwback to this trash deck concept. So fuzzing [35:17.990 --> 35:28.090] was invented in 1950, not 1981. Or at least manual fuzzing. So again, we find that [35:28.090 --> 35:34.810] program analysis techniques harken back to the middle of the century, and sometimes even [35:34.810 --> 35:41.970] farther to the 1800s. So now we have this kind of toolbox of a bunch of specifications that we [35:41.970 --> 35:50.710] can enforce, some goals that our analysis could try to achieve, and the technique through which [35:50.710 --> 35:59.490] we can achieve them. And next, we should evaluate them, understand how these different [36:03.410 --> 36:09.430] goals or how these different techniques help us achieve program analysis goals. And [36:11.310 --> 36:20.670] as a scientist, if you start thinking up an approach, and you have a cool idea, [36:20.670 --> 36:26.870] have a new program analysis technique, you want to evaluate it. So you want to take [36:28.090 --> 36:33.430] programs and specifications, feed them into your technique, and see how well it does. This is my [36:33.430 --> 36:42.510] clipart slide, by the way. So hopefully my clipart game is on point. So you run your analysis, [36:42.510 --> 36:47.910] you get your results, and you're happy, right? Well, there are a number of problems with this. [36:47.910 --> 36:55.350] One is that the analysis is more complex than you might think, because any program analysis [36:55.350 --> 37:01.390] has to deal with the environment of the program it's analyzing. And environments like Windows, [37:01.670 --> 37:11.250] macOS, Linux, mobile devices, cyber-physical devices, they have really complex environments. [37:11.730 --> 37:20.090] Having to model this environment, even before understanding how much better your program [37:20.090 --> 37:27.870] analysis technique is than previous techniques, is quite a big investment that people often don't [37:27.870 --> 37:37.290] make, or make in a very fast manner. Another problem is finding a good data set to evaluate [37:37.290 --> 37:43.130] on, right? There's not really a good data set for... or there wasn't a great data set for [37:43.130 --> 37:46.990] vulnerability research. This problem is actually being worked on, and new data sets are being [37:46.990 --> 37:54.390] created, as I'll talk about. But you need a good data set with ideally known vulnerabilities, [37:54.390 --> 38:00.810] so you can reason about how many of them your bug finds, and with variable vulnerabilities [38:00.810 --> 38:11.030] in different programs, so your technique isn't just specifically tailored for one style of [38:11.030 --> 38:15.890] vulnerability that you happen to detect, or one specific program that you happen to be very good [38:15.890 --> 38:20.810] at analyzing. Another problem is these specifications. Specifications in the real [38:20.810 --> 38:29.790] world are very complex, whereas specifications that you might want to use for your analysis tool [38:30.470 --> 38:35.970] initially in the early stages of development need to be fairly simple and ideally pre-provided. I [38:35.970 --> 38:43.710] mean, if you're looking at analyzing something like Chrome, and your specification is that Chrome [38:43.710 --> 38:51.130] should not leak user data to someone that should not get this user data, that's impossibly broad [38:51.130 --> 38:58.730] and impossible to enforce. Is your bank allowed to have your various cookies or something along [38:58.730 --> 39:05.650] these lines? So you need a very good data set, standard data set, with a very good [39:05.650 --> 39:12.850] standard implementation, standard set of specifications, so that you can analyze [39:12.850 --> 39:21.230] how well your technique runs compared to different work, and compare those results [39:21.230 --> 39:27.230] to prior work, because that's a very important part of science and technical development, [39:27.230 --> 39:37.870] understanding if you're making an improvement or not. And so we had problems as an analysis [39:37.870 --> 39:43.090] community in meeting all of these goals, and having a good data set of applications, [39:43.090 --> 39:51.600] with a good set of specifications, on a good environment that wasn't too complex to implement, [39:52.090 --> 39:56.310] and that could produce results that we could reason about, that we could say, [39:56.310 --> 40:04.090] we have ground truth data for the vulnerabilities that are actually in this data set, and we detect [40:04.790 --> 40:13.230] x of them, or we manage to rule out vulnerabilities in code that has no vulnerabilities, [40:13.230 --> 40:22.910] and so our program verification is correct. And so, like I mentioned, there have been [40:22.910 --> 40:29.790] several projects to solve this problem, to create these data sets, and one of these [40:30.750 --> 40:34.970] projects essentially was the Cyber Grand Challenge. If you guys were here last year, [40:34.970 --> 40:44.170] you probably saw all of the Cyber Grand Challenge, you know, hoopla, where for the first time in [40:44.170 --> 40:51.070] history, seven fully automated program analysis machines fought each other in a game of capture [40:51.070 --> 40:58.450] the flag. So the same game that I spent the entire weekend playing and only got four hours of sleep [40:59.050 --> 41:06.270] is the game that machines who didn't need to sleep played yesterday, last year rather. And [41:09.170 --> 41:13.510] these machines, of course, suffered from all of the problems that I just talked about, [41:13.510 --> 41:17.870] the environment problem, the specification problem, and so the Cyber Grand Challenge [41:17.870 --> 41:27.630] created a custom operating system with very specific vulnerability specifications to [41:29.470 --> 41:34.250] evaluate these systems. Now, for the actual competition, of course, the source code wasn't [41:34.250 --> 41:40.610] available, since then they released the source code, so you can really look at the source code, [41:40.610 --> 41:46.830] understand the vulnerability, and then reason about how well your tool finds certain [41:46.830 --> 41:56.590] vulnerabilities across 249 binaries. So it's a 249 program, so it's a data set that has a [41:56.590 --> 42:04.910] lot of variants, there are a lot of different types and different difficulties of vulnerabilities, [42:04.910 --> 42:13.970] and all of this is freely available for people to analyze their tool and understand how well it does. [42:13.970 --> 42:21.750] That's my other piece of clip art. So the Cyber Grand Challenge and the programs that [42:21.750 --> 42:27.530] were written for this, these 249 programs making up the Cyber Grand Challenge data set, [42:28.790 --> 42:36.390] allowed us to do what I call, to perform what I call the program analysis nursery experiments. [42:36.390 --> 42:40.310] So I see the Cyber Grand Challenge data set as the nursery of program analysis, where you can [42:40.310 --> 42:46.170] reason about different improvements for different techniques. So for example, Symbolic Execution on [42:46.170 --> 42:51.550] the entire data set finds nine vulnerabilities. This Symbolic Execution has implemented in [42:51.550 --> 42:56.910] Anger, which I'll talk about in a sec, which is an open source binary analysis program available [42:56.910 --> 43:05.090] on GitHub. But Symbolic Execution on this entire data set finds nine vulnerabilities. That's not a [43:05.090 --> 43:10.550] lot, right? There are vulnerabilities in every program of these 249 programs. It only finds [43:10.550 --> 43:16.210] vulnerabilities in nine of them. Of course, we can optimize Symbolic Execution using various [43:16.210 --> 43:22.250] tricks. So Anger supports, for example, concrete execution when there is no uncertainty in the [43:22.250 --> 43:28.610] state, when all the data is known, or when there are constraints on all the data. And so by [43:28.610 --> 43:38.450] utilizing all of these optimizations, we can get 26 crashes, crashing 26 binaries. [43:38.950 --> 43:45.730] Utilizing static analysis, so combining Symbolic Execution with Veritesting, which is a technique [43:45.730 --> 43:52.230] created by Carnegie Mellon University that utilizes parts of abstract interpretation to help [43:52.230 --> 43:57.470] with Symbolic Execution, we can push that up to 31. So I should say here that this is our [43:57.470 --> 44:04.050] implementation of Veritesting, and it might be suboptimal. So their Veritesting might be [44:04.050 --> 44:10.970] considerably better. But that all pales in comparison with fuzzing. This seemingly simple [44:10.970 --> 44:18.810] technique of throwing random data and seeing what happens finds 106 crashing binaries in the data [44:18.810 --> 44:26.350] set. So this gives us an idea of where program analysis is, and this is a good showcase for [44:26.350 --> 44:33.470] the simplicity of evaluating all of these different analyses on this data set and reasoning about [44:33.470 --> 44:40.230] the results. Because now we can look at them in terms of, you know, summation numbers. But [44:40.230 --> 44:46.570] there's also some subtleties there. They find bugs, different types of bugs in different binaries. So [44:46.570 --> 44:55.570] we can look into that and make inferences and try to create new approaches. So for example, [44:55.570 --> 45:00.650] we looked at the difference in the types of bugs that symbolic execution found and that fuzzing [45:00.650 --> 45:07.950] found, and we realized that they have very different coverage. So the types of the basic [45:07.950 --> 45:12.150] blocks that fuzzing can trigger are very different from the basic blocks that symbolic execution can [45:12.150 --> 45:16.830] trigger. And sometimes one finds a crash, sometimes another finds a crash, sometimes neither of them [45:16.830 --> 45:24.770] find a crash. In fact, very frequently. And so we decided to combine them in a very [45:26.690 --> 45:33.410] straightforward but careful way. And the idea is as follows. We begin by fuzzing the binary. This is [45:33.410 --> 45:38.410] nice and fast and achieves decent code coverage, but as we discussed, eventually gets stuck [45:38.410 --> 45:45.050] on complex checks. And then we use symbolic execution to find the constraint that can get [45:45.050 --> 45:50.890] through that check, but possibly suffer from other limitations of symbolic execution and not [45:50.890 --> 45:55.590] find the actual bug. And then we synchronize that back into the fuzzer. We synchronize the [45:55.590 --> 46:02.890] knowledge of how to bypass the complex check back into the fuzzer, and it continues to mutate that [46:02.890 --> 46:10.390] input until it finds the bug. And we do this iteratively, back and forth between the fuzzer [46:10.390 --> 46:18.910] and symbolic execution. So by implementing symbolic assistance for the fuzzer in this way, [46:18.910 --> 46:27.990] we achieve on this entire dataset 118 crashes. And an interesting thing here is that we have [46:27.990 --> 46:35.970] this 118 crashes in the dataset, but if you take the union of all of the different techniques, [46:35.970 --> 46:41.170] all the different techniques have crashed something like this from memory, 150 to 160 [46:42.010 --> 46:49.010] binaries. So there's a lot of uniqueness between the different techniques used here. [46:50.490 --> 46:56.030] Driller, the applicability of it varies by program, whether or not there are complex checks. [46:56.390 --> 47:01.810] We can run through a quick run here. So this is a control flow graph of an example program, [47:01.810 --> 47:11.890] and driller starts in the top left corner there. And it first starts by fuzzing a portion of the [47:11.890 --> 47:17.990] program before it gets stuck in a complex check. And this is the basic block coverage on the right [47:17.990 --> 47:25.070] in this graph here. You can see just kind of flat lines, right? So then if we run the symbolic [47:25.070 --> 47:33.910] execution engine to help the fuzzer reach extra code paths, it allows us to find just a little [47:33.910 --> 47:40.310] tiny bit more basic blocks in the executor, some more basic blocks in that control flow graph of [47:40.310 --> 47:47.210] the program. And if we keep invoking the symbol execution engine to help the fuzzer get unstuck [47:47.210 --> 47:54.450] every time that the coverage flat lines like that, we eventually drill into the program deep [47:54.450 --> 47:59.930] enough to find the bug. And so that's how driller works. There's still a lot to do. So there's this [47:59.930 --> 48:09.230] whole red area that however many programs, about 100 programs that we have never exploited before, [48:10.050 --> 48:16.230] that we've never crashed before using any automated techniques, which represent missing [48:17.830 --> 48:22.870] tools basically that humanity has yet to develop, or at least we have yet to develop. [48:23.730 --> 48:29.010] And so if this all sounds interesting to you, I encourage you to join in. There are several ways [48:29.010 --> 48:33.610] that you can participate in program analysis research. One is you can contribute to open [48:33.610 --> 48:40.250] source frameworks. So we run one of these frameworks in our research lab. It's called [48:40.250 --> 48:47.790] anger. Go to anger.io. There's a lot that we could use help with documentation, environment support, [48:47.790 --> 48:55.430] better techniques, and so on. And the other is that I'm always looking for students. I'm starting [48:55.430 --> 49:05.650] as a professor at Arizona State University. I just finished a PhD at UC Santa Barbara, and both of [49:05.650 --> 49:11.610] those places are incredible places to go to if you want to do research in program analysis or in [49:11.610 --> 49:20.090] general security. So if you're thinking about graduate school, or you are curious and want to [49:20.090 --> 49:26.850] do an internship, reach out to me. I'll put you in touch with the right people, and you could explore [49:26.850 --> 49:33.690] that. The presentation is available online. All my contact info is right here, and I guess we'll [49:33.690 --> 49:37.590] questions in the hall? Awesome. Thank you, guys.