*35C3 preroll music*
Herald angel: OK. Our next speaker will be trying to tame the chaos. Peter Sewell
from the University of Cambridge. A warm round of applause please.
*applause*
Sewell: Thank you! Okay. So here we are. C3 again with a program full of
fascinating and exciting and cool stuff. And if we look just at the security talks
all manner of interesting things. I'm going to go to a lot to these. You should
too. Let's see though if we read some of the titles: exploiting kernel memory
corruptions, attacking end to end e-mail encryption. What else have we got: modern
Windows user space exploitation, compromising online accounts. OK so a lot
of these talks, as usual, they're explaining to us that our computers,
they're not doing what we would like and this as usual is the merest tip of a tiny
iceberg, alright. We have a hundreds of thousands of known vulnerabilities and
many unknown vulnerabilities. Let me do it a bit dark here, but let me try some
audience participation. How many of you have in the last year written at least a
hundred lines of code? And of those people keep your hands up if you are completely
confident that code does the right thing. *laughter* I would like to talk to you
later *laughter* and so would the people in the self driving car that you're
probably engineering. So, so how many unknown vulnerabilities then. Well you can
take what's in your mind right now and multiply it by - oh, this doesnt work very
well. No. No, no. Computers, they do the wrong thing again and again and again.
*laughter and some applause* We can multiply by this estimate of about a 100
billion lines of new code each year. So if we take all of this: these talks, these
numbers, these should make us not happy and excited, these should make us sad,
very sad and frankly rather scared of what is going on in the world. So what can we
do? We can, option one, give up using computers altogether. *applause* In most
audiences this will be a hard sell but here I'm sure you're all happy to just
turn them off now. Or we can throw up our hands in the air and collapse in some kind
of pit of despair. Well, maybe, maybe not. My task today is to give you a tiny
smidgen, a very tall, a very small amount of hope that it may be possible to do
slightly better. But if we want to do better we first have to understand why
things are so bad and if we look at our aeronautical engineering colleagues for
example, they can make planes which very rarely fall out of the sky. Why is it that
they can do that and we are so shit at making computers? Well, I'm going to reuse
a picture that I used at 31C3, which is still the best description I can find of
the stack of hardware and software that we live above. Here we go. It's, there's so
much information in this, it's just ace. So we see down here all of this
transparent silicon, it's the hardware we live above. We see a stack of phases of a
C compiler, we see all kinds of other other bits and pieces. There might be a
slightly hostile wireless environment in this room for some reason. If we look at
this and think about the root causes for why our systems are so bad we can see
terrible things. So the first is, obviously there's a lot of legacy
complexity that we're really stuck with, alright. If you pull out one of those
pieces from the middle and try and replace it with something which is not of exactly
the same shape the whole pile will collapse. So we somehow need to find an
incremental path to a better world. And then, this is the most fundamental reason
that these are not like aeroplanes, these systems are discrete not continuous. If
you take an honest good I made out of a piece of steel and you push on it a little
bit it moves a little bit, basically in proportion. If it is 1 percent too strong,
1 percent to weak, basically it doesn't matter. But in these things one line of
code can mean you're open to a catastrophic exploit and one line in many,
many million. OK. And next thing... this really doesn't work. They're very
complicated. But the scary thing is not the static complexity of those lines of
code and the number of components although that's pretty intimidating the really
scary thing is that the exponential number of states and execution paths. So these
two together they mean that the testing that we rely on testing is the only way we
have to build systems which are not instantly broken. Testing can never save
us from these exploitable errors. And that means ultimately we need to do proof.
Honest machine checked mathematical proof. And this also tells us that we need to
arrange for our systems to be secure for simple reasons that do not depend on the
correctness of all of those hundred billion lines of code. Then another thing
that we have here. All these interfaces: the architecture interface, the C language
interface, the sockets API interface, the TCP interface. All of these we rely on to
let different parts of the system be engineered by different organizations. But
they're all really badly described and badly defined. So what you find is, for
each of these, typically a prose book varying in thickness between about that
and about that, full of text. Well, we still rely on testing - limited though it
is - but you can never test anything against those books. So we need instead
interface descriptions, definitions, specifications, that are more rigorous,
mathematically rigorous and that are executable - not in the normal sense of
executable as an implementation but executable as a test oracle. So you can
compute whether some observed behaviour is allowed or not and not have to read the
book and argue on the Internet. And we also need interface definitions that
support this proof that we need. And then all of this stuff was made up in the 1970s
or the sixties and in the 70s and the 60s the world was a happy place and people
walked around with flowers in their hair and nothing bad ever happened. And that is
no longer the case. And so we need defensive design, but we need defensive
design that is somehow compatible or can be made enough compatible with this legacy
investment. That's quite hard. And then - I can't say very much about this, but we
have at the moment very bad incentives, because we have a very strong incentive to
make things that are more complex than we can possibly handle or understand. We make
things, we add features, we make a thing which is just about shippable and then we
ship it. And then we go on to the next thing. So we need economic and legal
incentives for simplicity and for security that we do not yet have. But it's hard to
talk about those until we have the technical means to react to those
incentives. OK, so what I'm going to do now, I'm going to talk about two of these
interfaces, the architect interface and the C language interface, and see what we
can do to make things better. A lot of this has to do with memory. So whoever it
was that picked the subtitle for this meeting "refreshing memories" thank you,
because it's great, I love it. Let's refresh your memory quite a way. So I
invite you to think back to when you were very very young in about 1837 when cool
hacking was going on. Charles Babbage was designing the Analytical Engine and even
then you see there was this dichotomy between a mill performing operations and a
store holding numbers. This is a plan view of the analytical engine, well, it was
vaporware, but a design from the analytical engine, and you see here these
circles these are columns of numbers each made out of a stack of cogs, maybe a 50
digit decimal number in each of those columns. And this array, really, he
imagined it going on out to and over there somewhere, with about 1000 numbers. So
even then you have a memory which is an array of numbers. I think these were not-
I don't think you could do address computation on these things, I think
addresses were only constants, but, still, basically an array of numbers. So okay
what do we got now. Let's look a bit at C. How many of those people who have
programmed 100 lines of code, how many of you were C programmers? Quite a few. Or
maybe you're just embarrassed. I forgot to say. Those that didn't put your hands up
for that first question. You should feel proud and you should glory in your
innocence while you still have it. You are not yet complicit in this trainwreck. It
worked then. Okay so here's a little piece of C-code which I shall explain. I shall
explain it in several different ways. So we start out. It creates two locations x
and secret... Don't do that. This is so bad. Creates x, storing one and secret_key
which stores, I might get this wrong, your pin. And then there's some computation
which is supposed to only operate on x but maybe it's a teensy bit buggy or corrupted
by somebody and then we try and we make a pointer to x and in this execution x just
happened to be allocated at 14. This pointer contains the number 14 and then we
add one to that pointer. It's C so actually that adding one to the pointer it
really means add the four bytes which are the size of that thing. So we add 4 to 14
and we get 18. And then we try and read the thing which is pointed to. What's
going to happen. Let me compile this and run it in a conventional way. It printed a
secret key. Bad. This program, rather distressingly, this is characteristic by
no means of all security flaws but a very disturbingly large fraction of all the
security flaws are basically doing this. So does C really let you do that. Yes and
no. So if you look at the C standard, which is one of these beautiful books, it
says you, have to read moderately carefully to understand this, but it says
for this program has undefined behavior. And many of you will know what that means
but others won't, but, so that means as far as the standard is concerned for
programs like that there is no constraint on the behavior of the implementation at
all. Or said another way and maybe a more usefully way: The standard lets
implementations, so C compilers, assume that programmers don't have this kind of
stuff and it's the programmer's responsibility to ensure that. Now in
about 1970, 75 maybe 1980, this was a really good idea, it gives compilers a lot
of flexibility to do efficient implementation. Now not so much. How does
this work in the definition? So the standard somehow has to be able to look at
this program and identify it as having this undefined behavior. And indeed, well,
if we just think about the numbers in memory this 18, it points to a perfectly
legitimate storage location and that plus one was also something that you're
definitely allowed to do in C. So the only way that we can know that this is
undefined behavior is to keep track of the original allocation of this pointer. And
here I've got these allocation identifiers at 3, at 4, at 5, and you see here I've
still got this pointer despite the fact that I added 4 to it. I still remembered
the allocation idea so I can check, or the standard can check, when we try and read
from this whether that address is within the footprint of that original allocation,
i.e. is within there and in fact it is not, it's over here, it is not within
there at all. So this program is deemed to have undefined behavior. Just to clarify
something people often get confused. So we detect undefined behavior here but it
isn't really a temporal thing. The fact that there is undefined behavior anywhere
in the execution means the whole program is toast. Okay but this is really
interesting because we're relying for this critical part of the standard onto
information which is not there at run time in a conventional implementation. So just
to emphasize that point, if I compile this program, let's say to ARM assembly
language I get a sequence of store and load and add instructions, store, load,
add, store, load, load. And if I look at what the ARM architecture says can happen
these blue transitions... one thing to notice is that we can perfectly well do
some things out of order. At this point we could either do this load or we could do
that store. That would be a whole other talk. Let's stick with the sequential
execution for now. What I want to emphasize is that these, this load of this
address, really was loading a 64 bit number, which was the address of x and
adding 4 to it and then loading from that address, the secret key. So there is no
trace of these allocation ideas. No trace at all. Okay, let me step back a little
bit. I've been showing you some screenshots of C behaviour and ARM
behaviour and I claim that these are actually showing you all of the behaviours
allowed by what one would like the standards to be for these two things. And
really what I've been showing you are GUIs attached to mathematical models that we've
built in a big research project for the last many years. REMS: "Rigorous
Engineering of Mainstream Systems" sounds good, aspirational title I think I would
say. And in that we've built semantics, so mathematical models defining the envelope
of all allowed behaviour for a quite big fragment of C and for the concurrency
architecture of major processors ARM, and x86, and RISC-V, and IBM POWER and also
for the instruction set architecture of these processors, the details of how
individual instructions are executed. And in each case these are specs that are
executable as test oracles, you can compare algorithmically some observed
behaviour against whether spec says it's allowed or not, which you can't do with
those books. So is it just an idiot simple idea but for some reason the industry has
not taken it on board any time in the last five decades. It's not that hard to do.
These are also mathematical models, I'll come back to that later. But another thing
I want to emphasize here is that in each of these cases, especially these first
two, when you start looking really closely then you learn what you have to do is not
build a nice clean mathematical model of something which is well understood. What
you learn is that there are real open questions. For example within the C
standards committee and within ARM a few years ago about exactly what these things
even were. And that is a bit disturbing given that these are the foundations for
all of our information infrastructure. There is also a lot of other work going on
with other people within this REMS project on web assembly and Javascript and file
systems and other concurrency. I don't have time to talk about those but Hannes
Mehnert it is going to talk us a little bit about TCP later today. You should go
to that talk too if you like this one. If you don't like this one you should still
go to that talk. Okay so this is doing somewhat better. certainly more rigorous
engineering of specifications, but so far only for existing infrastructure for this
C language, ARM architecture, what have you. So what if we try and do better, what
if we try and build better security in. So the architectures that we have, really
they date back to the 1970s or even 60s with the idea of virtual memory. That
gives you - I need to go into what it is - but that gives you very coarse grain
protection. You can have your separate processes isolated from each other and on
a good day you might have separate browser tabs isolated from each other in some
browsers, sometimes, but it doesn't scale. It's just too expensive. You have lots of
little compartments. One thing we can do we can certainly design much better
programming languages than C but all of that legacy code, that's got a massive
inertia. So an obvious question is whether we can build in better security into the
hardware that doesn't need some kind of massive pervasive change to all the
software we ever wrote. And that's the question that a different large project,
the CHERI project has been addressing. So this is something that's been going on for
the last 8 years or so, mostly at SRI and at Cambridge funded by DARPA and the EPSRC
and ARM and other people, mostly led by Robert Watson, Simon Moore, Peter Neumann
and a cast of thousands. And me a tiny bit. So... How, don't do that. I should
learn to stop pushing this button. It's very hard to not push the button. So
here's the question in a more focused way that CHERI is asking: Can we build
hardware support which is both efficient enough and deployable enough that gives us
both fine grained memory protection to prevent that kind of bug that we were
talking about earlier, well that kind of leak at least, and also scalable
compartmentalization. So you can take bits of untrusted code and put them in safe
boxes and know that nothing bad is going to get out. That's the question. The
answer... The basic idea of the answer is pretty simple and it also dates back to
the 70s is to add hardware support for what people call capabilities, and we'll
see that working in a few moments. The idea is that this will let programmers
exercise the principle of least privilege, so with each little bit of code having
only the permissions it needs to do its job and also the principle of intentional
use. So with each little bit of code when it uses one of those capabilities, will
require it to explicitly use it rather than implicitly. So the intention of the
code has to be made plain. So let's see how this works. So these capabilities
they're basically replacing some or maybe all of the pointers in your code. So if we
take this example again in ISO C we had an address and in the standard, well, the
standard is not very clear about this but we're trying to make it more clear, an
allocation ID, say something like it. Now in Cherry C we can run the same code but
we might represent this pointer not just with that number at runtime but with
something that contains that number and the base of the original allocation and
the length of the original allocation and some permissions. And having all of those
in the pointer means that we can do.. the hardware can do, at run time, at access
time, a very efficient check that this is within this region of memory. And if it's
not it can fail stop and trap. No information leak. I need a bit more
machinery to make this actually work. So it would be nice if all of these were 64
bit numbers but then you get a 256 bit pointer, and that's a bit expensive so
there's a clever compression scheme that squeezes all this down into 1 to 8 bits
with enough accuracy. And then you need to design the instruction set of the CPU
carefully to ensure that you can never forge one of these capabilities with a
normal instruction. You can never just magic one up out of a bunch of bits that
you happen to find lying around. So all the capability manipulating instructions,
they're going to take a valid capability and construct another, possibly smaller,
in memory extent, or possibly with less permissions, new capability. They're never
going to grow the memory extent or add permissions. And when the hardware starts,
at hardware initialization time, the hardware will hand the software a
capability to everything and then as the operating system works and the linker
works and the C language allocator works, these capabilities will be chopped up into
ever finer and smaller pieces like to be handed out the right places. And then need
one more little thing. So this C language world we're living in here, or really a
machine code language world so there's nothing stopping code writing bytes of
stuff. So you have to somehow protect these capabilities against being forged by
the code, either on purpose or accidentally writing bytes over the top.
You need to preserve their integrity. So that's done by adding for each of these
128 bit sized underlined units of memory just a one extra bit. That holds a tag and
that tag records whether this memory holds are currently valid capability or not. So
all the capability manipulating instructions, if they're given a valid
capability with a tag set then the result will still have the tags set. But if you
write, so you just wrote that byte there which might change the base then the
hardware will clear that tag and these tags, they're not conventionally
addressable, they don't have addresses. They just stop there in the memory system
of the hardware. So there is no way that soft- ware can *inaudible* through these. So this is
really cool. We've taken, what in ISO was undefined behavior, in the standard, and
in implementations was a memory leak, and we've turned it into something that in
CHERI C is in both the specification and the implementation, is guaranteed to trap,
to fail stop, and not leak that information. So another few things about
the design that I should mention. I think all these blue things I think I've talked
about. But then a lot of care has gone in to make this be very flexible to make it
possible to adopt it. So you can use capabilities for all pointers, if you want
to, or just at some interfaces. You might for example use them at the kernel
userspace interface. It coexist very nicely with existing C and C++. You don't
need to change the source code very much at all, and we'll see some a tiny bit of
data about this, to make these to start using these. It coexists with the existing
virtual memory machinery, so you can use both capabilities and virtual memory, if
you want, or you can just use capabilities if you want or just use virtual memory if
you want. And then there's some more machinery, which I'm not going to talk
about, for doing this secure encapsulation stuff. What I've talked about so far is
basically the the fine grained memory protection story. And I should say the
focus so far is on spatial memory safety. So that's not in the first instance
protecting against reuse of an old capability in a bad way but there various
schemes for supporting temporal memory safety with basically the same setup. Okay
so. So how do we... Okay this is some kind of a high level idea. How do we know that
it can be made to work. Well the only way is to actually build it and see. And this
has been a really interesting process because mostly when you're building
something either in academia or an industry you have to keep most of the
parts fixed, I mean you are not routinely changing both the processor and the
operating system, because that would just be too scary. But here we have been doing
that and indeed we've really been doing a three way, three way codesign of building
hardware and building and adapting software to run above it and also building
these mathematical models all at the same time. This is, well. A, it's all the fun
because you can often get groups of people together that can do all of those things
but B, it's really effective. So what we've produced then is an architecture
specification. In fact, extending MIPS because it was conveniently free of IP
concerns and that specification is one of these mathematically rigorous things
expressed in a domain specific language specifically for writing instruction set
architecture specifications, and we've designed and implemented actually two of
those. And then there are hardware processor implementations that actually
run an FPGAs. And a lot of hardware research devoted to making this go fast
and be efficient despite these extra tags and whatnot. And then there's a big
software stack adapted to run over this stuff. Including Clang and a FreeBSD
kernel and FreeBSD userspace and WebKit and all kinds of pieces. So this is a very
major evaluation effort. That one is not normally able to do. This is why, this
combination of things is why that list of people up there was about 40 people. I say
this is based on MIPS but the ideas are not specific to MIPS, there are ongoing
research projects to see if this can be adapted to the ARM application class
architecture and the ARM microcontroller architecture and the RISC-V. We'll see how
that goes, in due course. Okay so then with all of these pieces we can evaluate
whether it actually works. And that's still kind of an ongoing process but the
data that we've got so far is pretty encouraging. So we see here first,
performance. So you see, maybe a percent or 2 in many cases of runtime overhead.
There are workloads where it performs badly if you have something that's very
pointer heavy, then the extra pressure from those larger pointers will be a bit
annoying, but really it seems to be surprisingly good. Then is it something
that can work without massive adaption to the existing code. Well, in this port of
the FreeBSD userspace, so all the programs that, all in all programs that run, they
were something like 20000 files and only 200 of those needed a change. And that's
been done by one or two people in not all that large an amount of time. Some of the
other code that's more and more like an operating system needs a bit more invasive
change but still, it seems to be viable. Is it actually more secure? How are you
going to measure that. We like measuring things as a whole we try and do science
where we can. Can we measure that? Not really. But it certainly does, the whole
setup certainly does, mitigate against quite a large family of known attacks. I
mean if you try and run Heartbleed you'll get a trap. It will say trap. I think he
will say signal 34 in fact. So that's pretty good. And if you think about
attacks, very many of them involve a chain of multiple floors put together by an
ingenious member of the C3 community or somebody else, and very often, at least
one of those is some kind of memory access permission flaw of some kind or other.
Okay so this is nice, but I was talking a lot in the first part of the talk, about
rigorous engineering. So here we've got formally defined definitions of the
architecture and that's been really useful for testing against and for doing test
generation on the basis of, and doing specification coverage in an automated
way. But surely we should be able to do more than that. So this formal definition
of the architecture, what does it look like. So for each instruction of this
CHERI MIPS processor, there's a definition and that definition, it looks a bit like
normal code. So here's a definition of how the instruction for "capability increment
cursor immediate" goes. So this is a thing that takes a capability register and an
immediate value and it tries to add something on to the cursor of that
capability. And what you see here is some code, looks like code, that defines
exactly what happens and also defines exactly what happens if something goes
wrong. You can see there's some kind of an exception case there. That's a processor.
No that's a... Yeah, that a "raising our processor" exception. So it looks like
code, but, from this, we can generate both reasonably high performance emulators,
reasonably in C and in OCaml, and also mathematical models in the theorem
provers. So three of the main theorem provers in the world are called Isabelle
and HOL and Coq. And we generate definitions in all of those. So then we
got a mathematical definition of the architecture. Then finally, we can start
stating some properties. So Cherrie's design with some kind of vague security
goals in mind from the beginning but now we can take, let'ssay one of those goals and
make it into a precise thing. So this is a kind of a secure encapsulation, kind of
thing not exactly the memory leak that we were looking at before. Sorry, the secret
leak that we were looking at. So let's take imagine some CHERI compartment.
Haven't told you exactly what that means but let's suppose that that's understood
and that inside that compartment there is a piece of software running. And that
might be maybe a video codec or a web browser or even a data structure
implementation maybe, or a C++ class and all of its objects maybe. So imagine that
compartment running and imagine the initial capabilities that it has access to
via registers and memory and via all the capabilities it has access to via the
memory that it has access to and so on recursively. So imagine all of those
capabilities. So the theorem says no matter how this code executes whatever it
does however compromised or buggy it was in an execution up until any point at
which it raises an exception or makes an inter compartment call it can't make any
access which is not allowed by those initial capabilities. You have to exclude
exceptions and into compartment calls because by design they do introduce new
capabilities into the execution. But until that point you get this guarantee. And
this is something that we've proved actually [...] has approved with a machine
check proof in in fact the Isabelle theorem prover. So this is a fact which is
about as solidly known as any fact the human race knows. These provers they're
checking a mathematical proof in exceedingly great detail with great care
and attention and they're structured in such a way that the soundness of approver
depends only on some tiny little kernel. So conceivably cosmic rays hit the
transistors at all the wrong points. But basically we know this for sure. I
emphasize this is a security property we have not proved, we certainly wouldn't
claim to have proved that CHERI is secure and there are all kinds of other kinds of
attack that this statement doesn't even address but at least this one property we
know it for real. So that's kind of comforting and not a thing that
conventional computer science engineering has been able to do on the whole. So, are
we taming the chaos then. Well no. Sorry. But I've shown you two kinds of things.
The first was showing how we can do somewhat more rigorous engineering for
that existing infrastructure. It's now feasible to do that and in fact I believe
it has been feasible to build specifications which you can use as test
oracles for many decades. We haven't needed any super fancy new tech for that.
We've just needed to focus on that idea. So that's for existing infrastructure and
then CHERI is a relatively light weight change that does built-in improved
security and we think it's demonstrably deployable at least in principle. Is it
deployable in practice? Are we going to have in all of our phones five years from
now? Will these all be CHERI enabled? I can't say. I think it is plausible that
that should happen and we're exploring various routes that might mean that there
happens and we'll see how that goes. Okay so with that I aiming to have given you at
least not a whole lot of hope but just a little bit of hope that the world can be
made a better place and I encourage you to think about ways to do it because Lord
knows we need it. But maybe you can at least dream for a few moments of living in
a better world. And with that I thank you for your attention.
*applause*
Herald Angel: Thanks very much. And with that we'll head straight into the Q and A.
We'll just start with mic number one which I can see right now.
Q: Yes thanks for the very encouraging talk. I have a question about how to C
code the part below that. The theorem that you stated assumes that the mentioned
description matches the hardware at least is describes the hardware accurately. But
are there any attempts to check that the hardware actually works like that? That
there are no wholes in the hardware? That some combination of mentioned commands
work differently or allow memory access there is not in the model? So, is it
possible to use hardware designs and check that it matches the spec and will Intel or
AMD try to check their model against that spec?
Sewell: OK. So the question is basically can we do provably correct hardware
underneath this architectural abstraction. And the answer is... So it's a good
question. People are working on that and it can be done I think on at least a
modest academic scale. Trying to do that in its full glory for a industrial
superscalar processor design, is right now out of reach. But it's certainly something
one would like to be able to do. I think we will get there maybe in a decade or so.
A decade is quick. Herald Angel: Thanks. Mic number four is
empty again. So we'll take the Internet. Sewell: Where is the internet?
Signal Angel: The internet is right here and everywhere so ruminate would like to
know is the effort and cost of building in security to hardware as you've described in your
talk significantly greater or less than the effort and cost of porting software to
more secure languages. Sewell: So, is the effort of building new
hardware more or less than the cost of porting existing software to better
languages? I think the answer has to be yes. It is less. The difficulty with
porting software is all of you and all your colleagues and all of your friends
and all your enemies have been beavering away writing lines of code for 50 years.
Really, I don't know what to say, effectively. Really numerously. There's an
awful lot of it. It's a really terrifying amount of code out there. It's very hard
to get people to rewrite it. Signal Angel: OK, mic two.
Q: OK, given that cost of ... of today on the software level not on the hardware level, is it
possible to go half way using an entire system as an oracle. So during development
there are code based with the secure hardware but then essentially ship the
same software to unsecure hardware and *inaudible* Sewell: So this question, if I paraphrase
it is can we use this hardware implementation really as the perfect
sanitiser? And I think there is scope for doing that. And you can even imagine
running this not on actual silicon hardware but in like a QEMU implementation
which we have in order to do that. And I think for for that purpose it could
already be a pretty effective bug finding tool. It would be worth doing. But you
would like as for any testing it will only explore a very tiny fraction of the
possible paths. So we would like to have it always on if we possibly can.
Herald Angel: OK. The internet again. Signal Angel: OK someone would like to
know how does your technique compare to Intel MPX which failed miserably with a *inaudible*
ignoring it. Will it better or faster? Could you talk a little bit about that.
Sewell: I think for that question, for a real answer to that question, you would
need one of my more hardware colleagues. What I can say is they make nasty faces
when you say MPX. Herald Angel: Well that's that. Mic number
one. Q: Somewhat inherent to your whole
construction was this idea of having an unchangeable bit which described whether
your pointer contents have been changed. Is this even something that can be done in
software? Or do you have to construct a whole extra RAM or something?
Sewell: So you can't do it exclusively in software because you need to protect it.
In the hardware implementations that my colleagues have built it's done in a
reasonably efficient way. So it's cached and managed in clever ways to ensure that
it's not terribly expensive to do. But you do need slightly wider data paths in your
cache protocol and things like that to manage it.
Herald Angel: OK. Mic seven. Q: How good does this system help securing
the control flow integrity compared to compared to other systems, like hardware
systems data flow isolation or code pointer integrity in ARM *inaudible*?
Sewell: Ah well, that's another question which is a bit hard to answer because then
it depends somewhat on how you're using the capabilities. So you can arrange here
that each state each C language allocation is independently protected and indeed you
can also arrange that each way - this is sensible - that each subobject is
independent protected. And those protections are going to give you
protection against trashing bits of the stack because they'll restrict the
capability to just those objects. Herald Angel: OK the internet again.
Signal Angel: Twitter would like to know is it possible to is it possible to run
CHERI C without custom hardware? Sewell: Can you run CHERI C without custom
hardware? And the answer is you can run it in emulation above this QEMU. That works
pretty fast, I mean fast enough for debugging as the earlier question was
talking about. You can imagine you know somewhat faster emulations of that. It's
not clear how much it's worth going down that route. The real potential big win is
to have this be always on and that's what we would like to have.
Herald Angel: OK. Mic one. Q: Do you have some examples of the kinds
of code changes that you need to the operating system and userland that you
mentioned? Sewell: So, okay so what kind of changes
do you need to to adapt code to CHERI? So, if you look at C-code there is the C
standard that deems a whole lot of things to be undefined behavior and then if you
look at actual C code you find that very very much of it does depend on some idiom
that the C standard does not approve of. So there is for example, *pause* there are
quite a lot of instances of code that constructs a pointer by doing more than
one more than plus one offset and then brings it back within range before you use
it. So in fact in CHERI C many of those cases are allowed but not all of them.
More exotic cases where there's really some crazy into object stuff going on or
where pointer arithmetic between objects - which the C standard is certainly quite
down on but which does happen - and code which is, say manipulating the low order
bits of a pointer to store some data in it. That's pretty common. You can do it in
CHERI C but you might have to adapt the code a little bit. Other cases are more
fundamental. So say, in operating system code if you swap out a page to disk and
then you swap it back in then somehow the operating system has to reconstruct new
capabilities from a large capability which it kept for the purpose. So that needs a
bit more work. Though it's kind of a combination. Some things you would regard
as good changes to the code anyway and others are more radical.
Herald Angel: OK, another one from the internet.
Signal Angel: I lost one *pause* Sewell: The Internet has gone quiet. Yes.
Signal Angel: Last question from the internet. Are there any plans to impact
test on Linux or just FreeBSD? Sewell: If anyone has a good number of
spare minutes then that would be lovely to try. The impact on Linux not just
previously the BSD code base is simpler and maybe cleaner and my systemsy
colleagues are already familiar with it. It's the obvious target for an academic
project doing it already a humungous amount of work. So I think we would love
to know how Linux and especially how Android could be adapted but it's not
something that we have the resource to do at the moment.
Herald Angel: Mic number on again. Q: How likely or dangerous.
Herald Angel: Mic number one is not working.
Q: How likely or dangerous you think it is for a programmer to screw up their
capabilities he specifies? Sewell: So how often will the programmer
screw up the capabilities? So in many cases the programmer is just doing an
access with a C or C++ pointer or C++ object in a normal way. They're not
manually constructing these things. So a lot of that is going to just work. If
you're building some particular secure encapsulation setup you have to be a bit
careful. But on the whole I think this is a small risk compared to the state of
software as we have it now. Herald Angel: OK. Mic eight.
Q: So existing memory protection techniques are quite patch-worky, like
canaries and address layout randomisation. Is this a system designed to replace or
supplement these measures? Sewell: I think if you *pause* So again it
depends a bit how you use it. So if you have capabilities really everywhere then
there's not much need for address space layout randomization or canaries to
protect against explicit information leaks. I imagine that you might still want
randomisation to protect against some side channel flows but canaries is not so much
on whether you actually do for side- channel flows - I don't know. That's a
good question. Herald Angel: Mic four please.
Q: Thanks for the very interesting talk you presented with CHERI, a system of
veryfying existing C-software, sort of post hoc and improving its security via
run-time mechanism...? A: Improving or Proving? Improving yes,
proving no, yes. Q: So what's your opinion on the viability
of using a static analysis and static verification for that. Would it be
possible to somehow analyse software that already exist and as written in these
unsafe languages and show that it nevertheless has some security properties
without writing all the proofs manually in like HOL or Isabelle?
A: Well so if you want to analyse existing software... So, static analysis is already
useful for finding bugs in existing software. If you want to have assurance
from static analysis, that's really very tough. So you certainly wouldn't want to
manually write proofs in terms of the definitional C semantics, you would need
intermediate infrastructure. And if you look at the people, who have done verified
software, so verified compilers and verified hypervisor, and verified
operating systems, all of those are now possible on significant scales, but they
use whole layers of proof and verification infrastructure for doing that. They're not
writing proofs by hand for every little detail. And some of those verification
methods either are, you can imagine them being basically like static analysis, you
know, you might use a static analysis to prove some relatively simple facts about
the code and then stitch those together into a larger assembly. I think any kind
of more complete thing I think is hard to imagine. I mean these analysis tools
mostly, they rely on making some approximation in order to be able to do
their thing at all. So it's hard to get assurance out of them.
Herald Angel: Okay, Mic one. Q: You said you modified an MIPS
architecture to add some logic to check their capabilities. Do you know what the cost of
this regarding computational power, an energetic power supply?
A: Sorry, can you repeat the last part of that?
Q: What the cost of this modification regarding computational power, and power
consumption. A: Ah, so what's the energy cost? So I
gave you a performance cost. I didn't give you, I carefully didn't give you an energy
cost estimate, because it's really hard to do in a scientifically credible way,
without making a more or less production superscalar implementation. And we are
sadly not in a position to do that, although if you have 10 or 20 million
pounds, then I would be happy to accept it.
Herald Angel: Mic number 7, please. Q: How does the class of problems that you
can address with CHERI compare to the class of problems that are excluded by,
for example, the Rust programming language?
A: So how does the problems of CHERI relate to the problems, sorry the problems
excluded by CHERI, relate to the problems excluded by Rust. So if you are happy to
write all of your code in Rust without ever using the word "unsafe", then maybe
there would be no point in CHERI, at all. Are you happy to do that?
Q: Probably not, no. A: I think someone shakes their head
sideways, yeah. Herald Angel: Mic number 1.
Q: What do you think about the following thesis: We are building a whole system of
things, with artificial intelligence and something like that. That is above this
technical level and it's building another chaos that isn't healing with those
things. A: It's dreadful, isn't it.
*Laughter* A: There are, so you might, in fact some
of my colleagues are interested in this question, if you, you might well want to
bound what your artificial intelligence can access or touch and for that you might
want this kind of technology. But this is not, we are, with machine learning systems
we are intrinsically building things that we, on the whole, don't understand and
that will have edge cases that go wrong. And this is not speaking to that in any
way. Herald Angel: OK. Does the internet have a
question? No, good. I don't see anyone else, so let's conclude this. Thank you
very much. A: Thank you.
*applause*
*35c3 postroll music*
subtitles created by c3subtitles.de in the year 2019. Join, and help us!