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

[+kosik]
[-google-caja-discuss, -cap-talk] Use e-lang as the only list for further
discussions.

Hi Mike, relevant to this is Matej Kosik's ocap taming of Benjamin Pierce's
Pict Language:
http://www2.fiit.stuba.sk/~kosik/doc/sofsem2008.pdf
http://www2.fiit.stuba.sk/~kosik/doc/tamed-pict--standard-library.pdf

It would be interesting to see
* This concrete example coded in Tamed Pict,
* The specs from the position paper formally restated in these spatial and
temporal types, and
* A proof (or even informal argument) that the Pict implementation
satisfies these types.


On Sun, Jul 7, 2013 at 10:43 AM, Mike Stay <[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]> 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 google-caja-discuss+unsubscribe-/JYPxA39Uh5TLH3MbocFF+G/[email protected]
> > For more options, visit https://groups.google.com/groups/opt_out.
> >
> >
>
>
>
> --
> Mike Stay - [email protected]
> http://www.cs.auckland.ac.nz/~mike
> http://reperiendi.wordpress.com
>
> --
>
> ---
> 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 google-caja-discuss+unsubscribe-/JYPxA39Uh5TLH3MbocFF+G/[email protected]
> For more options, visit https://groups.google.com/groups/opt_out.
>
>
>


-- 
Text by me above is hereby placed in the public domain

  Cheers,
  --MarkM

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