Return to Video

34C3 - How can you trust formally verified software?

  • 0:00 - 0:15
    34c3 intro
  • 0:15 - 0:16

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

more » « less
Video Language:
English
Duration:
28:40

English subtitles

Revisions Compare revisions