1
00:00:00,000 --> 00:00:08,100
Hopefully you guys will see this as a nice talk for setting the stage.

2
00:00:08,460 --> 00:00:14,740
The original idea was to have it as a very in-depth, very long two-panel talk.

3
00:00:14,740 --> 00:00:19,540
I think that was very optimistic.

4
00:00:19,960 --> 00:00:28,420
So this will be hopefully a cool talk in kind of the history and the uh, the field of program analysis.

5
00:00:28,420 --> 00:00:31,280
How we got where we got and where we came from.

6
00:00:32,940 --> 00:00:34,880
Let's see, we're almost there.

7
00:00:34,880 --> 00:00:35,780
Is it not?

8
00:00:36,160 --> 00:00:37,640
Can we have a countdown?

9
00:00:39,920 --> 00:00:40,740
New set?

10
00:00:40,840 --> 00:00:41,720
Alright!

11
00:00:42,800 --> 00:00:44,260
The stage is mine.

12
00:00:44,800 --> 00:00:45,380
Psych!

13
00:00:45,380 --> 00:00:46,820
I'm not talking about program analysis.

14
00:00:46,820 --> 00:00:49,180
We're gonna look at cats all day.

15
00:00:49,660 --> 00: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.

16
00:01:08,960 --> 00: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.

17
00:01:15,840 --> 00:01:18,220
And they were talking about this in the 90s.

18
00:01:18,220 --> 00:01:23,740
I wonder how much other such history has kind of fallen by the wayside.

19
00:01:24,900 --> 00: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.

20
00:01:35,300 --> 00:01:41,020
And then when I was putting together the slides, I realized that program analysis goes way farther back.

21
00:01:41,020 --> 00:01:48,160
So where does, you know, the 25 years number come from?

22
00:01:48,660 --> 00:01:50,960
And I thought about some more.

23
00:01:50,960 --> 00:01:54,480
I realized that 25 years is actually my involvement with program analysis.

24
00:01:54,480 --> 00: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.

25
00:02:08,360 --> 00:02:14,220
And it went through their adventures in computer land and taught kids all about computer.

26
00:02:14,220 --> 00:02:15,700
I was crazy about this book.

27
00:02:15,700 --> 00:02:20,440
I ditched classes in first grade to hide in the stairwell and reread this book over and over.

28
00:02:20,440 --> 00:02:23,220
And I learned basic from it.

29
00:02:23,240 --> 00:02:28,300
And then later on, moved on to C and so forth.

30
00:02:28,300 --> 00: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.

31
00:02:38,820 --> 00:02:45,220
So I actually triggered bugs with this last name, then the program would crash.

32
00:02:46,320 --> 00:02:48,600
That turns out to be a buffer overflow and so forth.

33
00:02:48,600 --> 00: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.

34
00:02:56,920 --> 00:02:59,460
I mean, that's a whole different world in there, right?

35
00:02:59,460 --> 00:03:04,780
A world of ones and zeros and assembly instructions and logic gates.

36
00:03:04,980 --> 00: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.

37
00:03:13,900 --> 00:03:18,760
And that's manual program analysis, understanding how this works.

38
00:03:18,760 --> 00:03:22,920
But then you can take that and make it automated.

39
00:03:22,920 --> 00:03:27,740
You can create programs that can understand programs.

40
00:03:27,740 --> 00:03:31,300
And it's like a whole level of craziness.

41
00:03:31,300 --> 00:03:35,360
That's like creating some sort of intelligence almost.

42
00:03:35,360 --> 00:03:37,240
And that's what fascinates me about program analysis.

43
00:03:37,240 --> 00:03:41,960
That's what's kept me going down the path I've been going for the last 25 years.

44
00:03:42,300 --> 00:03:48,820
And so this talk is about, you know, the history of program analysis.

45
00:03:48,920 --> 00: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.

46
00:03:58,940 --> 00: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.

47
00:04:14,460 --> 00:04:19,920
Program analysis is useful, but it's also kind of magical in a way.

48
00:04:19,920 --> 00:04:25,840
So with that said, let's move on to technical issues.

49
00:04:27,180 --> 00:04:28,300
Hmm.

50
00:04:28,480 --> 00:04:29,540
Hold on.

51
00:04:29,580 --> 00:04:30,640
Boom.

52
00:04:31,080 --> 00:04:32,200
Success.

53
00:04:32,240 --> 00:04:34,120
Let's move on to program analysis.

54
00:04:36,320 --> 00:04:44,080
Program analysis is a field that has basically three parts to it, right?

