4 ms·

Kind of a dumb question: have any operating systems been formally verified? Unless you are running an embedded application, verifying your software seems kind o

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.

brians 8y ago
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.
gok 8y ago
seL4
kccqzy 8y ago
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.
- heyjudy 8y ago
  Not to the rigor seL4 has, with multiple-levels of verification.
  - kccqzy 8y ago
    Yes I agree, but still with significantly more rigor than your typical operating system (Linux, Windows, macOS).
nickpsecurity 8y ago
Depends on if you mean design or code. In old days, there was STOP, GEMSOS, and LOCK. I have a description of two of them: http://www.cse.psu.edu/~trj1/cse443-s12/docs/ch6.pdf http://www.cse.psu.edu/~trj1/cse443-s12/docs/ch6.pdf Later on, the separation kernels: https://arxiv.org/pdf/1701.01535 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/2016/02/pldi117-yang.pdf 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/ https://muen.sk/
heyjudy 8y ago
seL4 https://sel4.systems/ https://sel4.systems/
pron 8y ago
PharOS RTOS: https://members.loria.fr/SMerz/papers/abz2016-pharos.html https://members.loria.fr/SMerz/papers/abz2016-pharos.html
Nokinside 8y ago
The question is to what degree. * 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-certification-for-fox-datadiode/ https://www.fox-it.com/datadiode/certificates/cc-eal7-certif...

brians 8y ago

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.

gok 8y ago

seL4

kccqzy 8y ago

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.

heyjudy 8y ago
Not to the rigor seL4 has, with multiple-levels of verification.
- kccqzy 8y ago
  Yes I agree, but still with significantly more rigor than your typical operating system (Linux, Windows, macOS).

nickpsecurity 8y ago

Depends on if you mean design or code. In old days, there was STOP, GEMSOS, and LOCK. I have a description of two of them: http://www.cse.psu.edu/~trj1/cse443-s12/docs/ch6.pdf http://www.cse.psu.edu/~trj1/cse443-s12/docs/ch6.pdf Later on, the separation kernels: https://arxiv.org/pdf/1701.01535 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/2016/02/pldi117-yang.pdf 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/ https://muen.sk/

heyjudy 8y ago

seL4 https://sel4.systems/ https://sel4.systems/

pron 8y ago

PharOS RTOS: https://members.loria.fr/SMerz/papers/abz2016-pharos.html https://members.loria.fr/SMerz/papers/abz2016-pharos.html

Nokinside 8y ago

The question is to what degree. * 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-certification-for-fox-datadiode/ https://www.fox-it.com/datadiode/certificates/cc-eal7-certif...