Lightweight Static Capabilities

Lightweight Static Capabilitites

We describe a modular programming style that harnesses modern type systems to verify safety conditions in practical systems. This style has three ingredients:

  1. A compact kernel of trust that is specific to the problem domain.
  2. Unique names (capabilities) that confer rights and certify properties, so as to extend the trust from the kernel to the rest of the application.
  3. Static (type) proxies for dynamic values.

We illustrate our approach using examples from the dependent-type literature, but our programs are written in Haskell and OCaml today, so our techniques are compatible with imperative code, native mutable arrays, and general recursion. The three ingredients of this programming style call for (1) an expressive core language, (2) higher-rank polymorphism, and (3) phantom types.

Pursuant to this thread about the membrane pattern in static languages from Mark Miller's excellent Ph.D. thesis. I don't yet know whether a solution is derivable from this work, but Mark was kind enough to point me to it, and Oleg seems to want to see it distributed, so here it is—Mark and/or Oleg, please let me know if this is premature.

Comment viewing options

Select your preferred way to display the comments and click "Save settings" to activate your changes.

Ah, I've been looking for

Ah, I've been looking for work like this. Thanks!

I'm pretty clueless about the best approach to security for a statically typed functional language. Oz-E holds some answers on the functional side I think. The techniques used by FlowCaml and in this paper might be a good start, but they seem very imprecise compared to the fine grained control over capabilities E gives you. Effect systems are probably quite closely related to security issues, and could help with this.

My Head...

...is very much in the question of how to do object-capability security a là E in a sufficiently expressive statically-typed language these days. My dream language would be something like a capability-secure Acute, except with syntax that won't scare C++/Java/C# programmers away. This is why I'm so interested in Tim Sweeney's work and so curious as to how he might be addressing security in it, since he made no mention of security in his "The Next Mainstream Programming Language" presentation. Tim, any comments? :-)

Statically typed E

It's possible to have a "statically typed E" right now given this appropriate type system for first-class messages:

http://www.eros-os.org/pipermail/e-lang/2005-June/010711.html

That would be a worthy experiment

I think that's plausible. But I also doubt it's an obvious or trivial undertaking[*]. It'd be especially cool if such an efforts also tried to fold in insights from Oleg and Shan's "Lightweight Static Capabilities". If anyone would like to try defining such a language, I'd be happy to help.

[*]In particular, AFAICT, the type system described in Shroff and Smith's Type Inference for First-Class Messages with Match-Functions, either by itself or in combination with Lightweight Static Capabilities, is still not be expressive enough to allow the membrane pattern.

(Not that I actually understand either one. I'm still a lightweight when it comes to type theory formalisms.)

Let's Do It

I'm keenly interested in attempting to implement the membrane pattern as widely as possible. My short list of targets would be:

  • MetaOCaml
  • O'Caml leveraging "Lightweight Static Capabilities"
  • Scala, either via metaprogramming or the moral equivalent of "Lightweight Static Capabilitites"
  • Haskell, presumably leveraging "Lightweight Static Capabilities"
  • Oz, in the guise of Oz-E

It seems to me extremely fortuitous that we have Mark Miller, Oleg Kiselyov, Peter Van Roy, and many other folks who, while not the authors of the systems and/or papers in question, are nevertheless expert in the use of programming languages to solve such thorny problems here on LtU. Can we somehow make a cross-language LtU project of this—kind of our own ICFP challenge? I think we'll learn a tremendous amount about the relationship among metaprogramming, static typing, and dynamic typing, as well as increasing the community's understanding of object-capability security, and even winding up with multiple implementations of some core technology. I literally can't think of anything else I'd rather be doing right now. Is anyone else interested?

Mark, FWIW, a year ago I was in your shoes. Let me highly recommend working through Pierce's "Types and Programming Languages," referenced on the Getting Started thread along with many other excellent recommendations. TAPL absolutely accomplished a 180° shift in my understanding of types and their relationship to programming, with LtU itself playing an invaluable supporting role. The next head-expander I recommend might be Coq'Art. It's extremely formal (naturally; it's about theorem proving, after all) but surprisingly accessible, even playful in places. Highly recommended, especially since you can (and should, IMHO) download the version of Coq used in the text and get your hands dirty.

Is it legit to have

