{"guid":"44e7cb13-011e-4242-b26a-1edf4ac15b83","title":"How can you trust formally verified software?","subtitle":null,"slug":"34c3-8915-how_can_you_trust_formally_verified_software","link":"https://fahrplan.events.ccc.de/congress/2017/Fahrplan/events/8915.html","description":"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.","original_language":"eng","persons":["Alastair Reid"],"tags":["34c3","8915","Resilience"],"view_count":1777,"promoted":false,"date":"2017-12-27T00:00:00.000+01:00","release_date":"2017-12-28T01:00:00.000+01:00","updated_at":"2026-04-03T03:30:03.576+02:00","length":1719,"duration":1719,"thumb_url":"https://static.media.ccc.de/media/congress/2017/8915-hd.jpg","poster_url":"https://static.media.ccc.de/media/congress/2017/8915-hd_preview.jpg","timeline_url":"https://static.media.ccc.de/media/congress/2017/44e7cb13-011e-4242-b26a-1edf4ac15b83-timeline.jpg","thumbnails_url":"https://static.media.ccc.de/media/congress/2017/44e7cb13-011e-4242-b26a-1edf4ac15b83-thumbnails.vtt","frontend_link":"https://media.ccc.de/v/34c3-8915-how_can_you_trust_formally_verified_software","url":"https://api.media.ccc.de/public/events/44e7cb13-011e-4242-b26a-1edf4ac15b83","conference_title":"34C3: TUWAT","conference_url":"https://api.media.ccc.de/public/conferences/34c3","related":[{"event_id":4762,"event_guid":"b036385c-ec1a-44e5-ae48-af703ce9b5d3","weight":32},{"event_id":4763,"event_guid":"2ef3b60f-6e5c-4c23-a145-d263685ec13e","weight":65},{"event_id":4766,"event_guid":"19b7e5d7-bba7-46da-afbc-f16d43fe395f","weight":78},{"event_id":4768,"event_guid":"a13dc0d2-55af-4b60-a07c-1786094da593","weight":82},{"event_id":4770,"event_guid":"a890dbd3-8859-4788-a72f-ded5c5c08e5f","weight":51},{"event_id":4776,"event_guid":"825add58-9218-4afe-a489-4dd8c4408e45","weight":61},{"event_id":4784,"event_guid":"65a25dfd-56dd-4e87-a910-334e2dc25a9c","weight":86},{"event_id":4790,"event_guid":"edd02e52-28f8-4f3e-8b17-75cffecb6d7f","weight":57},{"event_id":4791,"event_guid":"8d29d28d-a222-4731-bdfc-fde590385cae","weight":48},{"event_id":4794,"event_guid":"a2887b4a-0c9d-4220-a52f-c65c20ae25d7","weight":52},{"event_id":4795,"event_guid":"722ce759-9cde-4e3b-8db5-5a97aa9673d9","weight":50},{"event_id":4804,"event_guid":"0cccbcdd-1e5c-4457-883b-6141c04d754c","weight":71},{"event_id":4826,"event_guid":"16645200-2036-4a3c-a44d-a5ff44ac2991","weight":79},{"event_id":4830,"event_guid":"5cf8c222-47d3-4741-9324-be182b4d0fb8","weight":67},{"event_id":4832,"event_guid":"275f85de-d612-4440-8755-85dee5912f12","weight":53},{"event_id":4833,"event_guid":"e1a60f7b-6a56-4dce-ab3a-c686fa940aa8","weight":60},{"event_id":4846,"event_guid":"832b8fb8-beb1-4d92-93d0-ba3b7568905a","weight":59},{"event_id":4861,"event_guid":"bdccda64-ee80-43fb-8e56-931199444188","weight":73},{"event_id":4866,"event_guid":"117a52b4-f675-49dd-aafe-659c07b6bc9c","weight":63}],"recordings":[{"size":null,"length":null,"mime_type":"application/x-subrip","language":"eng","filename":"34c3-8915-eng-deu-How_can_you_trust_formally_verified_software.en.srt","state":"complete","folder":"","high_quality":true,"width":null,"height":null,"updated_at":"2021-02-21T17:46:59.608+01:00","recording_url":"https://cdn.media.ccc.de/congress/2017/34c3-8915-eng-deu-How_can_you_trust_formally_verified_software.en.srt","url":"https://api.media.ccc.de/public/recordings/44466","event_url":"https://api.media.ccc.de/public/events/44e7cb13-011e-4242-b26a-1edf4ac15b83","conference_url":"https://api.media.ccc.de/public/conferences/34c3"},{"size":147,"length":1719,"mime_type":"video/mp4","language":"eng","filename":"34c3-8915-eng-How_can_you_trust_formally_verified_software.mp4","state":"new","folder":"h264-hd","high_quality":true,"width":1920,"height":1080,"updated_at":"2017-12-28T11:28:36.812+01:00","recording_url":"https://cdn.media.ccc.de/congress/2017/h264-hd/34c3-8915-eng-How_can_you_trust_formally_verified_software.mp4","url":"https://api.media.ccc.de/public/recordings/20765","event_url":"https://api.media.ccc.de/public/events/44e7cb13-011e-4242-b26a-1edf4ac15b83","conference_url":"https://api.media.ccc.de/public/conferences/34c3"},{"size":147,"length":1719,"mime_type":"video/mp4","language":"deu","filename":"34c3-8915-deu-How_can_you_trust_formally_verified_software.mp4","state":"new","folder":"h264-hd","high_quality":true,"width":1920,"height":1080,"updated_at":"2017-12-28T11:28:42.445+01:00","recording_url":"https://cdn.media.ccc.de/congress/2017/h264-hd/34c3-8915-deu-How_can_you_trust_formally_verified_software.mp4","url":"https://api.media.ccc.de/public/recordings/20766","event_url":"https://api.media.ccc.de/public/events/44e7cb13-011e-4242-b26a-1edf4ac15b83","conference_url":"https://api.media.ccc.de/public/conferences/34c3"},{"size":226,"length":1719,"mime_type":"video/mp4","language":"eng-deu","filename":"34c3-8915-eng-deu-How_can_you_trust_formally_verified_software_hd.mp4","state":"new","folder":"h264-hd","high_quality":true,"width":1920,"height":1080,"updated_at":"2017-12-28T11:28:50.209+01:00","recording_url":"https://cdn.media.ccc.de/congress/2017/h264-hd/34c3-8915-eng-deu-How_can_you_trust_formally_verified_software_hd.mp4","url":"https://api.media.ccc.de/public/recordings/20767","event_url":"https://api.media.ccc.de/public/events/44e7cb13-011e-4242-b26a-1edf4ac15b83","conference_url":"https://api.media.ccc.de/public/conferences/34c3"},{"size":167,"length":1719,"mime_type":"video/webm","language":"eng-deu","filename":"34c3-8915-eng-deu-How_can_you_trust_formally_verified_software_webm-sd.webm","state":"new","folder":"webm-sd","high_quality":false,"width":720,"height":576,"updated_at":"2017-12-28T12:26:32.297+01:00","recording_url":"https://cdn.media.ccc.de/congress/2017/webm-sd/34c3-8915-eng-deu-How_can_you_trust_formally_verified_software_webm-sd.webm","url":"https://api.media.ccc.de/public/recordings/20794","event_url":"https://api.media.ccc.de/public/events/44e7cb13-011e-4242-b26a-1edf4ac15b83","conference_url":"https://api.media.ccc.de/public/conferences/34c3"},{"size":87,"length":1719,"mime_type":"video/mp4","language":"eng-deu","filename":"34c3-8915-eng-deu-How_can_you_trust_formally_verified_software_sd.mp4","state":"new","folder":"h264-sd","high_quality":false,"width":720,"height":576,"updated_at":"2017-12-28T12:28:29.455+01:00","recording_url":"https://cdn.media.ccc.de/congress/2017/h264-sd/34c3-8915-eng-deu-How_can_you_trust_formally_verified_software_sd.mp4","url":"https://api.media.ccc.de/public/recordings/20798","event_url":"https://api.media.ccc.de/public/events/44e7cb13-011e-4242-b26a-1edf4ac15b83","conference_url":"https://api.media.ccc.de/public/conferences/34c3"},{"size":296,"length":1719,"mime_type":"video/webm","language":"eng-deu","filename":"34c3-8915-eng-deu-How_can_you_trust_formally_verified_software_webm-hd.webm","state":"new","folder":"webm-hd","high_quality":true,"width":1920,"height":1080,"updated_at":"2017-12-28T12:55:07.878+01:00","recording_url":"https://cdn.media.ccc.de/congress/2017/webm-hd/34c3-8915-eng-deu-How_can_you_trust_formally_verified_software_webm-hd.webm","url":"https://api.media.ccc.de/public/recordings/20840","event_url":"https://api.media.ccc.de/public/events/44e7cb13-011e-4242-b26a-1edf4ac15b83","conference_url":"https://api.media.ccc.de/public/conferences/34c3"},{"size":17,"length":1704,"mime_type":"audio/opus","language":"eng","filename":"34c3-8915-eng-How_can_you_trust_formally_verified_software.opus","state":"new","folder":"opus","high_quality":false,"width":0,"height":0,"updated_at":"2017-12-28T13:06:05.135+01:00","recording_url":"https://cdn.media.ccc.de/congress/2017/opus/34c3-8915-eng-How_can_you_trust_formally_verified_software.opus","url":"https://api.media.ccc.de/public/recordings/20859","event_url":"https://api.media.ccc.de/public/events/44e7cb13-011e-4242-b26a-1edf4ac15b83","conference_url":"https://api.media.ccc.de/public/conferences/34c3"},{"size":26,"length":1704,"mime_type":"audio/mpeg","language":"eng","filename":"34c3-8915-eng-How_can_you_trust_formally_verified_software.mp3","state":"new","folder":"mp3","high_quality":false,"width":0,"height":0,"updated_at":"2017-12-28T13:06:35.600+01:00","recording_url":"https://cdn.media.ccc.de/congress/2017/mp3/34c3-8915-eng-How_can_you_trust_formally_verified_software.mp3","url":"https://api.media.ccc.de/public/recordings/20860","event_url":"https://api.media.ccc.de/public/events/44e7cb13-011e-4242-b26a-1edf4ac15b83","conference_url":"https://api.media.ccc.de/public/conferences/34c3"},{"size":107,"length":1719,"mime_type":"video/mp4","language":"eng-deu","filename":"34c3-8915-eng-deu-How_can_you_trust_formally_verified_software_hd-slides.mp4","state":"new","folder":"slides-h264-hd","high_quality":true,"width":1920,"height":1080,"updated_at":"2017-12-28T16:57:59.170+01:00","recording_url":"https://cdn.media.ccc.de/congress/2017/slides-h264-hd/34c3-8915-eng-deu-How_can_you_trust_formally_verified_software_hd-slides.mp4","url":"https://api.media.ccc.de/public/recordings/21030","event_url":"https://api.media.ccc.de/public/events/44e7cb13-011e-4242-b26a-1edf4ac15b83","conference_url":"https://api.media.ccc.de/public/conferences/34c3"},{"size":35,"length":1719,"mime_type":"video/mp4","language":"eng","filename":"34c3-8915-eng-How_can_you_trust_formally_verified_software_sd-slides.mp4","state":"new","folder":"slides-h264-sd","high_quality":false,"width":720,"height":576,"updated_at":"2018-01-02T15:19:18.117+01:00","recording_url":"https://cdn.media.ccc.de/congress/2017/slides-h264-sd/34c3-8915-eng-How_can_you_trust_formally_verified_software_sd-slides.mp4","url":"https://api.media.ccc.de/public/recordings/22255","event_url":"https://api.media.ccc.de/public/events/44e7cb13-011e-4242-b26a-1edf4ac15b83","conference_url":"https://api.media.ccc.de/public/conferences/34c3"},{"size":5,"length":null,"mime_type":"application/pdf","language":"eng","filename":"34c3-8915-how_can_you_trust_formally_verified_software.pdf","state":"new","folder":"slides-pdf","high_quality":true,"width":null,"height":null,"updated_at":"2018-01-08T18:51:29.929+01:00","recording_url":"https://cdn.media.ccc.de/congress/2017/slides-pdf/34c3-8915-how_can_you_trust_formally_verified_software.pdf","url":"https://api.media.ccc.de/public/recordings/22443","event_url":"https://api.media.ccc.de/public/events/44e7cb13-011e-4242-b26a-1edf4ac15b83","conference_url":"https://api.media.ccc.de/public/conferences/34c3"}]}