[Script Info]
Title: 
[Events]
Format: Layer, Start, End, Style, Name, MarginL, MarginR, MarginV, Effect, Text
Dialogue: 0,0:00:00.00,0:00:14.71,Default,,0000,0000,0000,,{\i1}34c3 intro{\i0}
Dialogue: 0,0:00:14.71,0:00:16.29,Default,,0000,0000,0000,,\NHerald: He's been publishing in academia
Dialogue: 0,0:00:16.29,0:00:22.52,Default,,0000,0000,0000,,for almost 30 years. Please join me in\Ngiving him a warm welcome to 34c3.
Dialogue: 0,0:00:22.52,0:00:30.37,Default,,0000,0000,0000,,{\i1}Applause{\i0}\NAlastiar Reid: Thank you very much for
Dialogue: 0,0:00:30.37,0:00:35.80,Default,,0000,0000,0000,,your introduction. So I'm going to be\Ntalking about the ARM processors and
Dialogue: 0,0:00:35.80,0:00:41.30,Default,,0000,0000,0000,,they're incredibly widely used. You find\Nthem in phones, tablets, IOT devices,
Dialogue: 0,0:00:41.30,0:00:46.45,Default,,0000,0000,0000,,hard-disk drives; they're all over. And if\Nyou think about it, what I'm saying is:
Dialogue: 0,0:00:46.45,0:00:50.50,Default,,0000,0000,0000,,They're in all the things, which contain\Nyour most private and personal data, so
Dialogue: 0,0:00:50.50,0:00:54.82,Default,,0000,0000,0000,,it's really, really important that they do\Nexactly what they should be doing and
Dialogue: 0,0:00:54.82,0:00:59.47,Default,,0000,0000,0000,,nothing else. We need to make sure we\Nreally understand them and that means it's
Dialogue: 0,0:00:59.47,0:01:05.31,Default,,0000,0000,0000,,important that we can analyze them for any\Nmalware, look for vulnerabilities and so
Dialogue: 0,0:01:05.31,0:01:11.99,Default,,0000,0000,0000,,on. So I'm going to be talking about some\Nwork I started about six years ago,
Dialogue: 0,0:01:11.99,0:01:19.56,Default,,0000,0000,0000,,creating a very precise specification of\Nwhat an ARM processor does and I'm going
Dialogue: 0,0:01:19.56,0:01:26.67,Default,,0000,0000,0000,,to be talking also about back in April I'm\Nreleased this their specification in a
Dialogue: 0,0:01:26.67,0:01:34.19,Default,,0000,0000,0000,,machine readable form. And I should say\Nthat I'm working with Kimbridge University
Dialogue: 0,0:01:34.19,0:01:42.54,Default,,0000,0000,0000,,to turn that in something you can use. So\Nso this talk I'm going to mostly actually
Dialogue: 0,0:01:42.54,0:01:47.56,Default,,0000,0000,0000,,talk about this executable processor\Nspecification, that's going to be the bulk
Dialogue: 0,0:01:47.56,0:01:53.25,Default,,0000,0000,0000,,of the talk but at the end that sets me up\Nvery nicely to talk about a formally
Dialogue: 0,0:01:53.25,0:01:57.98,Default,,0000,0000,0000,,verified software. So I thought, given the\Ntheme of the Congress, it would be more
Dialogue: 0,0:01:57.98,0:02:05.54,Default,,0000,0000,0000,,useful to emphasize things you could\Nactually do. So the specification that ARM
Dialogue: 0,0:02:05.54,0:02:10.66,Default,,0000,0000,0000,,released, what's in it? Well, there's lots\Nof instruction descriptions of course but
Dialogue: 0,0:02:10.66,0:02:14.69,Default,,0000,0000,0000,,there's also lots of really interesting\Nsecurity features; things to do with
Dialogue: 0,0:02:14.69,0:02:20.38,Default,,0000,0000,0000,,memory protection, exceptions, privilege\Nchecks and so on.
Dialogue: 0,0:02:20.38,0:02:24.44,Default,,0000,0000,0000,,So there's lots of really interesting\Nstuff ... of your interest in their how
Dialogue: 0,0:02:24.44,0:02:30.69,Default,,0000,0000,0000,,secure your devices and how to make sure\Nit really is secure. Throughout the talk
Dialogue: 0,0:02:30.69,0:02:36.08,Default,,0000,0000,0000,,I'll be giving a bunch of links; you can\Ngo and download the specs right now from
Dialogue: 0,0:02:36.08,0:02:42.58,Default,,0000,0000,0000,,the first link but please wait to the end\Nof the talk and there's also the
Dialogue: 0,0:02:42.58,0:02:47.79,Default,,0000,0000,0000,,specification rendered as HTML, as tools\Nthat can take the specification release
Dialogue: 0,0:02:47.79,0:02:52.56,Default,,0000,0000,0000,,apart and find useful information in it;\NI've written blogs and papers about it as
Dialogue: 0,0:02:52.56,0:03:00.91,Default,,0000,0000,0000,,well. And so let's just dive into, look at\Nthe bits of the actual specification. So
Dialogue: 0,0:03:00.91,0:03:07.15,Default,,0000,0000,0000,,the first thing is all the really\Nimportant security features in the specif-
Dialogue: 0,0:03:07.15,0:03:13.07,Default,,0000,0000,0000,,in our processor are controlled by, what I\Ncall, the system control registers and the
Dialogue: 0,0:03:13.07,0:03:19.57,Default,,0000,0000,0000,,top dog among all those control registers\Nis this one here called SCTLR. Just trips
Dialogue: 0,0:03:19.57,0:03:26.37,Default,,0000,0000,0000,,off the tongue, doesn't it? So SCTLR is\Nwhere - it's full of lots of individual
Dialogue: 0,0:03:26.37,0:03:32.12,Default,,0000,0000,0000,,control bits, which affect either\Noptimizations, the processor's doing, or
Dialogue: 0,0:03:32.12,0:03:36.95,Default,,0000,0000,0000,,also security features. And so let's just\Nzoom in and one of them, to give you an
Dialogue: 0,0:03:36.95,0:03:40.21,Default,,0000,0000,0000,,idea of what kind of information the spec\Ncontains.
Dialogue: 0,0:03:40.21,0:03:46.77,Default,,0000,0000,0000,,So here's some documentation, telling you\Nabout a WXN bit. What does that do? It
Dialogue: 0,0:03:46.77,0:03:53.19,Default,,0000,0000,0000,,makes sure that any code, any, that your\Nstack cannot contain code. you can't boot
Dialogue: 0,0:03:53.19,0:03:58.25,Default,,0000,0000,0000,,instructions on the code, and on the\Nstack, because they're proce- if you set
Dialogue: 0,0:03:58.25,0:04:04.18,Default,,0000,0000,0000,,this bit the processor won't execute them.\NIn other words: This is the bit that
Dialogue: 0,0:04:04.18,0:04:12.22,Default,,0000,0000,0000,,triggered the requirement for things like\Nreturn-oriented programming. Okay, so what
Dialogue: 0,0:04:12.22,0:04:18.38,Default,,0000,0000,0000,,can you do with this fact? Well, suppose\Nyou're in the habit of reverse engineering
Dialogue: 0,0:04:18.38,0:04:24.31,Default,,0000,0000,0000,,some code. You might, your disassemble may\Nshow you something like this. And you're
Dialogue: 0,0:04:24.31,0:04:28.12,Default,,0000,0000,0000,,probably all staring at this going: "What\Non earth does that do?", because it's
Dialogue: 0,0:04:28.12,0:04:33.13,Default,,0000,0000,0000,,extremely cryptic. But using the\Ninformation that's in the XML version of
Dialogue: 0,0:04:33.13,0:04:40.71,Default,,0000,0000,0000,,the release you could easily figure out\Nhow to build, how to decode some of the
Dialogue: 0,0:04:40.71,0:04:45.71,Default,,0000,0000,0000,,more cryptic parts and go "Oh actually,\Nit's that SCTLR register", right, so you
Dialogue: 0,0:04:45.71,0:04:50.49,Default,,0000,0000,0000,,could decode the cryptic name for the\Nnumber for the register into that. But you
Dialogue: 0,0:04:50.49,0:04:54.72,Default,,0000,0000,0000,,could do a bit more than that. You can see\Nit's setting one of the bits in the
Dialogue: 0,0:04:54.72,0:05:00.99,Default,,0000,0000,0000,,register so - it is of course the bit I\Njust told you about WXN, so we could dig
Dialogue: 0,0:05:00.99,0:05:08.74,Default,,0000,0000,0000,,into that and, so we could kind of use the\Ninformation from the XML to render it,
Dialogue: 0,0:05:08.74,0:05:13.56,Default,,0000,0000,0000,,perhaps, as like this.\NSo you can make things a bit more useful
Dialogue: 0,0:05:13.56,0:05:17.55,Default,,0000,0000,0000,,and you can also take that documentation\Nthat was there, that told you what the WXN
Dialogue: 0,0:05:17.55,0:05:23.47,Default,,0000,0000,0000,,bit does, and maybe, if you're a feeling\Nreally energetic, you could, when you
Dialogue: 0,0:05:23.47,0:05:27.32,Default,,0000,0000,0000,,click on it, mouse over or whatever, it\Ncould bring up some of that documentation.
Dialogue: 0,0:05:27.32,0:05:31.87,Default,,0000,0000,0000,,And and that makes specf- that makes it\Nmuch easier to understand what the cryptic
Dialogue: 0,0:05:31.87,0:05:36.24,Default,,0000,0000,0000,,piece of code at the top is doing. Okay,\Nso that's just a very shallow thing you
Dialogue: 0,0:05:36.24,0:05:43.72,Default,,0000,0000,0000,,can get from the specification. If we dig\Ninto the instruction descriptions there's
Dialogue: 0,0:05:43.72,0:05:52.57,Default,,0000,0000,0000,,also things like the assembly language of\N- the specification of the assembly syntax
Dialogue: 0,0:05:52.57,0:05:59.03,Default,,0000,0000,0000,,and. So, something I did a few years ago\Nand which I just wrote a blog article
Dialogue: 0,0:05:59.03,0:06:05.19,Default,,0000,0000,0000,,about over the weekend was was it's\Npossible to actually take that
Dialogue: 0,0:06:05.19,0:06:09.90,Default,,0000,0000,0000,,specification, turn it into a\Ndisassembler. So I first of all
Dialogue: 0,0:06:09.90,0:06:16.17,Default,,0000,0000,0000,,transformed it into the code I'm showing\Nat the bottom. What this is showing is how
Dialogue: 0,0:06:16.17,0:06:18.25,Default,,0000,0000,0000,,to\Ntake a binary description of an
Dialogue: 0,0:06:18.25,0:06:25.71,Default,,0000,0000,0000,,instruction so that's the the top line of\Ntypewriter font and and then turn that
Dialogue: 0,0:06:25.71,0:06:31.47,Default,,0000,0000,0000,,into strings, which is what this the code\Nat the bottom is describing how to do. So
Dialogue: 0,0:06:31.47,0:06:35.24,Default,,0000,0000,0000,,so you can use this as a disassembler.\NIt's actually possible to run it in
Dialogue: 0,0:06:35.24,0:06:41.94,Default,,0000,0000,0000,,reverse and use it as an assembler; you\Nbasically run the code from bottom to top
Dialogue: 0,0:06:41.94,0:06:47.08,Default,,0000,0000,0000,,and you can turn strings into binary\Ninstructions. And we'll see more of this
Dialogue: 0,0:06:47.08,0:06:57.43,Default,,0000,0000,0000,,running things in reverse in a few slides\Ntime. So the main thing about instructions
Dialogue: 0,0:06:57.43,0:07:03.33,Default,,0000,0000,0000,,is of course they do something. So the\Nspecification contains a description of
Dialogue: 0,0:07:03.33,0:07:08.65,Default,,0000,0000,0000,,exactly what an instruction does and that\Ndescription is as code, which, as a
Dialogue: 0,0:07:08.65,0:07:13.15,Default,,0000,0000,0000,,programmer, makes me very happy, right. I\Ndon't understand the English words in the
Dialogue: 0,0:07:13.15,0:07:17.90,Default,,0000,0000,0000,,specification but I do understand what the\Ncode does. So one thing you can do with
Dialogue: 0,0:07:17.90,0:07:22.22,Default,,0000,0000,0000,,code is execute it, so let's just walk\Nthrough - let's suppose ... take an
Dialogue: 0,0:07:22.22,0:07:29.30,Default,,0000,0000,0000,,instruction and I match against that\Ndiagram there. I might get some values for
Dialogue: 0,0:07:29.30,0:07:35.68,Default,,0000,0000,0000,,for some of the variables from that and\Nthen I can walk through, step by step,
Dialogue: 0,0:07:35.68,0:07:40.38,Default,,0000,0000,0000,,evaluating this code, until I eventually\Nrealize that register five is having some
Dialogue: 0,0:07:40.38,0:07:43.89,Default,,0000,0000,0000,,value assigned to it.\NOkay, so that's a fairly basic thing you
Dialogue: 0,0:07:43.89,0:07:47.38,Default,,0000,0000,0000,,can do with the specification;\Ninterpreters are fairly easy thing to
Dialogue: 0,0:07:47.38,0:07:53.21,Default,,0000,0000,0000,,implement but once you have it there's a\Nlot you can build on top of it. And one
Dialogue: 0,0:07:53.21,0:07:57.82,Default,,0000,0000,0000,,thing that's surprisingly easy to\Nimplement is to extract a symbolic
Dialogue: 0,0:07:57.82,0:08:01.68,Default,,0000,0000,0000,,representation of what the instruction\Ndoes. So I'll just show you quickly how
Dialogue: 0,0:08:01.68,0:08:07.40,Default,,0000,0000,0000,,you do that, using the interpreter. So\Nlet's take those same concrete values but
Dialogue: 0,0:08:07.40,0:08:11.60,Default,,0000,0000,0000,,I'm also, I've added three other variables\Nat the side there, which I'm going to
Dialogue: 0,0:08:11.60,0:08:16.62,Default,,0000,0000,0000,,treat as symbolic variables. And as I walk\Nthrough the code I won't just calculate
Dialogue: 0,0:08:16.62,0:08:24.23,Default,,0000,0000,0000,,some concrete values, like the value five\Nor 32, I'll also build up a graph,
Dialogue: 0,0:08:24.23,0:08:29.71,Default,,0000,0000,0000,,representing exactly how I came up with\Nthese values at five and so on. So as I'm
Dialogue: 0,0:08:29.71,0:08:34.83,Default,,0000,0000,0000,,executing the code I can build a graph\Nrepresenting exactly what this code is
Dialogue: 0,0:08:34.83,0:08:41.19,Default,,0000,0000,0000,,doing. And what I can do now is just throw\Naway the code and focus on what that graph
Dialogue: 0,0:08:41.19,0:08:46.26,Default,,0000,0000,0000,,is telling me.\NSo I now have a symbolic representation of
Dialogue: 0,0:08:46.26,0:08:51.54,Default,,0000,0000,0000,,one slice through that, through that\Ninstruction and I can feed that to a
Dialogue: 0,0:08:51.54,0:08:56.37,Default,,0000,0000,0000,,constraint solver, so if any of you have\Nheard of Z3 or SMT solvers, that's what
Dialogue: 0,0:08:56.37,0:09:05.13,Default,,0000,0000,0000,,I'm talking about here. And a constraint\Nsolver is a really useful tool, because
Dialogue: 0,0:09:05.13,0:09:09.94,Default,,0000,0000,0000,,you can run code forwards through it, so\Ngiven some input values you can say what
Dialogue: 0,0:09:09.94,0:09:16.93,Default,,0000,0000,0000,,are the outputs from this function or\Nfrom this instruction but you can also run
Dialogue: 0,0:09:16.93,0:09:22.28,Default,,0000,0000,0000,,them backwards, given some\Noutput value, some final result you want
Dialogue: 0,0:09:22.28,0:09:26.79,Default,,0000,0000,0000,,to see, you can ask what inputs would\Ncause this to happen. And this is just
Dialogue: 0,0:09:26.79,0:09:31.07,Default,,0000,0000,0000,,tremendously useful if you're trying to\Nfigure out what instructions you want to
Dialogue: 0,0:09:31.07,0:09:36.39,Default,,0000,0000,0000,,use to generate some particular effect.\NAll right, so if you're trying to figure
Dialogue: 0,0:09:36.39,0:09:41.80,Default,,0000,0000,0000,,out how some particular register could be\Naccessed, how some particular thing could
Dialogue: 0,0:09:41.80,0:09:47.45,Default,,0000,0000,0000,,be turned on or off, being able to ask\Nwhat inputs will cause this to happen is
Dialogue: 0,0:09:47.45,0:09:53.57,Default,,0000,0000,0000,,incredibly useful. And you can also use\Nthe constraint solver to ask for
Dialogue: 0,0:09:53.57,0:09:58.07,Default,,0000,0000,0000,,intermediate values, in the middle of the\Ncalculation. You know if you know some
Dialogue: 0,0:09:58.07,0:10:02.86,Default,,0000,0000,0000,,value you want to see there you can ask\Nwhat the inputs that would cause that to
Dialogue: 0,0:10:02.86,0:10:07.26,Default,,0000,0000,0000,,happen.\NSo, if any of you are familiar with tools
Dialogue: 0,0:10:07.26,0:10:13.95,Default,,0000,0000,0000,,like KLEE, which is a symbolic execution\Ntool for based on LLVM, then they use
Dialogue: 0,0:10:13.95,0:10:19.100,Default,,0000,0000,0000,,something similar to this. So, I've shown\Nyou are fairly simple draft, something I
Dialogue: 0,0:10:19.100,0:10:26.30,Default,,0000,0000,0000,,could show you how you build it, kind of\Non the fly. This is the actual graph for
Dialogue: 0,0:10:26.30,0:10:31.26,Default,,0000,0000,0000,,that same instruction. Here I've added in\Na lot more nodes to do with some of the
Dialogue: 0,0:10:31.26,0:10:35.98,Default,,0000,0000,0000,,functions that were being called and to do\Nwith the calculating, whether to take a
Dialogue: 0,0:10:35.98,0:10:46.28,Default,,0000,0000,0000,,branch or not. So this is about 80 or 90\Nnodes. And I've been experimenting with
Dialogue: 0,0:10:46.28,0:10:52.36,Default,,0000,0000,0000,,extending this in two ways. So this is\Njust one path through the execution of an
Dialogue: 0,0:10:52.36,0:10:56.78,Default,,0000,0000,0000,,instruction, so one way to improve on that\Nis to build a graph that represents all
Dialogue: 0,0:10:56.78,0:11:00.50,Default,,0000,0000,0000,,possible paths through the instruction.\NAnd that's much more useful, because you
Dialogue: 0,0:11:00.50,0:11:04.99,Default,,0000,0000,0000,,can you then can point at something and\Nsay "how can I make that happen?" and it
Dialogue: 0,0:11:04.99,0:11:11.92,Default,,0000,0000,0000,,will tell you exactly what inputs will\Ncause the path that will make that happen.
Dialogue: 0,0:11:11.92,0:11:16.35,Default,,0000,0000,0000,,I've also been experimenting with taking\Nthe entire specification, right, so that
Dialogue: 0,0:11:16.35,0:11:20.51,Default,,0000,0000,0000,,stuff that handles exceptions, that\Nfetches instructions or execute
Dialogue: 0,0:11:20.51,0:11:24.70,Default,,0000,0000,0000,,instructions. It contains all\Ninstructions. And I've been experimenting
Dialogue: 0,0:11:24.70,0:11:29.79,Default,,0000,0000,0000,,with building a graph representing the\Nentire specification all at once. And
Dialogue: 0,0:11:29.79,0:11:33.47,Default,,0000,0000,0000,,that's even more useful, because now\Npretty much any question you have about
Dialogue: 0,0:11:33.47,0:11:36.72,Default,,0000,0000,0000,,the specification, you can ask the\Nconstraint solver and it will come back
Dialogue: 0,0:11:36.72,0:11:43.49,Default,,0000,0000,0000,,and give you an answer. And this graph for\Nthe full specification is quite large.
Dialogue: 0,0:11:43.49,0:11:48.54,Default,,0000,0000,0000,,It's about half a million nodes and that's\Nfor the smallest specification that our
Dialogue: 0,0:11:48.54,0:11:53.05,Default,,0000,0000,0000,,major uses. So it's about half a million\Nnodes. But the great thing is modern
Dialogue: 0,0:11:53.05,0:11:58.01,Default,,0000,0000,0000,,constraint solvers can read in that half\Nmillion nodes and still give you answers.
Dialogue: 0,0:11:58.01,0:12:04.04,Default,,0000,0000,0000,,Typically in about 1 to 10 seconds for\Nmost of the questions posed to them. So,
Dialogue: 0,0:12:04.04,0:12:08.26,Default,,0000,0000,0000,,these are just tremendously useful tools,\Nif you're wanting to be able to understand
Dialogue: 0,0:12:08.26,0:12:15.67,Default,,0000,0000,0000,,exactly what the specification does,\Nand exactly how some program is going to
Dialogue: 0,0:12:15.67,0:12:20.69,Default,,0000,0000,0000,,behave or figure out what program you want\Nto write to make it behave some particular
Dialogue: 0,0:12:20.69,0:12:28.85,Default,,0000,0000,0000,,way. Okay so I've talked a lot about\Ninstructions, but most of us actually run
Dialogue: 0,0:12:28.85,0:12:33.99,Default,,0000,0000,0000,,programs, right? So to turn this the\Nspecification into something in execute
Dialogue: 0,0:12:33.99,0:12:38.26,Default,,0000,0000,0000,,programs, in other words turn it into a\Nsimulator for the ARM architecture, you
Dialogue: 0,0:12:38.26,0:12:43.84,Default,,0000,0000,0000,,need to add a little bit of a loop that\Nwill handle interrupts, fake instructions
Dialogue: 0,0:12:43.84,0:12:49.98,Default,,0000,0000,0000,,and then it can execute them and handle\Nany exceptions. So, I... So I did this. I
Dialogue: 0,0:12:49.98,0:12:55.86,Default,,0000,0000,0000,,added this loop to this specification. And\Nthen, I thought I'd better try testing the
Dialogue: 0,0:12:55.86,0:13:03.61,Default,,0000,0000,0000,,specification. And, so the good news for\Nme, because I work for ARM I have access
Dialogue: 0,0:13:03.61,0:13:08.26,Default,,0000,0000,0000,,to ARM's internal test suite. Which is\Nsomething that ARM has been working on
Dialogue: 0,0:13:08.26,0:13:12.72,Default,,0000,0000,0000,,basically since the company started 25, 30\Nyears ago. So it's quite a large test
Dialogue: 0,0:13:12.72,0:13:17.58,Default,,0000,0000,0000,,suite. It is extremely thorough, has tens\Nof thousands of test programs in it, runs
Dialogue: 0,0:13:17.58,0:13:25.14,Default,,0000,0000,0000,,billions of instructions. And so I set\Nabout testing the, testing the
Dialogue: 0,0:13:25.14,0:13:30.12,Default,,0000,0000,0000,,specification using this test suite. And\Nif any of you have tested software you'll
Dialogue: 0,0:13:30.12,0:13:33.62,Default,,0000,0000,0000,,be familiar with a graph that looks like\Nthis, right? The start things don't work
Dialogue: 0,0:13:33.62,0:13:39.53,Default,,0000,0000,0000,,all that well. Gradually you get things\Nworking pretty well but then there's a
Dialogue: 0,0:13:39.53,0:13:45.90,Default,,0000,0000,0000,,heavy tail of difficult to find bugs.\NOkay, so, and that's basically what I
Dialogue: 0,0:13:45.90,0:13:49.87,Default,,0000,0000,0000,,found when I was testing the\Nspecification. But you should all be
Dialogue: 0,0:13:49.87,0:13:56.38,Default,,0000,0000,0000,,shocked by what I just said. Because what\NI'm seeing is ARM's official specification
Dialogue: 0,0:13:56.38,0:14:03.29,Default,,0000,0000,0000,,could not pass ARM's official test suite\Nwhen I started, right. I mean that's
Dialogue: 0,0:14:03.29,0:14:10.27,Default,,0000,0000,0000,,that's pretty shocking. And I'm telling\Nyou this and emphasizing it, not because
Dialogue: 0,0:14:10.27,0:14:16.85,Default,,0000,0000,0000,,I think ARM's specification was especially\Nbad. I think it was just typically bad. I
Dialogue: 0,0:14:16.85,0:14:22.59,Default,,0000,0000,0000,,think if you were to take any\Nspecification for, you know, any real-
Dialogue: 0,0:14:22.59,0:14:27.82,Default,,0000,0000,0000,,world system and actually test it against\Nthe test suite, well first of all you'd
Dialogue: 0,0:14:27.82,0:14:32.39,Default,,0000,0000,0000,,find it's not an executable specification\Nmost the time and secondly you'd find it
Dialogue: 0,0:14:32.39,0:14:38.50,Default,,0000,0000,0000,,wouldn't work. And you'd probably find it\Nwould work as badly as ARM's did. So it's
Dialogue: 0,0:14:38.50,0:14:42.85,Default,,0000,0000,0000,,not just that it didn't pass all the\Ntests. It didn't pass any tests. In fact
Dialogue: 0,0:14:42.85,0:14:47.81,Default,,0000,0000,0000,,it took me weeks to get the processor or\Nthe specification to come out of reset.
Dialogue: 0,0:14:47.81,0:14:54.01,Default,,0000,0000,0000,,Right? Just to get the starting fix to get\Nthe first instruction took weeks. So and I
Dialogue: 0,0:14:54.01,0:15:00.38,Default,,0000,0000,0000,,think so I think you'd find this if you\Nwere to try any other specification.
Dialogue: 0,0:15:00.38,0:15:11.13,Default,,0000,0000,0000,,What's my next slide? So, moving on to\Nuseful thing you can do with the
Dialogue: 0,0:15:11.13,0:15:16.96,Default,,0000,0000,0000,,specification, something we tried last\Nsummer was using it for fuzz testing. So,
Dialogue: 0,0:15:16.96,0:15:21.49,Default,,0000,0000,0000,,fuzz testing consists of taking a program\Nand throwing random inputs at the
Dialogue: 0,0:15:21.49,0:15:27.96,Default,,0000,0000,0000,,program and just seeing what breaks and it\Npretty much always breaks and a modern
Dialogue: 0,0:15:27.96,0:15:34.33,Default,,0000,0000,0000,,fuzztester like maybe AFL to make it\Nmore effective. It monitors something
Dialogue: 0,0:15:34.33,0:15:39.35,Default,,0000,0000,0000,,about how the program is executing and\Nuses that to guide its choice of what to
Dialogue: 0,0:15:39.35,0:15:45.18,Default,,0000,0000,0000,,change next. So, if it's finding...in\Nparticular monitor whether an
Dialogue: 0,0:15:45.18,0:15:50.18,Default,,0000,0000,0000,,instruction... whether the program is\Ntaking a branch or not and if it sees it's
Dialogue: 0,0:15:50.18,0:15:54.24,Default,,0000,0000,0000,,taking lots of new branches then it goes:\N"Ok I'll keep trying more of what I'm
Dialogue: 0,0:15:54.24,0:15:58.38,Default,,0000,0000,0000,,doing at the moment because it seems to be\Neffective, and if it's and not finding any
Dialogue: 0,0:15:58.38,0:16:03.91,Default,,0000,0000,0000,,new branches, then it will look for\Nsomething else to try changing. So, that's
Dialogue: 0,0:16:03.91,0:16:06.97,Default,,0000,0000,0000,,kind of a normal fuzzing. What you're\Ndoing is basically trying to kind of
Dialogue: 0,0:16:06.97,0:16:15.23,Default,,0000,0000,0000,,maximize your branch coverage. So, what we\Ndid though, when we did this with the
Dialogue: 0,0:16:15.23,0:16:20.39,Default,,0000,0000,0000,,specification, was, we actually monitored\Nbranches not just in the in the binary
Dialogue: 0,0:16:20.39,0:16:28.40,Default,,0000,0000,0000,,that we were analyzing but also in the\Nspecification. And what this gave us was
Dialogue: 0,0:16:28.40,0:16:33.04,Default,,0000,0000,0000,,basically: if you got.. Suppose, your the\Nbinary you're analyzing is just straight
Dialogue: 0,0:16:33.04,0:16:37.46,Default,,0000,0000,0000,,line code. There's no branches in it at\Nall. Then there's nothing really for your
Dialogue: 0,0:16:37.46,0:16:41.52,Default,,0000,0000,0000,,fuzzer to work with right. So it doesn't\Nsee that the code is interesting, it
Dialogue: 0,0:16:41.52,0:16:47.20,Default,,0000,0000,0000,,quickly moves on to something else.\NBut maybe your straight line cord is doing
Dialogue: 0,0:16:47.20,0:16:50.94,Default,,0000,0000,0000,,something really interesting, like\Naccessing a privileged register. Well,
Dialogue: 0,0:16:50.94,0:16:54.90,Default,,0000,0000,0000,,there will be a branch around that to\Ncheck that you do have the privilege you
Dialogue: 0,0:16:54.90,0:16:58.25,Default,,0000,0000,0000,,require.\NOr maybe it's accessing a memory in which
Dialogue: 0,0:16:58.25,0:17:03.65,Default,,0000,0000,0000,,cases memory protection checks. There's\Nalso checks for: Is this a device
Dialogue: 0,0:17:03.65,0:17:09.75,Default,,0000,0000,0000,,register? Or is this a kind of RAM or ROM?\NSo, there's a number of different branches
Dialogue: 0,0:17:09.75,0:17:13.43,Default,,0000,0000,0000,,there and that gives the fuzzer\Ninteresting things to... interesting
Dialogue: 0,0:17:13.43,0:17:20.32,Default,,0000,0000,0000,,feedback to play with. So, when we set\Nthis going on one of our microkernel,
Dialogue: 0,0:17:22.77,0:17:30.13,Default,,0000,0000,0000,,we analyzed the system call interface for\Nthat microkernel. And one of the things
Dialogue: 0,0:17:30.13,0:17:35.33,Default,,0000,0000,0000,,the fuzzer surprised us with was it said:\NSuppose I take the stack pointer and point
Dialogue: 0,0:17:35.33,0:17:39.94,Default,,0000,0000,0000,,it into the middle of this device space\Nand then take an exception immediately,
Dialogue: 0,0:17:39.94,0:17:45.53,Default,,0000,0000,0000,,what happens? And the answer was: there\Nwas a bug in the microkernel and what it
Dialogue: 0,0:17:45.53,0:17:48.68,Default,,0000,0000,0000,,did was: it first thing it would do is\Nread from the stack, where the stack
Dialogue: 0,0:17:48.68,0:17:55.32,Default,,0000,0000,0000,,pointer was pointing, so we do a read from\None of the devices, which doesn't wasn't
Dialogue: 0,0:17:55.32,0:18:00.06,Default,,0000,0000,0000,,really what was intended. In fact it\Ncompletely breaks a security model. So,
Dialogue: 0,0:18:00.06,0:18:06.61,Default,,0000,0000,0000,,fuzztesting using not just coverage of\Nthe monitoring branches in the binary but
Dialogue: 0,0:18:06.61,0:18:10.94,Default,,0000,0000,0000,,also the specification can find you a\Nbunch of really interesting things. And I
Dialogue: 0,0:18:10.94,0:18:20.11,Default,,0000,0000,0000,,hope some of you will I pick this idea up\Nand run with it. So, the reason that I was
Dialogue: 0,0:18:20.11,0:18:29.29,Default,,0000,0000,0000,,doing all this work was I wanted to be\Nable to formally verify ARM processors and
Dialogue: 0,0:18:29.29,0:18:34.77,Default,,0000,0000,0000,,so I needed to create a specification\Nbefore I could do that. So, sorry, let me
Dialogue: 0,0:18:34.77,0:18:42.69,Default,,0000,0000,0000,,just take a drink here... So, this is an\Noverly simplified picture of a processor,
Dialogue: 0,0:18:42.69,0:18:48.16,Default,,0000,0000,0000,,it's more or less what processors looked\Nlike 25, 30 years ago, in fact.
Dialogue: 0,0:18:48.16,0:18:53.17,Default,,0000,0000,0000,,But it's good enough for the example. So,\Nif you want to check a processor, is
Dialogue: 0,0:18:53.17,0:18:59.77,Default,,0000,0000,0000,,correct, then what you can do is: add an\Nextra logic, which will monitor the values
Dialogue: 0,0:18:59.77,0:19:03.14,Default,,0000,0000,0000,,at the start of an instruction executing\Nthe values that are finally produced at
Dialogue: 0,0:19:03.14,0:19:07.70,Default,,0000,0000,0000,,the end of an instruction executing, and\Nthen if you feed those the specification
Dialogue: 0,0:19:07.70,0:19:11.83,Default,,0000,0000,0000,,you can see what the right answer should\Nhave been. You can compare that with what
Dialogue: 0,0:19:11.83,0:19:17.62,Default,,0000,0000,0000,,the processor actually did. So, you can do\Nthis using a test-based approach, right:
Dialogue: 0,0:19:17.62,0:19:21.20,Default,,0000,0000,0000,,just feed in inputs and check that\Neverything matches.
Dialogue: 0,0:19:21.20,0:19:25.57,Default,,0000,0000,0000,,But you can also do it using a formal\Nverification tool called a "bounded model
Dialogue: 0,0:19:25.57,0:19:31.25,Default,,0000,0000,0000,,checker". And a bounded model checker is\Nlike one of those constraint solvers I
Dialogue: 0,0:19:31.25,0:19:36.76,Default,,0000,0000,0000,,mentioned earlier on crack cocaine. So,\Nwhat it will do is: it won't just try kind
Dialogue: 0,0:19:36.76,0:19:41.80,Default,,0000,0000,0000,,of one step for what can happen but will\Nactually try multiple steps: all possible
Dialogue: 0,0:19:41.80,0:19:46.13,Default,,0000,0000,0000,,combinations of inputs for one\Ninstruction, two instructions, three
Dialogue: 0,0:19:46.13,0:19:49.81,Default,,0000,0000,0000,,instructions, longer and longer sequences\Nof instructions, looking for ways they can
Dialogue: 0,0:19:49.81,0:19:56.28,Default,,0000,0000,0000,,fail the property. So, and this turned out\Nto be an incredibly effective way of
Dialogue: 0,0:19:56.28,0:20:00.53,Default,,0000,0000,0000,,finding bugs in our processors.\NWe've actually, we're going to be using
Dialogue: 0,0:20:00.53,0:20:07.72,Default,,0000,0000,0000,,this on all future processor developments.\NSo, there's a paper that we wrote about
Dialogue: 0,0:20:07.72,0:20:12.30,Default,,0000,0000,0000,,this but, I recommend that you go\Nfind the video for the top by Clifford
Dialogue: 0,0:20:12.30,0:20:20.62,Default,,0000,0000,0000,,Wolf from a couple of hours ago, which\Ndescribes a very similar process. Okay, so
Dialogue: 0,0:20:20.62,0:20:25.78,Default,,0000,0000,0000,,I'm encouraging you to see the\Nspecification and find something awesome
Dialogue: 0,0:20:25.78,0:20:30.07,Default,,0000,0000,0000,,to do with it. There's a bunch of ideas I\Nhave suggested there, and there's a few
Dialogue: 0,0:20:30.07,0:20:36.85,Default,,0000,0000,0000,,extras which I didn't have time to\Ndescribe here. But now, let me turn to
Dialogue: 0,0:20:36.85,0:20:43.35,Default,,0000,0000,0000,,this title of the talk: How can you trust\Nformally verified software? So, what I'm
Dialogue: 0,0:20:43.35,0:20:50.20,Default,,0000,0000,0000,,talking about here is: verifying a program\Nagainst some specification. But, of
Dialogue: 0,0:20:50.20,0:20:54.51,Default,,0000,0000,0000,,course, programs don't just run in a\Nvacuum. They run into some operating
Dialogue: 0,0:20:54.51,0:21:01.56,Default,,0000,0000,0000,,system that, they use some libraries and\Nthey're also written in some programming
Dialogue: 0,0:21:01.56,0:21:08.21,Default,,0000,0000,0000,,language. And, so, when you verify your\Nprogram against your specification, you're
Dialogue: 0,0:21:08.21,0:21:15.31,Default,,0000,0000,0000,,also verifying them against the\Nspecifications of Linux, glibc and ISO-C,
Dialogue: 0,0:21:15.31,0:21:21.94,Default,,0000,0000,0000,,none of which have good specifications. In\Nfact, they're just terrible specifications
Dialogue: 0,0:21:21.94,0:21:27.55,Default,,0000,0000,0000,,which I bear little resemblance to what\Ncompilers and operating systems actually
Dialogue: 0,0:21:27.55,0:21:34.56,Default,,0000,0000,0000,,do in practice. So, if you... the current\Nstate of things is: if you do verify your
Dialogue: 0,0:21:34.56,0:21:39.58,Default,,0000,0000,0000,,program against these specifications, you\Nwill find lots of bugs. You will make your
Dialogue: 0,0:21:39.58,0:21:47.96,Default,,0000,0000,0000,,software a lot more reliable, but you'll\Nbe doing it against specifications, which
Dialogue: 0,0:21:47.96,0:21:51.64,Default,,0000,0000,0000,,are probably not very\Ngood. Just as ARM's specification was not
Dialogue: 0,0:21:51.64,0:21:57.85,Default,,0000,0000,0000,,very good before I tested it really\Nthoroughly. And so: Do I trust formally
Dialogue: 0,0:21:57.85,0:22:03.35,Default,,0000,0000,0000,,verified software? No, not really. It's a\Nlot better for being formally verified,
Dialogue: 0,0:22:03.35,0:22:06.59,Default,,0000,0000,0000,,but I'd also want to test it quite\Nthoroughly and maybe to use a bit of fuzz
Dialogue: 0,0:22:06.59,0:22:15.55,Default,,0000,0000,0000,,testing as well. Okay, so this is my final\Nslide, by the way. So, I'm encouraging you
Dialogue: 0,0:22:15.55,0:22:19.50,Default,,0000,0000,0000,,to go out and do something with the\Nspecification. If you're interested in
Dialogue: 0,0:22:19.50,0:22:25.78,Default,,0000,0000,0000,,this, then do contact me! Do ask me\Nquestions, if you have trouble. I'm also
Dialogue: 0,0:22:25.78,0:22:31.76,Default,,0000,0000,0000,,going to mention: if there's any white hat\Nhackers out there in the... white hat
Dialogue: 0,0:22:31.76,0:22:36.64,Default,,0000,0000,0000,,hackers in the audience, then do please\Ntalk to me or Milisch Meriac who's here in
Dialogue: 0,0:22:36.64,0:22:44.75,Default,,0000,0000,0000,,the front row, if you're interested in\Nworking at ARM and I like to thank a whole
Dialogue: 0,0:22:44.75,0:22:50.15,Default,,0000,0000,0000,,lot of people at ARM and elsewhere, who've\Nhelped me in this work and also I'd like
Dialogue: 0,0:22:50.15,0:22:54.15,Default,,0000,0000,0000,,to thank you for giving me your attention\Nfor the last half hour.
Dialogue: 0,0:22:54.15,0:22:59.79,Default,,0000,0000,0000,,{\i1}Applause{\i0}
Dialogue: 0,0:22:59.79,0:23:03.33,Default,,0000,0000,0000,,Herald: So, we have time for some
Dialogue: 0,0:23:03.33,0:23:06.34,Default,,0000,0000,0000,,questions. I would ask anyone that has a\Nquestion to line up at one of the
Dialogue: 0,0:23:06.34,0:23:10.56,Default,,0000,0000,0000,,microphones that are in the aisles here\None through eight. Questions for Alastair
Dialogue: 0,0:23:10.56,0:23:14.02,Default,,0000,0000,0000,,there about formal verification, about\Nworking at ARM, how is the weather in
Dialogue: 0,0:23:14.02,0:23:19.54,Default,,0000,0000,0000,,Cambridge. Try to keep it on topic. And\Nsignal angel: do we have already questions
Dialogue: 0,0:23:19.54,0:23:22.59,Default,,0000,0000,0000,,from online?\NSignal Angel: No questions yet.
Dialogue: 0,0:23:22.59,0:23:25.41,Default,,0000,0000,0000,,Herald: Okay, then let's go to microphone\Nnumber one.
Dialogue: 0,0:23:25.41,0:23:33.15,Default,,0000,0000,0000,,Microphone 1: Hi... I was just\NAR: Maybe tiptoes.
Dialogue: 0,0:23:33.15,0:23:38.01,Default,,0000,0000,0000,,MIC 1: Yes, I was just curious how are you\Nactually using the machine specification
Dialogue: 0,0:23:38.01,0:23:42.36,Default,,0000,0000,0000,,in order to generate VCs for the SMG\Nsolver. Because you didn't really get a
Dialogue: 0,0:23:42.36,0:23:47.76,Default,,0000,0000,0000,,chance to talk about that I guess.\NAR: Trying to think how I can describe
Dialogue: 0,0:23:47.76,0:23:56.64,Default,,0000,0000,0000,,that briefly... My basic idea is to take\Nthe specification, which basically... the
Dialogue: 0,0:23:56.64,0:24:00.63,Default,,0000,0000,0000,,specification is describing a piece of\Nhardware. And so, I try to do what a
Dialogue: 0,0:24:00.63,0:24:04.61,Default,,0000,0000,0000,,hardware engineer would do, if they were\Nactually building a machine that
Dialogue: 0,0:24:04.61,0:24:09.36,Default,,0000,0000,0000,,implemented it. So I end up with something\Nthat's essentially a giant circuit. So,
Dialogue: 0,0:24:09.36,0:24:14.29,Default,,0000,0000,0000,,that was the graph I was describing. So,\Nwhenever this control flow, whenever the
Dialogue: 0,0:24:14.29,0:24:18.96,Default,,0000,0000,0000,,control flow joins back up, I have to\Nintroduce things to slide between the
Dialogue: 0,0:24:18.96,0:24:22.26,Default,,0000,0000,0000,,value of what was calculated in the left\Nor the right. And so on.
Dialogue: 0,0:24:22.26,0:24:27.27,Default,,0000,0000,0000,,MIC 1: Yeah, I guess I'm mostly curious\Nabout, like, what logics you're using for,
Dialogue: 0,0:24:27.27,0:24:31.24,Default,,0000,0000,0000,,like, the solvers and stuff like that.\NAR: I see. Just very basic solvers because
Dialogue: 0,0:24:31.24,0:24:34.44,Default,,0000,0000,0000,,they run fastest.\NMIC 1: Then ugh
Dialogue: 0,0:24:34.44,0:24:40.54,Default,,0000,0000,0000,,H: Thank you. So, microphone 6 please.\NMIC 6: I was just wondering, if you could
Dialogue: 0,0:24:40.54,0:24:46.73,Default,,0000,0000,0000,,talk some little bit about the language\Nyou used to write your specification.
Dialogue: 0,0:24:46.73,0:24:54.31,Default,,0000,0000,0000,,AR: So this is a language which basically\NI inherited from ARM's documentation. So,
Dialogue: 0,0:24:54.31,0:24:58.44,Default,,0000,0000,0000,,all processors are described using\Npseudocode and what I realized was that
Dialogue: 0,0:24:58.44,0:25:02.79,Default,,0000,0000,0000,,the pseudocode the ARM had started writing\Nwas actually very close to being a
Dialogue: 0,0:25:02.79,0:25:06.88,Default,,0000,0000,0000,,language. And so, I sort of reverse\Nengineered the language hiding inside the
Dialogue: 0,0:25:06.88,0:25:14.20,Default,,0000,0000,0000,,pseudocode, built some tools for it, and\Njust kind of figured out what the language
Dialogue: 0,0:25:14.20,0:25:20.37,Default,,0000,0000,0000,,could possibly mean, given what I thought\Nprocessors actually did.
Dialogue: 0,0:25:20.37,0:25:27.85,Default,,0000,0000,0000,,And the language itself is... it's just a\Nvery simple imperative language. It's
Dialogue: 0,0:25:27.85,0:25:33.74,Default,,0000,0000,0000,,actually got inherits from BBC basic for\Nanyone who's about the same age as me and
Dialogue: 0,0:25:33.74,0:25:39.62,Default,,0000,0000,0000,,remembers BBC basic or it's a bit like\NPascal... It's it's not a complicated
Dialogue: 0,0:25:39.62,0:25:44.06,Default,,0000,0000,0000,,language. It's actually designed so that\Nas many people as possible can read it and
Dialogue: 0,0:25:44.06,0:25:47.54,Default,,0000,0000,0000,,know exactly what it says without any\Ndoubt, without having to consult a
Dialogue: 0,0:25:47.54,0:25:53.24,Default,,0000,0000,0000,,language lawyer.\NH: Signal angel? Yet anything?
Dialogue: 0,0:25:53.24,0:25:58.99,Default,,0000,0000,0000,,Signal Angel: Yes, now we've got a\Nquestion: "Has ARM its own form of the
Dialogue: 0,0:25:58.100,0:26:01.10,Default,,0000,0000,0000,,Intel Management engine?"
Dialogue: 0,0:26:08.95,0:26:12.22,Default,,0000,0000,0000,,AR: No is the short answer. Yeah, I don't
Dialogue: 0,0:26:12.22,0:26:20.16,Default,,0000,0000,0000,,think we have anything quite like that. If\Nyou... yeah, I'll just say no.
Dialogue: 0,0:26:20.16,0:26:22.93,Default,,0000,0000,0000,,{\i1}Laughter{\i0}\NH: Microphone one.
Dialogue: 0,0:26:22.93,0:26:27.97,Default,,0000,0000,0000,,MIC 1: Hi! On that question that we had\Nbefore about the specification language:
Dialogue: 0,0:26:27.97,0:26:33.78,Default,,0000,0000,0000,,Have you considered using Z3's own\Nlanguage for expressing the instructions?
Dialogue: 0,0:26:33.78,0:26:41.38,Default,,0000,0000,0000,,AR: So, Z3's own language is basically\Nwrite kind of s-expressions, which, if you
Dialogue: 0,0:26:41.38,0:26:46.69,Default,,0000,0000,0000,,like lisp is wonderful but for anybody who\Ndoesn't like Lisp it's a bit of a turn-off
Dialogue: 0,0:26:46.69,0:26:50.17,Default,,0000,0000,0000,,and a bit of a barrier to understanding\Nit. So, again the specification is
Dialogue: 0,0:26:50.17,0:26:54.41,Default,,0000,0000,0000,,designed so that people can look at it and\Ngo: "Oh, I see what's going on here", and
Dialogue: 0,0:26:54.41,0:26:57.26,Default,,0000,0000,0000,,not have... and I just try to minimize the\Nbarriers.
Dialogue: 0,0:26:57.26,0:27:03.23,Default,,0000,0000,0000,,MIC 1: Fair enough!\NH: Last call, signal angel!
Dialogue: 0,0:27:04.68,0:27:07.92,Default,,0000,0000,0000,,SA: How long does the complete test of the\Narms specification take?
Dialogue: 0,0:27:09.54,0:27:20.93,Default,,0000,0000,0000,,AR: About two years. So, yeah, so a modern\Nprocessor team about 80% of that team will
Dialogue: 0,0:27:20.93,0:27:26.68,Default,,0000,0000,0000,,be verification engineers. And, so,\Nthey're basically writing new tests,
Dialogue: 0,0:27:26.68,0:27:30.15,Default,,0000,0000,0000,,running old tests, diagnosing them, just\Ndoing that continuously for the entire
Dialogue: 0,0:27:30.15,0:27:34.96,Default,,0000,0000,0000,,life of a project, which is probably about\Nthree years. And after about the first
Dialogue: 0,0:27:34.96,0:27:38.86,Default,,0000,0000,0000,,year, you basically have a processor that it\Nmostly works, and after that it's kind of
Dialogue: 0,0:27:38.86,0:27:47.59,Default,,0000,0000,0000,,debugging it and it's, you know, kind of\Nfine-tuning the performance. So, yeah, it
Dialogue: 0,0:27:47.59,0:27:53.93,Default,,0000,0000,0000,,takes a really long time. To run the\Nactual tests, I don't actually know
Dialogue: 0,0:27:53.93,0:28:00.40,Default,,0000,0000,0000,,because actually one of my colleagues in\Nthe audience, they've actually run the
Dialogue: 0,0:28:00.40,0:28:07.96,Default,,0000,0000,0000,,tests. But, yeah, I don't know... and we\Nuse a lot of processors in parallel, so I
Dialogue: 0,0:28:07.96,0:28:12.62,Default,,0000,0000,0000,,really don't have an idea.\NH: Thank you so much, Alastair! Let's give
Dialogue: 0,0:28:12.62,0:28:18.48,Default,,0000,0000,0000,,him another warm round of applause!\N{\i1}Applause{\i0}
Dialogue: 0,0:28:18.48,0:28:24.02,Default,,0000,0000,0000,,{\i1}34c3 outro{\i0}
Dialogue: 0,0:28:24.02,0:28:40.00,Default,,0000,0000,0000,,subtitles created by c3subtitles.de\Nin the year 2018. Join, and help us!