We're sorry but this page doesn't work properly without JavaScript enabled. Please enable it to continue.
Feedback

How can you trust formally verified software?

Formal Metadata

Title
How can you trust formally verified software?
Title of Series
Number of Parts
167
Author
License
CC Attribution 4.0 International:
You are free to use, adapt and copy, distribute and transmit the work or content in adapted or unchanged form for any legal purpose as long as the work is attributed to the author in the manner specified by the author or licensor.
Identifiers
Publisher
Release Date
Language

Content Metadata

Subject Area
Genre
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.
Keywords