[cap-talk] "A Contribution to Techniques for Building Dependable Software Systems"

[David Wagner]

Mark S. Miller wrote:
> Interesting paper:
>
> http://www2.fiit.stuba.sk/~kosik/doc/ecbs-eerc-2011.pdf
> A Contribution to Techniques for Building Dependable Software Systems
> by Matej Kosic and Jiri Safarik

Thanks for sharing this!  Here's some feedback for the authors:

I'd be interested to learn more about how the defensive consistency of
the system built here was proven.  I think the question of how to prove
that a module is defensively consistent is a very interesting one.

Diving into the details of the paper, Figure 4 lists the proof
structure to justify the defnesive consistency of the system, but I
didn't understand the details.  I'm particularly looking at the two
leaves under vga.  The two clients of vga are apparently termianl
and uptime_morph.  The figure says terminal can't forge vga to provide
incorrect to uptime_morph, because terminal doesn't have authority to
do that.  I'm not sure what that means, or how we would justify it.
I presume terminal has the ability to interact with vga.  If vga is not
coded properly, perhaps there is some way that terminal's interaction
with vga corrupts its internal state and causes it to provide incorrect
service to uptime_morph.  To rule that possibility out, presumably we
have to look at the code of vga; we can't just claim terminal doesn't
have authority to do anything else beyond invoke vga.  So presumably
there must be some kind of verification of the code of vga; it would be
interesting to learn more about what properties were verified, how they
were specified, and how they were formally verified.  Or perhaps I have
misunderstood what is going on here?  Anyway, if the authors are reading
this, this might be an interesting part of the paper to elaborate on.

Other minutae: Section VII refers to Figure 3 as providing a
proof of correctness for terminal.  Is this a typo?  Figure 3 does
not seem to provide a proof of correctness for terminal.