55
00:04:44,080 --> 00:04:50,640
You want to analyze a program, but you always want to analyze a program to figure something out about it.

56
00:04:50,640 --> 00:04:56,080
So for example, you might want to make sure that a certain specification of the program holds.

57
00:04:56,080 --> 00: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.

58
00:05:09,440 --> 00:05:15,240
And you have a goal that you want to achieve with that specification.

59
00:05:15,240 --> 00: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.

60
00:05:26,380 --> 00:05:30,740
Or you might want to say, I want to make sure that that specification does not hold.

61
00:05:30,740 --> 00:05:32,000
I want to find the crash, right?

62
00:05:32,000 --> 00:05:34,420
So kind of, are you looking for bugs?

63
00:05:34,420 --> 00:05:36,220
Are you trying to make sure things are safe?

64
00:05:36,400 --> 00: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.

65
00:05:41,180 --> 00:05:48,360
What is the technique that you're going to use to reason about a specification on your program?

66
00:05:49,900 --> 00: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.

67
00:06:08,320 --> 00:06:17,420
And so we're going to commence on a brief history of computing, starting in the 1830s with Charles Babbage.

68
00:06:18,000 --> 00:06:20,540
Charles Babbage created the analytical engine.

69
00:06:20,540 --> 00:06:24,940
It was a mechanical computer, super far ahead of its time.

70
00:06:24,940 --> 00:06:27,300
And he wrote a bunch of programs for it.

71
00:06:27,500 --> 00:06:30,980
By all accounts, these programs were actually really buggy.

72
00:06:30,980 --> 00:06:32,260
So that's really interesting.

73
00:06:32,260 --> 00:06:35,340
Some of the first computer programs written were already buggy.

74
00:06:35,340 --> 00:06:36,400
We didn't have that term yet.

75
00:06:36,400 --> 00:06:37,900
I'll talk about that later.

76
00:06:37,980 --> 00: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.

77
00:06:54,800 --> 00:07:03,740
So this is Ada Lovelace's description of the execution trace of this program.

78
00:07:03,740 --> 00:07:06,760
And the program computed Bernoulli numbers.

79
00:07:06,760 --> 00:07:13,520
And so she goes through instruction by instruction and says how variables change, and so forth.

80
00:07:13,520 --> 00:07:17,200
And this is in the 1840s, right?

81
00:07:18,340 --> 00:07:21,380
And so that's where things started.

82
00:07:21,380 --> 00:07:30,440
In 1947, about 105 years later, we got the term bug.

83
00:07:30,440 --> 00:07:38,020
Grace Hopper found, or people working with her, a actual moth inside a computer causing a computer error.

84
00:07:38,060 --> 00: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.

85
00:07:51,260 --> 00:08:00,260
And this very quickly started getting people thinking about how do we kind of prevent actual software bugs.

86
00:08:00,260 --> 00:08:02,820
The moth, I guess, technically was kind of a wetware bug.

87
00:08:03,620 --> 00:08:06,440
But how do we prevent bugs in our software?

88
00:08:06,440 --> 00: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.

89
00:08:20,740 --> 00: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.

90
00:08:33,920 --> 00:08:36,440
And he published this in 1949.

91
00:08:36,440 --> 00: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.

92
00:08:47,020 --> 00:08:50,320
And this creates the field of program verification.

93
00:08:50,360 --> 00: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.

94
00:09:09,880 --> 00:09:18,980
So as an example, here's a simple program that has a crash, but that crash is not reachable, right?

95
00:09:18,980 --> 00: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.

96
00:09:32,580 --> 00:09:35,280
And you want to see if this program is safe.

97
00:09:35,280 --> 00: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.

98
00:09:52,680 --> 00:09:53,960
So that's great.

99
00:09:53,960 --> 00:09:59,240
And if everything worked like that in the real world, then we might not have bugs.

100
00:09:59,240 --> 00:10:03,620
And in certain cases, it does work like this in the real world.

101
00:10:03,620 --> 00:10:07,700
So there is formally verified hardware, according to a specific specification, of course.

102
00:10:07,700 --> 00: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.

103
00:10:17,960 --> 00:10:26,860
So there's, you know, hardware that can provably not contain kind of timing side channel attacks, for example.

104
00:10:26,860 --> 00:10:29,080
And there's verified software.

105
00:10:29,340 --> 00:10:35,960
I heard recently that Google, for example, is switching over to a formally verified crypto system.

106
00:10:36,720 --> 00: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.

