WEBVTT 00:00.000 --> 00:08.100 Hopefully you guys will see this as a nice talk for setting the stage. 00:08.460 --> 00:14.740 The original idea was to have it as a very in-depth, very long two-panel talk. 00:14.740 --> 00:19.540 I think that was very optimistic. 00:19.960 --> 00:28.420 So this will be hopefully a cool talk in kind of the history and the uh, the field of program analysis. 00:28.420 --> 00:31.280 How we got where we got and where we came from. 00:32.940 --> 00:34.880 Let's see, we're almost there. 00:34.880 --> 00:35.780 Is it not? 00:36.160 --> 00:37.640 Can we have a countdown? 00:39.920 --> 00:40.740 New set? 00:40.840 --> 00:41.720 Alright! 00:42.800 --> 00:44.260 The stage is mine. 00:44.800 --> 00:45.380 Psych! 00:45.380 --> 00:46.820 I'm not talking about program analysis. 00:46.820 --> 00:49.180 We're gonna look at cats all day. 00:49.660 --> 01:08.960 But in all seriousness, when I saw that it was the 25th anniversary of DEF CON, I had this thought because just the week before I read the CFP, I was reading some paper about program analysis that was published in the 90s. 01:08.960 --> 01:15.820 And I was thinking that, you know, wow, these guys had like a lot of the same ideas that we're having now. 01:15.840 --> 01:18.220 And they were talking about this in the 90s. 01:18.220 --> 01:23.740 I wonder how much other such history has kind of fallen by the wayside. 01:24.900 --> 01:35.000 And so I started looking a little bit, digging through, and I wrote this proposal for the CFP to kind of go through the last 25 years of program analysis. 01:35.300 --> 01:41.020 And then when I was putting together the slides, I realized that program analysis goes way farther back. 01:41.020 --> 01:48.160 So where does, you know, the 25 years number come from? 01:48.660 --> 01:50.960 And I thought about some more. 01:50.960 --> 01:54.480 I realized that 25 years is actually my involvement with program analysis. 01:54.480 --> 02:07.560 25 years ago, my grandma gifted me a book called Professor Fortran's Encyclopedia, which had like a cat named X and a professor named Fortran and a caterpillar named Caterpillar. 02:08.360 --> 02:14.220 And it went through their adventures in computer land and taught kids all about computer. 02:14.220 --> 02:15.700 I was crazy about this book. 02:15.700 --> 02:20.440 I ditched classes in first grade to hide in the stairwell and reread this book over and over. 02:20.440 --> 02:23.220 And I learned basic from it. 02:23.240 --> 02:28.300 And then later on, moved on to C and so forth. 02:28.300 --> 02:38.640 And I realized very early on that if I, you know, make a standard program that asks me for my name, and my name is too long, my last name, by the way, is Shorshutashvili. 02:38.820 --> 02:45.220 So I actually triggered bugs with this last name, then the program would crash. 02:46.320 --> 02:48.600 That turns out to be a buffer overflow and so forth. 02:48.600 --> 02:56.920 And then I started realizing that it's incredible to look at a computer program, try to understand how it really works. 02:56.920 --> 02:59.460 I mean, that's a whole different world in there, right? 02:59.460 --> 03:04.780 A world of ones and zeros and assembly instructions and logic gates. 03:04.980 --> 03:12.980 And somewhere along the line, it becomes alive and it starts behaving in ways that you don't quite understand ahead of time. 03:13.900 --> 03:18.760 And that's manual program analysis, understanding how this works. 03:18.760 --> 03:22.920 But then you can take that and make it automated. 03:22.920 --> 03:27.740 You can create programs that can understand programs. 03:27.740 --> 03:31.300 And it's like a whole level of craziness. 03:31.300 --> 03:35.360 That's like creating some sort of intelligence almost. 03:35.360 --> 03:37.240 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:48.820 And so this talk is about, you know, the history of program analysis. 03:48.920 --> 03:58.760 And it's about, you know, why we want to do program analysis in terms of kind of the dry things like we want to, you know, hack programs, we want to make sure programs are safe. 03:58.940 --> 04:14.380 But try to approach this topic from the sort of kid's perspective of discovering a whole new world of how programs work, and how programs might understand other programs. 04:14.460 --> 04:19.920 Program analysis is useful, but it's also kind of magical in a way. 04:19.920 --> 04:25.840 So with that said, let's move on to technical issues. 04:27.180 --> 04:28.300 Hmm. 04:28.480 --> 04:29.540 Hold on. 04:29.580 --> 04:30.640 Boom. 04:31.080 --> 04:32.200 Success. 04:32.240 --> 04:34.120 Let's move on to program analysis. 04:36.320 --> 04:44.080 Program analysis is a field that has basically three parts to it, right? 04:44.080 --> 04:50.640 You want to analyze a program, but you always want to analyze a program to figure something out about it. 04:50.640 --> 04:56.080 So for example, you might want to make sure that a certain specification of the program holds. 04:56.080 --> 05:08.580 The program doesn't crash, the program doesn't allow random people to unlock your smart key for your house, the program doesn't allow, you know, for your brakes to be remotely controlled, and so on. 05:09.440 --> 05:15.240 And you have a goal that you want to achieve with that specification. 05:15.240 --> 05:26.140 So for example, if your specification is, hey, I don't want this to crash, you could say, I want to make sure that that specification holds always. 05:26.380 --> 05:30.740 Or you might want to say, I want to make sure that that specification does not hold. 05:30.740 --> 05:32.000 I want to find the crash, right? 05:32.000 --> 05:34.420 So kind of, are you looking for bugs? 05:34.420 --> 05:36.220 Are you trying to make sure things are safe? 05:36.400 --> 05:41.180 And then, of course, once you decide what you want to do, you need to decide how you want to do it. 05:41.180 --> 05:48.360 What is the technique that you're going to use to reason about a specification on your program? 05:49.900 --> 06:07.960 And with these three kind of categories in mind, I'm going to run you through the history of program analysis and where along the line you collected different items, kind of different instances of these three categories. 06:08.320 --> 06:17.420 And so we're going to commence on a brief history of computing, starting in the 1830s with Charles Babbage. 06:18.000 --> 06:20.540 Charles Babbage created the analytical engine. 06:20.540 --> 06:24.940 It was a mechanical computer, super far ahead of its time. 06:24.940 --> 06:27.300 And he wrote a bunch of programs for it. 06:27.500 --> 06:30.980 By all accounts, these programs were actually really buggy. 06:30.980 --> 06:32.260 So that's really interesting. 06:32.260 --> 06:35.340 Some of the first computer programs written were already buggy. 06:35.340 --> 06:36.400 We didn't have that term yet. 06:36.400 --> 06:37.900 I'll talk about that later. 06:37.980 --> 06:54.800 And about a decade later, Ada Lovelace published a series of notes and more reasoning about this analytical engine, including the first complex program for one of these machines. 06:54.800 --> 07:03.740 So this is Ada Lovelace's description of the execution trace of this program. 07:03.740 --> 07:06.760 And the program computed Bernoulli numbers. 07:06.760 --> 07:13.520 And so she goes through instruction by instruction and says how variables change, and so forth. 07:13.520 --> 07:17.200 And this is in the 1840s, right? 07:18.340 --> 07:21.380 And so that's where things started. 07:21.380 --> 07:30.440 In 1947, about 105 years later, we got the term bug. 07:30.440 --> 07:38.020 Grace Hopper found, or people working with her, a actual moth inside a computer causing a computer error. 07:38.060 --> 07:50.840 So 100 years roughly after the first instance of kind of a computer in the semi-modern era, we have kind of this official term for the word bug. 07:51.260 --> 08:00.260 And this very quickly started getting people thinking about how do we kind of prevent actual software bugs. 08:00.260 --> 08:02.820 The moth, I guess, technically was kind of a wetware bug. 08:03.620 --> 08:06.440 But how do we prevent bugs in our software? 08:06.440 --> 08:20.660 And one of the kind of early visionaries here was Alan Turing, who's known for, of course, the Turing machine, but also cracking Enigma and onwards and onwards. 08:20.740 --> 08:32.340 But he also had the first paper that I could find that talked about, maybe we should try to make sure that the program is correct. 08:33.920 --> 08:36.440 And he published this in 1949. 08:36.440 --> 08:47.020 So two years after the kind of invention of the term bug, people start thinking about how do we make sure that there are no bugs in a program. 08:47.020 --> 08:50.320 And this creates the field of program verification. 08:50.360 --> 09:08.140 So program verification says, hey, given a program and the specification, we want to make sure that there are no bugs in this program, that this program carries out the computation needs to carry out and so forth, and doesn't go astray. 09:09.880 --> 09:18.980 So as an example, here's a simple program that has a crash, but that crash is not reachable, right? 09:18.980 --> 09:32.580 So if you give this program the somehow three numbers that add up, where a plus b equals c, but then c minus b is not equal to a, it'll crash. 09:32.580 --> 09:35.280 And you want to see if this program is safe. 09:35.280 --> 09:51.880 You can run a program verification on it, which will identify, you know, hopefully that this condition can never hold, and will produce a proof that tells you that the program is safe according to your specification. 09:52.680 --> 09:53.960 So that's great. 09:53.960 --> 09:59.240 And if everything worked like that in the real world, then we might not have bugs. 09:59.240 --> 10:03.620 And in certain cases, it does work like this in the real world. 10:03.620 --> 10:07.700 So there is formally verified hardware, according to a specific specification, of course. 10:07.700 --> 10:17.960 So things that the specification doesn't reason about, you know, maybe still can go wrong with that hardware, but things that are covered by the specification don't. 10:17.960 --> 10:26.860 So there's, you know, hardware that can provably not contain kind of timing side channel attacks, for example. 10:26.860 --> 10:29.080 And there's verified software. 10:29.340 --> 10:35.960 I heard recently that Google, for example, is switching over to a formally verified crypto system. 10:36.720 --> 10:48.480 And so the problems, of course, come when the software kind of gets bigger and complexity starts getting introduced, and verification stops being able to reason about things very effectively. 10:48.480 --> 10:52.740 So for example, here we have a different type of program, right? 10:52.740 --> 10:56.020 And this program also doesn't crash. 10:56.140 --> 11:02.080 That A cubed plus B cubed equals C cubed, that's Fermat's last theorem, right? 11:02.080 --> 11:03.700 That is not solvable. 11:03.700 --> 11:05.080 There's no solution. 11:05.480 --> 11:10.460 But it took humans hundreds of years to figure this out. 11:10.540 --> 11:19.040 And the computer, you know, verification tools, unless they're special coded for this, will also be unable to handle it. 11:19.040 --> 11:29.640 So it will kind of see this condition, it'll say, okay, well, if this condition is true, then the program will crash. 11:29.640 --> 11:31.960 Can I prove that the condition is always false? 11:31.960 --> 11:42.120 And if it can't prove that the condition is always false, it has no choice but to alert that the program cannot be verified. 11:42.820 --> 11:46.140 So what happens then, right? 11:46.140 --> 11:53.680 So then you have to go in and you have to start looking at the program manually and finding bugs. 11:53.680 --> 12:03.220 And if anyone's used kind of commercially available static analysis tools, you're very well familiar with the false positive problem, right? 12:03.220 --> 12:09.920 You open up a binary or a piece of software and the tool pops up alerts all over the place. 12:09.920 --> 12:12.460 And some of those are actual bugs. 12:12.460 --> 12:16.440 But you spend a lot of time chasing down the alerts. 12:16.580 --> 12:29.260 So when we look at, you know, software, open source software, for example, we often see, you know, a security check done twice, the same check. 12:29.320 --> 12:33.420 If A is not null, if A is not null. 12:33.420 --> 12:35.000 Why is that check there twice? 12:35.000 --> 12:47.480 Because for whatever reason, a program verification tool alerted that there could be a bug there and the programmer figured out some hack to make it shut up. 12:49.680 --> 12:58.500 So program verification, while it's a very useful field, like I said, there is verified software and hardware out there. 12:59.060 --> 13:03.440 It's not kind of the final answer on its own. 13:03.440 --> 13:06.780 So we also at some point need to have kind of the flip side. 13:06.780 --> 13:09.520 So program verification can say that is safe. 13:09.600 --> 13:13.460 But, you know, after that it says, okay, I can't really reason about it. 13:13.460 --> 13:17.580 So the flip side is you have a technique that says that is not safe. 13:17.580 --> 13:18.840 I can prove it. 13:18.840 --> 13:21.260 But I can't really prove, you know, if it is safe. 13:21.260 --> 13:24.360 But if it is not safe, I'll give you a counterexample. 13:24.860 --> 13:31.300 And the way this works is by, you know, finding counterexamples to whatever technique. 13:32.200 --> 13:48.640 So in this case, with a slightly different condition, that is A squared plus B squared equals C squared, a technique might find A, B, and C of three, four, and five as a counterexample that will reproduce a crash. 13:49.320 --> 13:58.620 And so this is, there are many techniques that, you know, we'll mention later that can be used to do program testing. 13:58.620 --> 14:14.980 But one of the very early ones, the first instance of program testing of this style that I found was in the 1950s, which is about four decades before I thought that this kind of idea was created. 14:15.560 --> 14:20.040 Programmers in the 1950s would program in punch cards. 14:20.040 --> 14:28.980 And to test their code, it was common practice to dig punch cards out of the trash and feed them as input to your program. 14:28.980 --> 14:32.680 This is unexpected input, just random stuff. 14:32.680 --> 14:36.460 And of course, by random stuff, program shouldn't crash. 14:36.460 --> 14:51.400 So this is kind of an early example of this sort of kind of institutionalized testing that we're, you know, only seeing come back recently. 14:52.200 --> 15:02.720 And so, you know, these early developments, verification, testing, the creation of those two ideas, and then the idea of what you might check for. 15:02.720 --> 15:07.600 So the, you know, trash decks check for crashes. 15:07.960 --> 15:11.520 Turing reasoned about ensuring logical properties. 15:11.740 --> 15:13.020 But this is all done manually. 15:13.020 --> 15:18.180 So this is kind of our first set of tools in our tool bag, and they're manual tools. 15:18.180 --> 15:19.200 We have to dig them out. 15:19.200 --> 15:22.780 Okay, let's get our trash, you know, cards. 15:22.780 --> 15:30.180 This one got eaten by something and, you know, put in the ones that won't jam your machine and try them. 15:30.600 --> 15:32.460 But none of this was automated. 15:32.460 --> 15:41.060 And so as computers became more and more ubiquitous, the need for automation started showing itself. 15:41.460 --> 15:53.880 So again, we come on a mention of Grace Hopper here, because she not only found the first bug, but she also invented the compiler. 15:54.300 --> 16:03.580 So Grace Hopper in 1952 published a paper saying, hey, what if we wrote in kind of higher level languages and it got, you know, squished down to computer code. 16:04.920 --> 16:09.340 And this took a little while to catch on. 16:09.340 --> 16:17.880 And the reason it took a while to catch 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:35.600 And so this identified another need, another goal of program analysis, transformation of binaries into something different, something faster in this case. 16:35.680 --> 16:43.640 And in the modern era, you know, 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:58.040 And so now we needed to optimize code because, you know, people write slow code when they're writing source for whatever reason. 16:59.640 --> 17:11.440 And another thing happened, people started realizing that we have all of these architectures with all of this data flowing around in them. 17:11.440 --> 17:22.720 And if you're not very, very, very careful, some data could be read from or written to a different location than intended, and the memory could be corrupted. 17:22.720 --> 17:30.840 So I just played, you know, two days of a CTF full of these errors, of course, memory corruption bugs. 17:31.780 --> 17:36.620 And this was first described in 1968. 17:36.620 --> 17:51.740 In 1968, there was a paper saying, hey, you know, we noticed that if the kernel, they called it a monitor at the time, blindly trusts everything that, you know, the user space sends it, bad things can start to happen. 17:52.020 --> 17:54.260 And so this paper introduced that concept. 17:54.260 --> 18:06.940 It's also the paper that, you know, one of the early works in memory protection and virtual memory and so forth, which is pretty interesting that immediately they realized this was a problem. 18:07.080 --> 18:19.060 And a little while later, there was, you know, Ken Thompson's reflecting on trusting trust, where he reasoned that you could build in a backdoor into a compiler that could build in backdoors into sensitive code. 18:19.060 --> 18:34.690 And so suddenly, we have two more things that we need to worry about in terms of specifications, or even more, but, you know, including memory safety, information disclosure, and authentication, right? 18:34.690 --> 18:39.810 So now you might want to verify that a program doesn't have a backdoor. 18:40.810 --> 18:46.550 Or you might verify that a program will not leak your sensitive private information. 18:46.550 --> 18:55.410 That is, that one is very relevant today with all of our phones having all of our information and very little control over it. 18:55.970 --> 19:06.190 And so the need for automation was pretty well established by the kind of turn of the century, for sure. 19:06.650 --> 19:14.730 But even before that, those papers were like in the 1960s or something, late 1960s. 19:14.730 --> 19:21.810 And very quickly, oops, sorry, very quickly, people started to meet this need. 19:21.810 --> 19:25.110 The research community started pumping out automated approaches. 19:25.110 --> 19:28.670 And so I'm going to introduce a couple of these automated approaches. 19:30.610 --> 19:39.370 And before I do so, I want to make you guys experts in program analysis, so that we can reason about what's going on here. 19:39.370 --> 19:44.330 So we'll talk about a couple of prerequisites, right? 19:44.330 --> 19:47.970 So let's say you have a program. 19:48.050 --> 19:55.450 So on the top right, there's like a little Python program that's already a vulnerable program, by the way. 19:57.110 --> 20:01.330 And so you have this program, and you want to analyze it. 20:01.330 --> 20:05.970 So you have to reason about a program in a slightly different way as a computer than as a human. 20:05.970 --> 20:11.390 So for example, a program is viewed by a computer as a set of basic blocks. 20:11.390 --> 20:19.370 A basic block is a piece of code that is executed all together before passing on control flow somewhere else. 20:19.370 --> 20:24.530 So in our case, we'll pretend that input is part of this basic block. 20:24.530 --> 20:30.470 So this X equals input is a single basic block, and then it might branch depending on the input, right? 20:30.470 --> 20:33.390 So if you put in 42, it'll do one thing. 20:33.390 --> 20:37.010 If you put in something else, it'll do another. 20:37.010 --> 20:45.050 And so this is the end of the basic block, and then the result of that if statement is two other basic blocks, the true case and the false case. 20:45.290 --> 20:51.770 And each of these has a constraint that has to be met, right? 20:51.770 --> 20:55.650 In order to go down one path, you have to put in 42. 20:55.650 --> 20:58.590 In order to go down another, you have to put in not 42. 20:58.590 --> 21:00.230 And so these are called constraints. 21:00.350 --> 21:11.330 If you then look at all of the basic blocks of a program, this is called a control flow graph because that's, you know, these are basic blocks and control flows between them. 21:11.730 --> 21:24.030 And if you look at a path down this graph, now in this case the graph is nice and simple, but in reality it could have loops, a path might hit the same node multiple times, and so on. 21:24.430 --> 21:29.110 And then you look at the constraints all along this path. 21:29.110 --> 21:34.010 These are the path predicates that uniquely identify this path. 21:34.010 --> 21:50.810 So if you collect all of these constraints and you say that x is not 42 but x is 1337, that input will... any input that matches those constraints will take the same path through the program. 21:51.830 --> 21:56.770 So these are kind of the prerequisites of our program analysis techniques. 21:56.770 --> 21:58.890 So now we'll go through three of them. 21:58.890 --> 22:02.310 Actually for time reasons we'll go through two of them and mention a third. 22:02.310 --> 22:05.170 But we'll start with symbolic execution. 22:05.410 --> 22:19.590 And symbolic execution got a lot of hype recently, especially with stuff like the cyber grant challenge and so on, as a way for machines to reason about program code. 22:20.030 --> 22:24.390 And you think that this is something new, but it turns out that it's not. 22:24.390 --> 22:26.790 It's quite old actually. 22:26.790 --> 22:33.890 So 40 years ago, a little bit more, the first symbolic execution paper that I could find was proposed. 22:35.290 --> 22:38.930 And there were several actually, right in one year basically. 22:38.930 --> 22:44.070 So this idea had some prerequisites that were met and then it exploded. 22:44.330 --> 22:51.690 And so the symbolic execution engines were developed that could then symbolically execute Fortran code. 22:51.690 --> 23:00.970 Now we have symbolic execution engines that you can download off GitHub that can execute binaries, Java, Android, whatever you want. 23:02.570 --> 23:08.530 And this is kind of a fairly powerful way of reasoning about programs. 23:08.530 --> 23:19.530 And let's run through an introduction of it with a slightly more complicated example than what we learned about program analysis with. 23:20.970 --> 23:22.450 Hold on. 23:23.350 --> 23:27.510 So here's a program that has several bugs, right? 23:27.910 --> 23:40.590 One is it, well, it definitely has one bug and that is if you enter a username of service and a command code of seven, it'll crash, right? 23:40.830 --> 23:46.190 You can imagine that instead of this crash, it does some system relevant stuff. 23:46.190 --> 23:51.910 So it could be a backdoor instant memory 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.830 So first let's look at the control flow graph of this program, starting from the beginning. 24:02.830 --> 24:08.570 Again, the control flow graph is made up of basic blocks and the control flow transitions between them. 24:08.570 --> 24:10.870 So we start at this input. 24:11.130 --> 24:13.830 If the input is service, it branches. 24:13.830 --> 24:25.070 If the username is service, it branches into one side of the equation of the program where it checks for the command code being seven. 24:25.170 --> 24:26.750 And if it is, it crashes. 24:26.750 --> 24:30.950 If not, it prints an on command and then it exits. 24:31.750 --> 24:37.690 On the other side of the branch, it asks for a passcode. 24:37.690 --> 24:42.010 If the passcode is invalid, it prints invalid passcode. 24:42.010 --> 24:46.470 Otherwise, it calls the authentication function, then it prints exit and exits. 24:46.470 --> 24:48.670 So this is our control flow graph. 24:48.670 --> 24:56.350 And how would we use symbolic execution to try to find that crash, try to find the ability to reach this crash? 24:56.350 --> 25:02.810 So we would start executing the program in an emulator. 25:02.890 --> 25:10.670 And in this emulator, instead of ones and zeros, we are working on X, Y, and other symbols. 25:10.750 --> 25:15.550 So, for example, username is a symbol in this emulator. 25:15.550 --> 25:22.530 So when we pull in an input, it will produce an unconstrained variable called username. 25:22.530 --> 25:23.650 And we don't know what username is. 25:23.650 --> 25:25.110 Username can be anything. 25:25.790 --> 25:30.690 Because, you know, that is how we implement our emulator. 25:31.450 --> 25:38.850 And as we check for values of username, we create what are called constraints, right? 25:38.850 --> 25:46.690 So these are the exact constraints that the basic block checks when it pushes execution forward. 25:47.190 --> 25:49.270 And we collect two constraints in this case. 25:49.270 --> 25:51.870 On the one side, username equals service. 25:51.870 --> 25:53.350 On the other side, it does not equal service. 25:53.350 --> 25:54.190 These are constraints. 25:54.190 --> 26:00.810 And we continue executing both sides of this statement with symbolic execution. 26:01.530 --> 26:06.690 But then we hit something that is very bad for symbolic execution. 26:06.690 --> 26:10.030 We hit, for example, string processing functions. 26:10.030 --> 26:17.990 So a string processing function like A2I might check a given byte, see if it is a number. 26:17.990 --> 26:19.990 If it is a number, it'll do one thing. 26:19.990 --> 26:22.590 If it's not, it'll do another, right? 26:22.590 --> 26:24.850 Or if it's a certain number, it might do one. 26:24.850 --> 26:27.190 If it's not a certain number, it'll do another. 26:27.190 --> 26:31.950 So it'll keep branching the symbolic emulator at every... 26:33.810 --> 26:34.950 I'm sorry? 26:35.790 --> 26:37.230 Oh, awesome. 26:37.330 --> 26:51.130 It'll keep branching the symbolic emulator at every if statement, every check on this number until we get into a situation where there are just too many checks, right? 26:51.130 --> 27:02.290 So it'll try to check for a command code of, you know, 10 bytes with arbitrary values of 9 bytes and so on. 27:02.290 --> 27:05.550 And there's an exponential path explosion here. 27:06.290 --> 27:13.350 And there are some approaches in the symbolic execution world to try to deal with this sort of path explosion. 27:13.350 --> 27:19.150 But in general, these approaches boil down to the requirement to remove paths, right? 27:19.150 --> 27:20.590 And lose this information. 27:20.590 --> 27:30.770 And so in the end, the symbolic execution engine might only find certain paths and not others and miss the bug. 27:30.770 --> 27:34.870 Because we have to simplify to keep things tractable. 27:35.090 --> 27:37.030 So that's symbolic execution. 27:37.030 --> 27:49.930 It might find the bug if you're lucky, but if you're not, and it has to simplify its state space essentially as it's executing, there are certain things that it might miss. 27:50.650 --> 27:55.630 Symbolic execution was proposed as you saw in 1975. 27:55.870 --> 28:11.590 But the interesting thing is that in Ada Lovelace's notes from 1942, we can see that she did a symbolic trace of the execution of her program. 28:11.590 --> 28:26.410 So where she has this sort of program execution log in her notes, she writes down the symbol, the equation for each variable as the program progresses. 28:26.410 --> 28:33.030 And this is the first symbolic trace of a program, done in 1842 before computers were invented. 28:33.210 --> 28:36.890 So that was a pretty interesting thing to find. 28:37.310 --> 28:45.250 And kind of a nice point of history that we can put as the start of program analysis in this sense. 28:45.730 --> 28:54.890 1842, not 1975 or 1949 or any of those much, much later dates. 28:54.890 --> 29:10.910 And so symbolic execution is a kind of tool in our tool set that we can use to achieve either verification of a specification, the testing of a specification , or to support the transformation of code. 29:11.110 --> 29:22.570 Of course, how you verify a program, for example , using symbolic execution is a pretty complex thing with the symbolic execution style that I described for program testing. 29:22.570 --> 29:27.330 It generates inputs to find vulnerabilities, but it can't prove that there aren't any. 29:28.930 --> 29:39.970 But that's kind of a, we could go down that route for an entire semester course, and not just a 45 minute introductory talk. 29:39.970 --> 29:43.470 So I'll leave that as future research for you guys. 29:43.470 --> 30:02.350 And we'll go on to static analysis, because static analysis can show that, for example, a program is immune to a certain class of vulnerabilities or properly implements a certain specification. 30:02.670 --> 30:15.950 Static analysis, or at least one of the very common ways to do static analysis, 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:49.630 It doesn't have to figure out how to reach a certain basic block to reason about properties of the program at that basic block, which is the problem that symbolic execution had, and the reason that symbolic execution could not find the bug in our example. 30:49.650 --> 31:03.590 And so static analysis with abstract interpretation might be able to find that bug, probably will be able to find that bug if it is a simple bug, or actually, I should say, will be able to find that bug. 31:04.190 --> 31:09.630 Because if it cannot prove that a piece of code is safe, it will raise an alert. 31:09.630 --> 31:13.590 The problem is that, as we talked about, there are false positives. 31:13.590 --> 31:25.350 So in our program, it might think that that function has a bug, even if 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:38.050 And so through abstract interpretation, we got a way to perform verification or specification on a program in 1977, 40 years ago. 31:38.050 --> 31:41.250 And then we moved on to fuzzing. 31:41.250 --> 31:49.390 And so fuzzing is kind of one of the biggest ways to find vulnerabilities in modern software. 31:49.390 --> 31:52.110 And it's actually surprisingly simple. 31:52.130 --> 32:01.230 Proposed in 1981, initially, in its most basic form, which was, hey, let's throw random input at a program and see if it crashes. 32:01.230 --> 32:03.650 It's evolved quite a bit since then. 32:03.650 --> 32:13.550 And so the specific implementation of fuzzing that I'll describe here is implemented by American Fuzzy Lab. 32:13.830 --> 32:20.250 It's a fuzzer that mutates its inputs when it detects differences in program execution. 32:20.970 --> 32:25.190 And so let's see how it would run on our program here. 32:25.270 --> 32:31.730 We'll start with some randomly generated test case or human-seeded test case. 32:31.730 --> 32:37.390 So a human might input a username of ASDF and a password of 111. 32:37.390 --> 32:44.350 And that input will trigger certain basic blocks to be executed, right? 32:44.350 --> 32:47.890 And so we executed the username input, of course. 32:47.890 --> 32:55.010 We executed the check for the kind of service username that could lead to the crash. 32:55.010 --> 33:06.290 We did not satisfy it, so we took the else branch, read in the passcode, and errored out on an invalid passcode and exited. 33:06.290 --> 33:08.170 So we triggered those basic blocks. 33:08.170 --> 33:12.330 And so the fuzzer starts mutating this input, right? 33:12.330 --> 33:15.890 It might make a capital D or something. 33:15.970 --> 33:25.670 Or it might mutate input in a way that passes another check. 33:25.670 --> 33:31.470 So it mutated the input in a way that passes that passcode check. 33:31.470 --> 33:36.310 It actually doesn't, because there's another bug in the program that I didn't notice before. 33:36.310 --> 33:49.350 But let's pretend that it creates a valid size of a passcode and triggers that authentication function, right? 33:49.350 --> 33:51.710 So that is a new basic block that it triggers. 33:51.710 --> 34:04.110 Now with fuzzing, we've triggered a block that symbolic execution before us wasn't able to trigger just through randomly mutating inputs. 34:04.110 --> 34:06.070 But then we get stuck. 34:06.070 --> 34:13.610 Because through randomly mutating inputs, we are unable to satisfy complex checks, right? 34:13.610 --> 34:19.430 We need a username of service, and we have randomly mutated usernames. 34:19.430 --> 34:25.590 The chances are that we'll create the string service are very slim, and we'll keep guessing and guessing and guessing. 34:25.590 --> 34:40.350 Of course, in this specific case, you could seed the fuzzer with the string service, and you could scan the program for all of its strings and automatically make the fuzzer pass this check. 34:40.350 --> 34:44.850 But string checks aren't the only complex checks in programs. 34:44.850 --> 34:53.850 There are hashes, there are complex input formats, dependencies between different input bytes. 34:53.850 --> 35:05.290 And so in the general case, we cannot guarantee, of course, with a fuzzer that we will find code that is protected by these complex checks. 35:07.110 --> 35:16.790 And so fuzzing with this random data, of course, is a throwback to this trash deck concept. 35:16.790 --> 35:22.550 So fuzzing was invented in 1950, not 1981. 35:23.690 --> 35:26.750 Or at least manual fuzzing. 35:26.750 --> 35:37.950 So again, we find that program analysis techniques harken back to the middle of the century, and sometimes even farther to the 1800s. 35:37.950 --> 35:52.790 So now we have this kind of toolbox of a bunch of specifications that we can enforce, some goals that our analysis could try to achieve, and the technique through which we can achieve them. 35:53.110 --> 35:59.490 And next, we should evaluate them, understand how these different 36:03.410 --> 36:09.210 goals or how these different techniques help us achieve program analysis goals. 36:09.350 --> 36:26.030 And as a scientist, if you start thinking up an approach, and you have a cool idea, have a new program analysis technique, you want to evaluate it. 36:26.030 --> 36:32.990 So you want to take programs and specifications, feed them into your technique, and see how well it does. 36:32.990 --> 36:36.210 This is my clipart slide, by the way. 36:36.210 --> 36:38.690 So hopefully my clipart game is on point. 36:39.950 --> 36:44.990 So you run your analysis, you get your results, and you're happy, right? 36:44.990 --> 36:47.910 Well, there are a number of problems with this. 36:47.910 --> 36:58.630 One is that the analysis is more complex than you might think, because any program analysis has to deal with the environment of the program it's analyzing. 36:58.630 --> 37:11.250 And environments like Windows, macOS, Linux, mobile devices, cyber-physical devices, they have really complex environments. 37:11.730 --> 37:33.750 Having to model this environment, even before understanding how much better your program analysis technique is than previous techniques, is quite a big investment that people often don't make, or make in a very fast manner. 37:33.750 --> 37:38.470 Another problem is finding a good data set to evaluate on, right? 37:38.470 --> 37:44.070 There's not really a good data set for... or there wasn't a great data set for vulnerability research. 37:44.070 --> 37:49.090 This problem is actually being worked on, and new data sets are being created, as I'll talk about. 37:49.090 --> 38:13.210 But you need a good data set with ideally known vulnerabilities, so you can reason about how many of them your bug finds, and with variable vulnerabilities in different programs, so your technique isn't just specifically tailored for one style of vulnerability that you happen to detect, 38:13.210 --> 38:17.110 or one specific program that you happen to be very good at analyzing. 38:17.370 --> 38:19.910 Another problem is these specifications. 38:19.910 --> 38:35.950 Specifications in the real world are very complex, whereas specifications that you might want to use for your analysis tool initially in the early stages of development need to be fairly simple and ideally pre-provided. 38:35.950 --> 38:52.450 I mean, if you're looking at analyzing something like Chrome, and your specification is that Chrome should not leak user data to someone that should not get this user data, that's impossibly broad and impossible to enforce. 38:52.450 --> 39:00.110 Is your bank allowed to have your various cookies or something along these lines? 39:01.530 --> 39:27.230 So you need a very good data set, standard data set, with a very good standard implementation, standard set of specifications, so that you can analyze how well your technique runs compared to different work, and compare those results to prior work, because that's a very important part of science and technical development, 39:27.230 --> 39:30.650 understanding if you're making an improvement or not. 39:32.250 --> 39:55.410 And so we had problems as an analysis community in meeting all of these goals, and having a good data set of applications, with a good set of specifications, on a good environment that wasn't too complex to implement, and that could produce results that we could reason about, 39:55.410 --> 40:18.130 that we could say, we have ground truth data for the vulnerabilities that are actually in this data set, and we detect x of them, or we manage to rule out vulnerabilities in code that has no vulnerabilities, and so our program verification is correct. 40:19.950 --> 40:33.170 And so, like I mentioned, there have been several projects to solve this problem, to create these data sets, and one of these projects essentially was the Cyber Grand Challenge. 40:33.170 --> 40:52.150 If you guys were here last year, you probably saw all of the Cyber Grand Challenge, you know, hoopla, where for the first time in history, seven fully automated program analysis machines fought each other in a game of capture the flag. 40:52.190 --> 41:05.750 So the same game that I spent the entire weekend playing and only got four hours of sleep is the game that machines who didn't need to sleep played yesterday, last year rather. 41:06.190 --> 41:30.950 And these machines, of course, suffered from all of the problems that I just talked about, the environment problem, the specification problem, and so the Cyber Grand Challenge created a custom operating system with very specific vulnerability specifications to evaluate these systems. 41:30.950 --> 41:50.030 Now, for the actual competition, of course, the source code wasn't available, since then they released the source code, so you can really look at the source code, understand the vulnerability, and then reason about how well your tool finds certain vulnerabilities across 249 binaries. 41:50.030 --> 42:13.970 So it's a 249 program, so it's a data set that has a lot of variants, there are a lot of different types and different difficulties of vulnerabilities, and all of this is freely available for people to analyze their tool and understand how well it does. 42:13.970 --> 42:16.270 That's my other piece of clip art. 42:17.590 --> 42:36.390 So the Cyber Grand Challenge and the programs that were written for this, these 249 programs making up the Cyber Grand Challenge data set, allowed us to do what I call, to perform what I call the program analysis nursery experiments. 42:36.390 --> 42:44.130 So I see the Cyber Grand Challenge data set as the nursery of program analysis, where you can reason about different improvements for different techniques. 42:44.190 --> 42:49.810 So for example, Symbolic Execution on the entire data set finds nine vulnerabilities. 42:49.810 --> 42:58.570 This Symbolic Execution has implemented in Anger, which I'll talk about in a sec, which is an open source binary analysis program available on GitHub. 42:58.910 --> 43:04.550 But Symbolic Execution on this entire data set finds nine vulnerabilities. 43:04.550 --> 43:06.150 That's not a lot, right? 43:06.150 --> 43:10.010 There are vulnerabilities in every program of these 249 programs. 43:10.010 --> 43:12.310 It only finds vulnerabilities in nine of them. 43:12.910 --> 43:16.650 Of course, we can optimize Symbolic Execution using various tricks. 43:16.650 --> 43:27.710 So Anger supports, for example, concrete execution when there is no uncertainty in the state, when all the data is known, or when there are constraints on all the data. 43:27.710 --> 43:38.450 And so by utilizing all of these optimizations, we can get 26 crashes, crashing 26 binaries. 43:38.950 --> 43:56.210 Utilizing static analysis, so combining Symbolic Execution with Veritesting, which is a technique created by Carnegie Mellon University that utilizes parts of abstract interpretation to help with Symbolic Execution, we can push that up to 31. 43:56.210 --> 44:02.350 So I should say here that this is our implementation of Veritesting, and it might be suboptimal. 44:02.370 --> 44:05.550 So their Veritesting might be considerably better. 44:05.970 --> 44:09.530 But that all pales in comparison with fuzzing. 44:09.530 --> 44:19.850 This seemingly simple technique of throwing random data and seeing what happens finds 106 crashing binaries in the data set. 44:20.330 --> 44:34.750 So this gives us an idea of where program analysis is, and this is a good showcase for the simplicity of evaluating all of these different analyses on this data set and reasoning about the results. 44:34.750 --> 44:40.070 Because now we can look at them in terms of, you know, summation numbers. 44:40.070 --> 44:42.130 But there's also some subtleties there. 44:42.130 --> 44:46.270 They find bugs, different types of bugs in different binaries. 44:46.270 --> 44:54.010 So we can look into that and make inferences and try to create new approaches. 44:54.010 --> 45:05.690 So for example, we looked at the difference in the types of bugs that symbolic execution found and that fuzzing found, and we realized that they have very different coverage. 45:05.690 --> 45:12.870 So the types of the basic blocks that fuzzing can trigger are very different from the basic blocks that symbolic execution can trigger. 45:12.870 --> 45:17.470 And sometimes one finds a crash, sometimes another finds a crash, sometimes neither of them find a crash. 45:17.470 --> 45:19.290 In fact, very frequently. 45:19.350 --> 45:28.750 And so we decided to combine them in a very straightforward but careful way. 45:28.830 --> 45:31.430 And the idea is as follows. 45:31.430 --> 45:33.150 We begin by fuzzing the binary. 45:33.150 --> 45:40.130 This is nice and fast and achieves decent code coverage, but as we discussed, eventually gets stuck on complex checks. 45:40.130 --> 45:52.450 And then we use symbolic execution to find the constraint that can get through that check, but possibly suffer from other limitations of symbolic execution and not find the actual bug. 45:52.530 --> 45:54.830 And then we synchronize that back into the fuzzer. 45:54.830 --> 46:05.990 We synchronize the knowledge of how to bypass the complex check back into the fuzzer, and it continues to mutate that input until it finds the bug. 46:06.530 --> 46:12.110 And we do this iteratively, back and forth between the fuzzer and symbolic execution. 46:12.230 --> 46:23.550 So by implementing symbolic assistance for the fuzzer in this way, we achieve on this entire dataset 118 crashes. 46:24.170 --> 46:42.670 And an interesting thing here is that we have this 118 crashes in the dataset, but if you take the union of all of the different techniques, all the different techniques have crashed something like this from memory, 150 to 160 binaries. 46:42.670 --> 46:49.010 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 --> 46:58.690 We can run through a quick run here. 46:58.690 --> 47:06.270 So this is a control flow graph of an example program, and driller starts in the top left corner there. 47:06.390 --> 47:14.750 And it first starts by fuzzing a portion of the program before it gets stuck in a complex check. 47:15.070 --> 47:19.370 And this is the basic block coverage on the right in this graph here. 47:19.370 --> 47:21.830 You can see just kind of flat lines, right? 47:21.830 --> 47:41.510 So then if we run the symbolic execution engine to help the fuzzer reach extra code paths, it allows us to find just a little tiny bit more basic blocks in the executor, some more basic blocks in that control flow graph of the program. 47:41.510 --> 47:55.750 And if we keep invoking the symbol execution engine to help the fuzzer get unstuck every time that the coverage flat lines like that, we eventually drill into the program deep enough to find the bug. 47:55.750 --> 47:57.990 And so that's how driller works. 47:58.030 --> 47:59.330 There's still a lot to do. 47:59.330 --> 48:20.750 So there's this whole red area that however many programs, about 100 programs that we have never exploited before, that we've never crashed before using any automated techniques, which represent missing tools basically that humanity has yet to develop, 48:20.750 --> 48:22.870 or at least we have yet to develop. 48:23.730 --> 48:27.990 And so if this all sounds interesting to you, I encourage you to join in. 48:27.990 --> 48:32.330 There are several ways that you can participate in program analysis research. 48:32.330 --> 48:34.730 One is you can contribute to open source frameworks. 48:34.730 --> 48:39.810 So we run one of these frameworks in our research lab. 48:39.810 --> 48:40.830 It's called anger. 48:40.830 --> 48:42.430 Go to anger.io. 48:42.430 --> 48:51.250 There's a lot that we could use help with documentation, environment support, better techniques, and so on. 48:51.250 --> 48:55.050 And the other is that I'm always looking for students. 48:55.050 --> 48:59.390 I'm starting as a professor at Arizona State University. 48:59.650 --> 49:12.930 I just finished a PhD at UC Santa Barbara, and both of those places are incredible places to go to if you want to do research in program analysis or in general security. 49:13.050 --> 49:22.170 So if you're thinking about graduate school, or you are curious and want to do an internship, reach out to me. 49:22.170 --> 49:27.630 I'll put you in touch with the right people, and you could explore that. 49:28.530 --> 49:31.110 The presentation is available online. 49:31.110 --> 49:35.270 All my contact info is right here, and I guess we'll questions in the hall? 49:35.890 --> 49:36.690 Awesome. 49:36.850 --> 49:37.590 Thank you, guys.