34c3 intro
Herald: He's been publishing in academia
for almost 30 years. Please join me in
giving him a warm welcome to 34c3.
Applause
Alastiar Reid: Thank you very much for
your introduction. So I'm going to be
talking about the ARM processors and
they're incredibly widely used. You find
them in phones, tablets, IOT devices,
hard-disk drives; they're all over. And if
you think about it, what I'm saying is:
They're in all the things, which contain
your most private and personal data, so
it's really, really important that they do
exactly what they should be doing and
nothing else. We need to make sure we
really understand them and that means it's
important that we can analyze them for any
malware, look for vulnerabilities and so
on. So I'm going to be talking about some
work I started about six years ago,
creating a very precise specification of
what an ARM processor does and I'm going
to be talking also about back in April I'm
released this their specification in a
machine readable form. And I should say
that I'm working with Kimbridge University
to turn that in something you can use. So
so this talk I'm going to mostly actually
talk about this executable processor
specification, that's going to be the bulk
of the talk but at the end that sets me up
very nicely to talk about a formally
verified software. So I thought, given the
theme of the Congress, it would be more
useful to emphasize things you could
actually do. So the specification that ARM
released, what's in it? Well, there's lots
of instruction descriptions of course but
there's also lots of really interesting
security features; things to do with
memory protection, exceptions, privilege
checks and so on.
So there's lots of really interesting
stuff ... of your interest in their how
secure your devices and how to make sure
it really is secure. Throughout the talk
I'll be giving a bunch of links; you can
go and download the specs right now from
the first link but please wait to the end
of the talk and there's also the
specification rendered as HTML, as tools
that can take the specification release
apart and find useful information in it;
I've written blogs and papers about it as
well. And so let's just dive into, look at
the bits of the actual specification. So
the first thing is all the really
important security features in the specif-
in our processor are controlled by, what I
call, the system control registers and the
top dog among all those control registers
is this one here called SCTLR. Just trips
off the tongue, doesn't it? So SCTLR is
where - it's full of lots of individual
control bits, which affect either
optimizations, the processor's doing, or
also security features. And so let's just
zoom in and one of them, to give you an
idea of what kind of information the spec
contains.
So here's some documentation, telling you
about a WXN bit. What does that do? It
makes sure that any code, any, that your
stack cannot contain code. you can't boot
instructions on the code, and on the
stack, because they're proce- if you set
this bit the processor won't execute them.
In other words: This is the bit that
triggered the requirement for things like
return-oriented programming. Okay, so what
can you do with this fact? Well, suppose
you're in the habit of reverse engineering
some code. You might, your disassemble may
show you something like this. And you're
probably all staring at this going: "What
on earth does that do?", because it's
extremely cryptic. But using the
information that's in the XML version of
the release you could easily figure out
how to build, how to decode some of the
more cryptic parts and go "Oh actually,
it's that SCTLR register", right, so you
could decode the cryptic name for the
number for the register into that. But you
could do a bit more than that. You can see
it's setting one of the bits in the
register so - it is of course the bit I
just told you about WXN, so we could dig
into that and, so we could kind of use the
information from the XML to render it,
perhaps, as like this.
So you can make things a bit more useful
and you can also take that documentation
that was there, that told you what the WXN
bit does, and maybe, if you're a feeling
really energetic, you could, when you
click on it, mouse over or whatever, it
could bring up some of that documentation.
And and that makes specf- that makes it
much easier to understand what the cryptic
piece of code at the top is doing. Okay,
so that's just a very shallow thing you
can get from the specification. If we dig
into the instruction descriptions there's
also things like the assembly language of
- the specification of the assembly syntax
and. So, something I did a few years ago
and which I just wrote a blog article
about over the weekend was was it's
possible to actually take that
specification, turn it into a
disassembler. So I first of all
transformed it into the code I'm showing
at the bottom. What this is showing is how
to
take a binary description of an
instruction so that's the the top line of
typewriter font and and then turn that
into strings, which is what this the code
at the bottom is describing how to do. So
so you can use this as a disassembler.
It's actually possible to run it in
reverse and use it as an assembler; you
basically run the code from bottom to top
and you can turn strings into binary
instructions. And we'll see more of this
running things in reverse in a few slides
time. So the main thing about instructions
is of course they do something. So the
specification contains a description of
exactly what an instruction does and that
description is as code, which, as a
programmer, makes me very happy, right. I
don't understand the English words in the
specification but I do understand what the
code does. So one thing you can do with
code is execute it, so let's just walk
through - let's suppose ... take an
instruction and I match against that
diagram there. I might get some values for
for some of the variables from that and
then I can walk through, step by step,
evaluating this code, until I eventually
realize that register five is having some
value assigned to it.
Okay, so that's a fairly basic thing you
can do with the specification;
interpreters are fairly easy thing to
implement but once you have it there's a
lot you can build on top of it. And one
thing that's surprisingly easy to
implement is to extract a symbolic
representation of what the instruction
does. So I'll just show you quickly how
you do that, using the interpreter. So
let's take those same concrete values but
I'm also, I've added three other variables
at the side there, which I'm going to
treat as symbolic variables. And as I walk
through the code I won't just calculate
some concrete values, like the value five
or 32, I'll also build up a graph,
representing exactly how I came up with
these values at five and so on. So as I'm
executing the code I can build a graph
representing exactly what this code is
doing. And what I can do now is just throw
away the code and focus on what that graph
is telling me.
So I now have a symbolic representation of
one slice through that, through that
instruction and I can feed that to a
constraint solver, so if any of you have
heard of Z3 or SMT solvers, that's what
I'm talking about here. And a constraint
solver is a really useful tool, because
you can run code forwards through it, so
given some input values you can say what
are the outputs from this function or
from this instruction but you can also run
them backwards, given some
output value, some final result you want
to see, you can ask what inputs would
cause this to happen. And this is just
tremendously useful if you're trying to
figure out what instructions you want to
use to generate some particular effect.
All right, so if you're trying to figure
out how some particular register could be
accessed, how some particular thing could
be turned on or off, being able to ask
what inputs will cause this to happen is
incredibly useful. And you can also use
the constraint solver to ask for
intermediate values, in the middle of the
calculation. You know if you know some
value you want to see there you can ask
what the inputs that would cause that to
happen.
So, if any of you are familiar with tools
like KLEE, which is a symbolic execution
tool for based on LLVM, then they use
something similar to this. So, I've shown
you are fairly simple draft, something I
could show you how you build it, kind of
on the fly. This is the actual graph for
that same instruction. Here I've added in
a lot more nodes to do with some of the
functions that were being called and to do
with the calculating, whether to take a
branch or not. So this is about 80 or 90
nodes. And I've been experimenting with
extending this in two ways. So this is
just one path through the execution of an
instruction, so one way to improve on that
is to build a graph that represents all
possible paths through the instruction.
And that's much more useful, because you
can you then can point at something and
say "how can I make that happen?" and it
will tell you exactly what inputs will
cause the path that will make that happen.
I've also been experimenting with taking
the entire specification, right, so that
stuff that handles exceptions, that
fetches instructions or execute
instructions. It contains all
instructions. And I've been experimenting
with building a graph representing the
entire specification all at once. And
that's even more useful, because now
pretty much any question you have about
the specification, you can ask the
constraint solver and it will come back
and give you an answer. And this graph for
the full specification is quite large.
It's about half a million nodes and that's
for the smallest specification that our
major uses. So it's about half a million
nodes. But the great thing is modern
constraint solvers can read in that half
million nodes and still give you answers.
Typically in about 1 to 10 seconds for
most of the questions posed to them. So,
these are just tremendously useful tools,
if you're wanting to be able to understand
exactly what the specification does,
and exactly how some program is going to
behave or figure out what program you want
to write to make it behave some particular
way. Okay so I've talked a lot about
instructions, but most of us actually run
programs, right? So to turn this the
specification into something in execute
programs, in other words turn it into a
simulator for the ARM architecture, you
need to add a little bit of a loop that
will handle interrupts, fake instructions
and then it can execute them and handle
any exceptions. So, I... So I did this. I
added this loop to this specification. And
then, I thought I'd better try testing the
specification. And, so the good news for
me, because I work for ARM I have access
to ARM's internal test suite. Which is
something that ARM has been working on
basically since the company started 25, 30
years ago. So it's quite a large test
suite. It is extremely thorough, has tens
of thousands of test programs in it, runs
billions of instructions. And so I set
about testing the, testing the
specification using this test suite. And
if any of you have tested software you'll
be familiar with a graph that looks like
this, right? The start things don't work
all that well. Gradually you get things
working pretty well but then there's a
heavy tail of difficult to find bugs.
Okay, so, and that's basically what I
found when I was testing the
specification. But you should all be
shocked by what I just said. Because what
I'm seeing is ARM's official specification
could not pass ARM's official test suite
when I started, right. I mean that's
that's pretty shocking. And I'm telling
you this and emphasizing it, not because
I think ARM's specification was especially
bad. I think it was just typically bad. I
think if you were to take any
specification for, you know, any real-
world system and actually test it against
the test suite, well first of all you'd
find it's not an executable specification
most the time and secondly you'd find it
wouldn't work. And you'd probably find it
would work as badly as ARM's did. So it's
not just that it didn't pass all the
tests. It didn't pass any tests. In fact
it took me weeks to get the processor or
the specification to come out of reset.
Right? Just to get the starting fix to get
the first instruction took weeks. So and I
think so I think you'd find this if you
were to try any other specification.
What's my next slide? So, moving on to
useful thing you can do with the
specification, something we tried last
summer was using it for fuzz testing. So,
fuzz testing consists of taking a program
and throwing random inputs at the
program and just seeing what breaks and it
pretty much always breaks and a modern
fuzztester like maybe AFL to make it
more effective. It monitors something
about how the program is executing and
uses that to guide its choice of what to
change next. So, if it's finding...in
particular monitor whether an
instruction... whether the program is
taking a branch or not and if it sees it's
taking lots of new branches then it goes:
"Ok I'll keep trying more of what I'm
doing at the moment because it seems to be
effective, and if it's and not finding any
new branches, then it will look for
something else to try changing. So, that's
kind of a normal fuzzing. What you're
doing is basically trying to kind of
maximize your branch coverage. So, what we
did though, when we did this with the
specification, was, we actually monitored
branches not just in the in the binary
that we were analyzing but also in the
specification. And what this gave us was
basically: if you got.. Suppose, your the
binary you're analyzing is just straight
line code. There's no branches in it at
all. Then there's nothing really for your
fuzzer to work with right. So it doesn't
see that the code is interesting, it
quickly moves on to something else.
But maybe your straight line cord is doing
something really interesting, like
accessing a privileged register. Well,
there will be a branch around that to
check that you do have the privilege you
require.
Or maybe it's accessing a memory in which
cases memory protection checks. There's
also checks for: Is this a device
register? Or is this a kind of RAM or ROM?
So, there's a number of different branches
there and that gives the fuzzer
interesting things to... interesting
feedback to play with. So, when we set
this going on one of our microkernel,
we analyzed the system call interface for
that microkernel. And one of the things
the fuzzer surprised us with was it said:
Suppose I take the stack pointer and point
it into the middle of this device space
and then take an exception immediately,
what happens? And the answer was: there
was a bug in the microkernel and what it
did was: it first thing it would do is
read from the stack, where the stack
pointer was pointing, so we do a read from
one of the devices, which doesn't wasn't
really what was intended. In fact it
completely breaks a security model. So,
fuzztesting using not just coverage of
the monitoring branches in the binary but
also the specification can find you a
bunch of really interesting things. And I
hope some of you will I pick this idea up
and run with it. So, the reason that I was
doing all this work was I wanted to be
able to formally verify ARM processors and
so I needed to create a specification
before I could do that. So, sorry, let me
just take a drink here... So, this is an
overly simplified picture of a processor,
it's more or less what processors looked
like 25, 30 years ago, in fact.
But it's good enough for the example. So,
if you want to check a processor, is
correct, then what you can do is: add an
extra logic, which will monitor the values
at the start of an instruction executing
the values that are finally produced at
the end of an instruction executing, and
then if you feed those the specification
you can see what the right answer should
have been. You can compare that with what
the processor actually did. So, you can do
this using a test-based approach, right:
just feed in inputs and check that
everything matches.
But you can also do it using a formal
verification tool called a "bounded model
checker". And a bounded model checker is
like one of those constraint solvers I
mentioned earlier on crack cocaine. So,
what it will do is: it won't just try kind
of one step for what can happen but will
actually try multiple steps: all possible
combinations of inputs for one
instruction, two instructions, three
instructions, longer and longer sequences
of instructions, looking for ways they can
fail the property. So, and this turned out
to be an incredibly effective way of
finding bugs in our processors.
We've actually, we're going to be using
this on all future processor developments.
So, there's a paper that we wrote about
this but, I recommend that you go
find the video for the top by Clifford
Wolf from a couple of hours ago, which
describes a very similar process. Okay, so
I'm encouraging you to see the
specification and find something awesome
to do with it. There's a bunch of ideas I
have suggested there, and there's a few
extras which I didn't have time to
describe here. But now, let me turn to
this title of the talk: How can you trust
formally verified software? So, what I'm
talking about here is: verifying a program
against some specification. But, of
course, programs don't just run in a
vacuum. They run into some operating
system that, they use some libraries and
they're also written in some programming
language. And, so, when you verify your
program against your specification, you're
also verifying them against the
specifications of Linux, glibc and ISO-C,
none of which have good specifications. In
fact, they're just terrible specifications
which I bear little resemblance to what
compilers and operating systems actually
do in practice. So, if you... the current
state of things is: if you do verify your
program against these specifications, you
will find lots of bugs. You will make your
software a lot more reliable, but you'll
be doing it against specifications, which
are probably not very
good. Just as ARM's specification was not
very good before I tested it really
thoroughly. And so: Do I trust formally
verified software? No, not really. It's a
lot better for being formally verified,
but I'd also want to test it quite
thoroughly and maybe to use a bit of fuzz
testing as well. Okay, so this is my final
slide, by the way. So, I'm encouraging you
to go out and do something with the
specification. If you're interested in
this, then do contact me! Do ask me
questions, if you have trouble. I'm also
going to mention: if there's any white hat
hackers out there in the... white hat
hackers in the audience, then do please
talk to me or Milisch Meriac who's here in
the front row, if you're interested in
working at ARM and I like to thank a whole
lot of people at ARM and elsewhere, who've
helped me in this work and also I'd like
to thank you for giving me your attention
for the last half hour.
Applause
Herald: So, we have time for some
questions. I would ask anyone that has a
question to line up at one of the
microphones that are in the aisles here
one through eight. Questions for Alastair
there about formal verification, about
working at ARM, how is the weather in
Cambridge. Try to keep it on topic. And
signal angel: do we have already questions
from online?
Signal Angel: No questions yet.
Herald: Okay, then let's go to microphone
number one.
Microphone 1: Hi... I was just
AR: Maybe tiptoes.
MIC 1: Yes, I was just curious how are you
actually using the machine specification
in order to generate VCs for the SMG
solver. Because you didn't really get a
chance to talk about that I guess.
AR: Trying to think how I can describe
that briefly... My basic idea is to take
the specification, which basically... the
specification is describing a piece of
hardware. And so, I try to do what a
hardware engineer would do, if they were
actually building a machine that
implemented it. So I end up with something
that's essentially a giant circuit. So,
that was the graph I was describing. So,
whenever this control flow, whenever the
control flow joins back up, I have to
introduce things to slide between the
value of what was calculated in the left
or the right. And so on.
MIC 1: Yeah, I guess I'm mostly curious
about, like, what logics you're using for,
like, the solvers and stuff like that.
AR: I see. Just very basic solvers because
they run fastest.
MIC 1: Then ugh
H: Thank you. So, microphone 6 please.
MIC 6: I was just wondering, if you could
talk some little bit about the language
you used to write your specification.
AR: So this is a language which basically
I inherited from ARM's documentation. So,
all processors are described using
pseudocode and what I realized was that
the pseudocode the ARM had started writing
was actually very close to being a
language. And so, I sort of reverse
engineered the language hiding inside the
pseudocode, built some tools for it, and
just kind of figured out what the language
could possibly mean, given what I thought
processors actually did.
And the language itself is... it's just a
very simple imperative language. It's
actually got inherits from BBC basic for
anyone who's about the same age as me and
remembers BBC basic or it's a bit like
Pascal... It's it's not a complicated
language. It's actually designed so that
as many people as possible can read it and
know exactly what it says without any
doubt, without having to consult a
language lawyer.
H: Signal angel? Yet anything?
Signal Angel: Yes, now we've got a
question: "Has ARM its own form of the
Intel Management engine?"
AR: No is the short answer. Yeah, I don't
think we have anything quite like that. If
you... yeah, I'll just say no.
Laughter
H: Microphone one.
MIC 1: Hi! On that question that we had
before about the specification language:
Have you considered using Z3's own
language for expressing the instructions?
AR: So, Z3's own language is basically
write kind of s-expressions, which, if you
like lisp is wonderful but for anybody who
doesn't like Lisp it's a bit of a turn-off
and a bit of a barrier to understanding
it. So, again the specification is
designed so that people can look at it and
go: "Oh, I see what's going on here", and
not have... and I just try to minimize the
barriers.
MIC 1: Fair enough!
H: Last call, signal angel!
SA: How long does the complete test of the
arms specification take?
AR: About two years. So, yeah, so a modern
processor team about 80% of that team will
be verification engineers. And, so,
they're basically writing new tests,
running old tests, diagnosing them, just
doing that continuously for the entire
life of a project, which is probably about
three years. And after about the first
year, you basically have a processor that it
mostly works, and after that it's kind of
debugging it and it's, you know, kind of
fine-tuning the performance. So, yeah, it
takes a really long time. To run the
actual tests, I don't actually know
because actually one of my colleagues in
the audience, they've actually run the
tests. But, yeah, I don't know... and we
use a lot of processors in parallel, so I
really don't have an idea.
H: Thank you so much, Alastair! Let's give
him another warm round of applause!
Applause
34c3 outro
subtitles created by c3subtitles.de
in the year 2018. Join, and help us!