I have wanted to see a real-world use of seL4 in a safety-critical system since I heard about it 2 years ago. This is really impressive, and I'm very happy to see this here.
Kind of a dumb question: have any operating systems been formally verified? Unless you are running an embedded application, verifying your software seems kind of pointless if you are still at the mercy of "unverified" system calls, memory manager, scheduler, etc etc.
Yes! But none you want to use on a workstation. Honeywell and Burroughs both produced A1 verified operating systems—presumably there are successors there or at General Dynamics. There are some Russian attempts as well. Nobody else had the engineers, the mathematicians, and the money to build a verified system.
The standards there assume a TCB of about 10 kloc; 5kloc for the OS, 5kloc for each application. Separation is by static allocation—of disk space and memory usage, but also static time-domain multiplexing of CPU cores and IO lanes, with caches flushed on every context switch. They’re ferociously expensive to acquire in the first place, and then you take a huge operational penalty for running multiple applications.
There are very few problems for which this is a helpful solution—maybe not none, but very few when you could just buy several distinct computers, run them airgapped, and go about your business.
Green Hills Software has the Integrity operating system rated to EAL6+, which stands for "Semiformally Verified Design and Tested" so almost there but not quite.
But honestly it's not something you would want to use in daily life.
* EAL5 (Semiformally Designed and Tested) Logical partitions in IBM System Z.
* EAL6 (Semiformally Verified Design and Tested) INTEGRITY-178B and SeL4 I think.
* EAL7 (EAL7: Formally Verified Design and Tested). No operating system has been verified to this level. Only small number of data diodes and other some specialized systems have this level of assurance. https://www.fox-it.com/datadiode/certificates/cc-eal7-certif...
Second day in a row where HN frontpage features formally verified software!
If you're like me, and would like to get started, or just see what this is all about, the TLA+ homepage and video course (narrated by Leslie Lamport himself), is a nice resource [1].
In about half an hour you will have a brief understanding of what "formal specification languages" are, write and 'prove' your first small program/spec. If you have another hour to spend, keep the cheatsheet [2] near you and follow through, you will write and 'prove' more complex specs, plus you'll start thinking about systems in a more abstract way. Finishing up the video course you'll be able to start reading complex specs others have written, or write a spec for any algorithm you think is fun!
I was told Coq but, after some checking, I can only find the B method indeed.
However I did find a paper mixing both ([0]) : using Coq to prove the more complex proofs generated by atelier B. So it might have been both.
18 comments
[ 3.0 ms ] story [ 42.5 ms ] threadThe standards there assume a TCB of about 10 kloc; 5kloc for the OS, 5kloc for each application. Separation is by static allocation—of disk space and memory usage, but also static time-domain multiplexing of CPU cores and IO lanes, with caches flushed on every context switch. They’re ferociously expensive to acquire in the first place, and then you take a huge operational penalty for running multiple applications.
There are very few problems for which this is a helpful solution—maybe not none, but very few when you could just buy several distinct computers, run them airgapped, and go about your business.
But honestly it's not something you would want to use in daily life.
http://www.cse.psu.edu/~trj1/cse443-s12/docs/ch6.pdf
Later on, the separation kernels:
https://arxiv.org/pdf/1701.01535
VerveOS was verified at least for safety down to assembly:
https://www.microsoft.com/en-us/research/wp-content/uploads/...
The Muen separation kernel and hypervisor is verified to be free of common problems:
https://muen.sk/
* EAL5 (Semiformally Designed and Tested) Logical partitions in IBM System Z.
* EAL6 (Semiformally Verified Design and Tested) INTEGRITY-178B and SeL4 I think.
* EAL7 (EAL7: Formally Verified Design and Tested). No operating system has been verified to this level. Only small number of data diodes and other some specialized systems have this level of assurance. https://www.fox-it.com/datadiode/certificates/cc-eal7-certif...
If you're like me, and would like to get started, or just see what this is all about, the TLA+ homepage and video course (narrated by Leslie Lamport himself), is a nice resource [1].
In about half an hour you will have a brief understanding of what "formal specification languages" are, write and 'prove' your first small program/spec. If you have another hour to spend, keep the cheatsheet [2] near you and follow through, you will write and 'prove' more complex specs, plus you'll start thinking about systems in a more abstract way. Finishing up the video course you'll be able to start reading complex specs others have written, or write a spec for any algorithm you think is fun!
[1] https://lamport.azurewebsites.net/video/videos.html [2] https://lamport.azurewebsites.net/tla/summary-standalone.pdf
https://en.wikipedia.org/wiki/Paris_M%C3%A9tro_Line_14
https://en.wikipedia.org/wiki/B-Method
[0] https://perso.crans.org/cauderlier/org/art%253A10.1007%252Fs...