[SystemSafety] Empirical Study on the Correctness of, Formally Verified Distributed Systems

[José Miguel Faria]

Thanks for the pointer, very interesting work.

As it reads, the quoted text might be a bit misleading. For the sake of
completeness, I'd add a bit more of text extracted from the paper:

"we observe that the identified bugs occur at the interface between
verified and other components, namely in the specification, shim layer, and
auxiliary tools
[...]
none of these bugs were found in the distributed protocols of verified
systems, despite that we specifically searched for protocol bugs and spent
more than eight months in this process. This result suggests that these
verified distributed systems correctly implement the distributed system
protocols, which is particularly impressive given the notorious complexity
of distributed protocols."


Ultimately, the paper stresses how difficult it is to achieve/demonstrate
*completeness* of verification. Even using formal proof, one can't prove
the 'entire world'; sooner or later, an issue related to a (wrong)
assumption will reveal.

Per se, that does not remove value to the formal proofs; it highlights the
importance of considering all other aspects outside the prove, and having a
global system-wise view of the problem.

On the positive side, still from the paper: "The absence of protocol bugs
found in the verified systems sharply contrasts with the results of an
analysis we conducted of known bugs in unverified distributed systems."


José

-- 

José M FariaSAFE PERSPECTIVE Ltd, Director
t: +44 (0)7918 200367
e: jmf at safeperspective.com


On Thu, Apr 20, 2017 at 4:17 PM, Derek M Jones <derek at knosof.co.uk> wrote:

> All,
>
> "This paper thoroughly analyzes three state-of-the-art, formally
> verified implementations of distributed systems: Iron-
> Fleet, Verdi, and Chapar. Through code review and testing,
> we found a total of 16 bugs, many of which produce serious
> consequences, including crashing servers, returning incorrect
> results to clients, and invalidating verification guarantees.
> These bugs were caused by violations of a wide-range
> of assumptions on which the verified components relied."
>
> https://homes.cs.washington.edu/~pfonseca/papers/eurosys2017-dsbugs.pdf
>
> --
> Derek M. Jones           Software analysis
> tel: +44 (0)1252 520667  blog:shape-of-code.coding-guidelines.com
> _______________________________________________
> The System Safety Mailing List
> systemsafety at TechFak.Uni-Bielefeld.DE
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://lists.techfak.uni-bielefeld.de/mailman/private/systemsafety/attachments/20170421/0ef06114/attachment.html>