[e-lang] Important new paper: The Need for Capability Policiies

[Mark S. Miller]

(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.

[Mark Miller]

[+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.

[+ 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.

(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
For more options, visit https://groups.google.com/groups/opt_out.

--
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
For more options, visit https://groups.google.com/groups/opt_out.

[Drossopoulou, Sophia]

Hi Mark,

Ø From: Mark Miller [mailto:***@gmail.com]

Ø 
 relevant to this is Matej Kosik's ocap taming of Benjamin Pierce's Pict Language: 
.

Ø 
 It would be interesting to see 
 A proof (or even informal argument) that the Pict implementation satisfies these types.

James and I have a sketch for a proof that the Joe code satisfies Pol_2. An interesting observation is that the proof makes use both of Hoare-logic-like specs and reasoning (sufficient conditions), and of type annotations like private and final (which are about “deny” properties). The sketch can be found in the slides from our talk at FtfJP’13 at pages 26-30. The slides are available from
http://www.doc.ic.ac.uk/~scd/CAPE-FTfJP%2713_slides.pdf

Sophia

PS Does

Ø [+kosik]

Ø [-google-caja-discuss, -cap-talk] Use e-lang as the only list for further discussions.
mean that the only recipients of these messages should be e-lang? Should I not have copied the other recipients?

From: Mark Miller [mailto:***@gmail.com]
Sent: 07 July 2013 20:32
To: Discussion of E and other capability languages; Matej Kosik
Cc: 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; Drossopoulou, Sophia; James Noble; Gregory Meredith
Subject: 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.

[Mark Miller]

On Mon, Jul 8, 2013 at 6:08 AM, Drossopoulou, Sophia <

Hi Mark,****
**Ø ** … relevant to this is Matej Kosik's ocap taming of Benjamin
Pierce's Pict Language: ….****
**Ø **… It would be interesting to see … A proof (or even informal
argument) that the Pict implementation satisfies these types.****
** **
James and I have a sketch for a proof that the Joe code satisfies Pol_2.
An interesting observation is that the proof makes use both of
Hoare-logic-like specs and reasoning (sufficient conditions), and of type
annotations like private and final (which are about “deny” properties). The
sketch can be found in the slides from our talk at FtfJP’13 at pages 26-30.
The slides are available from****
http://www.doc.ic.ac.uk/~scd/CAPE-FTfJP%2713_slides.pdf****
**

Hi Sophia, what's the diference between slides 28 and 29? The change in
font size makes other changes hard to spot.

**
Sophia****
** **
PS Does****
**Ø **[+kosik]****
**Ø **[-google-caja-discuss, -cap-talk] Use e-lang as the only list for
further discussions.****
mean that the only recipients of these messages should be e-lang? Should I
not have copied the other recipients?

I generally find that keeping more than one list in the addressees list is
bad, as replies from subscribers to one list are not seen by subscribers to
other lists. That's why my first message suggested "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.)"

By the same token, keeping a list + many individuals creates the same
problem. The e-lang list has been very quiet lately so I encourage everyone
here interested in this topic to subscribe (as Sophia has). After today, I
suggest we drop the other individual addressees and just continue this
thread on e-lang. (Also, the mailing list software flags messages with too
many addressees as needing administer approval, delaying their public
posting. So dropping the individual addressees will solve this as well.)

****
** **
*Sent:* 07 July 2013 20:32
*To:* Discussion of E and other capability languages; Matej Kosik
*Cc:* 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;
Drossopoulou, Sophia; James Noble; Gregory Meredith
*Subject:* 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.****
** **

[Drossopoulou, Sophia]

Hi Mark,

From: Mark Miller [mailto:***@gmail.com]

...
On Mon, Jul 8, 2013 at 6:08 AM, Drossopoulou, Sophia <***@imperial.ac.uk<mailto:***@imperial.ac.uk>> wrote:

James and I have a sketch for a proof that the Joe code satisfies Pol_2...

http://www.doc.ic.ac.uk/~scd/CAPE-FTfJP%2713_slides.pdf


Ø Hi Sophia, what's the diference between slides 28 and 29? The change in font size makes other changes hard to spot.

There is no difference! Sorry. I did not notice that when giving the talk. To avoid confusion, I have now replaced slide 29 by an empty slide.

Cheers,

Sophia

PS


From: Mark Miller [mailto:***@gmail.com]

Ø .. I suggest we drop the other individual addressees and just continue this thread on e-lang. ...
Yes will do that.

[Mark Miller]

Amusingly relevant:
https://mail.mozilla.org/pipermail/es-discuss/2013-July/031670.html



On Mon, Jul 8, 2013 at 8:57 AM, Drossopoulou, Sophia <

Hi Mark,****
** **
**
…****
On Mon, Jul 8, 2013 at 6:08 AM, Drossopoulou, Sophia <
James and I have a sketch for a proof that the Joe code satisfies Pol_2…*
***
http://www.doc.ic.ac.uk/~scd/CAPE-FTfJP%2713_slides.pdf****
** **
**Ø **Hi Sophia, what's the diference between slides 28 and 29? The
change in font size makes other changes hard to spot.****
** **
There is no difference! Sorry. I did not notice that when giving the
talk. To avoid confusion, I have now replaced slide 29 by an empty slide.*
***
** **
Cheers,****
** **
Sophia ****
** **
PS****
** **
**Ø **.. I suggest we drop the other individual addressees and just
continue this thread on e-lang. …****
Yes will do that.****
** **
* *****

[Drossopoulou, Sophia]

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:***@gmail.com]
Sent: 08 July 2013 12:29
To: Drossopoulou, Sophia
Cc: Mike Stay; <google-caja-***@googlegroups.com>; 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 <***@imperial.ac.uk<mailto:***@imperial.ac.uk>> wrote:
Dear Mark,

.... 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 <***@gmail.com<mailto:***@gmail.com>> wrote:


On Sun, Jul 7, 2013 at 10:43 AM, Mike Stay <***@gmail.com<mailto:***@gmail.com>> 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.

(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
For more options, visit https://groups.google.com/groups/opt_out.

--
Mike Stay - ***@gmail.com<mailto:***@gmail.com>
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

[Mike Stay]

[Resending at Mark's request: since I wasn't subscribed to e-lang, the
message bounced.]

On Mon, Jul 8, 2013 at 5:58 AM, Meredith Gregory

P.S. i think what Mike might have been saying about objects is something
like this.
Which formal model of objects are you choosing in which to prove things
about the relationship of computations over objects to the particular policy
language?
What's the relationship of that formal model to Javascript? As i understand
it, Javascript is one of the go-to languages for a big portion of ocap
practice.
How familiar is the community of ocap practice with the formal model and
it's relationship to their practice?
There are a few formal models of objects. Which one has wide enough
acceptance in the theoretical community that there might be enough momentum
to get it used in the community of practice for use in proving things about
policy-governed computation?

Yes, that's the gist of it. Everyone agrees on the rough idea of an
object, namely state + code, but the definition has to be expansive
enough to cover cases where the language doesn't even support
closures; I don't know of a formal definition of "object" that
everyone agrees on, whereas the formal semantics of a pi calculus term
are very clear.

A similar critique could certainly be levied against a mobile process
calculus based approach. Mike, are you suggesting that the ocap community of
practice also look at mobile process calculi for expression of practice
(writing executable code) as well as proving things about policy-governed
computation? That's a radical, but interesting idea!

I'm not saying that everyone should switch to programming in Pict, but
rather suggesting that there's a lot of interesting type theory around
pi calculus and that pi calculus satisfies the criteria for being an
ocap language. It would be really interesting to see, for instance, a
compiler from some subset of JavaScript into some variant of pi
calculus; I think that with some care, the compiler could be light
enough that types could be pulled back from pi to js. The end result,
I hope, would be insight into how to design a behavioral type system
for general ocap languages.

For example,
object-based code is going to suffer the principle port issue, not so for
process calculi!

I don't think that's really an issue; standard ocap practice is to
factor authority into facets, each of which is a different reference.

On the other hand, there are not a very many practical
implementations of process calculi based languages. JoCaml comes to mind.
Are you thinking of something like that or maybe embedding an implementation
in a more modern language, maybe like Molecule?

I'm asserting that by understanding process calculi better and their
behavioral types, the ocap community will be in a better position to
accomplish the goal laid out in this paper.

[Ben Laurie]

Thanks for bringing this very nice paper to our attention. Just one
editorial remark here. (Sorry to group-reply to a very large
distribution list, but I assume anyone who doesn't care has muted this
conversation by now...)
I've long commented to erights about the problem w/ capability
languages being that they push too much into Turing-complete code and
don't put enough in declarative, decidable policy languages.

Its not clear that this is actually a bad thing - for example, the
experience with SELinux appears to be that detaching policy from code
leads to very complex policies that do not stay in step with code. It
could be argued that capability policies are less likely to suffer
from this problem, since they are more clearly aligned with the
objects in the code than the kinds of objects SELinux has to put up
with. But I think the jury is still out on that one.

The key problem, it seems to me, is that most programmers just want to
get stuff done. They are not interested hugely in correctness, they
are more interested in functionality. Given that, how do we assist
them in avoiding overly lax policies, modified willy-nilly until stuff
works, without regard for the security consequences?

Given my
own experience, the area I've brought up most often is access control.
Unfortunately, mentioning ACLs to this crowd is a bit like bringing up
crosses and garlic to vampires, and leads to a lengthy discourse about
confused deputies, which confuses policy with implementation. Buried
inside every Web-based cap program is an ACL struggling to be heard.
(I even once saw erights write a program that had a hand-coded ACL in
it.)

My position is that ultimately you have to resort to policy, and
policy can be expressed in various ways - for example, "ask the user"
is a popular one, but ACLs are certainly a viable alternative. I
believe I said as much in http://www.links.org/files/capabilities.pdf.

The difference between ACLs and the kinds of policies in this paper is
that these look to me for the most part to be traditional program
*properties*. In contrast, policy languages are part of the active
execution of the program, usually as a callout to some policy
decision/enforcement agent.
Shriram

[Mark Miller]

Post by Ben Laurie

Thanks for bringing this very nice paper to our attention. Just one
editorial remark here. (Sorry to group-reply to a very large
distribution list, but I assume anyone who doesn't care has muted this
conversation by now...)

Hi Shriram, I never did see this message, only Ben's reply to it.

You may have missed it, but after the first day I suggested the
conversation continue only on e-lang (subscribe at <
http://www.eros-os.org/mailman/listinfo/e-lang>) because otherwise, as
people unsubscribed reply, the people attending this thread via e-lang miss
those replies.

IOW, one way to mute this conversation at this point is to not subscribe to
e-lang. Nevertheless, I don't know how I missed your message since you
apparently did preserve the long addressee list.

Post by Ben Laurie

I've long commented to erights about the problem w/ capability
languages being that they push too much into Turing-complete code and
don't put enough in declarative, decidable policy languages.

Its not clear that this is actually a bad thing - for example, the
experience with SELinux appears to be that detaching policy from code
leads to very complex policies that do not stay in step with code. It
could be argued that capability policies are less likely to suffer
from this problem, since they are more clearly aligned with the
objects in the code than the kinds of objects SELinux has to put up
with. But I think the jury is still out on that one.
The key problem, it seems to me, is that most programmers just want to
get stuff done. They are not interested hugely in correctness, they
are more interested in functionality. Given that, how do we assist
them in avoiding overly lax policies, modified willy-nilly until stuff
works, without regard for the security consequences?

Given my
own experience, the area I've brought up most often is access control.

I'll wait to respond to the rest of this until I see your original message,
but here I just want to clear up a terminological confusion. ACLs and ocaps
are both forms of access control.

Post by Ben Laurie

Unfortunately, mentioning ACLs to this crowd is a bit like bringing up
crosses and garlic to vampires, and leads to a lengthy discourse about
confused deputies, which confuses policy with implementation.

Confused deputy is not an implementation issue. The issue is the difficulty
of expressing meaningful policies (or policies that express what you
intended them to express) given the wrong primitives. Ignoring confused
deputy is like doing physics ignoring the Michelson–Morley experiment.
("But what if the speed of light didn't have the peculiar problem?")

Post by Ben Laurie
Buried

inside every Web-based cap program is an ACL struggling to be heard.
(I even once saw erights write a program that had a hand-coded ACL in
it.)

Indeed. Horton can be seen this way.

Post by Ben Laurie
My position is that ultimately you have to resort to policy, and
policy can be expressed in various ways - for example, "ask the user"
is a popular one, but ACLs are certainly a viable alternative. I
believe I said as much in http://www.links.org/files/capabilities.pdf.

The difference between ACLs and the kinds of policies in this paper is
that these look to me for the most part to be traditional program
*properties*. In contrast, policy languages are part of the active
execution of the program, usually as a callout to some policy
decision/enforcement agent.

Do you have a positive example?

Post by Ben Laurie

Shriram

--
---
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
For more options, visit https://groups.google.com/groups/opt_out.

[Drossopoulou, Sophia]

Hi Shriram,

Do you mean that "policy languages" expect to be monitored while the program is executed, and throw exceptions when not adhered to, while what James and I propose in our paper is something that is the property of a program, and would (most naturally) be checked statically?

Sophia

From: e-lang-***@mail.eros-os.org [mailto:e-lang-***@mail.eros-os.org] On Behalf Of Mark Miller
Sent: 11 July 2013 16:29
To: Shriram Krishnamurthi; Discussion of E and other capability languages
Subject: Re: [e-lang] [Caja] Important new paper: The Need for Capability Policiies

....

The difference between ACLs and the kinds of policies in this paper is
that these look to me for the most part to be traditional program
*properties*. In contrast, policy languages are part of the active
execution of the program, usually as a callout to some policy
decision/enforcement agent.

Do you have a positive example?

[Drossopoulou, Sophia]

Hi Shriram,

Thank you for clarifying the terminology.

Sophia Drossopoulou asked about a distinction I introduced in my
message. To repeat it -- and I should be clear that I don't think
there is any standard terminology here -- I want to make a distinction
between "statements about programs that are automatically enforced by
the implementation mechanism" and "statements about programs that need
to be checked for by some external mechanism". I use the terms
"policy" for the former and "property" for the latter. Properties are
the things that verification engines have consumed for ages, and the
properties I saw in the very nice Drossopoulou/Noble paper struck me,
ultimately, are not much different from a variety of properties that
have been written down about programs down the ages. (Short answer to
Sophia's question: Yes.)

Indeed, with the terminology suggested by Shriram Krishnamurthi, what James Noble and I are looking for is "properties".

However, I believe that expressing policies through program properties leads to properties which are somewhat different from those usually written down about programs, because a) they are "open|, and b) they have "deny" elements. "Open" means that these properties need to be maintained by the code as well as any extension of that code, and "deny" elements are properties of the code itself rather than of the effects of the code. Policy Pol_2 from the paper has such deny elements.

In a sun strand of this discussion, together with Greg Meredith, Mike Stay, Mark Miller and James Noble, we discussed more the shape of formalisation of such properties, and we came up with the following proposal:

a module P satisfies Policy(E,A)
iff
for all modules Q, and code CD:
if we execute code CD in the presence of P augmented with Q, and observe effect E, then the code CD has property A.

Cheers,

Sophia

[Mark S. Miller]

Shriram, I appreciate the distinction you point out, but it does not fit
with my sense of the meaning of "policy". Policies need to be expressed,
understood, and enforced. To be enforced, there needs to be some mechanism
that brings about the enforcement. Does this mechanism succeed at enforcing
the stated policy? How should we verify this? This question seems
independent of whether the code we're verifying is the code which also
implements the functionality, or is separate from that code. Sophia's
formulation would seem to apply equally well to both scenarios.

Many policies of interest cannot be enforced separately from the code
implementing the functionality -- which I think echoes what Ben was saying.
Hence the subtitle of <http://www.erights.org/talks/no-sep/> is "Why
security is not a separable concern". (This expanded into Part 4 of my
thesis, but I unwisely dropped the subtitle at that time. I've always
missed it.)

Shriram, this is the second message from you where I saw only the replies.
I also don't see your messages in the e-lang archive. Do you know why we're
missing these?





On Wed, Jul 17, 2013 at 1:49 PM, Drossopoulou, Sophia <

Post by Mark Miller
Hi Shriram,
Thank you for clarifying the terminology.
Sophia Drossopoulou asked about a distinction I introduced in my
message. To repeat it -- and I should be clear that I don't think
there is any standard terminology here -- I want to make a distinction
between "statements about programs that are automatically enforced by
the implementation mechanism" and "statements about programs that need
to be checked for by some external mechanism". I use the terms
"policy" for the former and "property" for the latter. Properties are
the things that verification engines have consumed for ages, and the
properties I saw in the very nice Drossopoulou/Noble paper struck me,
ultimately, are not much different from a variety of properties that
have been written down about programs down the ages. (Short answer to
Sophia's question: Yes.)
Indeed, with the terminology suggested by Shriram Krishnamurthi, what
James Noble and I are looking for is "properties".
However, I believe that expressing policies through program properties
leads to properties which are somewhat different from those usually written
down about programs, because a) they are "open|, and b) they have "deny"
elements. "Open" means that these properties need to be maintained by the
code as well as any extension of that code, and "deny" elements are
properties of the code itself rather than of the effects of the code.
Policy Pol_2 from the paper has such deny elements.
In a sun strand of this discussion, together with Greg Meredith, Mike
Stay, Mark Miller and James Noble, we discussed more the shape of
formalisation of such properties, and we came up with the following
a module P satisfies Policy(E,A) ****
iff****
if we execute code CD in the presence of P augmented with Q,
and observe effect E, then the code CD has property A.
Cheers,
Sophia
_______________________________________________
e-lang mailing list
http://www.eros-os.org/mailman/listinfo/e-lang

[Ben Laurie]

Shriram, this is the second message from you where I saw only the replies. I
also don't see your messages in the e-lang archive. Do you know why we're
missing these?

I also only saw the reply this time.

[Tom Van Cutsem]

Tangentially related:

I once wrote an article "Why programming
languages?<http://soft.vub.ac.be/~tvcutsem/invokedynamic/node/11>"
where I make the point that a language designer, unlike a library designer,
has the ability to define a language as a little universe with "physical
laws" by which all programs written in that language must abide. The
opening sentence I used was: "no amount of library code is going to turn C
into a memory-safe language. Just so, no amount of library code is going to
turn Java into a thread-safe language."

To me, these properties feel closely related to the "deny" properties that
Sophia and James point out. In fact, a fruitful line of related work might
be tools that aim to prove certain safety and liveness properties such as
data race and deadlock freedom for programs written in a language with
shared mutable state (such as Java). These properties, like ocap security,
depend on *all code* in the system to play by the rules.

Regards,
Tom

Post by Mark S. Miller
Shriram, I appreciate the distinction you point out, but it does not fit
with my sense of the meaning of "policy". Policies need to be expressed,
understood, and enforced. To be enforced, there needs to be some mechanism
that brings about the enforcement. Does this mechanism succeed at enforcing
the stated policy? How should we verify this? This question seems
independent of whether the code we're verifying is the code which also
implements the functionality, or is separate from that code. Sophia's
formulation would seem to apply equally well to both scenarios.
Many policies of interest cannot be enforced separately from the code
implementing the functionality -- which I think echoes what Ben was saying.
Hence the subtitle of <http://www.erights.org/talks/no-sep/> is "Why
security is not a separable concern". (This expanded into Part 4 of my
thesis, but I unwisely dropped the subtitle at that time. I've always
missed it.)
Shriram, this is the second message from you where I saw only the replies.
I also don't see your messages in the e-lang archive. Do you know why we're
missing these?
On Wed, Jul 17, 2013 at 1:49 PM, Drossopoulou, Sophia <

Post by Mark Miller
Hi Shriram,
Thank you for clarifying the terminology.
Sophia Drossopoulou asked about a distinction I introduced in my
message. To repeat it -- and I should be clear that I don't think
there is any standard terminology here -- I want to make a distinction
between "statements about programs that are automatically enforced by
the implementation mechanism" and "statements about programs that need
to be checked for by some external mechanism". I use the terms
"policy" for the former and "property" for the latter. Properties are
the things that verification engines have consumed for ages, and the
properties I saw in the very nice Drossopoulou/Noble paper struck me,
ultimately, are not much different from a variety of properties that
have been written down about programs down the ages. (Short answer to
Sophia's question: Yes.)
Indeed, with the terminology suggested by Shriram Krishnamurthi, what
James Noble and I are looking for is "properties".
However, I believe that expressing policies through program properties
leads to properties which are somewhat different from those usually written
down about programs, because a) they are "open|, and b) they have "deny"
elements. "Open" means that these properties need to be maintained by the
code as well as any extension of that code, and "deny" elements are
properties of the code itself rather than of the effects of the code.
Policy Pol_2 from the paper has such deny elements.
In a sun strand of this discussion, together with Greg Meredith, Mike
Stay, Mark Miller and James Noble, we discussed more the shape of
formalisation of such properties, and we came up with the following
a module P satisfies Policy(E,A) ****
iff****
if we execute code CD in the presence of P augmented with Q,
and observe effect E, then the code CD has property A.
Cheers,
Sophia
_______________________________________________
e-lang mailing list
http://www.eros-os.org/mailman/listinfo/e-lang

--
Cheers,
--MarkM
_______________________________________________
e-lang mailing list
http://www.eros-os.org/mailman/listinfo/e-lang

[Rob Meijer]

Post by Mark Miller

Post by Ben Laurie

inside every Web-based cap program is an ACL struggling to be heard.

Hmm, I would actually say that inside every web-credential/acl there is a
decompose tree of attenuable and authority waiting to be allowed to be
conveniently delegated and revoked using capabilities.

B.t.w, does this list honor any 'don't archive' mail headers? I think the
slides to an upcoming talk of mine may be relevant to this discussion, I
would like to share it with the list, but I don't want to make them
available yet through Google (searching my name of that of my talk) for
people not on the list that are going to be visiting the event.

Post by Mark Miller

Post by Ben Laurie

(I even once saw erights write a program that had a hand-coded ACL in
it.)

Indeed. Horton can be seen this way.

Post by Ben Laurie
My position is that ultimately you have to resort to policy, and
policy can be expressed in various ways - for example, "ask the user"
is a popular one, but ACLs are certainly a viable alternative. I
believe I said as much in http://www.links.org/files/capabilities.pdf.

The difference between ACLs and the kinds of policies in this paper is
that these look to me for the most part to be traditional program
*properties*. In contrast, policy languages are part of the active
execution of the program, usually as a callout to some policy
decision/enforcement agent.

Do you have a positive example?

Post by Ben Laurie

Shriram

--
---
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
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
http://www.eros-os.org/mailman/listinfo/e-lang

[Mark S. Miller]

Post by Rob Meijer

Post by Mark Miller

Post by Ben Laurie

inside every Web-based cap program is an ACL struggling to be heard.

Hmm, I would actually say that inside every web-credential/acl there is a
decompose tree of attenuable and authority waiting to be allowed to be
conveniently delegated and revoked using capabilities.
B.t.w, does this list honor any 'don't archive' mail headers? I think the
slides to an upcoming talk of mine may be relevant to this discussion, I
would like to share it with the list, but I don't want to make them
available yet through Google (searching my name of that of my talk) for
people not on the list that are going to be visiting the event.

I know of no such mechanism, so assume not.

Post by Rob Meijer

Post by Mark Miller

Post by Ben Laurie

(I even once saw erights write a program that had a hand-coded ACL in
it.)

Indeed. Horton can be seen this way.

Post by Ben Laurie
My position is that ultimately you have to resort to policy, and
policy can be expressed in various ways - for example, "ask the user"
is a popular one, but ACLs are certainly a viable alternative. I
believe I said as much in http://www.links.org/files/capabilities.pdf.

The difference between ACLs and the kinds of policies in this paper is
that these look to me for the most part to be traditional program
*properties*. In contrast, policy languages are part of the active
execution of the program, usually as a callout to some policy
decision/enforcement agent.

Do you have a positive example?

Post by Ben Laurie

Shriram

--
---
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
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
http://www.eros-os.org/mailman/listinfo/e-lang

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

[Daira Hopwood]

Post by Rob Meijer
B.t.w, does this list honor any 'don't archive' mail headers? I think the
slides to an upcoming talk of mine may be relevant to this discussion, I
would like to share it with the list, but I don't want to make them
available yet through Google (searching my name of that of my talk) for
people not on the list that are going to be visiting the event.

The pipermail archive at <http://www.eros-os.org/pipermail/cap-talk/>
honours the X-No-Archive header, as does the gmane archive at
<http://news.gmane.org/gmane.comp.capabilities.general>.

<http://www.gnu.org/software/mailman/mailman-admin/node26.html>
<http://gmane.org/expiry.php>

[r***@gmail.com]

Amusingly relevant:
https://mail.mozilla.org/pipermail/es-discuss/2013-July/031670.html

Oh that's a big problem with IEEE 64 bit floats I think...a
David Mercer
Portland, OR

[Daira Hopwood]

Post by Mark Miller
https://mail.mozilla.org/pipermail/es-discuss/2013-July/031670.html
Oh that's a big problem with IEEE 64 bit floats I think...

Awesome:

Nat(balance)
Nat(amount)
Nat(balance + amount)
Nat(balance) + Nat(amount) === Nat(balance + amount)

but Nat(balance) + Nat(amount) does not represent the same value as balance + amount!

What better argument could you make for fail-stop precise integer arithmetic?

("fail-stop precise" => give the exact result or fail)

[Karp, Alan H]

Post by Daira Hopwood
Nat(balance)
Nat(amount)
Nat(balance + amount)
Nat(balance) + Nat(amount) === Nat(balance + amount)
but Nat(balance) + Nat(amount) does not represent the same value as balance + amount!

Isn't the surprise really that Nat(balance+amount) doesn't throw but balance+amount is not in range?

________________________
Alan Karp
Principal Scientist
Enterprise Services, Office of the CTO
Hewlett-Packard Company
1501 Page Mill Road
Palo Alto, CA 94304
[phone], fax [phone]
http://www.hpl.hp.com/personal/Alan_Karp

[Mark S. Miller]

The computed sum of balance+amount is in range, and is returned by
Nat(balance+amount). But this computed sum is not the sum of balance and
amount. Note that this is fixed in current SES by admitting 2**53-1 but not
2**53, and is reflected in the definitions of MAX_SAFE_INTEGER and
isSafeInteger in EcmaScript 6.

Post by Daira Hopwood

Post by Daira Hopwood
Nat(balance)
Nat(amount)
Nat(balance + amount)
Nat(balance) + Nat(amount) === Nat(balance + amount)
but Nat(balance) + Nat(amount) does not represent the same value as

balance +

Post by Daira Hopwood
amount!

Isn't the surprise really that Nat(balance+amount) doesn't throw but
balance+amount is not in range?
________________________
Alan Karp
Principal Scientist
Enterprise Services, Office of the CTO
Hewlett-Packard Company
1501 Page Mill Road
Palo Alto, CA 94304
[phone], fax [phone]
http://www.hpl.hp.com/personal/Alan_Karp
_______________________________________________
e-lang mailing list
http://www.eros-os.org/mailman/listinfo/e-lang