back

How can you trust formally verified software?

If you suspend your transcription on amara.org, please add a timestamp below to indicate how far you progressed! This will help others to resume your work!

Please do not press “publish” on amara.org to save your progress, use “save draft” instead. Only press “publish” when you're done with quality control.

Video duration
00:28:39
Language
English
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.

This is an overview of the 6 year project to create (and publicly release) formal specifications of the Arm processor architecture.
The meat of the talk consists of the things I have done to make the specification correct:
- testing the specification with the test programs that Arm uses as part of the sign-off criteria for processors
- formally validating processor pipelines against the specification (which has the side-effect of finding bugs in the spec)
- formally verifying properties of the specification
- getting lots of different users - they all find different bugs
There are a lot of things that you can do with a formal specification: binary analysis, proving compilers or OSes correct, driving a superoptimizer, etc. so I hope that this will inspire the audience to go off and do something amazing with Arm's specification.

Talk ID
8915
Event:
34c3
Day
1
Room
Saal Borg
Start
3 p.m.
Duration
00:30:00
Track
Resilience
Type of
lecture
Speaker
Alastair Reid
Talk Slug & media link
34c3-8915-how_can_you_trust_formally_verified_software

Talk & Speaker speed statistics

Very rough underestimation:
147.3 wpm
816.7 spm
152.3 wpm
842.3 spm
100.0% Checking done100.0%
0.0% Syncing done0.0%
0.0% Transcribing done0.0%
0.0% Nothing done yet0.0%
  

Work on this video on Amara!

Talk & Speaker speed statistics with word clouds

Whole talk:
147.3 wpm
816.7 spm
specificationcodeinstructionlanguageinstructionsthingsbitarmprocessorthingfindtalkbasicallytestgraphprogramexactlyvalueswork1yearstestingturnarinterestingarm'sregisterprocessorsinputsmictoptestsquestionsconstrainthappenbuildbranchesbinarysuitetimeworkingsoftwaresolverunderstandtalkingsolversexecutesignalformallycontrol
Alastair Reid:
152.3 wpm
842.3 spm
specificationcodeinstructionthingsinstructionsfindthingarmprocessorbitprogramworktalkvaluesgraphtestexactlyturninterestingregisterinputstestingtopbuildconstrainthappenarm'sbranchestalkingunderstandagoformallysoftwarestackexecutefactbinarybasicallynodesgoodsuitespecificationsprocessorsyearsworkingverifiedcoursesecuritysystemsuppose