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!