4 ms·
No mention of verification like seL4 or CertiKOS?
by qznc 10y ago
No mention of verification like seL4 or CertiKOS?
- aerioux 10y ago^ i'm interested in this as well. Would it be faster to build a secure OS using similar tech from seL4/CertiKOS now than their 14 yrs?
- qznc 10y agoGernot Heiser, the leader behind seL4, thinks so: https://microkerneldude.wordpress.com/2016/06/16/verified-software-can-and-will-be-cheaper-than-buggy-stuff/ https://microkerneldude.wordpress.com/2016/06/16/verified-so... They built infrastructure to build verified OS stuff faster/cheaper. For example, they reimplemented ext2fs for Linux.
- minipci1321 10y agoI understand CertiKOS used Coq so the verification was at least half-automated? How L4 was certified -- what were the tools available at the time? Verification still remains huge work but sounds less heroic nowadays. Now that we have tools and methodologies for verification, the announce of yet another secure OS suddenly sounds much less impressive.
- sanxiyn 10y agoHere is seL4 proof: https://github.com/seL4/l4v https://github.com/seL4/l4v To quote, "Most proofs in this repository are conducted in the interactive proof assistant Isabelle/HOL".