107
00:10:48,480 --> 00:10:52,740
So for example, here we have a different type of program, right?

108
00:10:52,740 --> 00:10:56,020
And this program also doesn't crash.

109
00:10:56,140 --> 00:11:02,080
That A cubed plus B cubed equals C cubed, that's Fermat's last theorem, right?

110
00:11:02,080 --> 00:11:03,700
That is not solvable.

111
00:11:03,700 --> 00:11:05,080
There's no solution.

112
00:11:05,480 --> 00:11:10,460
But it took humans hundreds of years to figure this out.

113
00:11:10,540 --> 00:11:19,040
And the computer, you know, verification tools, unless they're special coded for this, will also be unable to handle it.

114
00:11:19,040 --> 00: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.

115
00:11:29,640 --> 00:11:31,960
Can I prove that the condition is always false?

116
00:11:31,960 --> 00: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.

117
00:11:42,820 --> 00:11:46,140
So what happens then, right?

118
00:11:46,140 --> 00:11:53,680
So then you have to go in and you have to start looking at the program manually and finding bugs.

119
00:11:53,680 --> 00: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?

120
00:12:03,220 --> 00:12:09,920
You open up a binary or a piece of software and the tool pops up alerts all over the place.

121
00:12:09,920 --> 00:12:12,460
And some of those are actual bugs.

122
00:12:12,460 --> 00:12:16,440
But you spend a lot of time chasing down the alerts.

123
00:12:16,580 --> 00: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.

124
00:12:29,320 --> 00:12:33,420
If A is not null, if A is not null.

125
00:12:33,420 --> 00:12:35,000
Why is that check there twice?

126
00:12:35,000 --> 00: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.

127
00:12:49,680 --> 00:12:58,500
So program verification, while it's a very useful field, like I said, there is verified software and hardware out there.

128
00:12:59,060 --> 00:13:03,440
It's not kind of the final answer on its own.

129
00:13:03,440 --> 00:13:06,780
So we also at some point need to have kind of the flip side.

130
00:13:06,780 --> 00:13:09,520
So program verification can say that is safe.

131
00:13:09,600 --> 00:13:13,460
But, you know, after that it says, okay, I can't really reason about it.

132
00:13:13,460 --> 00:13:17,580
So the flip side is you have a technique that says that is not safe.

133
00:13:17,580 --> 00:13:18,840
I can prove it.

134
00:13:18,840 --> 00:13:21,260
But I can't really prove, you know, if it is safe.

135
00:13:21,260 --> 00:13:24,360
But if it is not safe, I'll give you a counterexample.

136
00:13:24,860 --> 00:13:31,300
And the way this works is by, you know, finding counterexamples to whatever technique.

137
00:13:32,200 --> 00: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.

138
00:13:49,320 --> 00: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.

139
00:13:58,620 --> 00: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.

140
00:14:15,560 --> 00:14:20,040
Programmers in the 1950s would program in punch cards.

141
00:14:20,040 --> 00: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.

142
00:14:28,980 --> 00:14:32,680
This is unexpected input, just random stuff.

143
00:14:32,680 --> 00:14:36,460
And of course, by random stuff, program shouldn't crash.

144
00:14:36,460 --> 00: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.

145
00:14:52,200 --> 00: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.

146
00:15:02,720 --> 00:15:07,600
So the, you know, trash decks check for crashes.

147
00:15:07,960 --> 00:15:11,520
Turing reasoned about ensuring logical properties.

148
00:15:11,740 --> 00:15:13,020
But this is all done manually.

149
00:15:13,020 --> 00:15:18,180
So this is kind of our first set of tools in our tool bag, and they're manual tools.

150
00:15:18,180 --> 00:15:19,200
We have to dig them out.

151
00:15:19,200 --> 00:15:22,780
Okay, let's get our trash, you know, cards.

152
00:15:22,780 --> 00: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.

153
00:15:30,600 --> 00:15:32,460
But none of this was automated.

154
00:15:32,460 --> 00:15:41,060
And so as computers became more and more ubiquitous, the need for automation started showing itself.

155
00:15:41,460 --> 00: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.

156
00:15:54,300 --> 00: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.

157
00:16:04,920 --> 00:16:09,340
And this took a little while to catch on.

158
00:16:09,340 --> 00: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.

159
00:16:17,880 --> 00:16:24,920
It couldn't be, you know, optimized as well as handwritten assembly could at the time.

160
00:16:25,220 --> 00: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.

161
00:16:35,680 --> 00: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.

