WEBVTT
00:00:00.000 --> 00:00:18.010
35C3 preroll music
00:00:18.010 --> 00:00:29.239
Herald angel: OK. Our next speaker will be
trying to tame the chaos. Peter Sewell
00:00:29.239 --> 00:00:34.120
from the University of Cambridge. A warm
round of applause please.
00:00:34.120 --> 00:00:37.910
applause
00:00:37.910 --> 00:00:48.740
Sewell: Thank you! Okay. So here we are.
C3 again with a program full of
00:00:48.740 --> 00:00:56.710
fascinating and exciting and cool stuff.
And if we look just at the security talks
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
00:00:59.940 --> 00:01:06.830
too. Let's see though if we read some of
the titles: exploiting kernel memory
00:01:06.830 --> 00:01:18.750
corruptions, attacking end to end e-mail
encryption. What else have we got: modern
00:01:18.750 --> 00:01:31.550
Windows user space exploitation,
compromising online accounts. OK so a lot
00:01:31.550 --> 00:01:36.130
of these talks, as usual, they're
explaining to us that our computers,
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
00:01:42.950 --> 00:01:48.970
iceberg, alright. We have a hundreds of
thousands of known vulnerabilities and
00:01:48.970 --> 00:01:53.280
many unknown vulnerabilities. Let me do it
a bit dark here, but let me try some
00:01:53.280 --> 00:01:59.490
audience participation. How many of you
have in the last year written at least a
00:01:59.490 --> 00:02:09.019
hundred lines of code? And of those people
keep your hands up if you are completely
00:02:09.019 --> 00:02:17.550
confident that code does the right thing.
laughter I would like to talk to you
00:02:17.550 --> 00:02:23.200
later laughter and so would the people
in the self driving car that you're
00:02:23.200 --> 00:02:30.790
probably engineering. So, so how many
unknown vulnerabilities then. Well you can
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
00:02:39.160 --> 00:02:48.920
well. No. No, no. Computers, they do the
wrong thing again and again and again.
00:02:48.920 --> 00:02:54.421
laughter and some applause We can
multiply by this estimate of about a 100
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
00:03:00.630 --> 00:03:05.900
numbers, these should make us not happy
and excited, these should make us sad,
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
00:03:16.070 --> 00:03:25.610
do? We can, option one, give up using
computers altogether. applause In most
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
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
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
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
00:04:00.050 --> 00:04:04.099
slightly better. But if we want to do
better we first have to understand why
00:04:04.099 --> 00:04:10.560
things are so bad and if we look at our
aeronautical engineering colleagues for
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
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
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
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
00:04:35.990 --> 00:04:40.160
much information in this, it's just ace.
So we see down here all of this
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
00:04:45.430 --> 00:04:51.241
C compiler, we see all kinds of other
other bits and pieces. There might be a
00:04:51.241 --> 00:04:58.870
slightly hostile wireless environment in
this room for some reason. If we look at
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
00:05:03.230 --> 00:05:07.889
terrible things. So the first is,
obviously there's a lot of legacy
00:05:07.889 --> 00:05:12.810
complexity that we're really stuck with,
alright. If you pull out one of those
00:05:12.810 --> 00:05:16.240
pieces from the middle and try and replace
it with something which is not of exactly
00:05:16.240 --> 00:05:21.350
the same shape the whole pile will
collapse. So we somehow need to find an
00:05:21.350 --> 00:05:27.970
incremental path to a better world. And
then, this is the most fundamental reason
00:05:27.970 --> 00:05:33.220
that these are not like aeroplanes, these
systems are discrete not continuous. If
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
00:05:38.290 --> 00:05:44.270
bit it moves a little bit, basically in
proportion. If it is 1 percent too strong,
00:05:44.270 --> 00:05:50.090
1 percent to weak, basically it doesn't
matter. But in these things one line of
00:05:50.090 --> 00:05:56.490
code can mean you're open to a
catastrophic exploit and one line in many,
00:05:56.490 --> 00:06:05.970
many million. OK. And next thing... this
really doesn't work. They're very
00:06:05.970 --> 00:06:11.380
complicated. But the scary thing is not
the static complexity of those lines of
00:06:11.380 --> 00:06:15.080
code and the number of components although
that's pretty intimidating the really
00:06:15.080 --> 00:06:21.110
scary thing is that the exponential number
of states and execution paths. So these
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
00:06:26.139 --> 00:06:30.710
have to build systems which are not
instantly broken. Testing can never save
00:06:30.710 --> 00:06:40.550
us from these exploitable errors. And that
means ultimately we need to do proof.
00:06:40.550 --> 00:06:45.610
Honest machine checked mathematical proof.
And this also tells us that we need to
00:06:45.610 --> 00:06:51.289
arrange for our systems to be secure for
simple reasons that do not depend on the
00:06:51.289 --> 00:06:57.180
correctness of all of those hundred
billion lines of code. Then another thing
00:06:57.180 --> 00:07:03.360
that we have here. All these interfaces:
the architecture interface, the C language
00:07:03.360 --> 00:07:10.650
interface, the sockets API interface, the
TCP interface. All of these we rely on to
00:07:10.650 --> 00:07:17.500
let different parts of the system be
engineered by different organizations. But
00:07:17.500 --> 00:07:24.870
they're all really badly described and
badly defined. So what you find is, for
00:07:24.870 --> 00:07:30.130
each of these, typically a prose book
varying in thickness between about that
00:07:30.130 --> 00:07:36.909
and about that, full of text. Well, we
still rely on testing - limited though it
00:07:36.909 --> 00:07:44.000
is - but you can never test anything
against those books. So we need instead
00:07:44.000 --> 00:07:48.940
interface descriptions, definitions,
specifications, that are more rigorous,
00:07:48.940 --> 00:07:54.419
mathematically rigorous and that are
executable - not in the normal sense of
00:07:54.419 --> 00:07:58.940
executable as an implementation but
executable as a test oracle. So you can
00:07:58.940 --> 00:08:03.880
compute whether some observed behaviour is
allowed or not and not have to read the
00:08:03.880 --> 00:08:07.700
book and argue on the Internet. And we
also need interface definitions that
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
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
00:08:25.639 --> 00:08:32.068
walked around with flowers in their hair
and nothing bad ever happened. And that is
00:08:32.068 --> 00:08:36.340
no longer the case. And so we need
defensive design, but we need defensive
00:08:36.340 --> 00:08:41.149
design that is somehow compatible or can
be made enough compatible with this legacy
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
00:08:46.879 --> 00:08:50.360
have at the moment very bad incentives,
because we have a very strong incentive to
00:08:50.360 --> 00:08:55.420
make things that are more complex than we
can possibly handle or understand. We make
00:08:55.420 --> 00:09:00.410
things, we add features, we make a thing
which is just about shippable and then we
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
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
00:09:11.300 --> 00:09:17.109
talk about those until we have the
technical means to react to those
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
00:09:21.980 --> 00:09:26.230
interfaces, the architect interface and
the C language interface, and see what we
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
00:09:32.819 --> 00:09:38.209
was that picked the subtitle for this
meeting "refreshing memories" thank you,
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
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
00:09:52.959 --> 00:09:58.519
hacking was going on. Charles Babbage was
designing the Analytical Engine and even
00:09:58.519 --> 00:10:03.369
then you see there was this dichotomy
between a mill performing operations and a
00:10:03.369 --> 00:10:11.100
store holding numbers. This is a plan view
of the analytical engine, well, it was
00:10:11.100 --> 00:10:15.240
vaporware, but a design from the
analytical engine, and you see here these
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
00:10:21.689 --> 00:10:28.340
digit decimal number in each of those
columns. And this array, really, he
00:10:28.340 --> 00:10:34.681
imagined it going on out to and over there
somewhere, with about 1000 numbers. So
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-
00:10:42.850 --> 00:10:46.519
I don't think you could do address
computation on these things, I think
00:10:46.519 --> 00:10:53.649
addresses were only constants, but, still,
basically an array of numbers. So okay
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
00:10:59.370 --> 00:11:06.980
programmed 100 lines of code, how many of
you were C programmers? Quite a few. Or
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
00:11:12.660 --> 00:11:18.499
for that first question. You should feel
proud and you should glory in your
00:11:18.499 --> 00:11:26.460
innocence while you still have it. You are
not yet complicit in this trainwreck. It
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
00:11:31.680 --> 00:11:38.279
explain it in several different ways. So
we start out. It creates two locations x
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
00:11:52.670 --> 00:11:58.980
which stores, I might get this wrong, your
pin. And then there's some computation
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
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
00:12:13.620 --> 00:12:21.209
happened to be allocated at 14. This
pointer contains the number 14 and then we
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
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
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
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
00:12:48.549 --> 00:12:54.300
secret key. Bad. This program, rather
distressingly, this is characteristic by
00:12:54.300 --> 00:12:58.830
no means of all security flaws but a very
disturbingly large fraction of all the
00:12:58.830 --> 00:13:10.600
security flaws are basically doing this.
So does C really let you do that. Yes and
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
00:13:17.911 --> 00:13:22.859
says you, have to read moderately
carefully to understand this, but it says
00:13:22.859 --> 00:13:27.399
for this program has undefined behavior.
And many of you will know what that means
00:13:27.399 --> 00:13:32.949
but others won't, but, so that means as
far as the standard is concerned for
00:13:32.949 --> 00:13:39.329
programs like that there is no constraint
on the behavior of the implementation at
00:13:39.329 --> 00:13:47.039
all. Or said another way and maybe a more
usefully way: The standard lets
00:13:47.039 --> 00:13:52.329
implementations, so C compilers, assume
that programmers don't have this kind of
00:13:52.329 --> 00:13:59.569
stuff and it's the programmer's
responsibility to ensure that. Now in
00:13:59.569 --> 00:14:04.781
about 1970, 75 maybe 1980, this was a
really good idea, it gives compilers a lot
00:14:04.781 --> 00:14:14.000
of flexibility to do efficient
implementation. Now not so much. How does
00:14:14.000 --> 00:14:19.199
this work in the definition? So the
standard somehow has to be able to look at
00:14:19.199 --> 00:14:29.470
this program and identify it as having
this undefined behavior. And indeed, well,
00:14:29.470 --> 00:14:37.089
if we just think about the numbers in
memory this 18, it points to a perfectly
00:14:37.089 --> 00:14:42.189
legitimate storage location and that plus
one was also something that you're
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
00:14:48.149 --> 00:14:54.419
undefined behavior is to keep track of the
original allocation of this pointer. And
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
00:14:59.240 --> 00:15:03.689
still got this pointer despite the fact
that I added 4 to it. I still remembered
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
00:15:09.939 --> 00:15:15.290
from this whether that address is within
the footprint of that original allocation,
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
00:15:19.019 --> 00:15:25.509
there at all. So this program is deemed to
have undefined behavior. Just to clarify
00:15:25.509 --> 00:15:30.649
something people often get confused. So we
detect undefined behavior here but it
00:15:30.649 --> 00:15:35.299
isn't really a temporal thing. The fact
that there is undefined behavior anywhere
00:15:35.299 --> 00:15:41.790
in the execution means the whole program
is toast. Okay but this is really
00:15:41.790 --> 00:15:46.339
interesting because we're relying for this
critical part of the standard onto
00:15:46.339 --> 00:15:52.319
information which is not there at run time
in a conventional implementation. So just
00:15:52.319 --> 00:15:59.050
to emphasize that point, if I compile this
program, let's say to ARM assembly
00:15:59.050 --> 00:16:04.850
language I get a sequence of store and
load and add instructions, store, load,
00:16:04.850 --> 00:16:12.089
add, store, load, load. And if I look at
what the ARM architecture says can happen
00:16:12.089 --> 00:16:17.139
these blue transitions... one thing to
notice is that we can perfectly well do
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
00:16:21.639 --> 00:16:27.240
that store. That would be a whole other
talk. Let's stick with the sequential
00:16:27.240 --> 00:16:33.100
execution for now. What I want to
emphasize is that these, this load of this
00:16:33.100 --> 00:16:36.569
address, really was loading a 64 bit
number, which was the address of x and
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
00:16:44.419 --> 00:16:55.910
trace of these allocation ideas. No trace
at all. Okay, let me step back a little
00:16:55.910 --> 00:17:04.939
bit. I've been showing you some
screenshots of C behaviour and ARM
00:17:04.939 --> 00:17:12.109
behaviour and I claim that these are
actually showing you all of the behaviours
00:17:12.109 --> 00:17:19.359
allowed by what one would like the
standards to be for these two things. And
00:17:19.359 --> 00:17:26.529
really what I've been showing you are GUIs
attached to mathematical models that we've
00:17:26.529 --> 00:17:31.000
built in a big research project for the
last many years. REMS: "Rigorous
00:17:31.000 --> 00:17:34.929
Engineering of Mainstream Systems" sounds
good, aspirational title I think I would
00:17:34.929 --> 00:17:42.049
say. And in that we've built semantics, so
mathematical models defining the envelope
00:17:42.049 --> 00:17:47.580
of all allowed behaviour for a quite big
fragment of C and for the concurrency
00:17:47.580 --> 00:17:53.950
architecture of major processors ARM, and
x86, and RISC-V, and IBM POWER and also
00:17:53.950 --> 00:17:57.770
for the instruction set architecture of
these processors, the details of how
00:17:57.770 --> 00:18:03.940
individual instructions are executed. And
in each case these are specs that are
00:18:03.940 --> 00:18:08.350
executable as test oracles, you can
compare algorithmically some observed
00:18:08.350 --> 00:18:13.320
behaviour against whether spec says it's
allowed or not, which you can't do with
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
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.
00:18:26.960 --> 00:18:30.710
These are also mathematical models, I'll
come back to that later. But another thing
00:18:30.710 --> 00:18:34.529
I want to emphasize here is that in each
of these cases, especially these first
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
00:18:40.669 --> 00:18:44.400
build a nice clean mathematical model of
something which is well understood. What
00:18:44.400 --> 00:18:50.540
you learn is that there are real open
questions. For example within the C
00:18:50.540 --> 00:18:55.759
standards committee and within ARM a few
years ago about exactly what these things
00:18:55.759 --> 00:19:01.130
even were. And that is a bit disturbing
given that these are the foundations for
00:19:01.130 --> 00:19:06.009
all of our information infrastructure.
There is also a lot of other work going on
00:19:06.009 --> 00:19:11.010
with other people within this REMS project
on web assembly and Javascript and file
00:19:11.010 --> 00:19:16.000
systems and other concurrency. I don't
have time to talk about those but Hannes
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
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
00:19:22.760 --> 00:19:33.169
go to that talk. Okay so this is doing
somewhat better. certainly more rigorous
00:19:33.169 --> 00:19:41.519
engineering of specifications, but so far
only for existing infrastructure for this
00:19:41.519 --> 00:19:49.539
C language, ARM architecture, what have
you. So what if we try and do better, what
00:19:49.539 --> 00:19:54.750
if we try and build better security in. So
the architectures that we have, really
00:19:54.750 --> 00:20:00.250
they date back to the 1970s or even 60s
with the idea of virtual memory. That
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
00:20:04.759 --> 00:20:10.269
protection. You can have your separate
processes isolated from each other and on
00:20:10.269 --> 00:20:15.350
a good day you might have separate browser
tabs isolated from each other in some
00:20:15.350 --> 00:20:22.429
browsers, sometimes, but it doesn't scale.
It's just too expensive. You have lots of
00:20:22.429 --> 00:20:27.090
little compartments. One thing we can do
we can certainly design much better
00:20:27.090 --> 00:20:34.389
programming languages than C but all of
that legacy code, that's got a massive
00:20:34.389 --> 00:20:40.520
inertia. So an obvious question is whether
we can build in better security into the
00:20:40.520 --> 00:20:45.591
hardware that doesn't need some kind of
massive pervasive change to all the
00:20:45.591 --> 00:20:51.409
software we ever wrote. And that's the
question that a different large project,
00:20:51.409 --> 00:20:55.630
the CHERI project has been addressing. So
this is something that's been going on for
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
00:21:01.529 --> 00:21:06.570
and ARM and other people, mostly led by
Robert Watson, Simon Moore, Peter Neumann
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
00:21:14.660 --> 00:21:20.889
learn to stop pushing this button. It's
very hard to not push the button. So
00:21:20.889 --> 00:21:25.190
here's the question in a more focused way
that CHERI is asking: Can we build
00:21:25.190 --> 00:21:33.330
hardware support which is both efficient
enough and deployable enough that gives us
00:21:33.330 --> 00:21:37.340
both fine grained memory protection to
prevent that kind of bug that we were
00:21:37.340 --> 00:21:42.090
talking about earlier, well that kind of
leak at least, and also scalable
00:21:42.090 --> 00:21:45.990
compartmentalization. So you can take bits
of untrusted code and put them in safe
00:21:45.990 --> 00:21:52.879
boxes and know that nothing bad is going
to get out. That's the question. The
00:21:52.879 --> 00:21:57.389
answer... The basic idea of the answer is
pretty simple and it also dates back to
00:21:57.389 --> 00:22:02.800
the 70s is to add hardware support for
what people call capabilities, and we'll
00:22:02.800 --> 00:22:07.840
see that working in a few moments. The
idea is that this will let programmers
00:22:07.840 --> 00:22:12.460
exercise the principle of least privilege,
so with each little bit of code having
00:22:12.460 --> 00:22:17.809
only the permissions it needs to do its
job and also the principle of intentional
00:22:17.809 --> 00:22:25.790
use. So with each little bit of code when
it uses one of those capabilities, will
00:22:25.790 --> 00:22:30.419
require it to explicitly use it rather
than implicitly. So the intention of the
00:22:30.419 --> 00:22:36.129
code has to be made plain. So let's see
how this works. So these capabilities
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
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
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
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
00:23:00.960 --> 00:23:05.529
we might represent this pointer not just
with that number at runtime but with
00:23:05.529 --> 00:23:12.769
something that contains that number and
the base of the original allocation and
00:23:12.769 --> 00:23:17.399
the length of the original allocation and
some permissions. And having all of those
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
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
00:23:29.530 --> 00:23:36.269
not it can fail stop and trap. No
information leak. I need a bit more
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
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
00:23:45.940 --> 00:23:52.789
there's a clever compression scheme that
squeezes all this down into 1 to 8 bits
00:23:52.789 --> 00:24:00.299
with enough accuracy. And then you need to
design the instruction set of the CPU
00:24:00.299 --> 00:24:07.390
carefully to ensure that you can never
forge one of these capabilities with a
00:24:07.390 --> 00:24:13.120
normal instruction. You can never just
magic one up out of a bunch of bits that
00:24:13.120 --> 00:24:19.710
you happen to find lying around. So all
the capability manipulating instructions,
00:24:19.710 --> 00:24:27.159
they're going to take a valid capability
and construct another, possibly smaller,
00:24:27.159 --> 00:24:32.020
in memory extent, or possibly with less
permissions, new capability. They're never
00:24:32.020 --> 00:24:38.610
going to grow the memory extent or add
permissions. And when the hardware starts,
00:24:38.610 --> 00:24:43.370
at hardware initialization time, the
hardware will hand the software a
00:24:43.370 --> 00:24:48.909
capability to everything and then as the
operating system works and the linker
00:24:48.909 --> 00:24:55.820
works and the C language allocator works,
these capabilities will be chopped up into
00:24:55.820 --> 00:25:03.181
ever finer and smaller pieces like to be
handed out the right places. And then need
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
00:25:10.220 --> 00:25:16.330
machine code language world so there's
nothing stopping code writing bytes of
00:25:16.330 --> 00:25:23.340
stuff. So you have to somehow protect
these capabilities against being forged by
00:25:23.340 --> 00:25:28.210
the code, either on purpose or
accidentally writing bytes over the top.
00:25:28.210 --> 00:25:34.900
You need to preserve their integrity. So
that's done by adding for each of these
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
00:25:42.830 --> 00:25:55.159
that tag records whether this memory holds
are currently valid capability or not. So
00:25:55.159 --> 00:25:59.519
all the capability manipulating
instructions, if they're given a valid
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
00:26:06.100 --> 00:26:13.900
write, so you just wrote that byte there
which might change the base then the
00:26:13.900 --> 00:26:20.230
hardware will clear that tag and these
tags, they're not conventionally
00:26:20.230 --> 00:26:25.190
addressable, they don't have addresses.
They just stop there in the memory system
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
00:26:30.470 --> 00:26:39.240
really cool. We've taken, what in ISO was
undefined behavior, in the standard, and
00:26:39.240 --> 00:26:43.970
in implementations was a memory leak, and
we've turned it into something that in
00:26:43.970 --> 00:26:49.200
CHERI C is in both the specification and
the implementation, is guaranteed to trap,
00:26:49.200 --> 00:26:56.700
to fail stop, and not leak that
information. So another few things about
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
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
00:27:07.610 --> 00:27:12.499
possible to adopt it. So you can use
capabilities for all pointers, if you want
00:27:12.499 --> 00:27:18.999
to, or just at some interfaces. You might
for example use them at the kernel
00:27:18.999 --> 00:27:24.830
userspace interface. It coexist very
nicely with existing C and C++. You don't
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
00:27:29.139 --> 00:27:36.860
data about this, to make these to start
using these. It coexists with the existing
00:27:36.860 --> 00:27:41.140
virtual memory machinery, so you can use
both capabilities and virtual memory, if
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
00:27:45.960 --> 00:27:50.940
you want. And then there's some more
machinery, which I'm not going to talk
00:27:50.940 --> 00:27:54.999
about, for doing this secure encapsulation
stuff. What I've talked about so far is
00:27:54.999 --> 00:27:59.440
basically the the fine grained memory
protection story. And I should say the
00:27:59.440 --> 00:28:05.379
focus so far is on spatial memory safety.
So that's not in the first instance
00:28:05.379 --> 00:28:11.450
protecting against reuse of an old
capability in a bad way but there various
00:28:11.450 --> 00:28:17.711
schemes for supporting temporal memory
safety with basically the same setup. Okay
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
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
00:28:32.669 --> 00:28:36.950
has been a really interesting process
because mostly when you're building
00:28:36.950 --> 00:28:40.980
something either in academia or an
industry you have to keep most of the
00:28:40.980 --> 00:28:46.730
parts fixed, I mean you are not routinely
changing both the processor and the
00:28:46.730 --> 00:28:51.149
operating system, because that would just
be too scary. But here we have been doing
00:28:51.149 --> 00:28:57.850
that and indeed we've really been doing a
three way, three way codesign of building
00:28:57.850 --> 00:29:02.809
hardware and building and adapting
software to run above it and also building
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
00:29:09.249 --> 00:29:13.220
because you can often get groups of people
together that can do all of those things
00:29:13.220 --> 00:29:20.269
but B, it's really effective. So what
we've produced then is an architecture
00:29:20.269 --> 00:29:25.050
specification. In fact, extending MIPS
because it was conveniently free of IP
00:29:25.050 --> 00:29:32.190
concerns and that specification is one of
these mathematically rigorous things
00:29:32.190 --> 00:29:36.350
expressed in a domain specific language
specifically for writing instruction set
00:29:36.350 --> 00:29:40.139
architecture specifications, and we've
designed and implemented actually two of
00:29:40.139 --> 00:29:44.399
those. And then there are hardware
processor implementations that actually
00:29:44.399 --> 00:29:49.249
run an FPGAs. And a lot of hardware
research devoted to making this go fast
00:29:49.249 --> 00:29:54.379
and be efficient despite these extra tags
and whatnot. And then there's a big
00:29:54.379 --> 00:30:00.669
software stack adapted to run over this
stuff. Including Clang and a FreeBSD
00:30:00.669 --> 00:30:06.620
kernel and FreeBSD userspace and WebKit
and all kinds of pieces. So this is a very
00:30:06.620 --> 00:30:12.309
major evaluation effort. That one is not
normally able to do. This is why, this
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
00:30:18.049 --> 00:30:22.559
this is based on MIPS but the ideas are
not specific to MIPS, there are ongoing
00:30:22.559 --> 00:30:28.190
research projects to see if this can be
adapted to the ARM application class
00:30:28.190 --> 00:30:32.580
architecture and the ARM microcontroller
architecture and the RISC-V. We'll see how
00:30:32.580 --> 00:30:41.529
that goes, in due course. Okay so then
with all of these pieces we can evaluate
00:30:41.529 --> 00:30:46.269
whether it actually works. And that's
still kind of an ongoing process but the
00:30:46.269 --> 00:30:57.180
data that we've got so far is pretty
encouraging. So we see here first,
00:30:57.180 --> 00:31:08.230
performance. So you see, maybe a percent
or 2 in many cases of runtime overhead.
00:31:08.230 --> 00:31:11.500
There are workloads where it performs
badly if you have something that's very
00:31:11.500 --> 00:31:17.270
pointer heavy, then the extra pressure
from those larger pointers will be a bit
00:31:17.270 --> 00:31:24.090
annoying, but really it seems to be
surprisingly good. Then is it something
00:31:24.090 --> 00:31:31.419
that can work without massive adaption to
the existing code. Well, in this port of
00:31:31.419 --> 00:31:38.250
the FreeBSD userspace, so all the programs
that, all in all programs that run, they
00:31:38.250 --> 00:31:45.120
were something like 20000 files and only
200 of those needed a change. And that's
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
00:31:52.081 --> 00:31:57.230
other code that's more and more like an
operating system needs a bit more invasive
00:31:57.230 --> 00:32:06.070
change but still, it seems to be viable.
Is it actually more secure? How are you
00:32:06.070 --> 00:32:10.710
going to measure that. We like measuring
things as a whole we try and do science
00:32:10.710 --> 00:32:17.440
where we can. Can we measure that? Not
really. But it certainly does, the whole
00:32:17.440 --> 00:32:23.299
setup certainly does, mitigate against
quite a large family of known attacks. I
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
00:32:28.260 --> 00:32:36.499
will say signal 34 in fact. So that's
pretty good. And if you think about
00:32:36.499 --> 00:32:42.950
attacks, very many of them involve a chain
of multiple floors put together by an
00:32:42.950 --> 00:32:49.399
ingenious member of the C3 community or
somebody else, and very often, at least
00:32:49.399 --> 00:33:00.119
one of those is some kind of memory access
permission flaw of some kind or other.
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
00:33:03.539 --> 00:33:11.920
rigorous engineering. So here we've got
formally defined definitions of the
00:33:11.920 --> 00:33:16.779
architecture and that's been really useful
for testing against and for doing test
00:33:16.779 --> 00:33:22.889
generation on the basis of, and doing
specification coverage in an automated
00:33:22.889 --> 00:33:28.809
way. But surely we should be able to do
more than that. So this formal definition
00:33:28.809 --> 00:33:34.860
of the architecture, what does it look
like. So for each instruction of this
00:33:34.860 --> 00:33:40.669
CHERI MIPS processor, there's a definition
and that definition, it looks a bit like
00:33:40.669 --> 00:33:47.980
normal code. So here's a definition of how
the instruction for "capability increment
00:33:47.980 --> 00:33:54.159
cursor immediate" goes. So this is a thing
that takes a capability register and an
00:33:54.159 --> 00:33:58.310
immediate value and it tries to add
something on to the cursor of that
00:33:58.310 --> 00:34:03.640
capability. And what you see here is some
code, looks like code, that defines
00:34:03.640 --> 00:34:06.830
exactly what happens and also defines
exactly what happens if something goes
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.
00:34:13.140 --> 00:34:19.139
No that's a... Yeah, that a "raising our
processor" exception. So it looks like
00:34:19.139 --> 00:34:25.270
code, but, from this, we can generate both
reasonably high performance emulators,
00:34:25.270 --> 00:34:30.780
reasonably in C and in OCaml, and also
mathematical models in the theorem
00:34:30.780 --> 00:34:34.770
provers. So three of the main theorem
provers in the world are called Isabelle
00:34:34.770 --> 00:34:41.690
and HOL and Coq. And we generate
definitions in all of those. So then we
00:34:41.690 --> 00:34:46.489
got a mathematical definition of the
architecture. Then finally, we can start
00:34:46.489 --> 00:34:51.530
stating some properties. So Cherrie's
design with some kind of vague security
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
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
00:35:06.569 --> 00:35:12.540
thing not exactly the memory leak that we
were looking at before. Sorry, the secret
00:35:12.540 --> 00:35:17.820
leak that we were looking at. So let's
take imagine some CHERI compartment.
00:35:17.820 --> 00:35:22.020
Haven't told you exactly what that means
but let's suppose that that's understood
00:35:22.020 --> 00:35:27.490
and that inside that compartment there is
a piece of software running. And that
00:35:27.490 --> 00:35:35.559
might be maybe a video codec or a web
browser or even a data structure
00:35:35.559 --> 00:35:44.410
implementation maybe, or a C++ class and
all of its objects maybe. So imagine that
00:35:44.410 --> 00:35:50.049
compartment running and imagine the
initial capabilities that it has access to
00:35:50.049 --> 00:35:55.640
via registers and memory and via all the
capabilities it has access to via the
00:35:55.640 --> 00:35:59.510
memory that it has access to and so on
recursively. So imagine all of those
00:35:59.510 --> 00:36:06.359
capabilities. So the theorem says no
matter how this code executes whatever it
00:36:06.359 --> 00:36:15.730
does however compromised or buggy it was
in an execution up until any point at
00:36:15.730 --> 00:36:24.020
which it raises an exception or makes an
inter compartment call it can't make any
00:36:24.020 --> 00:36:30.530
access which is not allowed by those
initial capabilities. You have to exclude
00:36:30.530 --> 00:36:35.230
exceptions and into compartment calls
because by design they do introduce new
00:36:35.230 --> 00:36:42.690
capabilities into the execution. But until
that point you get this guarantee. And
00:36:42.690 --> 00:36:48.849
this is something that we've proved
actually [...] has approved with a machine
00:36:48.849 --> 00:36:55.980
check proof in in fact the Isabelle
theorem prover. So this is a fact which is
00:36:55.980 --> 00:37:03.589
about as solidly known as any fact the
human race knows. These provers they're
00:37:03.589 --> 00:37:10.450
checking a mathematical proof in
exceedingly great detail with great care
00:37:10.450 --> 00:37:14.230
and attention and they're structured in
such a way that the soundness of approver
00:37:14.230 --> 00:37:21.300
depends only on some tiny little kernel.
So conceivably cosmic rays hit the
00:37:21.300 --> 00:37:27.230
transistors at all the wrong points. But
basically we know this for sure. I
00:37:27.230 --> 00:37:34.299
emphasize this is a security property we
have not proved, we certainly wouldn't
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
00:37:39.440 --> 00:37:44.849
attack that this statement doesn't even
address but at least this one property we
00:37:44.849 --> 00:37:49.880
know it for real. So that's kind of
comforting and not a thing that
00:37:49.880 --> 00:38:01.420
conventional computer science engineering
has been able to do on the whole. So, are
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.
00:38:10.750 --> 00:38:15.980
The first was showing how we can do
somewhat more rigorous engineering for
00:38:15.980 --> 00:38:21.640
that existing infrastructure. It's now
feasible to do that and in fact I believe
00:38:21.640 --> 00:38:26.370
it has been feasible to build
specifications which you can use as test
00:38:26.370 --> 00:38:31.460
oracles for many decades. We haven't
needed any super fancy new tech for that.
00:38:31.460 --> 00:38:41.140
We've just needed to focus on that idea.
So that's for existing infrastructure and
00:38:41.140 --> 00:38:47.470
then CHERI is a relatively light weight
change that does built-in improved
00:38:47.470 --> 00:38:53.520
security and we think it's demonstrably
deployable at least in principle. Is it
00:38:53.520 --> 00:38:58.010
deployable in practice? Are we going to
have in all of our phones five years from
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
00:39:05.890 --> 00:39:09.590
that should happen and we're exploring
various routes that might mean that there
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
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
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
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
00:39:38.290 --> 00:39:46.010
a better world. And with that I thank you
for your attention.
00:39:46.010 --> 00:39:57.000
applause
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.
00:40:06.420 --> 00:40:10.210
We'll just start with mic number one which
I can see right now.
00:40:10.210 --> 00:40:15.720
Q: Yes thanks for the very encouraging
talk. I have a question about how to C
00:40:15.720 --> 00:40:21.500
code the part below that. The theorem that
you stated assumes that the mentioned
00:40:21.500 --> 00:40:28.200
description matches the hardware at least
is describes the hardware accurately. But
00:40:28.200 --> 00:40:33.130
are there any attempts to check that the
hardware actually works like that? That
00:40:33.130 --> 00:40:37.170
there are no wholes in the hardware? That
some combination of mentioned commands
00:40:37.170 --> 00:40:42.980
work differently or allow memory access
there is not in the model? So, is it
00:40:42.980 --> 00:40:48.990
possible to use hardware designs and check
that it matches the spec and will Intel or
00:40:48.990 --> 00:40:53.730
AMD try to check their model against that
spec?
00:40:53.730 --> 00:40:59.700
Sewell: OK. So the question is basically
can we do provably correct hardware
00:40:59.700 --> 00:41:05.560
underneath this architectural abstraction.
And the answer is... So it's a good
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
00:41:12.700 --> 00:41:22.130
modest academic scale. Trying to do that
in its full glory for a industrial
00:41:22.130 --> 00:41:27.830
superscalar processor design, is right now
out of reach. But it's certainly something
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.
00:41:35.259 --> 00:41:41.910
A decade is quick.
Herald Angel: Thanks. Mic number four is
00:41:41.910 --> 00:41:48.471
empty again. So we'll take the Internet.
Sewell: Where is the internet?
00:41:48.471 --> 00:41:53.359
Signal Angel: The internet is right here
and everywhere so ruminate would like to
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
00:41:59.960 --> 00:42:05.880
talk significantly greater or less than
the effort and cost of porting software to
00:42:05.880 --> 00:42:12.059
more secure languages.
Sewell: So, is the effort of building new
00:42:12.059 --> 00:42:17.349
hardware more or less than the cost of
porting existing software to better
00:42:17.349 --> 00:42:26.280
languages? I think the answer has to be
yes. It is less. The difficulty with
00:42:26.280 --> 00:42:30.700
porting software is all of you and all
your colleagues and all of your friends
00:42:30.700 --> 00:42:36.009
and all your enemies have been beavering
away writing lines of code for 50 years.
00:42:36.009 --> 00:42:42.409
Really, I don't know what to say,
effectively. Really numerously. There's an
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
00:42:46.280 --> 00:42:54.388
to get people to rewrite it.
Signal Angel: OK, mic two.
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
00:43:03.029 --> 00:43:11.940
possible to go half way using an entire
system as an oracle. So during development
00:43:11.940 --> 00:43:19.280
there are code based with the secure
hardware but then essentially ship the
00:43:19.280 --> 00:43:28.859
same software to unsecure hardware and inaudible
Sewell: So this question, if I paraphrase
00:43:28.859 --> 00:43:35.819
it is can we use this hardware
implementation really as the perfect
00:43:35.819 --> 00:43:45.020
sanitiser? And I think there is scope for
doing that. And you can even imagine
00:43:45.020 --> 00:43:49.750
running this not on actual silicon
hardware but in like a QEMU implementation
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
00:43:54.819 --> 00:44:00.720
already be a pretty effective bug finding
tool. It would be worth doing. But you
00:44:00.720 --> 00:44:06.250
would like as for any testing it will only
explore a very tiny fraction of the
00:44:06.250 --> 00:44:13.539
possible paths. So we would like to have
it always on if we possibly can.
00:44:13.539 --> 00:44:19.690
Herald Angel: OK. The internet again.
Signal Angel: OK someone would like to
00:44:19.690 --> 00:44:26.130
know how does your technique compare to
Intel MPX which failed miserably with a inaudible
00:44:26.130 --> 00:44:33.820
ignoring it. Will it better or faster?
Could you talk a little bit about that.
00:44:33.820 --> 00:44:38.400
Sewell: I think for that question, for a
real answer to that question, you would
00:44:38.400 --> 00:44:45.549
need one of my more hardware colleagues.
What I can say is they make nasty faces
00:44:45.549 --> 00:44:53.450
when you say MPX.
Herald Angel: Well that's that. Mic number
00:44:53.450 --> 00:44:56.880
one.
Q: Somewhat inherent to your whole
00:44:56.880 --> 00:45:02.460
construction was this idea of having an
unchangeable bit which described whether
00:45:02.460 --> 00:45:08.539
your pointer contents have been changed.
Is this even something that can be done in
00:45:08.539 --> 00:45:12.850
software? Or do you have to construct a
whole extra RAM or something?
00:45:12.850 --> 00:45:21.309
Sewell: So you can't do it exclusively in
software because you need to protect it.
00:45:21.309 --> 00:45:25.550
In the hardware implementations that my
colleagues have built it's done in a
00:45:25.550 --> 00:45:32.700
reasonably efficient way. So it's cached
and managed in clever ways to ensure that
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
00:45:38.730 --> 00:45:45.460
cache protocol and things like that to
manage it.
00:45:45.460 --> 00:45:51.527
Herald Angel: OK. Mic seven.
Q: How good does this system help securing
00:45:51.527 --> 00:45:56.850
the control flow integrity compared to
compared to other systems, like hardware
00:45:56.850 --> 00:46:03.870
systems data flow isolation or code
pointer integrity in ARM inaudible?
00:46:03.870 --> 00:46:09.310
Sewell: Ah well, that's another question
which is a bit hard to answer because then
00:46:09.310 --> 00:46:18.179
it depends somewhat on how you're using
the capabilities. So you can arrange here
00:46:18.179 --> 00:46:25.549
that each state each C language allocation
is independently protected and indeed you
00:46:25.549 --> 00:46:30.470
can also arrange that each way - this is
sensible - that each subobject is
00:46:30.470 --> 00:46:34.920
independent protected. And those
protections are going to give you
00:46:34.920 --> 00:46:39.310
protection against trashing bits of the
stack because they'll restrict the
00:46:39.310 --> 00:46:50.669
capability to just those objects.
Herald Angel: OK the internet again.
00:46:50.669 --> 00:46:57.740
Signal Angel: Twitter would like to know
is it possible to is it possible to run
00:46:57.740 --> 00:47:04.289
CHERI C without custom hardware?
Sewell: Can you run CHERI C without custom
00:47:04.289 --> 00:47:12.950
hardware? And the answer is you can run it
in emulation above this QEMU. That works
00:47:12.950 --> 00:47:18.040
pretty fast, I mean fast enough for
debugging as the earlier question was
00:47:18.040 --> 00:47:28.609
talking about. You can imagine you know
somewhat faster emulations of that. It's
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
00:47:34.340 --> 00:47:41.240
to have this be always on and that's what
we would like to have.
00:47:41.240 --> 00:47:47.390
Herald Angel: OK. Mic one.
Q: Do you have some examples of the kinds
00:47:47.390 --> 00:47:51.900
of code changes that you need to the
operating system and userland that you
00:47:51.900 --> 00:47:55.859
mentioned?
Sewell: So, okay so what kind of changes
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
00:48:07.140 --> 00:48:12.520
standard that deems a whole lot of things
to be undefined behavior and then if you
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
00:48:19.940 --> 00:48:28.650
that the C standard does not approve of.
So there is for example, pause there are
00:48:28.650 --> 00:48:34.740
quite a lot of instances of code that
constructs a pointer by doing more than
00:48:34.740 --> 00:48:42.380
one more than plus one offset and then
brings it back within range before you use
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.
00:48:49.450 --> 00:48:58.200
More exotic cases where there's really
some crazy into object stuff going on or
00:48:58.200 --> 00:49:03.339
where pointer arithmetic between objects -
which the C standard is certainly quite
00:49:03.339 --> 00:49:09.290
down on but which does happen - and code
which is, say manipulating the low order
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
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
00:49:18.170 --> 00:49:22.849
fundamental. So say, in operating system
code if you swap out a page to disk and
00:49:22.849 --> 00:49:28.460
then you swap it back in then somehow the
operating system has to reconstruct new
00:49:28.460 --> 00:49:35.200
capabilities from a large capability which
it kept for the purpose. So that needs a
00:49:35.200 --> 00:49:41.869
bit more work. Though it's kind of a
combination. Some things you would regard
00:49:41.869 --> 00:49:48.320
as good changes to the code anyway and
others are more radical.
00:49:48.320 --> 00:49:51.600
Herald Angel: OK, another one from the
internet.
00:49:51.600 --> 00:50:00.000
Signal Angel: I lost one pause
Sewell: The Internet has gone quiet. Yes.
00:50:00.000 --> 00:50:04.420
Signal Angel: Last question from the
internet. Are there any plans to impact
00:50:04.420 --> 00:50:11.950
test on Linux or just FreeBSD?
Sewell: If anyone has a good number of
00:50:11.950 --> 00:50:19.980
spare minutes then that would be lovely to
try. The impact on Linux not just
00:50:19.980 --> 00:50:26.400
previously the BSD code base is simpler
and maybe cleaner and my systemsy
00:50:26.400 --> 00:50:30.230
colleagues are already familiar with it.
It's the obvious target for an academic
00:50:30.230 --> 00:50:35.260
project doing it already a humungous
amount of work. So I think we would love
00:50:35.260 --> 00:50:40.910
to know how Linux and especially how
Android could be adapted but it's not
00:50:40.910 --> 00:50:46.259
something that we have the resource to do
at the moment.
00:50:46.259 --> 00:50:50.710
Herald Angel: Mic number on again.
Q: How likely or dangerous.
00:50:50.710 --> 00:50:55.460
Herald Angel: Mic number one is not
working.
00:50:55.460 --> 00:50:59.540
Q: How likely or dangerous you think it is
for a programmer to screw up their
00:50:59.540 --> 00:51:05.329
capabilities he specifies?
Sewell: So how often will the programmer
00:51:05.329 --> 00:51:10.750
screw up the capabilities? So in many
cases the programmer is just doing an
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
00:51:17.370 --> 00:51:23.560
manually constructing these things. So a
lot of that is going to just work. If
00:51:23.560 --> 00:51:28.170
you're building some particular secure
encapsulation setup you have to be a bit
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
00:51:34.280 --> 00:51:40.960
software as we have it now.
Herald Angel: OK. Mic eight.
00:51:40.960 --> 00:51:49.220
Q: So existing memory protection
techniques are quite patch-worky, like
00:51:49.220 --> 00:52:06.160
canaries and address layout randomisation.
Is this a system designed to replace or
00:52:06.160 --> 00:52:17.920
supplement these measures?
Sewell: I think if you pause So again it
00:52:17.920 --> 00:52:24.480
depends a bit how you use it. So if you
have capabilities really everywhere then
00:52:24.480 --> 00:52:33.240
there's not much need for address space
layout randomization or canaries to
00:52:33.240 --> 00:52:41.829
protect against explicit information
leaks. I imagine that you might still want
00:52:41.829 --> 00:52:48.500
randomisation to protect against some side
channel flows but canaries is not so much
00:52:48.500 --> 00:52:51.539
on whether you actually do for side-
channel flows - I don't know. That's a
00:52:51.539 --> 00:52:56.500
good question.
Herald Angel: Mic four please.
00:52:56.500 --> 00:53:02.580
Q: Thanks for the very interesting talk
you presented with CHERI, a system of
00:53:02.580 --> 00:53:07.529
veryfying existing C-software, sort of
post hoc and improving its security via
00:53:07.529 --> 00:53:12.450
run-time mechanism...?
A: Improving or Proving? Improving yes,
00:53:12.450 --> 00:53:18.560
proving no, yes.
Q: So what's your opinion on the viability
00:53:18.560 --> 00:53:23.020
of using a static analysis and static
verification for that. Would it be
00:53:23.020 --> 00:53:29.579
possible to somehow analyse software that
already exist and as written in these
00:53:29.579 --> 00:53:34.089
unsafe languages and show that it
nevertheless has some security properties
00:53:34.089 --> 00:53:40.830
without writing all the proofs manually in
like HOL or Isabelle?
00:53:40.830 --> 00:53:47.050
A: Well so if you want to analyse existing
software... So, static analysis is already
00:53:47.050 --> 00:53:53.029
useful for finding bugs in existing
software. If you want to have assurance
00:53:53.029 --> 00:53:58.869
from static analysis, that's really very
tough. So you certainly wouldn't want to
00:53:58.869 --> 00:54:07.430
manually write proofs in terms of the
definitional C semantics, you would need
00:54:07.430 --> 00:54:10.849
intermediate infrastructure. And if you
look at the people, who have done verified
00:54:10.849 --> 00:54:15.750
software, so verified compilers and
verified hypervisor, and verified
00:54:15.750 --> 00:54:25.029
operating systems, all of those are now
possible on significant scales, but they
00:54:25.029 --> 00:54:30.510
use whole layers of proof and verification
infrastructure for doing that. They're not
00:54:30.510 --> 00:54:35.829
writing proofs by hand for every little
detail. And some of those verification
00:54:35.829 --> 00:54:42.180
methods either are, you can imagine them
being basically like static analysis, you
00:54:42.180 --> 00:54:47.690
know, you might use a static analysis to
prove some relatively simple facts about
00:54:47.690 --> 00:54:54.820
the code and then stitch those together
into a larger assembly. I think any kind
00:54:54.820 --> 00:54:59.170
of more complete thing I think is hard to
imagine. I mean these analysis tools
00:54:59.170 --> 00:55:03.339
mostly, they rely on making some
approximation in order to be able to do
00:55:03.339 --> 00:55:09.750
their thing at all. So it's hard to get
assurance out of them.
00:55:09.750 --> 00:55:16.869
Herald Angel: Okay, Mic one.
Q: You said you modified an MIPS
00:55:16.869 --> 00:55:22.740
architecture to add some logic to check their
capabilities. Do you know what the cost of
00:55:22.740 --> 00:55:30.219
this regarding computational power,
an energetic power supply?
00:55:30.219 --> 00:55:33.030
A: Sorry, can you repeat the last part of
that?
00:55:33.030 --> 00:55:39.190
Q: What the cost of this modification
regarding computational power, and power
00:55:39.190 --> 00:55:42.300
consumption.
A: Ah, so what's the energy cost? So I
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
00:55:46.609 --> 00:55:52.599
cost estimate, because it's really hard to
do in a scientifically credible way,
00:55:52.599 --> 00:55:59.250
without making a more or less production
superscalar implementation. And we are
00:55:59.250 --> 00:56:03.500
sadly not in a position to do that,
although if you have 10 or 20 million
00:56:03.500 --> 00:56:09.249
pounds, then I would be happy to accept
it.
00:56:09.249 --> 00:56:15.220
Herald Angel: Mic number 7, please.
Q: How does the class of problems that you
00:56:15.220 --> 00:56:21.440
can address with CHERI compare to the
class of problems that are excluded by,
00:56:21.440 --> 00:56:26.680
for example, the Rust programming
language?
00:56:26.680 --> 00:56:30.460
A: So how does the problems of CHERI
relate to the problems, sorry the problems
00:56:30.460 --> 00:56:39.529
excluded by CHERI, relate to the problems
excluded by Rust. So if you are happy to
00:56:39.529 --> 00:56:50.859
write all of your code in Rust without
ever using the word "unsafe", then maybe
00:56:50.859 --> 00:56:56.240
there would be no point in CHERI, at all.
Are you happy to do that?
00:56:56.240 --> 00:57:00.750
Q: Probably not, no.
A: I think someone shakes their head
00:57:00.750 --> 00:57:10.000
sideways, yeah.
Herald Angel: Mic number 1.
00:57:10.000 --> 00:57:14.640
Q: What do you think about the following
thesis: We are building a whole system of
00:57:14.640 --> 00:57:21.109
things, with artificial intelligence and
something like that. That is above this
00:57:21.109 --> 00:57:29.760
technical level and it's building another
chaos that isn't healing with those
00:57:29.760 --> 00:57:34.009
things.
A: It's dreadful, isn't it.
00:57:34.009 --> 00:57:45.700
Laughter
A: There are, so you might, in fact some
00:57:45.700 --> 00:57:50.320
of my colleagues are interested in this
question, if you, you might well want to
00:57:50.320 --> 00:57:58.819
bound what your artificial intelligence
can access or touch and for that you might
00:57:58.819 --> 00:58:03.720
want this kind of technology. But this is
not, we are, with machine learning systems
00:58:03.720 --> 00:58:07.410
we are intrinsically building things that
we, on the whole, don't understand and
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
00:58:11.960 --> 00:58:17.240
way.
Herald Angel: OK. Does the internet have a
00:58:17.240 --> 00:58:24.793
question? No, good. I don't see anyone
else, so let's conclude this. Thank you
00:58:24.793 --> 00:58:28.932
very much.
A: Thank you.
00:58:28.932 --> 00:58:30.289
applause
00:58:30.289 --> 00:58:35.930
35c3 postroll music
00:58:35.930 --> 00:58:53.000
subtitles created by c3subtitles.de
in the year 2019. Join, and help us!