1 00:00:00,000 --> 00:00:18,010 *35C3 preroll music* 2 00:00:18,010 --> 00:00:29,239 Herald angel: OK. Our next speaker will be trying to tame the chaos. Peter Sewell 3 00:00:29,239 --> 00:00:34,120 from the University of Cambridge. A warm round of applause please. 4 00:00:34,120 --> 00:00:37,910 *applause* 5 00:00:37,910 --> 00:00:48,740 Sewell: Thank you! Okay. So here we are. C3 again with a program full of 6 00:00:48,740 --> 00:00:56,710 fascinating and exciting and cool stuff. And if we look just at the security talks 7 00:00:56,710 --> 00:00:59,940 all manner of interesting things. I'm going to go to a lot to these. You should 8 00:00:59,940 --> 00:01:06,830 too. Let's see though if we read some of the titles: exploiting kernel memory 9 00:01:06,830 --> 00:01:18,750 corruptions, attacking end to end e-mail encryption. What else have we got: modern 10 00:01:18,750 --> 00:01:31,550 Windows user space exploitation, compromising online accounts. OK so a lot 11 00:01:31,550 --> 00:01:36,130 of these talks, as usual, they're explaining to us that our computers, 12 00:01:36,130 --> 00:01:42,950 they're not doing what we would like and this as usual is the merest tip of a tiny 13 00:01:42,950 --> 00:01:48,970 iceberg, alright. We have a hundreds of thousands of known vulnerabilities and 14 00:01:48,970 --> 00:01:53,280 many unknown vulnerabilities. Let me do it a bit dark here, but let me try some 15 00:01:53,280 --> 00:01:59,490 audience participation. How many of you have in the last year written at least a 16 00:01:59,490 --> 00:02:09,019 hundred lines of code? And of those people keep your hands up if you are completely 17 00:02:09,019 --> 00:02:17,550 confident that code does the right thing. *laughter* I would like to talk to you 18 00:02:17,550 --> 00:02:23,200 later *laughter* and so would the people in the self driving car that you're 19 00:02:23,200 --> 00:02:30,790 probably engineering. So, so how many unknown vulnerabilities then. Well you can 20 00:02:30,790 --> 00:02:39,160 take what's in your mind right now and multiply it by - oh, this doesnt work very 21 00:02:39,160 --> 00:02:48,920 well. No. No, no. Computers, they do the wrong thing again and again and again. 22 00:02:48,920 --> 00:02:54,421 *laughter and some applause* We can multiply by this estimate of about a 100 23 00:02:54,421 --> 00:03:00,630 billion lines of new code each year. So if we take all of this: these talks, these 24 00:03:00,630 --> 00:03:05,900 numbers, these should make us not happy and excited, these should make us sad, 25 00:03:05,900 --> 00:03:16,070 very sad and frankly rather scared of what is going on in the world. So what can we 26 00:03:16,070 --> 00:03:25,610 do? We can, option one, give up using computers altogether. *applause* In most 27 00:03:25,610 --> 00:03:29,640 audiences this will be a hard sell but here I'm sure you're all happy to just 28 00:03:29,640 --> 00:03:40,180 turn them off now. Or we can throw up our hands in the air and collapse in some kind 29 00:03:40,180 --> 00:03:54,830 of pit of despair. Well, maybe, maybe not. My task today is to give you a tiny 30 00:03:54,830 --> 00:04:00,050 smidgen, a very tall, a very small amount of hope that it may be possible to do 31 00:04:00,050 --> 00:04:04,099 slightly better. But if we want to do better we first have to understand why 32 00:04:04,099 --> 00:04:10,560 things are so bad and if we look at our aeronautical engineering colleagues for 33 00:04:10,560 --> 00:04:15,739 example, they can make planes which very rarely fall out of the sky. Why is it that 34 00:04:15,739 --> 00:04:22,880 they can do that and we are so shit at making computers? Well, I'm going to reuse 35 00:04:22,880 --> 00:04:27,970 a picture that I used at 31C3, which is still the best description I can find of 36 00:04:27,970 --> 00:04:35,990 the stack of hardware and software that we live above. Here we go. It's, there's so 37 00:04:35,990 --> 00:04:40,160 much information in this, it's just ace. So we see down here all of this 38 00:04:40,160 --> 00:04:45,430 transparent silicon, it's the hardware we live above. We see a stack of phases of a 39 00:04:45,430 --> 00:04:51,241 C compiler, we see all kinds of other other bits and pieces. There might be a 40 00:04:51,241 --> 00:04:58,870 slightly hostile wireless environment in this room for some reason. If we look at 41 00:04:58,870 --> 00:05:03,230 this and think about the root causes for why our systems are so bad we can see 42 00:05:03,230 --> 00:05:07,889 terrible things. So the first is, obviously there's a lot of legacy 43 00:05:07,889 --> 00:05:12,810 complexity that we're really stuck with, alright. If you pull out one of those 44 00:05:12,810 --> 00:05:16,240 pieces from the middle and try and replace it with something which is not of exactly 45 00:05:16,240 --> 00:05:21,350 the same shape the whole pile will collapse. So we somehow need to find an 46 00:05:21,350 --> 00:05:27,970 incremental path to a better world. And then, this is the most fundamental reason 47 00:05:27,970 --> 00:05:33,220 that these are not like aeroplanes, these systems are discrete not continuous. If 48 00:05:33,220 --> 00:05:38,290 you take an honest good I made out of a piece of steel and you push on it a little 49 00:05:38,290 --> 00:05:44,270 bit it moves a little bit, basically in proportion. If it is 1 percent too strong, 50 00:05:44,270 --> 00:05:50,090 1 percent to weak, basically it doesn't matter. But in these things one line of 51 00:05:50,090 --> 00:05:56,490 code can mean you're open to a catastrophic exploit and one line in many, 52 00:05:56,490 --> 00:06:05,970 many million. OK. And next thing... this really doesn't work. They're very 53 00:06:05,970 --> 00:06:11,380 complicated. But the scary thing is not the static complexity of those lines of 54 00:06:11,380 --> 00:06:15,080 code and the number of components although that's pretty intimidating the really 55 00:06:15,080 --> 00:06:21,110 scary thing is that the exponential number of states and execution paths. So these 56 00:06:21,110 --> 00:06:26,139 two together they mean that the testing that we rely on testing is the only way we 57 00:06:26,139 --> 00:06:30,710 have to build systems which are not instantly broken. Testing can never save 58 00:06:30,710 --> 00:06:40,550 us from these exploitable errors. And that means ultimately we need to do proof. 59 00:06:40,550 --> 00:06:45,610 Honest machine checked mathematical proof. And this also tells us that we need to 60 00:06:45,610 --> 00:06:51,289 arrange for our systems to be secure for simple reasons that do not depend on the 61 00:06:51,289 --> 00:06:57,180 correctness of all of those hundred billion lines of code. Then another thing 62 00:06:57,180 --> 00:07:03,360 that we have here. All these interfaces: the architecture interface, the C language 63 00:07:03,360 --> 00:07:10,650 interface, the sockets API interface, the TCP interface. All of these we rely on to 64 00:07:10,650 --> 00:07:17,500 let different parts of the system be engineered by different organizations. But 65 00:07:17,500 --> 00:07:24,870 they're all really badly described and badly defined. So what you find is, for 66 00:07:24,870 --> 00:07:30,130 each of these, typically a prose book varying in thickness between about that 67 00:07:30,130 --> 00:07:36,909 and about that, full of text. Well, we still rely on testing - limited though it 68 00:07:36,909 --> 00:07:44,000 is - but you can never test anything against those books. So we need instead 69 00:07:44,000 --> 00:07:48,940 interface descriptions, definitions, specifications, that are more rigorous, 70 00:07:48,940 --> 00:07:54,419 mathematically rigorous and that are executable - not in the normal sense of 71 00:07:54,419 --> 00:07:58,940 executable as an implementation but executable as a test oracle. So you can 72 00:07:58,940 --> 00:08:03,880 compute whether some observed behaviour is allowed or not and not have to read the 73 00:08:03,880 --> 00:08:07,700 book and argue on the Internet. And we also need interface definitions that 74 00:08:07,700 --> 00:08:19,820 support this proof that we need. And then all of this stuff was made up in the 1970s 75 00:08:19,820 --> 00:08:25,639 or the sixties and in the 70s and the 60s the world was a happy place and people 76 00:08:25,639 --> 00:08:32,068 walked around with flowers in their hair and nothing bad ever happened. And that is 77 00:08:32,068 --> 00:08:36,340 no longer the case. And so we need defensive design, but we need defensive 78 00:08:36,340 --> 00:08:41,149 design that is somehow compatible or can be made enough compatible with this legacy 79 00:08:41,149 --> 00:08:46,879 investment. That's quite hard. And then - I can't say very much about this, but we 80 00:08:46,879 --> 00:08:50,360 have at the moment very bad incentives, because we have a very strong incentive to 81 00:08:50,360 --> 00:08:55,420 make things that are more complex than we can possibly handle or understand. We make 82 00:08:55,420 --> 00:09:00,410 things, we add features, we make a thing which is just about shippable and then we 83 00:09:00,410 --> 00:09:06,550 ship it. And then we go on to the next thing. So we need economic and legal 84 00:09:06,550 --> 00:09:11,300 incentives for simplicity and for security that we do not yet have. But it's hard to 85 00:09:11,300 --> 00:09:17,109 talk about those until we have the technical means to react to those 86 00:09:17,109 --> 00:09:21,980 incentives. OK, so what I'm going to do now, I'm going to talk about two of these 87 00:09:21,980 --> 00:09:26,230 interfaces, the architect interface and the C language interface, and see what we 88 00:09:26,230 --> 00:09:32,819 can do to make things better. A lot of this has to do with memory. So whoever it 89 00:09:32,819 --> 00:09:38,209 was that picked the subtitle for this meeting "refreshing memories" thank you, 90 00:09:38,209 --> 00:09:45,429 because it's great, I love it. Let's refresh your memory quite a way. So I 91 00:09:45,429 --> 00:09:52,959 invite you to think back to when you were very very young in about 1837 when cool 92 00:09:52,959 --> 00:09:58,519 hacking was going on. Charles Babbage was designing the Analytical Engine and even 93 00:09:58,519 --> 00:10:03,369 then you see there was this dichotomy between a mill performing operations and a 94 00:10:03,369 --> 00:10:11,100 store holding numbers. This is a plan view of the analytical engine, well, it was 95 00:10:11,100 --> 00:10:15,240 vaporware, but a design from the analytical engine, and you see here these 96 00:10:15,240 --> 00:10:21,689 circles these are columns of numbers each made out of a stack of cogs, maybe a 50 97 00:10:21,689 --> 00:10:28,340 digit decimal number in each of those columns. And this array, really, he 98 00:10:28,340 --> 00:10:34,681 imagined it going on out to and over there somewhere, with about 1000 numbers. So 99 00:10:34,681 --> 00:10:42,850 even then you have a memory which is an array of numbers. I think these were not- 100 00:10:42,850 --> 00:10:46,519 I don't think you could do address computation on these things, I think 101 00:10:46,519 --> 00:10:53,649 addresses were only constants, but, still, basically an array of numbers. So okay 102 00:10:53,649 --> 00:10:59,370 what do we got now. Let's look a bit at C. How many of those people who have 103 00:10:59,370 --> 00:11:06,980 programmed 100 lines of code, how many of you were C programmers? Quite a few. Or 104 00:11:06,980 --> 00:11:12,660 maybe you're just embarrassed. I forgot to say. Those that didn't put your hands up 105 00:11:12,660 --> 00:11:18,499 for that first question. You should feel proud and you should glory in your 106 00:11:18,499 --> 00:11:26,460 innocence while you still have it. You are not yet complicit in this trainwreck. It 107 00:11:26,460 --> 00:11:31,680 worked then. Okay so here's a little piece of C-code which I shall explain. I shall 108 00:11:31,680 --> 00:11:38,279 explain it in several different ways. So we start out. It creates two locations x 109 00:11:38,279 --> 00:11:52,670 and secret... Don't do that. This is so bad. Creates x, storing one and secret_key 110 00:11:52,670 --> 00:11:58,980 which stores, I might get this wrong, your pin. And then there's some computation 111 00:11:58,980 --> 00:12:05,129 which is supposed to only operate on x but maybe it's a teensy bit buggy or corrupted 112 00:12:05,129 --> 00:12:13,620 by somebody and then we try and we make a pointer to x and in this execution x just 113 00:12:13,620 --> 00:12:21,209 happened to be allocated at 14. This pointer contains the number 14 and then we 114 00:12:21,209 --> 00:12:25,389 add one to that pointer. It's C so actually that adding one to the pointer it 115 00:12:25,389 --> 00:12:32,600 really means add the four bytes which are the size of that thing. So we add 4 to 14 116 00:12:32,600 --> 00:12:40,059 and we get 18. And then we try and read the thing which is pointed to. What's 117 00:12:40,059 --> 00:12:48,549 going to happen. Let me compile this and run it in a conventional way. It printed a 118 00:12:48,549 --> 00:12:54,300 secret key. Bad. This program, rather distressingly, this is characteristic by 119 00:12:54,300 --> 00:12:58,830 no means of all security flaws but a very disturbingly large fraction of all the 120 00:12:58,830 --> 00:13:10,600 security flaws are basically doing this. So does C really let you do that. Yes and 121 00:13:10,600 --> 00:13:17,911 no. So if you look at the C standard, which is one of these beautiful books, it 122 00:13:17,911 --> 00:13:22,859 says you, have to read moderately carefully to understand this, but it says 123 00:13:22,859 --> 00:13:27,399 for this program has undefined behavior. And many of you will know what that means 124 00:13:27,399 --> 00:13:32,949 but others won't, but, so that means as far as the standard is concerned for 125 00:13:32,949 --> 00:13:39,329 programs like that there is no constraint on the behavior of the implementation at 126 00:13:39,329 --> 00:13:47,039 all. Or said another way and maybe a more usefully way: The standard lets 127 00:13:47,039 --> 00:13:52,329 implementations, so C compilers, assume that programmers don't have this kind of 128 00:13:52,329 --> 00:13:59,569 stuff and it's the programmer's responsibility to ensure that. Now in 129 00:13:59,569 --> 00:14:04,781 about 1970, 75 maybe 1980, this was a really good idea, it gives compilers a lot 130 00:14:04,781 --> 00:14:14,000 of flexibility to do efficient implementation. Now not so much. How does 131 00:14:14,000 --> 00:14:19,199 this work in the definition? So the standard somehow has to be able to look at 132 00:14:19,199 --> 00:14:29,470 this program and identify it as having this undefined behavior. And indeed, well, 133 00:14:29,470 --> 00:14:37,089 if we just think about the numbers in memory this 18, it points to a perfectly 134 00:14:37,089 --> 00:14:42,189 legitimate storage location and that plus one was also something that you're 135 00:14:42,189 --> 00:14:48,149 definitely allowed to do in C. So the only way that we can know that this is 136 00:14:48,149 --> 00:14:54,419 undefined behavior is to keep track of the original allocation of this pointer. And 137 00:14:54,419 --> 00:14:59,240 here I've got these allocation identifiers at 3, at 4, at 5, and you see here I've 138 00:14:59,240 --> 00:15:03,689 still got this pointer despite the fact that I added 4 to it. I still remembered 139 00:15:03,689 --> 00:15:09,939 the allocation idea so I can check, or the standard can check, when we try and read 140 00:15:09,939 --> 00:15:15,290 from this whether that address is within the footprint of that original allocation, 141 00:15:15,290 --> 00:15:19,019 i.e. is within there and in fact it is not, it's over here, it is not within 142 00:15:19,019 --> 00:15:25,509 there at all. So this program is deemed to have undefined behavior. Just to clarify 143 00:15:25,509 --> 00:15:30,649 something people often get confused. So we detect undefined behavior here but it 144 00:15:30,649 --> 00:15:35,299 isn't really a temporal thing. The fact that there is undefined behavior anywhere 145 00:15:35,299 --> 00:15:41,790 in the execution means the whole program is toast. Okay but this is really 146 00:15:41,790 --> 00:15:46,339 interesting because we're relying for this critical part of the standard onto 147 00:15:46,339 --> 00:15:52,319 information which is not there at run time in a conventional implementation. So just 148 00:15:52,319 --> 00:15:59,050 to emphasize that point, if I compile this program, let's say to ARM assembly 149 00:15:59,050 --> 00:16:04,850 language I get a sequence of store and load and add instructions, store, load, 150 00:16:04,850 --> 00:16:12,089 add, store, load, load. And if I look at what the ARM architecture says can happen 151 00:16:12,089 --> 00:16:17,139 these blue transitions... one thing to notice is that we can perfectly well do 152 00:16:17,139 --> 00:16:21,639 some things out of order. At this point we could either do this load or we could do 153 00:16:21,639 --> 00:16:27,240 that store. That would be a whole other talk. Let's stick with the sequential 154 00:16:27,240 --> 00:16:33,100 execution for now. What I want to emphasize is that these, this load of this 155 00:16:33,100 --> 00:16:36,569 address, really was loading a 64 bit number, which was the address of x and 156 00:16:36,569 --> 00:16:44,419 adding 4 to it and then loading from that address, the secret key. So there is no 157 00:16:44,419 --> 00:16:55,910 trace of these allocation ideas. No trace at all. Okay, let me step back a little 158 00:16:55,910 --> 00:17:04,939 bit. I've been showing you some screenshots of C behaviour and ARM 159 00:17:04,939 --> 00:17:12,109 behaviour and I claim that these are actually showing you all of the behaviours 160 00:17:12,109 --> 00:17:19,359 allowed by what one would like the standards to be for these two things. And 161 00:17:19,359 --> 00:17:26,529 really what I've been showing you are GUIs attached to mathematical models that we've 162 00:17:26,529 --> 00:17:31,000 built in a big research project for the last many years. REMS: "Rigorous 163 00:17:31,000 --> 00:17:34,929 Engineering of Mainstream Systems" sounds good, aspirational title I think I would 164 00:17:34,929 --> 00:17:42,049 say. And in that we've built semantics, so mathematical models defining the envelope 165 00:17:42,049 --> 00:17:47,580 of all allowed behaviour for a quite big fragment of C and for the concurrency 166 00:17:47,580 --> 00:17:53,950 architecture of major processors ARM, and x86, and RISC-V, and IBM POWER and also 167 00:17:53,950 --> 00:17:57,770 for the instruction set architecture of these processors, the details of how 168 00:17:57,770 --> 00:18:03,940 individual instructions are executed. And in each case these are specs that are 169 00:18:03,940 --> 00:18:08,350 executable as test oracles, you can compare algorithmically some observed 170 00:18:08,350 --> 00:18:13,320 behaviour against whether spec says it's allowed or not, which you can't do with 171 00:18:13,320 --> 00:18:19,030 those books. So is it just an idiot simple idea but for some reason the industry has 172 00:18:19,030 --> 00:18:26,960 not taken it on board any time in the last five decades. It's not that hard to do. 173 00:18:26,960 --> 00:18:30,710 These are also mathematical models, I'll come back to that later. But another thing 174 00:18:30,710 --> 00:18:34,529 I want to emphasize here is that in each of these cases, especially these first 175 00:18:34,529 --> 00:18:40,669 two, when you start looking really closely then you learn what you have to do is not 176 00:18:40,669 --> 00:18:44,400 build a nice clean mathematical model of something which is well understood. What 177 00:18:44,400 --> 00:18:50,540 you learn is that there are real open questions. For example within the C 178 00:18:50,540 --> 00:18:55,759 standards committee and within ARM a few years ago about exactly what these things 179 00:18:55,759 --> 00:19:01,130 even were. And that is a bit disturbing given that these are the foundations for 180 00:19:01,130 --> 00:19:06,009 all of our information infrastructure. There is also a lot of other work going on 181 00:19:06,009 --> 00:19:11,010 with other people within this REMS project on web assembly and Javascript and file 182 00:19:11,010 --> 00:19:16,000 systems and other concurrency. I don't have time to talk about those but Hannes 183 00:19:16,000 --> 00:19:19,640 Mehnert it is going to talk us a little bit about TCP later today. You should go 184 00:19:19,640 --> 00:19:22,760 to that talk too if you like this one. If you don't like this one you should still 185 00:19:22,760 --> 00:19:33,169 go to that talk. Okay so this is doing somewhat better. certainly more rigorous 186 00:19:33,169 --> 00:19:41,519 engineering of specifications, but so far only for existing infrastructure for this 187 00:19:41,519 --> 00:19:49,539 C language, ARM architecture, what have you. So what if we try and do better, what 188 00:19:49,539 --> 00:19:54,750 if we try and build better security in. So the architectures that we have, really 189 00:19:54,750 --> 00:20:00,250 they date back to the 1970s or even 60s with the idea of virtual memory. That 190 00:20:00,250 --> 00:20:04,759 gives you - I need to go into what it is - but that gives you very coarse grain 191 00:20:04,759 --> 00:20:10,269 protection. You can have your separate processes isolated from each other and on 192 00:20:10,269 --> 00:20:15,350 a good day you might have separate browser tabs isolated from each other in some 193 00:20:15,350 --> 00:20:22,429 browsers, sometimes, but it doesn't scale. It's just too expensive. You have lots of 194 00:20:22,429 --> 00:20:27,090 little compartments. One thing we can do we can certainly design much better 195 00:20:27,090 --> 00:20:34,389 programming languages than C but all of that legacy code, that's got a massive 196 00:20:34,389 --> 00:20:40,520 inertia. So an obvious question is whether we can build in better security into the 197 00:20:40,520 --> 00:20:45,591 hardware that doesn't need some kind of massive pervasive change to all the 198 00:20:45,591 --> 00:20:51,409 software we ever wrote. And that's the question that a different large project, 199 00:20:51,409 --> 00:20:55,630 the CHERI project has been addressing. So this is something that's been going on for 200 00:20:55,630 --> 00:21:01,529 the last 8 years or so, mostly at SRI and at Cambridge funded by DARPA and the EPSRC 201 00:21:01,529 --> 00:21:06,570 and ARM and other people, mostly led by Robert Watson, Simon Moore, Peter Neumann 202 00:21:06,570 --> 00:21:14,660 and a cast of thousands. And me a tiny bit. So... How, don't do that. I should 203 00:21:14,660 --> 00:21:20,889 learn to stop pushing this button. It's very hard to not push the button. So 204 00:21:20,889 --> 00:21:25,190 here's the question in a more focused way that CHERI is asking: Can we build 205 00:21:25,190 --> 00:21:33,330 hardware support which is both efficient enough and deployable enough that gives us 206 00:21:33,330 --> 00:21:37,340 both fine grained memory protection to prevent that kind of bug that we were 207 00:21:37,340 --> 00:21:42,090 talking about earlier, well that kind of leak at least, and also scalable 208 00:21:42,090 --> 00:21:45,990 compartmentalization. So you can take bits of untrusted code and put them in safe 209 00:21:45,990 --> 00:21:52,879 boxes and know that nothing bad is going to get out. That's the question. The 210 00:21:52,879 --> 00:21:57,389 answer... The basic idea of the answer is pretty simple and it also dates back to 211 00:21:57,389 --> 00:22:02,800 the 70s is to add hardware support for what people call capabilities, and we'll 212 00:22:02,800 --> 00:22:07,840 see that working in a few moments. The idea is that this will let programmers 213 00:22:07,840 --> 00:22:12,460 exercise the principle of least privilege, so with each little bit of code having 214 00:22:12,460 --> 00:22:17,809 only the permissions it needs to do its job and also the principle of intentional 215 00:22:17,809 --> 00:22:25,790 use. So with each little bit of code when it uses one of those capabilities, will 216 00:22:25,790 --> 00:22:30,419 require it to explicitly use it rather than implicitly. So the intention of the 217 00:22:30,419 --> 00:22:36,129 code has to be made plain. So let's see how this works. So these capabilities 218 00:22:36,129 --> 00:22:44,120 they're basically replacing some or maybe all of the pointers in your code. So if we 219 00:22:44,120 --> 00:22:51,050 take this example again in ISO C we had an address and in the standard, well, the 220 00:22:51,050 --> 00:22:54,549 standard is not very clear about this but we're trying to make it more clear, an 221 00:22:54,549 --> 00:23:00,960 allocation ID, say something like it. Now in Cherry C we can run the same code but 222 00:23:00,960 --> 00:23:05,529 we might represent this pointer not just with that number at runtime but with 223 00:23:05,529 --> 00:23:12,769 something that contains that number and the base of the original allocation and 224 00:23:12,769 --> 00:23:17,399 the length of the original allocation and some permissions. And having all of those 225 00:23:17,399 --> 00:23:23,020 in the pointer means that we can do.. the hardware can do, at run time, at access 226 00:23:23,020 --> 00:23:29,530 time, a very efficient check that this is within this region of memory. And if it's 227 00:23:29,530 --> 00:23:36,269 not it can fail stop and trap. No information leak. I need a bit more 228 00:23:36,269 --> 00:23:41,090 machinery to make this actually work. So it would be nice if all of these were 64 229 00:23:41,090 --> 00:23:45,940 bit numbers but then you get a 256 bit pointer, and that's a bit expensive so 230 00:23:45,940 --> 00:23:52,789 there's a clever compression scheme that squeezes all this down into 1 to 8 bits 231 00:23:52,789 --> 00:24:00,299 with enough accuracy. And then you need to design the instruction set of the CPU 232 00:24:00,299 --> 00:24:07,390 carefully to ensure that you can never forge one of these capabilities with a 233 00:24:07,390 --> 00:24:13,120 normal instruction. You can never just magic one up out of a bunch of bits that 234 00:24:13,120 --> 00:24:19,710 you happen to find lying around. So all the capability manipulating instructions, 235 00:24:19,710 --> 00:24:27,159 they're going to take a valid capability and construct another, possibly smaller, 236 00:24:27,159 --> 00:24:32,020 in memory extent, or possibly with less permissions, new capability. They're never 237 00:24:32,020 --> 00:24:38,610 going to grow the memory extent or add permissions. And when the hardware starts, 238 00:24:38,610 --> 00:24:43,370 at hardware initialization time, the hardware will hand the software a 239 00:24:43,370 --> 00:24:48,909 capability to everything and then as the operating system works and the linker 240 00:24:48,909 --> 00:24:55,820 works and the C language allocator works, these capabilities will be chopped up into 241 00:24:55,820 --> 00:25:03,181 ever finer and smaller pieces like to be handed out the right places. And then need 242 00:25:03,181 --> 00:25:10,220 one more little thing. So this C language world we're living in here, or really a 243 00:25:10,220 --> 00:25:16,330 machine code language world so there's nothing stopping code writing bytes of 244 00:25:16,330 --> 00:25:23,340 stuff. So you have to somehow protect these capabilities against being forged by 245 00:25:23,340 --> 00:25:28,210 the code, either on purpose or accidentally writing bytes over the top. 246 00:25:28,210 --> 00:25:34,900 You need to preserve their integrity. So that's done by adding for each of these 247 00:25:34,900 --> 00:25:42,830 128 bit sized underlined units of memory just a one extra bit. That holds a tag and 248 00:25:42,830 --> 00:25:55,159 that tag records whether this memory holds are currently valid capability or not. So 249 00:25:55,159 --> 00:25:59,519 all the capability manipulating instructions, if they're given a valid 250 00:25:59,519 --> 00:26:06,100 capability with a tag set then the result will still have the tags set. But if you 251 00:26:06,100 --> 00:26:13,900 write, so you just wrote that byte there which might change the base then the 252 00:26:13,900 --> 00:26:20,230 hardware will clear that tag and these tags, they're not conventionally 253 00:26:20,230 --> 00:26:25,190 addressable, they don't have addresses. They just stop there in the memory system 254 00:26:25,190 --> 00:26:30,470 of the hardware. So there is no way that soft- ware can *inaudible* through these. So this is 255 00:26:30,470 --> 00:26:39,240 really cool. We've taken, what in ISO was undefined behavior, in the standard, and 256 00:26:39,240 --> 00:26:43,970 in implementations was a memory leak, and we've turned it into something that in 257 00:26:43,970 --> 00:26:49,200 CHERI C is in both the specification and the implementation, is guaranteed to trap, 258 00:26:49,200 --> 00:26:56,700 to fail stop, and not leak that information. So another few things about 259 00:26:56,700 --> 00:27:01,500 the design that I should mention. I think all these blue things I think I've talked 260 00:27:01,500 --> 00:27:07,610 about. But then a lot of care has gone in to make this be very flexible to make it 261 00:27:07,610 --> 00:27:12,499 possible to adopt it. So you can use capabilities for all pointers, if you want 262 00:27:12,499 --> 00:27:18,999 to, or just at some interfaces. You might for example use them at the kernel 263 00:27:18,999 --> 00:27:24,830 userspace interface. It coexist very nicely with existing C and C++. You don't 264 00:27:24,830 --> 00:27:29,139 need to change the source code very much at all, and we'll see some a tiny bit of 265 00:27:29,139 --> 00:27:36,860 data about this, to make these to start using these. It coexists with the existing 266 00:27:36,860 --> 00:27:41,140 virtual memory machinery, so you can use both capabilities and virtual memory, if 267 00:27:41,140 --> 00:27:45,960 you want, or you can just use capabilities if you want or just use virtual memory if 268 00:27:45,960 --> 00:27:50,940 you want. And then there's some more machinery, which I'm not going to talk 269 00:27:50,940 --> 00:27:54,999 about, for doing this secure encapsulation stuff. What I've talked about so far is 270 00:27:54,999 --> 00:27:59,440 basically the the fine grained memory protection story. And I should say the 271 00:27:59,440 --> 00:28:05,379 focus so far is on spatial memory safety. So that's not in the first instance 272 00:28:05,379 --> 00:28:11,450 protecting against reuse of an old capability in a bad way but there various 273 00:28:11,450 --> 00:28:17,711 schemes for supporting temporal memory safety with basically the same setup. Okay 274 00:28:17,711 --> 00:28:24,820 so. So how do we... Okay this is some kind of a high level idea. How do we know that 275 00:28:24,820 --> 00:28:32,669 it can be made to work. Well the only way is to actually build it and see. And this 276 00:28:32,669 --> 00:28:36,950 has been a really interesting process because mostly when you're building 277 00:28:36,950 --> 00:28:40,980 something either in academia or an industry you have to keep most of the 278 00:28:40,980 --> 00:28:46,730 parts fixed, I mean you are not routinely changing both the processor and the 279 00:28:46,730 --> 00:28:51,149 operating system, because that would just be too scary. But here we have been doing 280 00:28:51,149 --> 00:28:57,850 that and indeed we've really been doing a three way, three way codesign of building 281 00:28:57,850 --> 00:29:02,809 hardware and building and adapting software to run above it and also building 282 00:29:02,809 --> 00:29:09,249 these mathematical models all at the same time. This is, well. A, it's all the fun 283 00:29:09,249 --> 00:29:13,220 because you can often get groups of people together that can do all of those things 284 00:29:13,220 --> 00:29:20,269 but B, it's really effective. So what we've produced then is an architecture 285 00:29:20,269 --> 00:29:25,050 specification. In fact, extending MIPS because it was conveniently free of IP 286 00:29:25,050 --> 00:29:32,190 concerns and that specification is one of these mathematically rigorous things 287 00:29:32,190 --> 00:29:36,350 expressed in a domain specific language specifically for writing instruction set 288 00:29:36,350 --> 00:29:40,139 architecture specifications, and we've designed and implemented actually two of 289 00:29:40,139 --> 00:29:44,399 those. And then there are hardware processor implementations that actually 290 00:29:44,399 --> 00:29:49,249 run an FPGAs. And a lot of hardware research devoted to making this go fast 291 00:29:49,249 --> 00:29:54,379 and be efficient despite these extra tags and whatnot. And then there's a big 292 00:29:54,379 --> 00:30:00,669 software stack adapted to run over this stuff. Including Clang and a FreeBSD 293 00:30:00,669 --> 00:30:06,620 kernel and FreeBSD userspace and WebKit and all kinds of pieces. So this is a very 294 00:30:06,620 --> 00:30:12,309 major evaluation effort. That one is not normally able to do. This is why, this 295 00:30:12,309 --> 00:30:18,049 combination of things is why that list of people up there was about 40 people. I say 296 00:30:18,049 --> 00:30:22,559 this is based on MIPS but the ideas are not specific to MIPS, there are ongoing 297 00:30:22,559 --> 00:30:28,190 research projects to see if this can be adapted to the ARM application class 298 00:30:28,190 --> 00:30:32,580 architecture and the ARM microcontroller architecture and the RISC-V. We'll see how 299 00:30:32,580 --> 00:30:41,529 that goes, in due course. Okay so then with all of these pieces we can evaluate 300 00:30:41,529 --> 00:30:46,269 whether it actually works. And that's still kind of an ongoing process but the 301 00:30:46,269 --> 00:30:57,180 data that we've got so far is pretty encouraging. So we see here first, 302 00:30:57,180 --> 00:31:08,230 performance. So you see, maybe a percent or 2 in many cases of runtime overhead. 303 00:31:08,230 --> 00:31:11,500 There are workloads where it performs badly if you have something that's very 304 00:31:11,500 --> 00:31:17,270 pointer heavy, then the extra pressure from those larger pointers will be a bit 305 00:31:17,270 --> 00:31:24,090 annoying, but really it seems to be surprisingly good. Then is it something 306 00:31:24,090 --> 00:31:31,419 that can work without massive adaption to the existing code. Well, in this port of 307 00:31:31,419 --> 00:31:38,250 the FreeBSD userspace, so all the programs that, all in all programs that run, they 308 00:31:38,250 --> 00:31:45,120 were something like 20000 files and only 200 of those needed a change. And that's 309 00:31:45,120 --> 00:31:52,081 been done by one or two people in not all that large an amount of time. Some of the 310 00:31:52,081 --> 00:31:57,230 other code that's more and more like an operating system needs a bit more invasive 311 00:31:57,230 --> 00:32:06,070 change but still, it seems to be viable. Is it actually more secure? How are you 312 00:32:06,070 --> 00:32:10,710 going to measure that. We like measuring things as a whole we try and do science 313 00:32:10,710 --> 00:32:17,440 where we can. Can we measure that? Not really. But it certainly does, the whole 314 00:32:17,440 --> 00:32:23,299 setup certainly does, mitigate against quite a large family of known attacks. I 315 00:32:23,299 --> 00:32:28,260 mean if you try and run Heartbleed you'll get a trap. It will say trap. I think he 316 00:32:28,260 --> 00:32:36,499 will say signal 34 in fact. So that's pretty good. And if you think about 317 00:32:36,499 --> 00:32:42,950 attacks, very many of them involve a chain of multiple floors put together by an 318 00:32:42,950 --> 00:32:49,399 ingenious member of the C3 community or somebody else, and very often, at least 319 00:32:49,399 --> 00:33:00,119 one of those is some kind of memory access permission flaw of some kind or other. 320 00:33:00,119 --> 00:33:03,539 Okay so this is nice, but I was talking a lot in the first part of the talk, about 321 00:33:03,539 --> 00:33:11,920 rigorous engineering. So here we've got formally defined definitions of the 322 00:33:11,920 --> 00:33:16,779 architecture and that's been really useful for testing against and for doing test 323 00:33:16,779 --> 00:33:22,889 generation on the basis of, and doing specification coverage in an automated 324 00:33:22,889 --> 00:33:28,809 way. But surely we should be able to do more than that. So this formal definition 325 00:33:28,809 --> 00:33:34,860 of the architecture, what does it look like. So for each instruction of this 326 00:33:34,860 --> 00:33:40,669 CHERI MIPS processor, there's a definition and that definition, it looks a bit like 327 00:33:40,669 --> 00:33:47,980 normal code. So here's a definition of how the instruction for "capability increment 328 00:33:47,980 --> 00:33:54,159 cursor immediate" goes. So this is a thing that takes a capability register and an 329 00:33:54,159 --> 00:33:58,310 immediate value and it tries to add something on to the cursor of that 330 00:33:58,310 --> 00:34:03,640 capability. And what you see here is some code, looks like code, that defines 331 00:34:03,640 --> 00:34:06,830 exactly what happens and also defines exactly what happens if something goes 332 00:34:06,830 --> 00:34:13,140 wrong. You can see there's some kind of an exception case there. That's a processor. 333 00:34:13,140 --> 00:34:19,139 No that's a... Yeah, that a "raising our processor" exception. So it looks like 334 00:34:19,139 --> 00:34:25,270 code, but, from this, we can generate both reasonably high performance emulators, 335 00:34:25,270 --> 00:34:30,780 reasonably in C and in OCaml, and also mathematical models in the theorem 336 00:34:30,780 --> 00:34:34,770 provers. So three of the main theorem provers in the world are called Isabelle 337 00:34:34,770 --> 00:34:41,690 and HOL and Coq. And we generate definitions in all of those. So then we 338 00:34:41,690 --> 00:34:46,489 got a mathematical definition of the architecture. Then finally, we can start 339 00:34:46,489 --> 00:34:51,530 stating some properties. So Cherrie's design with some kind of vague security 340 00:34:51,530 --> 00:34:57,809 goals in mind from the beginning but now we can take, let'ssay one of those goals and 341 00:34:57,809 --> 00:35:06,569 make it into a precise thing. So this is a kind of a secure encapsulation, kind of 342 00:35:06,569 --> 00:35:12,540 thing not exactly the memory leak that we were looking at before. Sorry, the secret 343 00:35:12,540 --> 00:35:17,820 leak that we were looking at. So let's take imagine some CHERI compartment. 344 00:35:17,820 --> 00:35:22,020 Haven't told you exactly what that means but let's suppose that that's understood 345 00:35:22,020 --> 00:35:27,490 and that inside that compartment there is a piece of software running. And that 346 00:35:27,490 --> 00:35:35,559 might be maybe a video codec or a web browser or even a data structure 347 00:35:35,559 --> 00:35:44,410 implementation maybe, or a C++ class and all of its objects maybe. So imagine that 348 00:35:44,410 --> 00:35:50,049 compartment running and imagine the initial capabilities that it has access to 349 00:35:50,049 --> 00:35:55,640 via registers and memory and via all the capabilities it has access to via the 350 00:35:55,640 --> 00:35:59,510 memory that it has access to and so on recursively. So imagine all of those 351 00:35:59,510 --> 00:36:06,359 capabilities. So the theorem says no matter how this code executes whatever it 352 00:36:06,359 --> 00:36:15,730 does however compromised or buggy it was in an execution up until any point at 353 00:36:15,730 --> 00:36:24,020 which it raises an exception or makes an inter compartment call it can't make any 354 00:36:24,020 --> 00:36:30,530 access which is not allowed by those initial capabilities. You have to exclude 355 00:36:30,530 --> 00:36:35,230 exceptions and into compartment calls because by design they do introduce new 356 00:36:35,230 --> 00:36:42,690 capabilities into the execution. But until that point you get this guarantee. And 357 00:36:42,690 --> 00:36:48,849 this is something that we've proved actually [...] has approved with a machine 358 00:36:48,849 --> 00:36:55,980 check proof in in fact the Isabelle theorem prover. So this is a fact which is 359 00:36:55,980 --> 00:37:03,589 about as solidly known as any fact the human race knows. These provers they're 360 00:37:03,589 --> 00:37:10,450 checking a mathematical proof in exceedingly great detail with great care 361 00:37:10,450 --> 00:37:14,230 and attention and they're structured in such a way that the soundness of approver 362 00:37:14,230 --> 00:37:21,300 depends only on some tiny little kernel. So conceivably cosmic rays hit the 363 00:37:21,300 --> 00:37:27,230 transistors at all the wrong points. But basically we know this for sure. I 364 00:37:27,230 --> 00:37:34,299 emphasize this is a security property we have not proved, we certainly wouldn't 365 00:37:34,299 --> 00:37:39,440 claim to have proved that CHERI is secure and there are all kinds of other kinds of 366 00:37:39,440 --> 00:37:44,849 attack that this statement doesn't even address but at least this one property we 367 00:37:44,849 --> 00:37:49,880 know it for real. So that's kind of comforting and not a thing that 368 00:37:49,880 --> 00:38:01,420 conventional computer science engineering has been able to do on the whole. So, are 369 00:38:01,420 --> 00:38:10,750 we taming the chaos then. Well no. Sorry. But I've shown you two kinds of things. 370 00:38:10,750 --> 00:38:15,980 The first was showing how we can do somewhat more rigorous engineering for 371 00:38:15,980 --> 00:38:21,640 that existing infrastructure. It's now feasible to do that and in fact I believe 372 00:38:21,640 --> 00:38:26,370 it has been feasible to build specifications which you can use as test 373 00:38:26,370 --> 00:38:31,460 oracles for many decades. We haven't needed any super fancy new tech for that. 374 00:38:31,460 --> 00:38:41,140 We've just needed to focus on that idea. So that's for existing infrastructure and 375 00:38:41,140 --> 00:38:47,470 then CHERI is a relatively light weight change that does built-in improved 376 00:38:47,470 --> 00:38:53,520 security and we think it's demonstrably deployable at least in principle. Is it 377 00:38:53,520 --> 00:38:58,010 deployable in practice? Are we going to have in all of our phones five years from 378 00:38:58,010 --> 00:39:05,890 now? Will these all be CHERI enabled? I can't say. I think it is plausible that 379 00:39:05,890 --> 00:39:09,590 that should happen and we're exploring various routes that might mean that there 380 00:39:09,590 --> 00:39:20,260 happens and we'll see how that goes. Okay so with that I aiming to have given you at 381 00:39:20,260 --> 00:39:25,760 least not a whole lot of hope but just a little bit of hope that the world can be 382 00:39:25,760 --> 00:39:30,670 made a better place and I encourage you to think about ways to do it because Lord 383 00:39:30,670 --> 00:39:38,290 knows we need it. But maybe you can at least dream for a few moments of living in 384 00:39:38,290 --> 00:39:46,010 a better world. And with that I thank you for your attention. 385 00:39:46,010 --> 00:39:57,000 *applause* 386 00:39:57,000 --> 00:40:06,420 Herald Angel: Thanks very much. And with that we'll head straight into the Q and A. 387 00:40:06,420 --> 00:40:10,210 We'll just start with mic number one which I can see right now. 388 00:40:10,210 --> 00:40:15,720 Q: Yes thanks for the very encouraging talk. I have a question about how to C 389 00:40:15,720 --> 00:40:21,500 code the part below that. The theorem that you stated assumes that the mentioned 390 00:40:21,500 --> 00:40:28,200 description matches the hardware at least is describes the hardware accurately. But 391 00:40:28,200 --> 00:40:33,130 are there any attempts to check that the hardware actually works like that? That 392 00:40:33,130 --> 00:40:37,170 there are no wholes in the hardware? That some combination of mentioned commands 393 00:40:37,170 --> 00:40:42,980 work differently or allow memory access there is not in the model? So, is it 394 00:40:42,980 --> 00:40:48,990 possible to use hardware designs and check that it matches the spec and will Intel or 395 00:40:48,990 --> 00:40:53,730 AMD try to check their model against that spec? 396 00:40:53,730 --> 00:40:59,700 Sewell: OK. So the question is basically can we do provably correct hardware 397 00:40:59,700 --> 00:41:05,560 underneath this architectural abstraction. And the answer is... So it's a good 398 00:41:05,560 --> 00:41:12,700 question. People are working on that and it can be done I think on at least a 399 00:41:12,700 --> 00:41:22,130 modest academic scale. Trying to do that in its full glory for a industrial 400 00:41:22,130 --> 00:41:27,830 superscalar processor design, is right now out of reach. But it's certainly something 401 00:41:27,830 --> 00:41:35,259 one would like to be able to do. I think we will get there maybe in a decade or so. 402 00:41:35,259 --> 00:41:41,910 A decade is quick. Herald Angel: Thanks. Mic number four is 403 00:41:41,910 --> 00:41:48,471 empty again. So we'll take the Internet. Sewell: Where is the internet? 404 00:41:48,471 --> 00:41:53,359 Signal Angel: The internet is right here and everywhere so ruminate would like to 405 00:41:53,359 --> 00:41:59,960 know is the effort and cost of building in security to hardware as you've described in your 406 00:41:59,960 --> 00:42:05,880 talk significantly greater or less than the effort and cost of porting software to 407 00:42:05,880 --> 00:42:12,059 more secure languages. Sewell: So, is the effort of building new 408 00:42:12,059 --> 00:42:17,349 hardware more or less than the cost of porting existing software to better 409 00:42:17,349 --> 00:42:26,280 languages? I think the answer has to be yes. It is less. The difficulty with 410 00:42:26,280 --> 00:42:30,700 porting software is all of you and all your colleagues and all of your friends 411 00:42:30,700 --> 00:42:36,009 and all your enemies have been beavering away writing lines of code for 50 years. 412 00:42:36,009 --> 00:42:42,409 Really, I don't know what to say, effectively. Really numerously. There's an 413 00:42:42,409 --> 00:42:46,280 awful lot of it. It's a really terrifying amount of code out there. It's very hard 414 00:42:46,280 --> 00:42:54,388 to get people to rewrite it. Signal Angel: OK, mic two. 415 00:42:54,388 --> 00:43:03,029 Q: OK, given that cost of ... of today on the software level not on the hardware level, is it 416 00:43:03,029 --> 00:43:11,940 possible to go half way using an entire system as an oracle. So during development 417 00:43:11,940 --> 00:43:19,280 there are code based with the secure hardware but then essentially ship the 418 00:43:19,280 --> 00:43:28,859 same software to unsecure hardware and *inaudible* Sewell: So this question, if I paraphrase 419 00:43:28,859 --> 00:43:35,819 it is can we use this hardware implementation really as the perfect 420 00:43:35,819 --> 00:43:45,020 sanitiser? And I think there is scope for doing that. And you can even imagine 421 00:43:45,020 --> 00:43:49,750 running this not on actual silicon hardware but in like a QEMU implementation 422 00:43:49,750 --> 00:43:54,819 which we have in order to do that. And I think for for that purpose it could 423 00:43:54,819 --> 00:44:00,720 already be a pretty effective bug finding tool. It would be worth doing. But you 424 00:44:00,720 --> 00:44:06,250 would like as for any testing it will only explore a very tiny fraction of the 425 00:44:06,250 --> 00:44:13,539 possible paths. So we would like to have it always on if we possibly can. 426 00:44:13,539 --> 00:44:19,690 Herald Angel: OK. The internet again. Signal Angel: OK someone would like to 427 00:44:19,690 --> 00:44:26,130 know how does your technique compare to Intel MPX which failed miserably with a *inaudible* 428 00:44:26,130 --> 00:44:33,820 ignoring it. Will it better or faster? Could you talk a little bit about that. 429 00:44:33,820 --> 00:44:38,400 Sewell: I think for that question, for a real answer to that question, you would 430 00:44:38,400 --> 00:44:45,549 need one of my more hardware colleagues. What I can say is they make nasty faces 431 00:44:45,549 --> 00:44:53,450 when you say MPX. Herald Angel: Well that's that. Mic number 432 00:44:53,450 --> 00:44:56,880 one. Q: Somewhat inherent to your whole 433 00:44:56,880 --> 00:45:02,460 construction was this idea of having an unchangeable bit which described whether 434 00:45:02,460 --> 00:45:08,539 your pointer contents have been changed. Is this even something that can be done in 435 00:45:08,539 --> 00:45:12,850 software? Or do you have to construct a whole extra RAM or something? 436 00:45:12,850 --> 00:45:21,309 Sewell: So you can't do it exclusively in software because you need to protect it. 437 00:45:21,309 --> 00:45:25,550 In the hardware implementations that my colleagues have built it's done in a 438 00:45:25,550 --> 00:45:32,700 reasonably efficient way. So it's cached and managed in clever ways to ensure that 439 00:45:32,700 --> 00:45:38,730 it's not terribly expensive to do. But you do need slightly wider data paths in your 440 00:45:38,730 --> 00:45:45,460 cache protocol and things like that to manage it. 441 00:45:45,460 --> 00:45:51,527 Herald Angel: OK. Mic seven. Q: How good does this system help securing 442 00:45:51,527 --> 00:45:56,850 the control flow integrity compared to compared to other systems, like hardware 443 00:45:56,850 --> 00:46:03,870 systems data flow isolation or code pointer integrity in ARM *inaudible*? 444 00:46:03,870 --> 00:46:09,310 Sewell: Ah well, that's another question which is a bit hard to answer because then 445 00:46:09,310 --> 00:46:18,179 it depends somewhat on how you're using the capabilities. So you can arrange here 446 00:46:18,179 --> 00:46:25,549 that each state each C language allocation is independently protected and indeed you 447 00:46:25,549 --> 00:46:30,470 can also arrange that each way - this is sensible - that each subobject is 448 00:46:30,470 --> 00:46:34,920 independent protected. And those protections are going to give you 449 00:46:34,920 --> 00:46:39,310 protection against trashing bits of the stack because they'll restrict the 450 00:46:39,310 --> 00:46:50,669 capability to just those objects. Herald Angel: OK the internet again. 451 00:46:50,669 --> 00:46:57,740 Signal Angel: Twitter would like to know is it possible to is it possible to run 452 00:46:57,740 --> 00:47:04,289 CHERI C without custom hardware? Sewell: Can you run CHERI C without custom 453 00:47:04,289 --> 00:47:12,950 hardware? And the answer is you can run it in emulation above this QEMU. That works 454 00:47:12,950 --> 00:47:18,040 pretty fast, I mean fast enough for debugging as the earlier question was 455 00:47:18,040 --> 00:47:28,609 talking about. You can imagine you know somewhat faster emulations of that. It's 456 00:47:28,609 --> 00:47:34,340 not clear how much it's worth going down that route. The real potential big win is 457 00:47:34,340 --> 00:47:41,240 to have this be always on and that's what we would like to have. 458 00:47:41,240 --> 00:47:47,390 Herald Angel: OK. Mic one. Q: Do you have some examples of the kinds 459 00:47:47,390 --> 00:47:51,900 of code changes that you need to the operating system and userland that you 460 00:47:51,900 --> 00:47:55,859 mentioned? Sewell: So, okay so what kind of changes 461 00:47:55,859 --> 00:48:07,140 do you need to to adapt code to CHERI? So, if you look at C-code there is the C 462 00:48:07,140 --> 00:48:12,520 standard that deems a whole lot of things to be undefined behavior and then if you 463 00:48:12,520 --> 00:48:19,940 look at actual C code you find that very very much of it does depend on some idiom 464 00:48:19,940 --> 00:48:28,650 that the C standard does not approve of. So there is for example, *pause* there are 465 00:48:28,650 --> 00:48:34,740 quite a lot of instances of code that constructs a pointer by doing more than 466 00:48:34,740 --> 00:48:42,380 one more than plus one offset and then brings it back within range before you use 467 00:48:42,380 --> 00:48:49,450 it. So in fact in CHERI C many of those cases are allowed but not all of them. 468 00:48:49,450 --> 00:48:58,200 More exotic cases where there's really some crazy into object stuff going on or 469 00:48:58,200 --> 00:49:03,339 where pointer arithmetic between objects - which the C standard is certainly quite 470 00:49:03,339 --> 00:49:09,290 down on but which does happen - and code which is, say manipulating the low order 471 00:49:09,290 --> 00:49:13,549 bits of a pointer to store some data in it. That's pretty common. You can do it in 472 00:49:13,549 --> 00:49:18,170 CHERI C but you might have to adapt the code a little bit. Other cases are more 473 00:49:18,170 --> 00:49:22,849 fundamental. So say, in operating system code if you swap out a page to disk and 474 00:49:22,849 --> 00:49:28,460 then you swap it back in then somehow the operating system has to reconstruct new 475 00:49:28,460 --> 00:49:35,200 capabilities from a large capability which it kept for the purpose. So that needs a 476 00:49:35,200 --> 00:49:41,869 bit more work. Though it's kind of a combination. Some things you would regard 477 00:49:41,869 --> 00:49:48,320 as good changes to the code anyway and others are more radical. 478 00:49:48,320 --> 00:49:51,600 Herald Angel: OK, another one from the internet. 479 00:49:51,600 --> 00:50:00,000 Signal Angel: I lost one *pause* Sewell: The Internet has gone quiet. Yes. 480 00:50:00,000 --> 00:50:04,420 Signal Angel: Last question from the internet. Are there any plans to impact 481 00:50:04,420 --> 00:50:11,950 test on Linux or just FreeBSD? Sewell: If anyone has a good number of 482 00:50:11,950 --> 00:50:19,980 spare minutes then that would be lovely to try. The impact on Linux not just 483 00:50:19,980 --> 00:50:26,400 previously the BSD code base is simpler and maybe cleaner and my systemsy 484 00:50:26,400 --> 00:50:30,230 colleagues are already familiar with it. It's the obvious target for an academic 485 00:50:30,230 --> 00:50:35,260 project doing it already a humungous amount of work. So I think we would love 486 00:50:35,260 --> 00:50:40,910 to know how Linux and especially how Android could be adapted but it's not 487 00:50:40,910 --> 00:50:46,259 something that we have the resource to do at the moment. 488 00:50:46,259 --> 00:50:50,710 Herald Angel: Mic number on again. Q: How likely or dangerous. 489 00:50:50,710 --> 00:50:55,460 Herald Angel: Mic number one is not working. 490 00:50:55,460 --> 00:50:59,540 Q: How likely or dangerous you think it is for a programmer to screw up their 491 00:50:59,540 --> 00:51:05,329 capabilities he specifies? Sewell: So how often will the programmer 492 00:51:05,329 --> 00:51:10,750 screw up the capabilities? So in many cases the programmer is just doing an 493 00:51:10,750 --> 00:51:17,370 access with a C or C++ pointer or C++ object in a normal way. They're not 494 00:51:17,370 --> 00:51:23,560 manually constructing these things. So a lot of that is going to just work. If 495 00:51:23,560 --> 00:51:28,170 you're building some particular secure encapsulation setup you have to be a bit 496 00:51:28,170 --> 00:51:34,280 careful. But on the whole I think this is a small risk compared to the state of 497 00:51:34,280 --> 00:51:40,960 software as we have it now. Herald Angel: OK. Mic eight. 498 00:51:40,960 --> 00:51:49,220 Q: So existing memory protection techniques are quite patch-worky, like 499 00:51:49,220 --> 00:52:06,160 canaries and address layout randomisation. Is this a system designed to replace or 500 00:52:06,160 --> 00:52:17,920 supplement these measures? Sewell: I think if you *pause* So again it 501 00:52:17,920 --> 00:52:24,480 depends a bit how you use it. So if you have capabilities really everywhere then 502 00:52:24,480 --> 00:52:33,240 there's not much need for address space layout randomization or canaries to 503 00:52:33,240 --> 00:52:41,829 protect against explicit information leaks. I imagine that you might still want 504 00:52:41,829 --> 00:52:48,500 randomisation to protect against some side channel flows but canaries is not so much 505 00:52:48,500 --> 00:52:51,539 on whether you actually do for side- channel flows - I don't know. That's a 506 00:52:51,539 --> 00:52:56,500 good question. Herald Angel: Mic four please. 507 00:52:56,500 --> 00:53:02,580 Q: Thanks for the very interesting talk you presented with CHERI, a system of 508 00:53:02,580 --> 00:53:07,529 veryfying existing C-software, sort of post hoc and improving its security via 509 00:53:07,529 --> 00:53:12,450 run-time mechanism...? A: Improving or Proving? Improving yes, 510 00:53:12,450 --> 00:53:18,560 proving no, yes. Q: So what's your opinion on the viability 511 00:53:18,560 --> 00:53:23,020 of using a static analysis and static verification for that. Would it be 512 00:53:23,020 --> 00:53:29,579 possible to somehow analyse software that already exist and as written in these 513 00:53:29,579 --> 00:53:34,089 unsafe languages and show that it nevertheless has some security properties 514 00:53:34,089 --> 00:53:40,830 without writing all the proofs manually in like HOL or Isabelle? 515 00:53:40,830 --> 00:53:47,050 A: Well so if you want to analyse existing software... So, static analysis is already 516 00:53:47,050 --> 00:53:53,029 useful for finding bugs in existing software. If you want to have assurance 517 00:53:53,029 --> 00:53:58,869 from static analysis, that's really very tough. So you certainly wouldn't want to 518 00:53:58,869 --> 00:54:07,430 manually write proofs in terms of the definitional C semantics, you would need 519 00:54:07,430 --> 00:54:10,849 intermediate infrastructure. And if you look at the people, who have done verified 520 00:54:10,849 --> 00:54:15,750 software, so verified compilers and verified hypervisor, and verified 521 00:54:15,750 --> 00:54:25,029 operating systems, all of those are now possible on significant scales, but they 522 00:54:25,029 --> 00:54:30,510 use whole layers of proof and verification infrastructure for doing that. They're not 523 00:54:30,510 --> 00:54:35,829 writing proofs by hand for every little detail. And some of those verification 524 00:54:35,829 --> 00:54:42,180 methods either are, you can imagine them being basically like static analysis, you 525 00:54:42,180 --> 00:54:47,690 know, you might use a static analysis to prove some relatively simple facts about 526 00:54:47,690 --> 00:54:54,820 the code and then stitch those together into a larger assembly. I think any kind 527 00:54:54,820 --> 00:54:59,170 of more complete thing I think is hard to imagine. I mean these analysis tools 528 00:54:59,170 --> 00:55:03,339 mostly, they rely on making some approximation in order to be able to do 529 00:55:03,339 --> 00:55:09,750 their thing at all. So it's hard to get assurance out of them. 530 00:55:09,750 --> 00:55:16,869 Herald Angel: Okay, Mic one. Q: You said you modified an MIPS 531 00:55:16,869 --> 00:55:22,740 architecture to add some logic to check their capabilities. Do you know what the cost of 532 00:55:22,740 --> 00:55:30,219 this regarding computational power, an energetic power supply? 533 00:55:30,219 --> 00:55:33,030 A: Sorry, can you repeat the last part of that? 534 00:55:33,030 --> 00:55:39,190 Q: What the cost of this modification regarding computational power, and power 535 00:55:39,190 --> 00:55:42,300 consumption. A: Ah, so what's the energy cost? So I 536 00:55:42,300 --> 00:55:46,609 gave you a performance cost. I didn't give you, I carefully didn't give you an energy 537 00:55:46,609 --> 00:55:52,599 cost estimate, because it's really hard to do in a scientifically credible way, 538 00:55:52,599 --> 00:55:59,250 without making a more or less production superscalar implementation. And we are 539 00:55:59,250 --> 00:56:03,500 sadly not in a position to do that, although if you have 10 or 20 million 540 00:56:03,500 --> 00:56:09,249 pounds, then I would be happy to accept it. 541 00:56:09,249 --> 00:56:15,220 Herald Angel: Mic number 7, please. Q: How does the class of problems that you 542 00:56:15,220 --> 00:56:21,440 can address with CHERI compare to the class of problems that are excluded by, 543 00:56:21,440 --> 00:56:26,680 for example, the Rust programming language? 544 00:56:26,680 --> 00:56:30,460 A: So how does the problems of CHERI relate to the problems, sorry the problems 545 00:56:30,460 --> 00:56:39,529 excluded by CHERI, relate to the problems excluded by Rust. So if you are happy to 546 00:56:39,529 --> 00:56:50,859 write all of your code in Rust without ever using the word "unsafe", then maybe 547 00:56:50,859 --> 00:56:56,240 there would be no point in CHERI, at all. Are you happy to do that? 548 00:56:56,240 --> 00:57:00,750 Q: Probably not, no. A: I think someone shakes their head 549 00:57:00,750 --> 00:57:10,000 sideways, yeah. Herald Angel: Mic number 1. 550 00:57:10,000 --> 00:57:14,640 Q: What do you think about the following thesis: We are building a whole system of 551 00:57:14,640 --> 00:57:21,109 things, with artificial intelligence and something like that. That is above this 552 00:57:21,109 --> 00:57:29,760 technical level and it's building another chaos that isn't healing with those 553 00:57:29,760 --> 00:57:34,009 things. A: It's dreadful, isn't it. 554 00:57:34,009 --> 00:57:45,700 *Laughter* A: There are, so you might, in fact some 555 00:57:45,700 --> 00:57:50,320 of my colleagues are interested in this question, if you, you might well want to 556 00:57:50,320 --> 00:57:58,819 bound what your artificial intelligence can access or touch and for that you might 557 00:57:58,819 --> 00:58:03,720 want this kind of technology. But this is not, we are, with machine learning systems 558 00:58:03,720 --> 00:58:07,410 we are intrinsically building things that we, on the whole, don't understand and 559 00:58:07,410 --> 00:58:11,960 that will have edge cases that go wrong. And this is not speaking to that in any 560 00:58:11,960 --> 00:58:17,240 way. Herald Angel: OK. Does the internet have a 561 00:58:17,240 --> 00:58:24,793 question? No, good. I don't see anyone else, so let's conclude this. Thank you 562 00:58:24,793 --> 00:58:28,932 very much. A: Thank you. 563 00:58:28,932 --> 00:58:30,289 *applause* 564 00:58:30,289 --> 00:58:35,930 *35c3 postroll music* 565 00:58:35,930 --> 00:58:53,000 subtitles created by c3subtitles.de in the year 2019. Join, and help us!