Forgot your password?
typodupeerror

Comment: Re:World's First Formally-Proven OS Kernel - NOT (Score 1) 517

by neongenesis (#29062099) Attached to: World's First Formally-Proven OS Kernel
Back At-cha

Virgil's paper talks about the HARDWARE verification (also important, but...) not the software verification.

The SCOMP OS was general purpose. It had a Unix emulation layer over its kernel similar to BSD over Mach. And the kernel WAS verified. The Unix System-call layer was modelled and verified against a security model. They have 10000 theorems, we had about 3500. They use Isabell, we used Boyer-Moore. Sounds like a fairly similar approach.

And you are right: It was a very cool piece of work for the time. I am not trying to denigrate the referenced paper. It sounds wonderful and I look forward to reading it. I just object to terms like "unique" and "first".

New crypt. See /usr/news/crypt.

Working...