*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*