162
00:16:43,640 --> 00:16:48,000
Transfer programs to meet any sort of specification around on a different set of hardware.

163
00:16:50,000 --> 00: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.

164
00:16:59,640 --> 00: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.

165
00:17:11,440 --> 00: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.

166
00:17:22,720 --> 00:17:30,840
So I just played, you know, two days of a CTF full of these errors, of course, memory corruption bugs.

167
00:17:31,780 --> 00:17:36,620
And this was first described in 1968.

168
00:17:36,620 --> 00: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.

169
00:17:52,020 --> 00:17:54,260
And so this paper introduced that concept.

170
00:17:54,260 --> 00: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.

171
00:18:07,080 --> 00: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.

172
00:18:19,060 --> 00: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?

173
00:18:34,690 --> 00:18:39,810
So now you might want to verify that a program doesn't have a backdoor.

174
00:18:40,810 --> 00:18:46,550
Or you might verify that a program will not leak your sensitive private information.

175
00:18:46,550 --> 00: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.

176
00:18:55,970 --> 00:19:06,190
And so the need for automation was pretty well established by the kind of turn of the century, for sure.

177
00:19:06,650 --> 00:19:14,730
But even before that, those papers were like in the 1960s or something, late 1960s.

178
00:19:14,730 --> 00:19:21,810
And very quickly, oops, sorry, very quickly, people started to meet this need.

179
00:19:21,810 --> 00:19:25,110
The research community started pumping out automated approaches.

180
00:19:25,110 --> 00:19:28,670
And so I'm going to introduce a couple of these automated approaches.

181
00:19:30,610 --> 00: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.

182
00:19:39,370 --> 00:19:44,330
So we'll talk about a couple of prerequisites, right?

183
00:19:44,330 --> 00:19:47,970
So let's say you have a program.

184
00:19:48,050 --> 00:19:55,450
So on the top right, there's like a little Python program that's already a vulnerable program, by the way.

185
00:19:57,110 --> 00:20:01,330
And so you have this program, and you want to analyze it.

186
00:20:01,330 --> 00:20:05,970
So you have to reason about a program in a slightly different way as a computer than as a human.

187
00:20:05,970 --> 00:20:11,390
So for example, a program is viewed by a computer as a set of basic blocks.

188
00:20:11,390 --> 00:20:19,370
A basic block is a piece of code that is executed all together before passing on control flow somewhere else.

189
00:20:19,370 --> 00:20:24,530
So in our case, we'll pretend that input is part of this basic block.

190
00:20:24,530 --> 00:20:30,470
So this X equals input is a single basic block, and then it might branch depending on the input, right?

191
00:20:30,470 --> 00:20:33,390
So if you put in 42, it'll do one thing.

192
00:20:33,390 --> 00:20:37,010
If you put in something else, it'll do another.

193
00:20:37,010 --> 00: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.

194
00:20:45,290 --> 00:20:51,770
And each of these has a constraint that has to be met, right?

195
00:20:51,770 --> 00:20:55,650
In order to go down one path, you have to put in 42.

196
00:20:55,650 --> 00:20:58,590
In order to go down another, you have to put in not 42.

197
00:20:58,590 --> 00:21:00,230
And so these are called constraints.

198
00:21:00,350 --> 00: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.

199
00:21:11,730 --> 00: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.

200
00:21:24,430 --> 00:21:29,110
And then you look at the constraints all along this path.

201
00:21:29,110 --> 00:21:34,010
These are the path predicates that uniquely identify this path.

202
00:21:34,010 --> 00: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.

203
00:21:51,830 --> 00:21:56,770
So these are kind of the prerequisites of our program analysis techniques.

204
00:21:56,770 --> 00:21:58,890
So now we'll go through three of them.

205
00:21:58,890 --> 00:22:02,310
Actually for time reasons we'll go through two of them and mention a third.

206
00:22:02,310 --> 00:22:05,170
But we'll start with symbolic execution.

207
00:22:05,410 --> 00: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.

208
00:22:20,030 --> 00:22:24,390
And you think that this is something new, but it turns out that it's not.

209
00:22:24,390 --> 00:22:26,790
It's quite old actually.

210
00:22:26,790 --> 00:22:33,890
So 40 years ago, a little bit more, the first symbolic execution paper that I could find was proposed.

211
00:22:35,290 --> 00:22:38,930
And there were several actually, right in one year basically.

212
00:22:38,930 --> 00:22:44,070
So this idea had some prerequisites that were met and then it exploded.

213
00:22:44,330 --> 00:22:51,690
And so the symbolic execution engines were developed that could then symbolically execute Fortran code.

