Capabilities interact nicely with Substructural Types and Reactivity

I've recently been designing capabilities into my reactive demand
programming (RDP) language, Awelon. RDP has several differences from
traditional OOP. Two of these differences are:

* instead of message passing I have continuous signals,
* instead of stateful objects I have stateless behaviors that may infuence
and observe external state.

But the basic ideas of capability security still fit. In many ways, they
even fit *better* for RDP than they do for OOP. For example, because I
grant authority through a continuous signal instead of fire-and-forget
messaging, I get uniform revocation (simply stop granting the authority)
and a great deal more visibility for which authorities I've granted. I also
can update those authorities at any time - e.g. to constrain or audit them.
(Update is greatly simplified by keeping state external.)

Due to fire-and-forget messaging and internal state, OOP systems require
foresight, discipline, and design to get similar advantages.

Awelon augments RDP with substructural types. A block in Awelon is normally
'used' when you apply it, so you must copy it first if you want to use it
more than once. Any block can be marked 'noCopy' or 'noDrop', corresponding
to affine types and relevant types, and any composition of blocks will
inherit the properties of the components. If both attributes are applied,
you have a linear type. I believe substructural types are a very
significant boon for modeling robust, compositional security, and are quite
easy to enforce with respect to integrating untrusted code with an
application.

Affine Types first:

OOP assumes an *ambient authority* to create unique objects, and to create
state that is initially exclusive (which is useful to control
communication, and for implementation hiding). These authorities are useful
for expressiveness. But  they can be problematic from certain security
perspectives - e.g. when integrating untrusted code, it can be difficult to
enforce deterministic behavior or certain forms of confinement.

RDP does not have this ambient authority, but consequently lacks the
expressiveness. To cover this gap, I introduced a notion of an affine-typed
uniqueness source - basically a *capability* to create initially unique
values. These unique values can include: initially exclusive bindings to
state, unique unique sealer/unsealer pairs, new GUIDs. (That's it, at the
moment.) After these unique objects have been created, they often can be
copied and distributed. There may be exceptions for some state models, for
which substructural types can usefully enforce exclusive-writer or
master-writer relationships.

Now, I'm still not creating 'new' state; rather, the unique value
represents an "exclusive binding" to external state, like a unique filename
or a unique key in a database. This has many nice properties: we still get
the encapsulation, flow control, and implementation-hiding advantages of
OOP. Exclusive binding to external state also has advantages for secure
reflection, introspection, and auditing. Only the 'parent' has the ability
to see what a subprogram is using, thus we can still integrate mutually
distrustful code (by modeling said code in a sibling relationship,
potentially a networked model, instead of parent/child relationship).  But
the parent is free to observe and audit how a subprogram uses state
internally.

If we stabilize the unique identifier against a variety of source-code
changes, we also get a very natural basis for orthogonal persistence that
will be robust to code update or live programming. To stabilize uniqueness
source, I map unique values onto a filesystem-like path. Programmers can
"split" the unique source, creating a child with a given text name, and a
parent that cannot again use that name. The child is then passed on to the
reusable subprogram, while the parent is held for further use. Obtaining a
unique value will also require text which cannot be reused. Unlike simple
left/right splits, this tree-structured uniqueness is very robust to
reorganizing code or adding new subprograms upstream.

(I've discussed the virtues of tree-structured state in cap-talk before,
but I cannot find the conversation.)

Affine types are also very useful for modeling limited resources, or
controlling fan-in on a limited resource.


Relevant Types next:

"With great power comes great responsibility," - Stan Lee, Voltaire, and
others.

A "relevant type" is a type that cannot be dropped. In context of OOP, a
'relevant object' would be one that absolutely requires a message. And...
if it doesn't like the message, it might return a new 'relevant object' so
you're forced to try again. Relevant types are very effective for modeling
responsibilities.

Modeling responsibility seems very useful for security purposes. We can
enforce that promises are resolved, that handshakes or protocols are
completed, that continuations are continued. We can ensure that, no matter
how untrustworthy a particular subprogram might be, that at least it does
its job. Responsibility and an authority can be tightly coupled: a
capability that must be used, perhaps one that requires a sealed value to
prove certain dataflows are involved.

Responsibilities are subject to similar rules as capabilities: they can be
created, delegated, and received with a message. If some nefarious
subprogram attempts to foist its responsibilities onto an unwilling object,
it can simply be returned, or prevented by the type system.

Linear types have both properties: in many cases, responsibilities are
"once and only once" - e.g. for promises, handshakes, trade protocols.

Naturally, there are some limits on how well we can enforce substructural
types an open network. But it can work very well in certain conditions:

* when executing untrusted code locally
* interactions modeled through a mutually trusted third party

OOP has some ability to model 'affine' types by using state to rejecting
all messages after the first one. But OOP has much more difficulty modeling
responsibilities without support of a type system. I think this would be a
worthy investment in many capability languages.


(I've also included the message to my RDP group, which says some of the
same things but with different emphasis.)

---------- Forwarded message ----------
From: David Barbour <[email protected]>
Date: Wed, Sep 11, 2013 at 12:04 AM
Subject: Capability Security in Awelon
To: reactive-demand-/[email protected]

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.

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