[cap-talk] is defensive correctness a plausible null

[Mark S. Miller]

sent from android
On May 19, 2011 3:02 PM, "Ankur Taly" <ataly at stanford.edu> wrote:
>
> Hi All,
>
> Sorry for the delayed reply.
>
> (In the rest of the mail, I have assumed that defensive consistency means:
good clients get good or no service. Further, I am assuming that in order to
guarantee good service, the function relies on certain critical resources
satisfying a particular invariant. So defensive consistency boils down to
showing that bad clients cannot break the invariant on these critical
resources)

Please recheck def in thesis, im traveling.

I think defensive consistency (like all  local correctness issues) is
relative to a reliance set. If x's spec says x may rely on the correctness
or consistency of r, then if r becomes corrupted at no fault of x,  x's
subsequent misbehavior is within d.c.

>
> Our confinement analysis for SESlight APIs does quantify the set of all
possible attacker programs, but it abstracts out information about primitive
values. This is still sound as for a confinement analysis we only care about
the flows of object references. However a proof of defensive consistency
would require showing that certain invariants are preserved on the critical
resources before an after each call to the API. Proving these invariants
would perhaps require tracking of primitive values. The flow insensitivity
of our analysis could lead to a large number of false positives if we extend
to tracking primitive values.
>
> On the positive side, defensive consistency cannot hold without
confinement of the critical resources, so establishing confinement is at
least a first step. It might be possible to suitably rewrite a function such
that defensive consistency boils down exactly to showing confinement of the
critical resources. For example, at each point in the code where you are
writing to a critical resource, you can add a run-time check so that the
value that is written does not break the resource invariant. This way as
long as we know that the resources are confined and only the trusted
function writes to them we would be fine.
>
> Best,
> Ankur.
>
>
>
> ----- Original Message -----
> From: "Mark S. Miller" <erights at google.com>
> To: "General discussions concerning capability systems." <
cap-talk at mail.eros-os.org>, "Fred Spiessens" <fred at evoluware.eu>, "Ankur
Taly" <ataly at stanford.edu>
> Sent: Tuesday, May 17, 2011 8:00:01 AM
> Subject: Re: [cap-talk] is defensive correctness a plausible null
>
>
> [+fred, +ataly]
>
> On Tue, May 17, 2011 at 4:40 AM, Viswanathan, Kapaleeswaran (HP Labs
India) < kapali at hp.com > wrote:
>
>
>
> The two paper OZE.pdf and TGC05.pdf appear to describe defensive
consistency differently. TGC05 talks about defensive consistency in terms of
service guarantees: server provides well-behaved clients with either no
service or correct service but never provides a wrong service. OZE talks in
terms of well-formed inputs. I am not sure if both are equivalent or not.
>
>
>
> I do not believe they are equivalent, though perhaps Fred (cc'ed) can
comment. The term was coined in TGC05 and further expanded on in my thesis.
I will proceed considering the version in my thesis definitive.
>
>
>
> Are you talking about a mathematicians (human verifiable) proof or a
machine verifiable proof of defensive consistency? I do not believe that the
concept may be ameneable to machine verifiable proof.
>
>
>
> What about < http://www-cs-students.stanford.edu/~ataly/Papers/sp11.pdf >
by Ankur Taly (cc'ed)? (Paper shortly to be presented at IEEE Symposium on
Security and Privacy)
>
>
> Ankur, this paper does not talk about defensive consistency per se. But it
does quantify the attackers over all possible attacker programs and
behaviors, which would seem to amount to the same thing. Do these proofs
constitute proofs of defensive consistency?
>
>
>
>
>
>
> _______________________________________________
> cap-talk mailing list
> cap-talk at mail.eros-os.org
> http://www.eros-os.org/mailman/listinfo/cap-talk
>
>
>
> --
> Cheers,
> --MarkM
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://www.eros-os.org/pipermail/cap-talk/attachments/20110519/ff8faff3/attachment.html