214
00:22:51,690 --> 00:23:00,970
Now we have symbolic execution engines that you can download off GitHub that can execute binaries, Java, Android, whatever you want.

215
00:23:02,570 --> 00:23:08,530
And this is kind of a fairly powerful way of reasoning about programs.

216
00:23:08,530 --> 00: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.

217
00:23:20,970 --> 00:23:22,450
Hold on.

218
00:23:23,350 --> 00:23:27,510
So here's a program that has several bugs, right?

219
00:23:27,910 --> 00: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?

220
00:23:40,830 --> 00:23:46,190
You can imagine that instead of this crash, it does some system relevant stuff.

221
00:23:46,190 --> 00: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.

222
00:23:51,910 --> 00:23:56,210
So let's see how we might approach this problem with symbolic execution, right?

223
00:23:57,290 --> 00:24:02,830
So first let's look at the control flow graph of this program, starting from the beginning.

224
00:24:02,830 --> 00:24:08,570
Again, the control flow graph is made up of basic blocks and the control flow transitions between them.

225
00:24:08,570 --> 00:24:10,870
So we start at this input.

226
00:24:11,130 --> 00:24:13,830
If the input is service, it branches.

227
00:24:13,830 --> 00: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.

228
00:24:25,170 --> 00:24:26,750
And if it is, it crashes.

229
00:24:26,750 --> 00:24:30,950
If not, it prints an on command and then it exits.

230
00:24:31,750 --> 00:24:37,690
On the other side of the branch, it asks for a passcode.

231
00:24:37,690 --> 00:24:42,010
If the passcode is invalid, it prints invalid passcode.

232
00:24:42,010 --> 00:24:46,470
Otherwise, it calls the authentication function, then it prints exit and exits.

233
00:24:46,470 --> 00:24:48,670
So this is our control flow graph.

234
00:24:48,670 --> 00: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?

235
00:24:56,350 --> 00:25:02,810
So we would start executing the program in an emulator.

236
00:25:02,890 --> 00:25:10,670
And in this emulator, instead of ones and zeros, we are working on X, Y, and other symbols.

237
00:25:10,750 --> 00:25:15,550
So, for example, username is a symbol in this emulator.

238
00:25:15,550 --> 00:25:22,530
So when we pull in an input, it will produce an unconstrained variable called username.

239
00:25:22,530 --> 00:25:23,650
And we don't know what username is.

240
00:25:23,650 --> 00:25:25,110
Username can be anything.

241
00:25:25,790 --> 00:25:30,690
Because, you know, that is how we implement our emulator.

242
00:25:31,450 --> 00:25:38,850
And as we check for values of username, we create what are called constraints, right?

243
00:25:38,850 --> 00:25:46,690
So these are the exact constraints that the basic block checks when it pushes execution forward.

244
00:25:47,190 --> 00:25:49,270
And we collect two constraints in this case.

245
00:25:49,270 --> 00:25:51,870
On the one side, username equals service.

246
00:25:51,870 --> 00:25:53,350
On the other side, it does not equal service.

247
00:25:53,350 --> 00:25:54,190
These are constraints.

248
00:25:54,190 --> 00:26:00,810
And we continue executing both sides of this statement with symbolic execution.

249
00:26:01,530 --> 00:26:06,690
But then we hit something that is very bad for symbolic execution.

250
00:26:06,690 --> 00:26:10,030
We hit, for example, string processing functions.

251
00:26:10,030 --> 00:26:17,990
So a string processing function like A2I might check a given byte, see if it is a number.

252
00:26:17,990 --> 00:26:19,990
If it is a number, it'll do one thing.

253
00:26:19,990 --> 00:26:22,590
If it's not, it'll do another, right?

254
00:26:22,590 --> 00:26:24,850
Or if it's a certain number, it might do one.

255
00:26:24,850 --> 00:26:27,190
If it's not a certain number, it'll do another.

256
00:26:27,190 --> 00:26:31,950
So it'll keep branching the symbolic emulator at every...

257
00:26:33,810 --> 00:26:34,950
I'm sorry?

258
00:26:35,790 --> 00:26:37,230
Oh, awesome.

259
00:26:37,330 --> 00: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?

260
00:26:51,130 --> 00: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.

261
00:27:02,290 --> 00:27:05,550
And there's an exponential path explosion here.

262
00:27:06,290 --> 00:27:13,350
And there are some approaches in the symbolic execution world to try to deal with this sort of path explosion.

