| ▲ | bassp 3 days ago | |
> Some problems are straightforward to specify. A file system is a good example. I’ve got to disagree with this - if only specifying a file system were easy! From the horse’s mouth, the authors of the first “properly” verified FS (that I’m aware of), FSCQ, note that: > we wrote specifications for a subset of the POSIX system calls using CHL, implemented those calls inside of Coq, and proved that the implementation of each call meets its specification. We devoted substantial effort to building reusable proof automation for CHL. However, writing specifications and proofs still took a significant amount of time, compared to the time spent writing the implementation (Reference: https://dspace.mit.edu/bitstream/handle/1721.1/122622/cacm%2...) And that’s for a file system that only implements a subset of posix system calls! | ||
| ▲ | Animats 2 days ago | parent [-] | |
Ah, they're trying to specify file system recovery, which exposes the internals. I did that once, as part of a very old secure operating system project, KSOS.[1] The specs were in SPECIAL, a forgotten language from SRI International.[2] The file system had two key invariants. The weak invariant was true at the end of every write. The strong invariant was true when the file system was clean and unmounted. The job of file recovery was to take a file system for which the weak invariant was true and make the strong invariant true. We had a spec, but nobody could prove anything about it at the time. The tools didn't exist in the early 1980s. And trying to cram KSOS into a PDP-11 didn't really fit. It ran, but was too slow. All of this was just too early. Today you can do it. [1] https://seclab.cs.ucdavis.edu/projects/history/papers/ford78... [2] https://www.sciencedirect.com/science/article/abs/pii/016412... | ||