Capability Security in Awelon

[David Barbour]

One of my goals for RDP has always been to support object capability security patterns. If you aren't familiar with object capability model, I suggest the following reading [1][2]:

[1] http://erights.org/elib/capability/ode/ode-capabilities.html

[2] http://wiki.erights.org/wiki/Walnut/Secure_Distributed_Computing/Capability_Patterns

In RDP, capabilities are modeled with RDP behaviors. Some behaviors enable programmers to observe sensors, influence actuators, query or control databases. In accordance with capability security model, an *explict act of granting* a behavior should be necessary for a subprogram to utilize it. 

RDP is designed with an assumption of dynamic behaviors. Use-cases include runtime resource discovery, linking, and service brokering. A common technique for dynamic behaviors is to *publish* dynamic behaviors to a shared space (basically, announcing or advertising one's services). The shared space may be varying degrees of public or private. RDP is designed to be metacircular and staged: applications can always be considered dynamic behaviors in a larger application. 

Due to its continuous, reactive communication model, RDP has a significant advantage for capability security relative to OOP or Actors model: 

* the granting of authority is continuously visible

* to stop granting represents implicit revocation

* transition to updated behavior is transparent

Transition is transparent  because RDP forbids internal state, i.e. a capability can access external stateful resources (such as a file or database) but cannot itself contain state. For security purposes, transparent transition is useful for latent auditing or management. (Transition is also useful for failovers, runtime upgrade, live programming, debugging, and forward security.) Altogether, RDP provides uniform models for visibility, revocability, auditing, and control, effectively addressing several of Ka-Ping Yee's principles for Secure Interaction Design. With actors or OOP, similar solutions require discipline and up-front design. 

With regards to security, Awelon improves on RDP's model in many ways.

* Awelon supports static dataflows containing behaviors

* Awelon supports affine types to model exclusivity

* unique sealer/unsealer pairs can be constructed

* state resources can be exclusively bound to subprograms

* Awelon supports relevant types to model responsibility

* Awelon has heterogeneous partitions with distinct resources

* Dataflow between partitions can be asymmetric

In Awelon, behaviors-as-values are simply called 'blocks'. Blocks are syntactically represented with square brackets, such as [swap] or [add]. The words within a block describe a behavior, but the description becomes a static value on the current stack. Blocks can be statically (at compile-time) applied to all or part of the environment, depending on which combinator word is used.  Any block may arbitrarily be marked 'noCopy' (affine type) or 'noDrop' (relevant type) - a block marked with both attributes is effectively linear. Blocks may be composed, and the composite will inherit the substructural types of both inputs.

Blocks are not closures. They cannot capture signals. The 'no capture' limitation is important for safe, simple interaction of blocks with (x + y) sum types or dynamic behaviors. The 'no capture' limitation is mitigated by ability to lift static values to behaviors taking unit signal. Also, there are many ways to indirectly model objects that capture signals, e.g. by coupling a block with a signal, possibly sealing them together. 

Syntactically defined blocks in Awelon lack authority. This is the "no ambient authority" rule of capability security. 

A MISTAKE AVOIDED: I had been waffling on whether or not to support ambient authority. An idea I had was to leverage partition types: some partitions would support ambient authority, but would be associated with logical 'sandbox' partitions that require capabilities. Capabilities used in the sandbox partition leverage ambient authority. This design has some advantages: ambient authorities are somewhat simpler to standardize, optimize, integrate, and compile, and it's a close match to how many capability systems are actually constructed. But, in pseudocode, I found it difficult to distinguish which blocks are capabilities, or even define what it means to use a capability "in" a partition if static inputs or applications are involved. Capabilities have advantages of being more expressive, compositional, and work better with Awelon's staged programming model.

Capabilities are provided through a 'powerblock'. All authority in an application originates from the powerblock.

Every application receives two main inputs: 

* the 'go' signal, a runtime unit signal that controls application activity

* the powerblock, an affine static block that provides capabilities and authority

The powerblock is primarily used statically to obtain authority: e.g. if a developer wants access to a mouse signal, they might build some static text like "mouse" apply the powerblock to this. The powerblock would then return the mouse capability... along with an updated powerblock. There will also be ways to wrap the authority (pre-mouse, post-mouse). Basically, this models a 'powerbox' pattern, though without any built-in support for dynamic negotiations. (It seems feasible to build in such patterns, e.g. returning capabilities that use some provider-controlled state to decide their actual behavior.)  

The powerblock cannot be copied, but it can be 'split' into a child and parent. 

The powerblock doubles as the uniqueness source in Awelon, which enables sealer/unsealer pairs and exclusive binding to state. For state - in context of live programming, continuous deployment, or orthogonal persistence - it is very important that identity be stable across source-code changes. To achieve this stability each child must be given a unique text name. In general, the child block will be passed to a subprogram, while the parent is kept. A developer can control which authorities a subprogram will be granted. A powerbox may be constrained after it is formed - blacklisting or whitelisting authorities, potentially setting a 'security level' on a child powerblock (the meaning of which would be determined by de-facto standardization). Importantly, a child powerblock can also be molded *before* it is formed. (This sort of deep override is very useful for extensible systems.) A developer can build up a set of actions to perform on a child just after it is created. 

Sealer/unsealer pairs are very useful for modeling ADTs or objects. They may also be used to suggest points for extra encryption, though sealer/unsealers are mostly a compile-time phenomenon, used to control introspection and enforce some useful forms of type safety.

Exclusive binding to state was not a feature initially envisioned for RDP, but is made available due to substructural types. By nature, state is always 'external' to an RDP behavior. Resources are stateful, and that state can be observed and influenced, but RDP behaviors themselves are not stateful. But exclusive binding to state enables external state to effectively be encapsulated; with it, RDP can model objects and software agents that can be considered to "contain" state or define their own state models. 

Unlike local state, exclusive binding to external state does not hinder persistence or update. Also, extension can be supported, e.g. by read-only observers, or enabling more limited write-access to all but the observer.

The use of 'noDrop' on a block has a very interesting impact: the block becomes a literal "responsibility" - it must be applied to some form of signal, a 'response'. Combined with type safety, this can be a very powerful basis for certain security problems, i.e. responsibilities of many software components can be enforced. (Usefully: even if you don't trust a component, you can enforce that it at least does part of its job.) I tongue-in-cheek call this the "Stan Lee's principle for security: authority should be tightly coupled to responsibility."  Though, I don't have any default responsibilities for applications.

Dynamic behaviors in Awelon are achieved by lowering a static block into the runtime - i.e. by mapping the block to a runtime unit signal. Within a runtime signal, blocks can interact with other runtime signals - e.g. in terms of composition, or lifting values within a signal as though they were static. While any block can be lowered, dynamic behaviors have very severe constraints on where they can actually be 'evaluated', i.e. all the input signals must be in one partition (modulo static inputs), and there are also constraints on the output types. But despite the limitations,  dynamic behaviors have a wide number of use-cases.

This leaves two challenges: (1) securing capabilities, (2) compiling with capabilities.

Securing capabilities is an issue because we have capabilities going out to shared spaces - potentially shared with independently developed RDP applications - then returning for application. I can think of a few ways to secure capabilities that are distributed this way: HMAC, PKI, or just mapping them to a GUID. Occasionally, these capabilities might be updated, for forward security reasons, but that could be achieved through the reactive model. I haven't worked out all the details, but I think it won't be a problem.

Compiling with capabilities is more an issue. Somehow, the compiler needs to know enough to provide the powerbox, which really requires some de-facto standardization if nothing else. Maybe each compiler should have an Awelon module that describes its initial powerbox; this could be very useful for type checking.