263
00:27:13,350 --> 00:27:19,150
But in general, these approaches boil down to the requirement to remove paths, right?

264
00:27:19,150 --> 00:27:20,590
And lose this information.

265
00:27:20,590 --> 00:27:30,770
And so in the end, the symbolic execution engine might only find certain paths and not others and miss the bug.

266
00:27:30,770 --> 00:27:34,870
Because we have to simplify to keep things tractable.

267
00:27:35,090 --> 00:27:37,030
So that's symbolic execution.

268
00:27:37,030 --> 00: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.

269
00:27:50,650 --> 00:27:55,630
Symbolic execution was proposed as you saw in 1975.

270
00:27:55,870 --> 00: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.

271
00:28:11,590 --> 00: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.

272
00:28:26,410 --> 00:28:33,030
And this is the first symbolic trace of a program, done in 1842 before computers were invented.

273
00:28:33,210 --> 00:28:36,890
So that was a pretty interesting thing to find.

274
00:28:37,310 --> 00:28:45,250
And kind of a nice point of history that we can put as the start of program analysis in this sense.

275
00:28:45,730 --> 00:28:54,890
1842, not 1975 or 1949 or any of those much, much later dates.

276
00:28:54,890 --> 00: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.

277
00:29:11,110 --> 00: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.

278
00:29:22,570 --> 00:29:27,330
It generates inputs to find vulnerabilities, but it can't prove that there aren't any.

279
00:29:28,930 --> 00: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.

280
00:29:39,970 --> 00:29:43,470
So I'll leave that as future research for you guys.

281
00:29:43,470 --> 00: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.

282
00:30:02,670 --> 00: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.

283
00:30:15,950 --> 00:30:30,610
And abstract interpretation looks at the control flow graph, the program as a whole, essentially.

284
00:30:30,610 --> 00: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.

285
00:30:49,650 --> 00: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.

286
00:31:04,190 --> 00:31:09,630
Because if it cannot prove that a piece of code is safe, it will raise an alert.

287
00:31:09,630 --> 00:31:13,590
The problem is that, as we talked about, there are false positives.

288
00:31:13,590 --> 00: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.

289
00:31:26,670 --> 00: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.

290
00:31:38,050 --> 00:31:41,250
And then we moved on to fuzzing.

291
00:31:41,250 --> 00:31:49,390
And so fuzzing is kind of one of the biggest ways to find vulnerabilities in modern software.

292
00:31:49,390 --> 00:31:52,110
And it's actually surprisingly simple.

293
00:31:52,130 --> 00: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.

294
00:32:01,230 --> 00:32:03,650
It's evolved quite a bit since then.

295
00:32:03,650 --> 00:32:13,550
And so the specific implementation of fuzzing that I'll describe here is implemented by American Fuzzy Lab.

296
00:32:13,830 --> 00:32:20,250
It's a fuzzer that mutates its inputs when it detects differences in program execution.

297
00:32:20,970 --> 00:32:25,190
And so let's see how it would run on our program here.

298
00:32:25,270 --> 00:32:31,730
We'll start with some randomly generated test case or human-seeded test case.

299
00:32:31,730 --> 00:32:37,390
So a human might input a username of ASDF and a password of 111.

300
00:32:37,390 --> 00:32:44,350
And that input will trigger certain basic blocks to be executed, right?

301
00:32:44,350 --> 00:32:47,890
And so we executed the username input, of course.

302
00:32:47,890 --> 00:32:55,010
We executed the check for the kind of service username that could lead to the crash.

303
00:32:55,010 --> 00: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.

304
00:33:06,290 --> 00:33:08,170
So we triggered those basic blocks.

305
00:33:08,170 --> 00:33:12,330
And so the fuzzer starts mutating this input, right?

306
00:33:12,330 --> 00:33:15,890
It might make a capital D or something.

307
00:33:15,970 --> 00:33:25,670
Or it might mutate input in a way that passes another check.

308
00:33:25,670 --> 00:33:31,470
So it mutated the input in a way that passes that passcode check.

309
00:33:31,470 --> 00:33:36,310
It actually doesn't, because there's another bug in the program that I didn't notice before.

310
00:33:36,310 --> 00:33:49,350
But let's pretend that it creates a valid size of a passcode and triggers that authentication function, right?

311
00:33:49,350 --> 00:33:51,710
So that is a new basic block that it triggers.

312
00:33:51,710 --> 00: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.

313
00:34:04,110 --> 00:34:06,070
But then we get stuck.

