Formally Verified Software in the Real World (2018)

Formally Verified Software in the Real World (2018)(cacm.acm.org)

186 points by icc97 7 years ago | 17 comments

tpaschalis 7 years 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 [2] https://lamport.azurewebsites.net/tla/summary-standalone.pdf

drharby 7 years ago | |

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

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

nickpsecurity 7 years 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

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/

heyjudy 7 years ago | |

seL4 https://sel4.systems/

kccqzy 7 years 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 7 years ago | | |

Not to the rigor seL4 has, with multiple-levels of verification.

Nokinside 7 years 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-certif...

pron 7 years ago | |

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

gok 7 years ago | |

seL4

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

nestorD 7 years 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 7 years ago | |

Are you sure on that? It was B method they used afaik.

cpeterso 7 years 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/B-Method

nestorD 7 years 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%252Fs...