[cap-talk] controversial article

[Matej Kosik]

Mark Miller wrote:
> On Sat, Jul 4, 2009 at 3:12 PM, Matej Kosik<kosik at fiit.stuba.sk> wrote:
>> Toby Murray wrote:
>>> ...
>>>
>>> So defensive consistency asserts that no misbehaving client can cause a
>>> server to give incorrect service to a well behaved client.
>>>
>>> Defensive correctness asserts that no misbehaving client can prevent a
>>> server from giving incorrect service to a well behaved client. It is
>>> like a liveness property because it asserts that something ("correct
>>> service being rendered to all well behaved clients, regardless of the
>>> actions of misbehaving clients") must happen.
>> I have somewhat updated my viewpoint.
>> I have rewritten sections 2 and 3 in
>> http://altair.fiit.stuba.sk/mediawiki/upload/2/2d/Sofsem2010.pdf
>> Now I draw some analogies of our two properties with which we are concerned:
>> - defensive consistency
>> - defensive correctness
>> with other safety or liveness properties. The new text makes more sense
>> to. I must yet update the rest of the paper.
> 
> 
> Hi Matej, still absorbing. But one quick comment:

Hi Mark :)

> 
> "In order to prove that a given subsystem is defensively correct, it is
> in general not enough to review its own code but it may be necessary to review
> also client’s code."
> 
> This contradicts the definition of defensive correctness, including
> the definition you give in the preceding paragraph.

I do not understand why you see a contradiction.

In order to prove that a given subsystem is defensively correct, I would
(also) have to prove that none of its subsystems can disrupt services
(for other well-behaving clients) that this subsystem provides.

That is possible to prove, but in general (without special special help
of the underlying platform) I have to go through all the potential
clients and check (among other things) that:
- none of them behaves as a "cancer"
- none of them behaves as a "spammer"
In general, we are force to proceed this way.

In a special case (if we choose the right mechanisms for interaction) we
can defend servers from those threats regardless of how clients behave.

The article informally specifies such mechanisms.
(More formal and more complete specification is elsewhere

and would not fit within limited space. I rather devote significant
space to general topic and my only ambition is to give enough
information to enable others to implement such mechanisms for different
languages if they decided that they want it. I think this can be achieved.)

Whether they can be implemented for distributed environment I do not
know (I guess yes---the remaining vulnerabilities would result from what
threats are below may layer). However, it is straightforwardly possible
to implement that specification for non-distributed environment. In this
non-distributed environment it is then possible to defend servers from
clients that might try to behave as "cancer" or "spammer" or in a
similar malicious way trying to deplete free memory.

> The rest of your
> paper seems consistent with your definition rather than with the quote
> above. Perhaps you meant "totally correct" in this quote?