Bestand wählen
Merken

How can you trust formally verified software?

Zitierlink des Filmsegments
Embed Code

Automatisierte Medienanalyse

Beta
Erkannte Entitäten
Sprachtranskript
tree and the and
the without a lot of the youth and publishing in academia for almost 30 years please join me in giving him a warm welcome to 34 these 3 the FIL have uh lecture was the introduction of something talking
maybe on processes and they're incredibly widely used you find them in their phones tablets IT devices hard disk drives the all over and if you think basic 1 thing is the in of all the things which continue 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 we can analyze and for any now where they look for vulnerabilities and so on I the the so remember talking but some workers started by about 6 years ago tracing of a precise specification of all of a point on processor dollars 1 day I'm talking also about I back in April on released this a the specification in a machine readable form a the and I should say that by working with kimage university to turn on something you can use so I so this talk
on women mostly actually talk about this executable process uh specification that's going be the both the talk but the and that's that's not very nicely to talk about a formally verified software but don't given the theme of the congress it I would be more useful to emphasize things you could actually do so this specification
arm released was it will there's lots of instruction descriptions of course but but is also lots of really interesting and security features Institute memory protection as exceptions privilege checks and so on so there's lots of really interesting stuff your interest in their house secure your devices and heights nature really is secure a flight to talk a bit giving a bunch of links you can go and download the yeah right now you from met the 1st link but please greater than the top and and there's also a the specification vendor there's a HTML was tools that can take the specification the Lisa apart and find useful information at a recent blogs and papers of ice as well the and so let's just dive in to look at the bits of actual specification so the 1st thing is
I all the really important security features in the space in our process there are controlled by or call the system control registers and the top dog among all those control registers is this 1 here called ACT are just trips off the tongue does not so SET a lot is we're this FIL of lots of individual control bits which affects either optimization of processes doing or a also security features a so it's just 2 men 1 of them
as give an idea of what kind of information the state contains so and this and documentation tell you about a wx and that was that do it makes sure that at any code any uh that use that cannot contain called the Contras instructions in the code and understand stack because a force if you set this bit processor want to exclude them I In other words this is a bit bit that triggered the yeah requirement for things like return oriented programming OK so I hope you do with this Arafat's play well suppose you in the habit of reverse engineering some code you might
you December might show you something like that and you probably all staring at this going on after that date because it's extremely cryptic but using the information that's in the uh the XML version the release you can easily figure out how to build or a high high to decode some of the more cryptic parts I go all actually it's a city already so right so you could decode the trip to name for the record number for the register into that uh they could do a bit more than that you can see it's aspects in 1 of the bits in the register so a is of course but I just told about the lyrics and so we can dig into that and uh so so we could and use the information from XML to render perhaps as I like this so you can make things a bit more useful uh and you can also take that documentation that is the told you what the w and that does and
maybe if you're a feeling really yeah energetic you could you click on that most over wherever they could bring up some of that documentation and and that makes best uh that it's much easier to understand what the tryptic discordant top is doing this was just a very shallow thing you can get the specification
there is also a if we dig into the instruction descriptions is also things like the assembly language both the specification of a the assembly syntax and uh so something that a few years ago and which had a stroke blog
article about over the weekend was was it is possible to actually the that specification turn it into a by a disassembler so 1st of all they transformed into the uh the codon showing at the bottom on what this is showing is highest take a binary description of an instruction so that's the the top line of typewriter font and a and then turn that into strings which is what this the code at the bottom is describing how to do so as the use as a disassembler is actually possible to run in reverse uh and users in the same way you basically when the code from bottom to top I and you can turn strings into binary instructions almost the more this running things in reverse in a few slides time we so
I the the main thing of instructions this course do something so that they the specification things are a description of exactly what instruction does and that description is as cold which the programmer meeting very happy right I do understand English words in the specification by do you understand what the code does so the 1 thing you can do this code is
executed so let's just walk through but suppose that the construction and then matched against a that diagram there I might get some values for a for some the variables not on and I can walk through and that was set by evaluating this code until eventually realize that register 5 is having some value assigned to it OK so that's a fairly basic thing you can do specification untapped is a fairly easy thing to implement but once you have it is a lot you can build on top of it uh on 1 thing that's surprisingly easy to implement is to extract a symbolic representation of what instruction does so just show you quickly you do that using the character that so they see the
same concrete values from all so I've added of any variable so this idea which which the symbolic variables and as I walked through the code would just calculate some concrete values for the value 5 after to also and build up a graph representing exactly how I came up with these values at 5 and so on so as a makes the cold I can build a graph
representing exactly what this code is doing and what you do now is just
through with a cold and focus on what that draft is telling me so I wanna have a symbolic representation of 1 slice through that through that instruction and I can feed that a constraint solver so if any of you've heard of these 3 your SMT solvers but from talking about here the the and a constraint solver is a really useful tool because you can run code forwards through its so given some input values you can see the plots of the outputs and from uh from this function from this instruction we can also run them backwards at a given some given some output value some final result you want to see you can ask what inputs to cause this to happen and this is just tremendously useful if you're trying to figure out what instructions you want it to you to to generate some particular effects right so if you're trying to fit right post some particular a register could be accessed how some x siculus think be turned on or off and be able to ask what inputs will cause this happens is incredibly useful of and you can also use a constraint solver to the to ask for intermediate values in the middle of the calculation you if you know some value you would see there you can ask what the inputs and that would cause that to happen so that if any of you familiar with a tools like clique which the symbolic execution too far LVM then the use something similar to this so a showing you feel simple graphs on outage show you how you build that active on the fly this this
actual draft for that same instructions I view of I did a lot more nodes had to do with their some the functions of a being called and to do with their the calculating whether think a branch and not so this debate say if you're 19 nodes are and have been experimenting with
a extending this in 2 ways so this is just 1 path through a the execution of an instruction so 1 way to improve and that is to build a graph that represents all possible paths through the instructions and that's much more useful because you can you then can point something in the how can I make that happen and it will be a tell you exactly a what inputs will cause a path that we now happened of also been experimenting with taking the entire specification right so that's Self the handles exceptions it fetches instructions executes instructions it contains all instructions on a 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 red specification you can ask a constraint solver I will come back and say give me an answer and this draft for the full specification is quite large it's about half a million nodes and that's the smallest a specification that there are many users that about half a million nodes but the great thing is modern constraint solvers can can read and that half million nodes as still give you answers to play in about 1 to 10 seconds for most the questions of the course to them so you just tremendously useful tools if you're wanting to be able to understand exactly they what this says I put the specification does an exactly how some program is going to behave or figure out what program you want to write to make it gave some particularly a case of talks a lot about
a right instructions but most of us actually run programs right so to turn this and assess cation something can execute programs in other words stern enter a simulator for the OMB architecture you need to add a little bit over there it looked at will handle in drops FH instructions and and then it can execute them and handling exceptions so that so that this I added said this loop to this specification and then I thought basis try testing specifications and it has uh and so the good news for me because I worked for arm i have access arms internal a test suite
which is something are working on basically since the company started 25 30 years ago this guy large test suite is extremely thorough as tens of thousands of fair test programs that one's billions of instructions of and so about testing the yeah testing 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 it's start things that work all that well I gradually you get things that working pretty well but then there's a heavy tail of difficult to find bugs OK so the basically what I found for those testing specification but you should all be short by why just said because 1 thing is arms officials specification could not pass on his official a test suites when I started quite another that's pretty shocking of I'm telling you this in emphasizing it's not because the thing on specification was an especially bad I think it was just typically bad I think if you were to take any specification a foreign you know any real world systems and actually taste against the test suite will 1st of all you find nonexecutable specification was designed a 2nd later you'd find it wouldn't work and you probably find it would work as badly is on that so it is not just that it didn't pass all the taste it in passing the tests effect it took me weeks to get the process of for the specifications come to reset by just to get the starting fixed the 1st instruction 2 weeks so and I think so that I think you'd find the and if you were to try any other specifications but the next so OK
so moving on to a useful things that you can do with specification as something we tried last summer was a using it for 1st testing so 1st testing consists of taking a program of storing random inputs and at the program and just seeing what breaks and it pretty much always breaks and uh of modern was test the light maybe AFL and to make it more effective monitors something about how the program is excusing and using that to guide it's a choice of what to change next so if it's finding something put should as where the instruction are for the program taking an avalanche in art and if it sees taking lots of new branches the goes OK keep trying more fun doing at the moment it seems to be effective and effects and not finding any new branches and will look for something else to try changing so uh that's kind of the normal fussing what you doing is basically trying to a can of maximize you're a branch coverage of so what we did don't when we had that that that this with specification was we actually modern branches is not just in the in the binary that we're analyzing but also in the in the specification on what they see as a diverse uh was basically forgot suppose you're headed by no you analyzing is just straight line code is no branches in at all then there's nothing really for your force after work with right so it doesn't see that the code is interesting it quickly moves on to something else what may be a straight line code is doing something really interesting like accessing a privilege register will there will be a branch around that to check that you do have the privilege to require or maybe it's accessing and memory in which cases memory protection checks is also checks for is this on a device registers as a I can around or on so there's a number of different branches the and that gives the fossa or interesting things to interesting feedback and play with so when we say this going on uh 1 of our eyes also microkernel by we will analyze the the had a system call interface for that might kernel and 1 of things further surprises with was it says suppose I take the stack pointer and pointing into the middle of this device space and then taken exception immediately what happens answer was there was a bug in the microkernel on what it did was it the 1st thing we do is read from the site where the stack pointer was pointing so we do read from my a from 1 of the devices which doesn't it wasn't really what was intended in fact the completely breaks the security model so 1st tasting using not just coverage of the loop monitoring branches in the binary but also the specification can find you a bunch of really interesting things as a hope some of you will die take this side you often don't run with that so so the reason I was doing all
this work was I wanted to be able to formally verify on processes and of and so I needed stress specification before to do that so cial images to drinking about the the so this is overly simplified and picture of a process it's more or less for processes which like 25 30 years ago in fact of but is good enough for the example so i if you want to check processor is correct then we can do
is add an extra logic which will monitor the yeah the values of stocks of instruction expressing the values of finally produced at the end of 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 a point the process are actually dead the so you can do this using a text based approach I just feed inputs and their check that said everything matches but you can also do it using our formal verification tool called are by model checker of when the model checkers like 1 of those constraints it as solvers I mentioned earlier on crack cocaine so was it will do is it would just try and can of 1 instead of what can happen will actually try multiple steps all possible combinations of inputs for 1 instruction to instructions to instructions longer and longer sequences of instructions looking for ways they can feel the property so i'm and this turned out to be incredibly effective way of finding Ned books not processes were actually were going to be using this on all future processor developments of so there's a paper banner that we wrote about this but say I recommend you AG defined a video for the topic Clifford will fire from a couple of hours ago which share the sides of a similar process of
OK so I'm encouraging you to take a specification find find something awesome to do with it is a bunch of ideas of suggested their eyes and is a few extras which I didn't have time to describe here the let me turn
to the title of the talk page you trust formally verified softer so 1 talking about here is verifying a program against some specification of course programs so just 1 in a vacuum luminance up the some operating system that said they use some men libraries and a and also written some programming language and so on when you verify your program against a your specification you also verifying them against the specifications of Linux juleps C and ISO see none of which have good specifications in fact yeah they're they're just terrible specifications which may bear little resemblance what's compilers and operating systems actually do in practice so far so if you the current state of things is if you do verify your program against the specifications you will find lots about you will make yourself there are a lot more reliable but are you be doing against specifications which further a which are probably not very good just as on the specification is not very good before it tasted that I really thoroughly and so I don't trust formally verified sulfur no not really is a lot better for being formally verified but I'd also want to takes the quite thoroughly individually that fuzz testing as well
OK so by this so is my final slide by the way I'm and so on encouraging you to go out and do something with specification if you're interested in this then add to arrive do contact me just the questions that have trouble on the most of any mention if there's any quite hat hackers idea in the might have actors in the audience then do please talk to me or relation mayor actors here in the front row and if your working at a time and the like to thank all the people of almonds that elsewhere who help me in this work and and also like to thank you forgive me your attention for last half hour the thank you so we have time for some questions I would ask anyone that has a question to line up at 1 of the microphones that are in the files you want to read the question trouser about formal verification about working in how is the weather in Cambridge and try to keep it on topic and signal angel that we have already questions from online male residents of OK then that's got a microphone number 1 the I o just do the notice of those yes I was just curious how you're actually using machine specification layer in order to generate the various solvent because you can't believe get they're just above a of of traffic correction describe them briefly the way they think idea is to say the specification which basically specification is writing a piece of hardware and so I trying to do what hardware and you would do if they were actually building implemented at some end up with something it's essentially a giant circuit so that the graph of describing and so whenever this control flow whenever the control joins and back up I have to choose slight between the value of count with the left to the right of animals as on but I'm I'm some curious about what logic to using for like the solvers and stuff like that of course just very basic always 61 fastest and I know that you so of microphones explains um monocistronic could of talk some a little bit about the language we used to write a specification I we so this is a language which basically inherited from an arms documentation so all processes are described using pseudo code and I realized was the pseudo code on started writing was actually very close to being a language and source of reverse engineer the language hiding inside the code both tools for and you just you can forget what language they could possibly mean different thought processes actually dead and the language itself is is is just a very simple imperative language it's on it's actually got inherits from BBC basic for for anyone is about the same age you mean as mean remembers BBC basic of or it's a bit like Pascal it's is not a complicated languages actually designed so that as many people as possible can read it and know exactly what it sees without any doubt without having to consult the language law they to going to get anything yes no we've got a question of has on its own form of being told management giant in I the only I the known as the source and some of you don't think we have anything and I quite like that of if you the pulsar signal the microphone 1 in am I um on that question that we had before about the specification language having considered using these theories on language for expressing the instructions also so the these uh on languages that basically right so can have its expressions which if you like list is wonderful book for anybody who doesn't like list it's a bit of turned off under the barrier to understanding it so again this specications signs so that people can look at that and go on I see what's going on here and not have a right minimizer barriers the so enough the last call signaling tools how long does the complete test of beyond specification take but 2 years that of so yes so our approach of modern process team about 80 % that team will be verification engineers and so they're basically right the new tests 1 angle test diagnosing them just doing that continuously for the entire life of a project uh which probably 3 years and after with the 1st year you basically have a process that mostly works and after that it's can debugging it's and it's uh and it's a you know can a fine-tuning the performance but so yeah it takes a really long time to run actual tests I don't know I should know because that's the 1 might and colleagues in the audience that I we leave actually run the test some but yeah I don't know and we use a lot of processes say in parallel so I really don't have no idea because it was always there was given another warm round of applause now want to do is
of the the the the a thank you is that the the PEP talk
Netzwerktopologie
Software
Umwandlungsenthalpie
Architektur <Informatik>
Punkt
Prozess <Physik>
Virtuelle Maschine
Programmverifikation
Malware
Tablet PC
Analysis
Coprozessor
Benutzerprofil
Virtuelle Maschine
Festplattenlaufwerk
Software
Bildschirmmaske
Softwareschwachstelle
Tablet PC
Computersicherheit
Biprodukt
Festplattenlaufwerk
Coprozessor
Grundraum
Logik höherer Stufe
Sichtbarkeitsverfahren
Bit
Prozess <Physik>
Kontrollstruktur
Web log
Ausnahmebehandlung
Natürliche Zahl
Minimierung
Virtuelle Maschine
Programmverifikation
Speicherschutz
Parser
ROM <Informatik>
Raum-Zeit
Physikalisches System
Deskriptive Statistik
Charakteristisches Polynom
Computersicherheit
CAD
Inklusion <Mathematik>
Umwandlungsenthalpie
Architektur <Informatik>
Speicherschutz
Computersicherheit
Ausnahmebehandlung
Physikalisches System
CAM
Binder <Informatik>
Web log
Menge
Rechter Winkel
Verschlingung
Gamecontroller
Information
Körpertheorie
Zeitzone
Zentraleinheit
Bit
Kontrollstruktur
Division
Programm
Versionsverwaltung
Keller <Informatik>
ROM <Informatik>
Code
Physikalisches System
Software
Datensatz
Charakteristisches Polynom
Forcing
Reverse Engineering
Mereologie
Translation <Mathematik>
Wort <Informatik>
Coprozessor
Information
Körpertheorie
TLB <Informatik>
Aggregatzustand
Umwandlungsenthalpie
Open Source
Deskriptive Statistik
Software
Kontrollstruktur
Web log
Assembler
Translation <Mathematik>
Zeiger <Informatik>
Assembler
ROM <Informatik>
Umwandlungsenthalpie
Verschiebungsoperator
Programm
Aliasing
Assembler
Binärcode
Code
Disassembler
Rechenschieber
Deskriptive Statistik
Ganze Zahl
Verbandstheorie
Font
Rechter Winkel
Reverse Engineering
Minimum
Wort <Informatik>
Disassembler
Sehne <Geometrie>
Gerade
Zeichenkette
Umwandlungsenthalpie
Verschiebungsoperator
Konstruktor <Informatik>
Diagramm
Variable
Ganze Zahl
Graph
Selbstrepräsentation
Information
Code
Resultante
Soundverarbeitung
Verschiebungsoperator
Lineares Funktional
Nebenbedingung
Zwischenwertsatz
Program Slicing
Selbstrepräsentation
Nebenbedingung
Plot <Graphische Darstellung>
Ein-Ausgabe
Rechnen
Code
Endlicher Graph
Ganze Zahl
Funktion <Mathematik>
Ein-Ausgabe
Selbstrepräsentation
Evolutionsstrategie
Clique <Graphentheorie>
Funktion <Mathematik>
Umwandlungsenthalpie
Lineares Funktional
Nebenbedingung
Graph
Zwei
Verzweigendes Programm
Programm
Ausnahmebehandlung
Ein-Ausgabe
Knotenmenge
Graph
Knotenmenge
Rechter Winkel
Ganze Funktion
Ganze Funktion
Programm
Softwaretest
Umwandlungsenthalpie
Suite <Programmpaket>
Bit
Architektur <Informatik>
Zehn
Programm
Ausnahmebehandlung
Coprozessor
Loop
Festplattenlaufwerk
Softwaretest
Interrupt <Informatik>
Suite <Programmpaket>
Software
Diskrete Simulation
Basisvektor
Wort <Informatik>
Computerarchitektur
Tropfen
Rückkopplung
Web Site
Subtraktion
Kontrollstruktur
Momentenproblem
Extrempunkt
Programm
Parser
Zahlenbereich
Binärcode
Code
Raum-Zeit
Kernel <Informatik>
Loop
Mikrokernel
Informationsmodellierung
Softwaretest
Reelle Zahl
Kontrollstruktur
Zeiger <Informatik>
Gerade
Auswahlaxiom
Schnittstelle
Binärdaten
Soundverarbeitung
Umwandlungsenthalpie
Softwaretest
Binärcode
Suite <Programmpaket>
Graph
Speicherschutz
Fuzzy-Logik
Computersicherheit
Verzweigendes Programm
Systemaufruf
Ausnahmebehandlung
Programmfehler
Auswahlaxiom
Forcing
Rechter Winkel
Festspeicher
Ein-Ausgabe
Evolutionsstrategie
Umwandlungsenthalpie
Nebenbedingung
Folge <Mathematik>
Prozess <Physik>
Punkt
Matching <Graphentheorie>
Kategorie <Mathematik>
Schaltnetz
Programmverifikation
Programmverifikation
Ein-Ausgabe
Mathematische Logik
Videokonferenz
Model Checking
Maximum-Entropie-Methode
Coprozessor
Softwareentwickler
Normalspannung
Zentraleinheit
Bildgebendes Verfahren
Compiler
Leistungsbewertung
Programmverifikation
Programm
Assembler
Information
Analysis
Physikalisches System
Softwaretest
Programmbibliothek
Programm
Softwaretest
Umwandlungsenthalpie
Programmiersprache
Güte der Anpassung
Betriebssystem
Strömungsrichtung
Physikalisches System
Interpretierer
Wiki
Umsetzung <Informatik>
Coprozessor
Software
Fuzzy-Logik
Rückkopplung
Hochvakuum
Disassembler
Logik höherer Stufe
Aggregatzustand
Bit
Prozess <Physik>
Digital Rights Management
Formale Sprache
Zahlenbereich
Unrundheit
Zählen
Gesetz <Physik>
Mathematische Logik
Physikalische Theorie
Code
Hypermedia
Medianwert
Systemprogrammierung
Virtuelle Maschine
Bildschirmmaske
Arithmetischer Ausdruck
Computerspiel
Reverse Engineering
Vorzeichen <Mathematik>
Vererbungshierarchie
Kontrollstruktur
Hacker
Hacker
Algorithmische Programmierung
Feuchteleitung
Umwandlungsenthalpie
Softwaretest
Extremwert
Hardware
Vervollständigung <Mathematik>
Graph
Winkel
Relativitätstheorie
Pauli-Prinzip
Programmverifikation
Systemaufruf
Mailing-Liste
Quellcode
Elektronische Publikation
Gesetz <Physik>
Rechenschieber
Rechter Winkel
Gamecontroller
Projektive Ebene
Ordnung <Mathematik>

