Re:Writing correct lock-free and distributed stateful system...
by nickpsecurity on Sunday May 21, 2017 @04:27PM
(#14389094)
"There is something interesting you could try, though: You could express global correctness properties in TLA+, and show (in TLA+) that they are preserved if some simple low-level properties are preserved, and then express and verify those in JML/SPARK. This is very interesting, and I'd love to hear about such an experience (or even try it myself), but my gut feeling is that that it would still be too costly. If someone does do that, however, that's something certainly publication-worthy."
That might have been how E-SPARK connected Event-B and SPARK. TLA+ is easier to use than Evdnt-B and often in similar domains. Ill try to remember this option.
Not really. Frama-C aside, JML and SPARK simply cannot express those global correctness properties you naturally express in TLA+. Frama-C is really a set of ad-hoc tools.
> So, solution for this proposal is to try to encode correctness conditions from TLA+ or another analysis in SPARK.
But SPARK simply isn't rich enough to do that in general. You're right that if the TLA+ specification is at an abstraction level that's very close to the code, you can try to express some of those properties in SPARK, but I doubt even that is possible. Concurrent algorithms require liveness properties, and I'd be very surprised if SPARK could express them.
There is something interesting you could try, though: You could express global correctness properties in TLA+, and show (in TLA+) that they are preserved if some simple low-level properties are preserved, and then express and verify those in JML/SPARK. This is very interesting, and I'd love to hear about such an experience (or even try it myself), but my gut feeling is that that it would still be too costly. If someone does do that, however, that's something certainly publication-worthy.
> One can see that in ACL2, Isabelle/HOL and Coq ecosystems for projects that actually use what's already there. Or even in CompCert work where new CompSci just keeps adding new components to it to save time/effort.
But I still don't know of a single nontrivial real-world project that has been affordably verified, even with all that reuse.
> The other thing is that seL4 targeted C language. That language wasn't designed for verification...
Again, everything you say is true, but still there are no examples of affordably end-to-end-verified real-world projects.
> I imagine they'd need at least one specialist for that kind of verification.
Not if TLA+ is used. Amazon (and I, too) specify and verify such properties all the time and they (and I) are not verification experts.
> Also, recall the COGENT work where the key components of an ext2 filesystem was done with half the code in C without painful analysis of mutable state that seL4 had to do. Easier proofs with C code coming out that preserves those properties.
I know the person behind Cogent (he'd also worked on seL4), but he points out that the language targets a very narrow domain. Most programs you can think of cannot be written in Cogent.
> Really ad hoc, though.
That pretty much sums up all of formal methods at this stage, especially end-to-end ones. TLA+ is relatively rare in its universality and depth, but it intentionally gives up on end-to-end both because it is currently infeasible (in general) and because 99.99% of software simply doesn't require such strong guarantees.