Is it legit to have functions that yield messages (with a phantom type used to check who it's OK to send the message to) which can then be sent with the expectation of yielding a result? I'd probably end up implementing the object model along similar lines in Haskell.

Sign me up

> Is anyone else interested?

Sign me up. Marc Stiegler and I (mostly Marc) are also working on Emily - essentially the subset of O'Caml language which does not violate object-capability safety. For example, Emily has no mutable static variables. All variables at the top level of a module - all per module values - may only be transitively immutable. Likewise, modules that provide ambient authority for accessing the world outside the program, like opening a file, must be suppressed.

The Emily implementation is essentially O'Caml with an extra verifier in front of it, to ensure that submitted programs use only the object-capability-safe subset of O'Caml. I'm interested in understanding the relationship between the dynamic object-capabilities of Emily and the static capabilities of Oleg and Shan's paper. In any case, everywhere you say "O'Caml" in your list, I'm hoping to say "Emily" instead.

> Let me highly recommend working through Pierce's "Types and Programming Languages" [TAPL]

I have made it about half way through Pierce's TAPL, and it is indeed excellent. However, until recently, I've been quite skeptical of the value of static type systems, for reasons explained in my thesis. (See especially section 26.4 on SCOLL.) This skepticism is also reflected in the E design, which has only dynamic type safety and soft typing. Now that Oleg has explained to me some of the magic expressible with static type systems, I'll go back and try to complete Pierce's TAPL. Thanks.

Skepticism

Skepticism is good; it's the vital engine that drives Popperian scientific philosophy. "Let's Do It!" is my rallying cry to respond to the challenge and see if some of the loose ends that seem to be so tantalizingly close to each other can in fact be tied together. There are some initial solutions in the increasingly-misnamed "Advantages of Soft Typing" thread that I hope you have the opportunity to examine. This is exciting stuff!

Membrance pattern

In particular, AFAICT, the type system described in Shroff and Smith's Type Inference for First-Class Messages with Match-Functions, either by itself or in combination with Lightweight Static Capabilities, is still not be expressive enough to allow the membrane pattern.

Can a membrane be built on transparent forwarding? If so, then I believe the theory in the cited paper is sufficient. Assuming I have this right, at most you simply wrap each argument of a message in a transparent forwarder. That forwarder then wraps everything returned via itself in another such forwarder (whether it's pure data, or it carries authority). IIRC, the destruction of a membrane invalidates all capabilities passed through it, thus, each forwarder requires at most a reference to the base forwarder (membrane) to ensure its validity. This is like a "viral Caretaker" pattern. I think that would work, but I haven't completely thought through all the implications.

Can a membrane be built on

Can a membrane be built on transparent forwarding?

By this I meant "transparent, revocable forwarders" of course.

What about arguments?

For any tuple, (a, b), the call (wrap (a, b)) must yield the tuple (wrap(a), wrap(b)). Similarly, and especially if we're using polymorphic variants as messages, then (wrap (`MsgName a b)) must yield (`MsgName wrap(a) wrap(b)). In order to do this, we'd need to, for example, iterate over a tuple as a heterogenous list. How would one do that?

match-functions vs GADTs

Btw, what's the relationship is between match-functions and GADTs? Given GADTs, can one express Shroff and Smith's match-functions directly?

Polymorphic variants seem

Polymorphic variants seem essential to allow different objects to accept different sets of message.

GADTs can provide the limited dependent typing needed, but you would need to provide a witness to the mapping between message type and result type somehow. I think passing around witnesses directly would be basically equivalent to hardcoding the result type into the types of first class messages. If you're willing to do that, Daan Leijen's work in First-class labels for extensible rows can provide the polymorphism.

The mapping from label + argument types to result type could probably be computed with the type functions from Sheard's Omega, or the interaction between fancy type classes and GADTs proposed in A Framework for Extended Algebraic Data Types.

I'm dubious about doing it with (current) GHC Haskell, but I think a satisfactory implementation in Omega might be possible.

match-functions vs GADTs

GADTs do appear to be isomorphic to match-types (the type equivalent of match-functions). However, the key difference seems to be that type inference of GADTs, as presented in paper titled "Simple Unification-based Type Inference for GADTs", relies significantly on programmer annotations as opposed to match-types which can be inferred without any programmer declarations. However, the closure algorithm for the type inference of match-functions is constraint based, that is, the type inference results in a set of constraints. The simplification of this constraint set to generate a human readable type (as given by say the Caml top loop) is non-trivial.

The type inference algorithm presented by Simon Peyton Jones in the above mentioned paper might be a practical solution for incorporating first-class messages in existing languages.

Top down vs bottom up proof engineering

I think one of the most fascinating aspects of Oleg and Shan's Lightweight Static Capabilities is that they enable piecemeal proofs of correctness to be organized top down rather than bottom up.

Rather than working upwards only from the semantics of the base system, which rarely gets us very far, we can instead proceed to make assumptions (postponed proof obligations) that match the natural structure of our program: Assuming that the exported operations of component X correctly provide semantics Y, then prove various properties of X's clients by standing on Y's semantics. This way of organizing piecemeal formal reasoning seems a better match for the way good object programmers informally use encapsulation to organize assumptions. Even if we never get around to discharging most of these proof obligations, we could substantially raise our confidence in many aspects of our programs.

For most components, for the foreseeable future, the definitive statement of the component's spec will remain the component itself. For proof technology to contribute to our confidence in realistic large messy programs, some way must be found to specify and prove a few useful properties of crucial fragments, where these fragments are embedded within systems that are largely unproven and unspecified. I think Oleg and Shan's paper points in a good direction.

*Bump* -- what about proving

*Bump* -- what about proving membranes correct via something like Jeff Foster's 'security via type qualifiers' work?

I've been playing with a few proof strategies tonight, and it seems viable.