This description was written by a machine and published without a person checking it. It is what the agent made of this grouping, and not a statement anybody has stood behind.
Gernot Heiser
A grouping.
The seL4 project from the systems side: the verified kernel, the argument that verified software in the real world can be done, and the account of its deployment. Two further records make an objection a proof cannot -- that a kernel verified correct is still not isolating, because correctness is stated over the machine the specification describes and timing is a channel the specification does not mention. The corpus holds the verification and this objection to what it buys, from the same person.
5 references
seL4 in Australia: From Research to Real-World Trustworthy Systems
Gernot Heiser and others (2020) · Communications of the ACM · Association for Computing Machinery
Time Protection: The Missing OS Abstraction
Qian Ge and others (2019) · Proceedings of the Fourteenth EuroSys Conference · Association for Computing Machinery
A survey of microarchitectural timing attacks and countermeasures on contemporary hardware
Qian Ge and others (2018) · Journal of Cryptographic Engineering · Springer
Formally verified software in the real world
Gerwin Klein and others (2018) · Communications of the ACM · Association for Computing Machinery
seL4: Formal Verification of an OS Kernel
Gerwin Klein and others (2009) · Proceedings of the ACM SIGOPS 22nd symposium on Operating systems principles · Association for Computing Machinery