Formally Verified Software in the Real World

From AcaWiki
Jump to: navigation, search

Citation: Gerwin Klein, June Andronick, Matthew Fernandez, Ihor Kuz, Toby Murray, Gernot Heiser (2018) Formally Verified Software in the Real World. Communications of the ACM (RSS)
DOI (original publisher): 10.1145/3230627
Semantic Scholar (metadata): 10.1145/3230627
Sci-Hub (fulltext): 10.1145/3230627
Internet Archive Scholar (search for fulltext): Formally Verified Software in the Real World
Wikidata (metadata): Q61038956
Download: https://cacm.acm.org/magazines/2018/10/231372-formally-verified-software-in-the-real-world/fulltext
Tagged:

Summary

Describes a "seismic security retrofit" of the systems of an autonomous helicopter, with verified componentization of untrusted Linux VMs running on a seL4 based hypervisor. The autonomous helicopter's safety was not affected by an attack in which the attackers were given root on one of the untrusted VMs controlling an on-board camera.


Retrieved from "https://acawiki.org/index.php?title=Formally_Verified_Software_in_the_Real_World&oldid=11444"