Re: [Caja] Important new paper: The Need for Capability Policiies

Hi Greg,

Ø  … represent deniability via the following schema: Deny( C, a, S ) := ( C => <a>S ) & ( ~C => ~<a>true )?

Ø  …  if P meets the condition C, then P can take action a and move to state S, otherwise P cannot take action a.
I do not see  such a style of specification could capture the essence of Pol_2. Namely, a specification as the one above says that “P”  may do “a”  if “C”, while what James and I are proposing (and what we think is necessary to express Pol_2) is more like if “P” (or any extension of P)  has an effect “\phi” (namely the effect may be the outcome of a sequence of different actions), then “P” must satisfy property “C”.

In other words, a specification as you are outlining above is about sufficient conditions, while “deny” properties are about necessary conditions.

The distinction is crucial, but not obvious – I think that this is mainly due to the fact that we are used to thinking more about sufficient conditions rather than necessary ones. Thank you for helping in finding better ways of expressing.



Ø  … probe the notion of extension in operation here. I think that extending P in environment P|Q without any constraints on Q  …
I think that the notion of “extension” depends on the context. In the case of Java, it means that Q can be compiled in the presence of P and more code, or even that Q is bytecode which can be run without throwing linking and verification exceptions when P has been loaded. In the context of E,  it would mean that Q is legal E code.

Cheers,

Sophia

From: Meredith Gregory [mailto:[email protected]]
Sent: 08 July 2013 12:29
To: Drossopoulou, Sophia
Cc: Mike Stay; <[email protected]>; General discussions concerning capability systems.; Discussion of E and other capability languages; Stephen Chong; Robert N. M. Watson; Toby Murray; Fred Spiessens; John Mitchell; Benjamin Pierce; Shriram Krishnamurthi; Joe Gibbs Politz; Arjun Guha; Gareth Smith; Gardner, Philippa A; Ankur Taly; David Wagner; Adrian Mettler; Ben Laurie; Jonathan Shapiro; M. Scott Doerrie; James Noble
Subject: Re: [Caja] Important new paper: The Need for Capability Policiies

Dear Sophia,

Thanks for your question and engagement!

i'm still coming up to speed on your paper, so allow me to answer a question with a few questions of my own.

  *   Does it seem reasonable to represent deniability via the following schema: Deny( C, a, S ) := ( C => <a>S ) & ( ~C => ~<a>true )?

     *   Suppose P |= Deny( C, a, S ) then if P meets the condition C, then P can take action a and move to state S, otherwise P cannot take action a.

  *   If so, then let me probe the notion of extension in operation here. i think that extending P in environment P|Q without any constraints on Q would mean we want P|Q |= Deny( C, a, S ) | true which suggests all kinds of simplifications. Naturally, we have to be careful introducing the adjunct to the -|- type to avoid overwhelming complexity in type/model checking.
Is this the sort of thing you're talking about or have i missed it completely?

Best wishes,

--greg

On Mon, Jul 8, 2013 at 2:35 AM, Drossopoulou, Sophia <[email protected]<mailto:[email protected]>> wrote:
Dear Mark,



> From: "Mark S. Miller" <[email protected]<mailto:[email protected]>>
> .... I think the investigation they outline is the next important research step ...

Thank you for your endorsement. Indeed, James and I are particularly excited about this work, and we believe in the need of a new kind of specification for these policies. And we look forward to the discussion on this list.

Dear Mike and Greg,

> Spatial and behavioral types like those of Luis Caires ... look like they
> could ... encode the policy language described here.
Thank you for the pointer. My knowledge of this work is not as deep as it should. Could you explain how these types can encode the "deny" aspects of capability policies. For example, Pol_2 from Mark et al's paper in Financial Cryspotgraphy, says that "only someone with the mint of a given currency can violate conservation of that currency". It is indeed possible to write code that has this property, but the question is how to specify this property. Our idea is that the specification must have the "flavour" of an implication, i.e.:
     Program P satisfies policy Pol_2
iff
     For all possible extensions Q of P, and for all executions of code C in that extension (P|Q)
 if execution of C modifies the currency of a mint M, then C has access to M
This specification has the characteristics that it quantifies over all possible extensions of the program, and rather than describe the change of state, it guarantees that a certain change of state can only happen if the code satisfied some property. Therefore, I see a closer connection with refinement types, but there are still differences.

Best regards,

Sophia
PS As a minor point

