[cap-talk] is defensive correctness a plausible null hypothesis?

[David Barbour]

On Mon, May 16, 2011 at 5:20 AM, Matej Kosik <kosik at fiit.stuba.sk> wrote:

> >
> >   P is defensively correct if it protects against all of its clients.
> >
> >   Correctness can be divided into consistency (safety) and progress
> (liveness).
> >   An object that is vulnerable to denial-of-service by its clients may
> >   nevertheless be defensively consistent.
> >
> > If you have a system:
> > - composed from three processes: P, Q, R.
> > - P relies on R
> >   (i.e. P can provide correct services only if R provides correct
> services)
> > - Q relies on R
> >   (i.e. Q can provide correct services only if R provides correct
> services)
> > in some realistic system (bounded memory/CPU speed); you can choose.
> >
> > How would you prove that R is, e.g., defensively consistent.
> >
> > AFAIK, above goal generates the following two subgoals:
> > 1. Regardless of P's behavior,
> >      if P requests a service from R, and if that request will be served,
> then it will be served correctly.
> > 2. Regardless of Q's behavior,
> >      if Q requests a service from R, and if that request will be served,
> then it will be served correctly.
>
> I guess the proof could proceed in the following way:
> - P does not have sufficient authority to alter R's services offered to Q.
>  (if we can describe and prove the extent of P's authority)
> - Q does not have sufficient authority to alter R's services offered to P.
>  (if we can describe and prove the extent of P's authority)
> Sounds good, doesn't it?
>
>
Saying "no alteration" is too strong. For example, R could be a blackboard
or bulletin board or database. For correctness, any relationship between the
service provided to clients P and Q must be authorized (and not through some
unintentional mistake or rights amplification mechanism).

There are many instances where you can prove R is defensively correct, at
least on the assumption that its implementation is faithful to the
semantics. But you prove this by looking at the exposed capabilities to R,
not at P or Q.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.eros-os.org/pipermail/cap-talk/attachments/20110516/374007cf/attachment.html