314
00:34:06,070 --> 00:34:13,610
Because through randomly mutating inputs, we are unable to satisfy complex checks, right?

315
00:34:13,610 --> 00:34:19,430
We need a username of service, and we have randomly mutated usernames.

316
00:34:19,430 --> 00: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.

317
00:34:25,590 --> 00: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.

318
00:34:40,350 --> 00:34:44,850
But string checks aren't the only complex checks in programs.

319
00:34:44,850 --> 00:34:53,850
There are hashes, there are complex input formats, dependencies between different input bytes.

320
00:34:53,850 --> 00: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.

321
00:35:07,110 --> 00:35:16,790
And so fuzzing with this random data, of course, is a throwback to this trash deck concept.

322
00:35:16,790 --> 00:35:22,550
So fuzzing was invented in 1950, not 1981.

323
00:35:23,690 --> 00:35:26,750
Or at least manual fuzzing.

324
00:35:26,750 --> 00: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.

325
00:35:37,950 --> 00: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.

326
00:35:53,110 --> 00:35:59,490
And next, we should evaluate them, understand how these different

327
00:36:03,410 --> 00:36:09,210
goals or how these different techniques help us achieve program analysis goals.

328
00:36:09,350 --> 00: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.

329
00:36:26,030 --> 00:36:32,990
So you want to take programs and specifications, feed them into your technique, and see how well it does.

330
00:36:32,990 --> 00:36:36,210
This is my clipart slide, by the way.

331
00:36:36,210 --> 00:36:38,690
So hopefully my clipart game is on point.

332
00:36:39,950 --> 00:36:44,990
So you run your analysis, you get your results, and you're happy, right?

333
00:36:44,990 --> 00:36:47,910
Well, there are a number of problems with this.

334
00:36:47,910 --> 00: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.

335
00:36:58,630 --> 00:37:11,250
And environments like Windows, macOS, Linux, mobile devices, cyber-physical devices, they have really complex environments.

336
00:37:11,730 --> 00: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.

337
00:37:33,750 --> 00:37:38,470
Another problem is finding a good data set to evaluate on, right?

338
00:37:38,470 --> 00:37:44,070
There's not really a good data set for... or there wasn't a great data set for vulnerability research.

339
00:37:44,070 --> 00:37:49,090
This problem is actually being worked on, and new data sets are being created, as I'll talk about.

340
00:37:49,090 --> 00: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,

341
00:38:13,210 --> 00:38:17,110
or one specific program that you happen to be very good at analyzing.

342
00:38:17,370 --> 00:38:19,910
Another problem is these specifications.

343
00:38:19,910 --> 00: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.

344
00:38:35,950 --> 00: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.

345
00:38:52,450 --> 00:39:00,110
Is your bank allowed to have your various cookies or something along these lines?

346
00:39:01,530 --> 00: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,

347
00:39:27,230 --> 00:39:30,650
understanding if you're making an improvement or not.

348
00:39:32,250 --> 00: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,

349
00:39:55,410 --> 00: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.

350
00:40:19,950 --> 00: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.

351
00:40:33,170 --> 00: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.

352
00:40:52,190 --> 00: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.

353
00:41:06,190 --> 00: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.

354
00:41:30,950 --> 00: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.

355
00:41:50,030 --> 00: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.

356
00:42:13,970 --> 00:42:16,270
That's my other piece of clip art.

357
00:42:17,590 --> 00: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.

358
00:42:36,390 --> 00: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.

359
00:42:44,190 --> 00:42:49,810
So for example, Symbolic Execution on the entire data set finds nine vulnerabilities.

360
00:42:49,810 --> 00: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.

361
00:42:58,910 --> 00:43:04,550
But Symbolic Execution on this entire data set finds nine vulnerabilities.

362
00:43:04,550 --> 00:43:06,150
That's not a lot, right?

363
00:43:06,150 --> 00:43:10,010
There are vulnerabilities in every program of these 249 programs.

364
00:43:10,010 --> 00:43:12,310
It only finds vulnerabilities in nine of them.

365
00:43:12,910 --> 00:43:16,650
Of course, we can optimize Symbolic Execution using various tricks.

366
00:43:16,650 --> 00: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.

367
00:43:27,710 --> 00:43:38,450
And so by utilizing all of these optimizations, we can get 26 crashes, crashing 26 binaries.

368
00:43:38,950 --> 00: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.

369
00:43:56,210 --> 00:44:02,350
So I should say here that this is our implementation of Veritesting, and it might be suboptimal.

370
00:44:02,370 --> 00:44:05,550
So their Veritesting might be considerably better.

