5 ms·

Formally Verified Software in the Real World (2018)

186 points by icc97 8y ago

jschwartzi 8y ago
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.
deleted 8y ago
[deleted]
dahfizz 8y ago
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...
tpaschalis 8y ago
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! [1] https://lamport.azurewebsites.net/video/videos.html https://lamport.azurewebsites.net/video/videos.html [2] https://lamport.azurewebsites.net/tla/summary-standalone.pdf https://lamport.azurewebsites.net/tla/summary-standalone.pdf
- drharby 8y ago
  I really want this to be a sarcastic post demonstrating how thinly veiled some pr efforts are
nestorD 8y ago
The exemple I was given while studying the subject is that the sofware for the driverless metro line 14 in Paris has been proven in Coq.
- fuklief 8y ago
  Are you sure on that? It was B method they used afaik.
  - cpeterso 8y ago
    Wikipedia says B-Method. Parts of the train control system use OpenVMS! https://en.wikipedia.org/wiki/Paris_M%C3%A9tro_Line_14 https://en.wikipedia.org/wiki/Paris_M%C3%A9tro_Line_14 https://en.wikipedia.org/wiki/B-Method https://en.wikipedia.org/wiki/B-Method
  - nestorD 8y ago
    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. [0] https://perso.crans.org/cauderlier/org/art%253A10.1007%252Fs10270-013-0322-z.pdf https://perso.crans.org/cauderlier/org/art%253A10.1007%252Fs...

186 points by icc97 8y ago

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.

deleted 8y ago

[deleted]

dahfizz 8y ago

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...

tpaschalis 8y ago

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! [1] https://lamport.azurewebsites.net/video/videos.html https://lamport.azurewebsites.net/video/videos.html [2] https://lamport.azurewebsites.net/tla/summary-standalone.pdf https://lamport.azurewebsites.net/tla/summary-standalone.pdf

drharby 8y ago
I really want this to be a sarcastic post demonstrating how thinly veiled some pr efforts are

nestorD 8y ago

The exemple I was given while studying the subject is that the sofware for the driverless metro line 14 in Paris has been proven in Coq.

fuklief 8y ago
Are you sure on that? It was B method they used afaik.
- cpeterso 8y ago
  Wikipedia says B-Method. Parts of the train control system use OpenVMS! https://en.wikipedia.org/wiki/Paris_M%C3%A9tro_Line_14 https://en.wikipedia.org/wiki/Paris_M%C3%A9tro_Line_14 https://en.wikipedia.org/wiki/B-Method https://en.wikipedia.org/wiki/B-Method
- nestorD 8y ago
  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. [0] https://perso.crans.org/cauderlier/org/art%253A10.1007%252Fs10270-013-0322-z.pdf https://perso.crans.org/cauderlier/org/art%253A10.1007%252Fs...