Metadaten

Formale Metadaten

Titel How can you trust formally verified software?
Serientitel 34th Chaos Communication Congress
Autor Reid, Alastair
Lizenz CC-Namensnennung 4.0 International:
Sie dürfen das Werk bzw. den Inhalt zu jedem legalen Zweck nutzen, verändern und in unveränderter oder veränderter Form vervielfältigen, verbreiten und öffentlich zugänglich machen, sofern Sie den Namen des Autors/Rechteinhabers in der von ihm festgelegten Weise nennen.
DOI 10.5446/34805
Herausgeber Chaos Computer Club e.V.
Erscheinungsjahr 2017
Sprache Englisch

Inhaltliche Metadaten

Fachgebiet Informatik
Abstract Formal verification of software has finally started to become viable: we have examples of formally verified microkernels, realistic compilers, hypervisors etc. These are huge achievements and we can expect to see even more impressive results in the future but the correctness proofs depend on a number of assumptions about the Trusted Computing Base that the software depends on. Two key questions to ask are: Are the specifications of the Trusted Computing Base correct? And do the implementations match the specifications? I will explore the philosophical challenges and practical steps you can take in answering that question for one of the major dependencies: the hardware your software runs on. I will describe the combination of formal verification and testing that ARM uses to verify the processor specification and I will talk about our current challenge: getting the specification down to zero bugs while the architecture continues to evolve.
Schlagwörter Resilience

Zugehöriges Material

Ähnliche Filme

Loading...
Feedback