371
00:44:05,970 --> 00:44:09,530
But that all pales in comparison with fuzzing.

372
00:44:09,530 --> 00:44:19,850
This seemingly simple technique of throwing random data and seeing what happens finds 106 crashing binaries in the data set.

373
00:44:20,330 --> 00: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.

374
00:44:34,750 --> 00:44:40,070
Because now we can look at them in terms of, you know, summation numbers.

375
00:44:40,070 --> 00:44:42,130
But there's also some subtleties there.

376
00:44:42,130 --> 00:44:46,270
They find bugs, different types of bugs in different binaries.

377
00:44:46,270 --> 00:44:54,010
So we can look into that and make inferences and try to create new approaches.

378
00:44:54,010 --> 00: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.

379
00:45:05,690 --> 00: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.

380
00:45:12,870 --> 00:45:17,470
And sometimes one finds a crash, sometimes another finds a crash, sometimes neither of them find a crash.

381
00:45:17,470 --> 00:45:19,290
In fact, very frequently.

382
00:45:19,350 --> 00:45:28,750
And so we decided to combine them in a very straightforward but careful way.

383
00:45:28,830 --> 00:45:31,430
And the idea is as follows.

384
00:45:31,430 --> 00:45:33,150
We begin by fuzzing the binary.

385
00:45:33,150 --> 00:45:40,130
This is nice and fast and achieves decent code coverage, but as we discussed, eventually gets stuck on complex checks.

386
00:45:40,130 --> 00: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.

387
00:45:52,530 --> 00:45:54,830
And then we synchronize that back into the fuzzer.

388
00:45:54,830 --> 00: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.

389
00:46:06,530 --> 00:46:12,110
And we do this iteratively, back and forth between the fuzzer and symbolic execution.

390
00:46:12,230 --> 00:46:23,550
So by implementing symbolic assistance for the fuzzer in this way, we achieve on this entire dataset 118 crashes.

391
00:46:24,170 --> 00: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.

392
00:46:42,670 --> 00:46:49,010
So there's a lot of uniqueness between the different techniques used here.

393
00:46:50,490 --> 00:46:56,030
Driller, the applicability of it varies by program, whether or not there are complex checks.

394
00:46:56,390 --> 00:46:58,690
We can run through a quick run here.

395
00:46:58,690 --> 00:47:06,270
So this is a control flow graph of an example program, and driller starts in the top left corner there.

396
00:47:06,390 --> 00:47:14,750
And it first starts by fuzzing a portion of the program before it gets stuck in a complex check.

397
00:47:15,070 --> 00:47:19,370
And this is the basic block coverage on the right in this graph here.

398
00:47:19,370 --> 00:47:21,830
You can see just kind of flat lines, right?

399
00:47:21,830 --> 00: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.

400
00:47:41,510 --> 00: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.

401
00:47:55,750 --> 00:47:57,990
And so that's how driller works.

402
00:47:58,030 --> 00:47:59,330
There's still a lot to do.

403
00:47:59,330 --> 00: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,

404
00:48:20,750 --> 00:48:22,870
or at least we have yet to develop.

405
00:48:23,730 --> 00:48:27,990
And so if this all sounds interesting to you, I encourage you to join in.

406
00:48:27,990 --> 00:48:32,330
There are several ways that you can participate in program analysis research.

407
00:48:32,330 --> 00:48:34,730
One is you can contribute to open source frameworks.

408
00:48:34,730 --> 00:48:39,810
So we run one of these frameworks in our research lab.

409
00:48:39,810 --> 00:48:40,830
It's called anger.

410
00:48:40,830 --> 00:48:42,430
Go to anger.io.

411
00:48:42,430 --> 00:48:51,250
There's a lot that we could use help with documentation, environment support, better techniques, and so on.

412
00:48:51,250 --> 00:48:55,050
And the other is that I'm always looking for students.

413
00:48:55,050 --> 00:48:59,390
I'm starting as a professor at Arizona State University.

414
00:48:59,650 --> 00: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.

415
00:49:13,050 --> 00: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.

416
00:49:22,170 --> 00:49:27,630
I'll put you in touch with the right people, and you could explore that.

417
00:49:28,530 --> 00:49:31,110
The presentation is available online.

418
00:49:31,110 --> 00:49:35,270
All my contact info is right here, and I guess we'll questions in the hall?

419
00:49:35,890 --> 00:49:36,690
Awesome.

420
00:49:36,850 --> 00:49:37,590
Thank you, guys.