Re: Coercion, membranes, serialization, and printing are the same thing

Hi Tom, 

Recently, we’ve been studying how we can reason about using membranes to control the flow of capabilities in web applications. As part of this, we’ve also been working on establishing the relationship between ownership and membranes in ocap languages.

We developed a formal system that uses higher-order contracts to track the ownership of capabilities. This mechanism can be considered a particular type of membrane. We show that the mechanism soundly tracks the ownership of capabilities. Thus, the technique may be useful in showing that membranes are sufficient to track ownership in other (non-capability safe) settings (like JavaScript), or what additional conditions are required to do so.

For those that are interested, in addition to tracking the ownership of capabilities we extend our model of a capability-safe language with access control and information-flow policy annotations on capabilities that describe restrictions on which parts of the program may access the capabilities or influence their use. Access control policies can be used to ensure that capabilities are not “leaked” from the abstractions (membranes) designed to protect them. The information-flow policies can be used to enforce stronger invariants: that certain parts of the program may not affect the use of certain capabilities (i.e. integrity of use), even *indirectly*.

We use the higher-order contracts described above as membranes to enforce the access control policies. For the information-flow policies, we use an information-flow type system. We also show how to compose these mechanisms, in particular allowing for programs in which some parts enforce only access control policies and others enforce information-flow policies.

If you are interested in our work, please drop us a line and we can send you a draft of our paper. (It's joint work with Christos Dimoulas, Aslan Askarov, and Stephen Chong here at Harvard.)

Cheers,
Scott Moore

On Oct 28, 2013, at 4:17 PM, Tom Van Cutsem <[email protected]> wrote:

> Hi James,
> 
> 2013/10/19 James Noble <[email protected]>
> there's an older paper on dynamic ownership here - http://dl.acm.org/citation.cfm?id=1297090 & attached.
> 
> Thanks for the reference. I was aware of this work, it's also cited by Wernli's DLS2012 paper.
> 
> One thing that's still different from a membrane-based approach to implementing ownership, is that your work on dynamic ownership (and also Wernli's work on Filters), augments objects with explicit ownership pointers, and adds runtime checks on all method calls to verify ownership.
> 
> What I'm considering with membranes is to define ownership *implicitly*: all objects wrapped by the same membrane would be considered "owned" by the same owner. Then, instead of intercepting all method calls to perform runtime ownership checks, only the proxies at the boundary of the membrane would perform the ownership checks.
> 
> Now, this approach is really only viable in an ocap language, because membranes can easily be circumvented when there is global shared mutable state.
> 
> I've implemented a first prototype of membrane-based ownership in JavaScript (extensive README available here <https://github.com/tvcutsem/harmony-reflect/tree/master/examples/ownership>). It's based on Wernli's ideas of filters, but implemented using membranes and proxies rather than by augmenting objects with ownership pointers (the latter would require either changing the VM or doing a full source-to-source translation).
>  
> I think the question of where & how ownership ("property rights") should be enforced is an interesting one.
> Patterns like being careful about private or protected names can give effect to ownership in Java;
> in Javascript, nested lambda scopes can protect names --- but you'll need another (static?) analysis
> to ensure that objects that are intended to be confined are not leaked out.
> (see eg. here: http://dx.doi.org/10.1145/949343.949339, http://www.cs.tau.ac.il/~msagiv/courses/encapsulate/p82-vitek.pdf)
> 
> But in terms of capturing programmer's intention ---- audibility ---
> being able to say "this engine is mine", and being sure that gives rise to
> some dependable semantics, is going to be safer than depending on rather
> fiddly programming patterns.
> 
> Agreed!
> 
> Even with support for ownership (static or dynamic), there is still a danger that the programmer forgets to express the right ownership boundaries, but at least having a language abstraction to express the ownership boundaries is a step in the right direction.
> 
> Regards,
> Tom
> _______________________________________________
> e-lang mailing list
> [email protected]
> http://www.eros-os.org/mailman/listinfo/e-lang