How can you trust formally verified software?
This is a modal window.
The media could not be loaded, either because the server or network failed or because the format is not supported.
Formal Metadata
| Title |
| |
| Title of Series | ||
| Number of Parts | 167 | |
| Author | ||
| License | CC Attribution 4.0 International: You are free to use, adapt and copy, distribute and transmit the work or content in adapted or unchanged form for any legal purpose as long as the work is attributed to the author in the manner specified by the author or licensor. | |
| Identifiers | 10.5446/34805 (DOI) | |
| Publisher | ||
| Release Date | ||
| Language |
Content Metadata
| Subject Area | ||
| Genre | ||
| Abstract |
| |
| Keywords |
34th Chaos Communication Congress149 / 167
1
2
3
4
5
6
7
10
11
12
14
15
25
26
29
30
31
33
34
39
40
42
43
45
46
49
50
53
58
59
61
63
65
68
69
71
73
77
78
79
81
82
83
85
86
87
88
91
92
94
99
100
101
102
108
109
110
113
114
115
116
118
119
122
124
125
126
127
129
130
131
132
133
134
136
138
139
140
141
145
147
148
150
151
152
153
154
157
159
160
161
163
164
165
166
167
00:00
Network topologyComputer animation
00:30
ArchitectureProduct (business)ArmFormal verificationCoprocessorVirtual machineComputer architectureHard disk driveTablet computerHigher-order logicInformation securityMalwareMathematical analysisSoftwareComputer-aided designBefehlsprozessorInclusion mapParsingBlogSpeicherschutzTime zoneException handlingLink (knot theory)Physical systemRead-only memoryControl flowTranslation (relic)Assembly languagePointer (computer programming)Open sourceShift operatorAliasingIntegerGenetic programmingoutputFunction (mathematics)Representation (politics)Constraint (mathematics)Graph (mathematics)Latent heatProgram slicingCodeInterpreter (computing)Greatest elementCoprocessorRepresentation (politics)Binary codeReverse engineeringVirtual machineBlogDisassemblerBitAssembly languageFocus (optics)String (computer science)outputInformationComputer programRevision controlSound effectFunction (mathematics)Variable (mathematics)Mathematical optimizationNumberResultantArmGame controllerDiagramCoefficient of determinationInformation securityDescriptive statisticsWordPhysical systemHard disk driveSemiconductor memoryLink (knot theory)Vulnerability (computing)Form (programming)Constraint (mathematics)Line (geometry)Multiplication signInternet der DingeState of matterUniverse (mathematics)Stack (abstract data type)Process (computing)Point (geometry)PlotterComputer fontFunctional (mathematics)SpeicherschutzRow (database)Lattice (order)MereologyRight angleSpacetimeConstructor (object-oriented programming)Set (mathematics)Exception handlingTablet computerSlide ruleForcing (mathematics)Natural numberComputer animationXML
09:47
Genetic programmingoutputFunction (mathematics)Representation (politics)Constraint (mathematics)Exception handlingInterrupt <Informatik>Computer programBefehlsprozessorFormal verificationArmReduced instruction set computing10 (number)Branch (computer science)Stress (mechanics)Suite (music)Graph (mathematics)Latent heatSoftware testingBitLine (geometry)MikrokernelLoop (music)WebsiteDrop (liquid)Basis <Mathematik>Computer programSystem callEndliche ModelltheorieKernel (computing)Graph (mathematics)Spacetime2 (number)Exception handlingCASE <Informatik>Hard disk driveSpeicherschutzWordSoftware bugComputer simulationInformation securityEntire functionRight angleIntermediate value theoremInterface (computing)Moment (mathematics)FeedbackoutputCodeCalculationFunctional (mathematics)Pointer (computer programming)Clique problemDifferent (Kate Ryan album)Sound effectConstraint (mathematics)Axiom of choiceSemiconductor memoryForcing (mathematics)NumberSoftwareCoprocessorControl flowBinary codeArmComputer-generated imageryReal numberProcess (computing)Computer architectureLogicMaxima and minimaFuzzy logicSymbol tableReading (process)Point (geometry)Stack (abstract data type)Goodness of fitMessage passingComputer animationEngineering drawingDrawingDiagramProgram flowchart
19:04
Formal verificationArmBefehlsprozessorPhysical systemMathematical analysisInformationSoftware testingHigher-order logicData conversionDisassemblerAssembly languagePerformance appraisalPersonal digital assistantInterpreter (computing)FeedbackCoprocessorSoftwareComputer programHacker (term)Menu (computing)Model checkingOrder (biology)Maxima and minimaWikiRight angleOperating systemGraph (mathematics)Process (computing)Computer hardwareSequenceCategory of beingSystem callCodeVapor barrierMultiplication signFormal verificationLine (geometry)Sign (mathematics)Latent heatMatching (graph theory)Computer fileFormal languageConstraint (mathematics)outputArmCombinational logicDigital rights managementTheory of relativityTheoryBitNumberLogicVirtual machinePhysical lawSlide ruleForm (programming)Hacker (term)Electronic mailing listCountingSoftware testingOcean currentState of matterFuzzy logicComputer programExpressionGoodness of fitInheritance (object-oriented programming)Compilation albumPhysical systemImperative programmingPoint (geometry)AngleCoprocessorVacuumVideo gameLibrary (computing)Projective planeProgramming languageControl flowGame controllerOpen sourceReverse engineeringComplete metric spaceSoftware developerVideoconferencingShared memoryRoundness (object)Bound stateSoftware bugQuicksortDigital electronicsSoftwareWriting1 (number)Computer engineeringEngineering drawingDiagramComputer animation
28:21
MedianPauli exclusion principleComputer animationJSONXMLUML
Transcript: English(auto-generated)
00:14
He has been publishing in academia for almost 30 years. Please join me in giving him a warm welcome to 34C3.
00:30
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.
00:44
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
01:00
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
01:20
also about back in April ARM released their specification in machine readable form and I should say that I'm working with Cambridge University to turn that into something you can use. So this talk, I'm going to mostly actually talk about this executable processor specification.
01:46
That's going to be the bulk of the talk but at the end that sets me up very nicely to talk about formally verified software. So I thought given the theme of the Congress, it would be more useful to emphasize things you could actually do.
02:03
So this 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.
02:20
So there's lots of really interesting stuff if you're interested in how secure your device is 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 spec right now from the first link but please wait till the end of the talk. There's also the specification rendered as HTML, there's tools that can take the specification
02:47
release apart and find useful information in it. I've written blogs and papers about it as well. So let's just dive in to look at the bits of the actual specification. So the first thing is all the really important security features in our processor are controlled
03:09
by what are called the system control registers. The top dog among all those control registers is this one here called SCTLR, just trips off the tongue doesn't it?
03:21
So SCTLR is where it's full of lots of individual control bits which affect either optimisations the processor is doing or also security features. So let's just zoom in on one of them to give you an idea of what kind of information the spec contains.
03:40
So here's some documentation telling you about the WXN bit. What does that do? It makes sure that any code, that your stack cannot contain code. You can't put instructions on the code on the stack because if you set this bit the processor won't execute them.
04:01
In other words, this is the bit that triggered the requirement for things like return-oriented programming. So what can you do with this practically? Well, suppose you're in the habit of reverse engineering some code.
04:20
Your disassembler might 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 our, how to decode some of the more cryptic parts and go oh
04:43
actually, it's that SCTLR register, so you could decode the cryptic 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
05:05
of use the information from the XML to render it perhaps 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 feeling really
05:22
energetic, you could, when you click on it, mouse over, whatever, it could bring up some of that documentation, and that makes it much easier to understand what the cryptic piece of code at the top is doing. 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,
05:49
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 it's possible to
06:04
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 top line of typewriter font, and then turn that into strings,
06:27
which is what the code at the bottom is describing how to do. 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.
06:46
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,
07:05
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.
07:21
Let's suppose I've taken instruction, and I match it against that diagram there. I might get some values for some of the variables from that, and then I can walk through, step by step, evaluating this code until I eventually realise that register five is having some value assigned to it.
07:42
Okay, so that's a fairly basic thing you can do with a specification. An interpreter is a fairly easy thing to implement, but once you have it, there's a lot you can build on top of it. One thing that's surprisingly easy to implement is to extract a symbolic representation of what the instruction does.
08:01
So I'll just show you quickly how you do that using the interpreter. So let's take those same concrete values, but 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 of five or 32, I'll also build up a graph representing exactly how I came up with these values,
08:27
like 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.
08:43
So I now have a symbolic representation of one slice 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.
09:01
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,
09:23
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. So if you're trying to figure out how some particular register could be accessed,
09:40
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, if you know some value you want to see there, you can ask what the inputs that would cause that to happen.
10:04
So if any of you are familiar with tools like CLAY, which is a symbolic execution tool based on LLVM, then they use something similar to this. So I've shown you a fairly simple graph, something I could show you how you build it kind of on the fly.
10:25
This 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 calculating whether to take a branch or not. So this is about 80 or 90 nodes.
10:42
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 then can point at something and say,
11:03
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's stuff that handles exceptions, it fetches instructions, it executes instructions, it contains all instructions,
11:23
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 a constraint solver and it will come back and give you an answer. And this graph for the full specification is quite large.
11:43
It's about half a million nodes, and that's for the smallest specification that Arm uses. So it's about half a million nodes, but the great thing is modern constraint solvers can read in that half a million nodes and still give you answers, typically in about 1 to 10 seconds for most of the questions I've posed to them.
12:04
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.
12:23
Okay, so I've talked a lot about instructions, but most of us actually run programs, right? So to turn this specification into something that can execute programs, in other words, to turn it into a simulator for the Arm architecture, you need to add a little bit of a loop that will handle in drops,
12:43
fetch instructions, and then it can execute them and handle any exceptions. So I did this. I added this loop to the specification, and then I thought I'd better try testing the specification. And so the good news for me, because I work for Arm,
13:03
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's extremely thorough. It has tens of thousands of test programs in it, runs billions of instructions.
13:21
And so I set about 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? At 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.
13:42
OK, so 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 saying is Arm's official specification could not pass Arm's official test suite when I started.
14:01
I mean, 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 any real
14:23
world system and actually test it against the test suite, well, first of all, you'd find it's not an executable specification most of 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.
14:40
It didn't pass any tests. In fact, it took me weeks to get the process or the specification to come out of reset, right? Just to get to starting to execute the first instruction took weeks. So, and I think you'd find this if you were to try any other specification.
15:04
So, okay, so moving on to useful things 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.
15:24
And it pretty much always breaks. And a modern fuzz tester 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.
15:41
So if it's finding, so in particular, it monitors whether the program is taking a branch or not. And if it sees it's taking lots of new branches, then it goes, okay, I'll keep trying more of what I'm doing at the moment because it seems to be effective. And if it's not finding any new branches, then it will look for something else to try changing.
16:03
So that's kind of the 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 binary
16:20
that we were analyzing, but also in the specification. And what this gave us was basically if you've got, suppose 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
16:41
and it quickly moves on to something else. But maybe your straight line code 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 memory, in which case there's memory protection checks.
17:00
There's also checks for is this a device register or is this 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 little microkernel,
17:23
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?
17:40
And the answer was, there was a bug in the microkernel and what it did was, the first thing it would do is read where the stack pointer was pointing. So it would do a read from one of the devices, which wasn't really what was intended. In fact, it completely breaks the security model. So fuzz testing using not just coverage
18:04
of the monitoring branches in the binary, but also the specification, can find you a bunch of really interesting things. And so I hope some of you will pick this idea up and run with it. So the reason that I was doing all this work
18:21
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 a overly simplified picture of a process.
18:43
So 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 in extra logic, which will monitor the values at the start of an instruction executing
19:01
and 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.
19:21
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 that 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 it will actually try multiple steps,
19:41
all possible combinations of inputs for one instruction, two instructions, three instructions, longer and longer sequences of instructions looking for ways that can fail the property. So, and this turned out to be an incredibly effective way of finding bugs in our processors. We're actually going to be using this
20:01
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 talk by Clifford Wolf from a couple of hours ago, which describes a very similar process. Okay, so I'm encouraging you to take this specification
20:24
and find something awesome to do with it. There's a bunch of ideas I've suggested there, and there's a few extras which I didn't have time to describe here. But now, let me turn to the title of the talk. How can you trust formally verified software?
20:41
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 on top of some operating system that they use some libraries and they're also written in some programming language.
21:02
And so, when you verify your program against your specification, you're also verifying them against the specifications of Linux, GLibc, and IsoC, none of which have good specifications. In fact, yeah, they're just terrible specifications
21:22
which bear little resemblance to what compilers and operating systems actually do in practice. So, 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.
21:42
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.
22:01
It's a lot better for being formally verified, but I'd also want to test it quite thoroughly and maybe do 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,
22:23
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 audience, then do please talk to me or Milosz Mariak, who's here in the front row, if you're interested in working at ARM.
22:42
And I'd 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.
23:01
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 Alistair 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?
23:21
No questions yet. Okay, then let's go to microphone number one. Hi, I was just... Maybe tiptoes. Yeah. I was just curious how you're actually using the machine specification in order to generate VCs for the SMP solver, because you didn't really
23:41
get a chance to talk about that, I guess. Try to think how I can describe that briefly. The 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
24:03
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 there's control flow, whenever the control flow joins back up, I have to introduce things to select between the value that was calculated in the left or the right, and so on.
24:24
I guess I'm mostly curious about what logics you're using for the solvers and stuff like that. Or is it just very basic solvers because they run fastest. And then... Thank you. So microphone six, please. Thank you. I was just wondering if you could talk a little bit
24:42
about the language you used to write your specification. 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 that ARM had started writing
25:00
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 just a very simple,
25:23
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 not a complicated language. It's actually designed so that as many people as possible
25:43
can read it and know exactly what it says without any doubt, without having to consult a language lawyer. Signal Angel, yet anything? Yes, now we've got a question. Has ARM its own form of Intel's management engine?
26:08
No, it's a short answer. Yeah, I don't think we have anything quite like that. If you, yeah, I'll just say no.
26:21
Microphone one. Hi, on that question that we had before about the specification language, have you considered using Z3's own language for expressing the instructions? So Z3's own language is basically you write kind of S expressions,
26:40
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, this specification is designed so that people can look at it and go, ah, I see what's going on here and not have, and just try to minimize the barriers. Fair enough.
27:01
Okay, last call, Signal Angel. How long does the complete test of the ARM specification take? About two years. So yeah, so a modern processor team, about 80% of that team will be verification engineers.
27:23
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 mostly works, and after that it's kind of debugging it and it's kind of fine tuning the performance.
27:46
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.
28:03
But yeah, I don't know. And we use a lot of processors in parallel, so I really don't have an idea. Thank you so much, Alistair. Let's give him another warm round of applause. Thank you so much.