> … "objects" aren't nearly as well defined.
Well, I do not agree on the above. Moreover, if we target programming languages with objects, and if the specifications talk about objects, then I believe we should stick with objects. But I also think this is not a central point to the argument.  … I do not expect that we can agree on this one . :-)


On 8 Jul 2013, at 00:19, Meredith Gregory <[email protected]<mailto:[email protected]>> wrote:


 On Sun, Jul 7, 2013 at 10:43 AM, Mike Stay <[email protected]<mailto:[email protected]>> wrote:
[+ Greg Meredith]

You can think of pi calculus as being an ocaps language where channels
are facets.  The nice thing about pi calculus is that there's a very
clearly defined notion of a process and a tremendous literature on
typing, whereas "objects" aren't nearly as well defined.  Spatial and
behavioral types like those of Luis Caires [1, 2, 3] look like they
could (or could easily be extended to) encode the policy language
described here.

Greg, care to comment?

[1] Caires, Luís. "Behavioral and Spatial Observations in a Logic for
the π-Calculus".  In FoSSaCS, pages 72–89, 2004.
[2] Caires, Luís and Luca Cardelli.  "A spatial logic for concurrency
(part i)". Inf. Comput., 186(2):194–235, 2003.
[3] Caires, Luís and Luca Cardelli.  "A spatial logic for concurrency
(part ii)".  Theor. Comput. Sci., 322 (3) : 517–565, 2004.

On Sun, Jul 7, 2013 at 9:27 AM, Mark S. Miller <[email protected]<mailto:[email protected]>> wrote:
> (John, could you forward to David Mazières? Thanks.)
>
> A position paper at <http://dl.acm.org/citation.cfm?doid=2489804.2489811>
> and
> <http://types.cs.washington.edu/ftfjp2013/preprints/a6-Drossopoulou.pdf>. I
> think the investigation they outline is the next important research step
> that object-capabilities need to take. Without something like this, it is
> hard to see how we could preserve security under code maintenance -- for the
> reasons they state. Although the form of specification they suggest would
> apply to both ocap OSes and languages, the corresponding analysis would seem
> to apply much more to ocap languages. Thus, I suggest that further general
> discussion should occur only on the e-lang list. (Subscribe at
> <http://www.eros-os.org/mailman/listinfo/e-lang>. You need to subscribe to
> post.)
>
> I have separately been discussing with several of you the adaptation of
> other formalisms -- decentralized info flow, separation logic, and (with the
> authors) ownership types -- to serve as a specification language for
> checking ocap implementations. But these discussions have not had clear
> goals about what needs to be specified. The specification needs explained in
> this paper, concretely in terms of this example, sets good challenge goals.
> How might these or other formalisms contribute towards specifying,
> verifying, or enforcing such policies?
>
>
> The Need for Capability Policiies
>
> by Sophia Drossopoulou and James Noble, (cc'ed)
>
> The object-capability model is one of the industry standards adopted for the
> implementation of security policies for web-based software.
> Object-capabilities in various forms are supported by programming languages
> such as E, Joe-E, Newspeak, Grace, and the newer versions of Javascript.
> Unfortunately, code written using capabilities tends to concentrate on the
> low-level mechanism rather than the high-level policy.
>
> In this position paper, we argue that current specification methodologies
> cannot adequately capture all aspects of the capability policies required to
> support object-capability systems. We outline informally the features that
> such security policies should support, and we demonstrate (also informally)
> how we can reason that examples satisfy the capability policies.
>
>
> --
>     Cheers,
>     --MarkM
>
> --
>
> ---
> You received this message because you are subscribed to the Google Groups
> "Google Caja Discuss" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to [email protected]<mailto:google-caja-discuss%[email protected]>.
> For more options, visit https://groups.google.com/groups/opt_out.
>
>



--
Mike Stay - [email protected]<mailto:[email protected]>
http://www.cs.auckland.ac.nz/~mike
http://reperiendi.wordpress.com<http://reperiendi.wordpress.com/>



--
L.G. Meredith
Managing Partner
Biosimilarity LLC
7329 39th Ave SW
Seattle, WA 98136

+1 206.650.3740<tel:%2B1%20206.650.3740>

http://biosimilarity.blogspot.com<http://biosimilarity.blogspot.com/>




--
L.G. Meredith
Managing Partner
Biosimilarity LLC
7329 39th Ave SW
Seattle, WA 98136

+1 206.650.3740

http://biosimilarity.blogspot.com

_______________________________________________
e-lang mailing list
[email protected]
http://www.eros-os.org/mailman/listinfo/e-lang