Capabilities: Effects for Free

Abstract

Object capabilities are increasingly used to reason informally about the properties of secure systems. But can capabilities also aid in formal reasoning? To answer this question, we examine a calculus that uses effects to capture resource use and extend it to support capability-based reasoning. We demonstrate that capabilities provide a way to reason about effects: we can bound the effects of an expression based on the capabilities to which it has access. This reasoning is “free” in that it relies only on type-checking (not effect-checking), does not require the programmer to add effect annotations within the expression, and does not require the expression to be analysed for its effects. Our result sheds light on the essence of what capabilities provide and suggests ways of integrating lightweight capability-based reasoning into languages.

1 Introduction

Capabilities have been recently gaining attention as a promising mechanism for controlling access to resources, particularly in object-oriented languages and systems [4,5,6, 16]. A capability is an unforgeable token that can be used by its bearer to perform some operation on a resource [3]. In a capability-safe language, all resources must be accessed through object capabilities, and a resource-access capability must be obtained from an object that already has it: “only connectivity begets connectivity” [16]. For example, a $\mathtt {logger}$ component that provides a logging service would need to be initialised with an object capability providing the ability to append to the log file.

Capability-safe languages prohibit the ambient authority [17] that is present in non-capability-safe languages. An implementation of a $\mathtt {logger}$ in Java, for example, does not need to be initialised with a log file capability, as it can simply import the appropriate file-access library and open the log file for appending by itself. But critically, a malicious implementation could also delete the log, read from another file, or exfiltrate logging information over the network. Other mechanisms such as sandboxing can be used to limit the damage of such malicious components, but recent work has found that Java’s sandbox (for instance) is difficult to use and therefore often misused [1, 11].

In practice, reasoning about resource use in capability-based systems is mostly done informally. But if capabilities are useful for informal reasoning, shouldn’t they also aid in formal reasoning? Recent work by Drossopoulou et al. [6] sheds some light on this question by presenting a logic that formalizes capability-based reasoning about trust between objects. Two other trains of work, rather than formalise capability-based reasoning itself, reason about how capabilities may be used: Dimoulas et al. [5] developed a formalism for reasoning about which components may use a capability and which may influence (perhaps indirectly) the use of a capability, while Devriese et al. [4] formulate an effect parametricity theorem that limits the effects of an object based on the capabilities it possesses, and then use logical relations to reason about capability use in higher-order settings. Overall, this prior work presents new formal systems for reasoning about capability use, or reasoning about new properties using capabilities.

We are interested in a different question: can capabilities be used to enhance formal reasoning that is currently done without relying on capabilities? In other words, what value do capabilities add to existing formal reasoning approaches?

To answer this question, we decided to pick a simple and practical formal reasoning system, and see if capability-based reasoning could help. A natural choice for our investigation is effect systems [18]. Effect systems are a relatively simple formal reasoning approach, which augment type systems with the ability to reason about dynamic effects—and keeping things simple will help to highlight the difference made by capabilities. Effects also have an intuitive link to capabilities: in a system that uses capabilities to protect resources, an expression can only have an effect on a resource if it is given a capability to do so.

One challenge to the wider adoption of effect systems is their annotation overhead [19]. For example, Java’s checked exception system, which is a kind of effect system, is often criticised for being cumbersome [8]. While effect inference can be used to reduce the annotations required [9], understanding error messages that arise through effect inference requires a detailed understanding of the internal structure of the code, not just its interface. Capabilities are a promising alternative for reducing the overhead of effect annotations, as suggested by the following example:

Fig. 1.

Declaring an effect

Our examples are written in a capability-safe language supporting first-class, object-like modules, similar to Wyvern [14], in which expressions declare what capabilities they need to execute. In this case, an expression $\mathtt {e}$ must be passed a function of type $\mathtt {String \rightarrow Unit}$,¹ which incurs no more than the effect $\mathtt {File.write}$ when invoked. This function is bound to the name $\mathtt {log}$ inside $\mathtt {e}$.

What can we say about the effects that evaluating $\mathtt {e}$ will have on resources, such as the file system or network? Because we are in a capability-safe language, $\mathtt {e}$ has no ambient authority, so the only way it could have any effects is via the $\mathtt {log}$ function given to it. Since the $\mathtt {log}$ function is annotated as having no more than the $\mathtt {File.write}$ effect, this is an upper-bound on the effects of $\mathtt {e}$. Note we only required that $\mathtt {e}$ obeys the rules of capability safety. We did not require it to have effect annotations, and we didn’t analyse its structure, as an effect inference would. Also note that $\mathtt {e}$ might be arbitrarily large, perhaps consisting of an entire program we have downloaded from a source we trust enough to write to a log, but not enough to access any other resources. Thus in this scenario, capabilities can be used to reason “for free” about the effects of a large body of code ($\mathtt {e}$), based on a few annotations on the components it imports ($\mathtt {log}$).

This example illustrates the central intuition of this paper: in a capability-safe setting, the effects of an unannotated expression can be bounded by the effects latent in the variables that are in scope. In the remainder of this paper, we formalise these ideas in a capability calculus ($\mathtt {CC}$; Sect. 2). Along the way we must generalise this intuition: what if $\mathtt {log}$ takes a higher-order argument? If $\mathtt {e}$ evaluates, not to $\mathtt {unit}$, but to a function, what can we say about its effects? We then show how $\mathtt {CC}$ can model practical situations by encoding a range of Wyvern-like programs Sect. 3). A more thorough discussion, including a proof of soundness is given in an accompanying technical report [2].

2 Capability Calculus ($\mathtt {CC}$)

While the current resurgence of interest in capabilities is primarily focused on object-oriented languages, for simplicity our formal definitions build on a typed lambda calculus with a simple notion of capabilities and their operations. $\mathtt {CC}$ permits the nesting of unannotated code inside annotated code in a controlled, capability-safe manner using the $\mathtt {import}$ form from Fig. 1. This allows us to reason about unannotated code by inspecting what capabilities are passed into it from its unannotated surroundings.

Allowing effect-annotated and unannotated code to be mixed helps reduce the cognitive overhead on developers, allowing them to prototype in the unannotated sublanguage and incrementally add annotations as they are needed. Reasoning about unannotated code is difficult in general. Figure 2 demonstrates why: $\mathtt {apply}$ takes a function f as input and executes it, but the effects of f depend on its implementation. Without more information, there is no way to know what effects might be incurred by $\mathtt {apply}$.

Fig. 2.

What effects can $\mathtt {apply}$ incur?

Consider another scenario, where a developer must decide whether or not to use the $\mathtt {logger}$ functor defined in Fig. 3. This functor takes two capabilities as input, $\mathtt {File}$ and $\mathtt {Socket}$.² It instantiates an object-like module that has a single, unannotated $\mathtt {log}$ method with access to these capabilities. The type of this object-like module is $\mathtt {Logger}$, which is assumed to be defined elsewhere.

Fig. 3.

In a capability-safe setting, $\mathtt {logger}$ can only exercise authority over the $\mathtt {File}$ and $\mathtt {Socket}$ capabilities given to it.

How can we determine what effects will be incurred if $\mathtt {Logger.log}$ is invoked? One approach is to manually³ examine its source code, but this is tedious and error-prone. In many real-world situations, the source code may be obfuscated or unavailable. A capability-based argument can do better, since a $\mathtt {Logger}$ can only exercise the authority it is explicitly given. In this case, the $\mathtt {logger}$ functor must be given $\mathtt {File}$ and $\mathtt {Socket}$, so an upper bound on the effects of the $\mathtt {Logger}$ it instantiates will be the set of all operations on those resources, $\mathtt {\{File.*, Socket.*\}}$. Knowing the $\mathtt {Logger}$ could perform arbitrary reads and writes to $\mathtt {File}$, or communicate with $\mathtt {Socket}$, the developer decides this implementation cannot be trusted and does not use it.

To model this situation in $\mathtt {CC}$, we add a new $\mathtt {import}$ expression that selects what authority $\varepsilon _s$ the unannotated code may exercise. In the above example, the expected least authority of $\mathtt {Logger}$ is $\{ \mathtt {File.append} \}$, so that is what the corresponding $\mathtt {import}$ would select. The type system can then check whether the capabilities being passed into the unannotated code exceed $\varepsilon _s$. If it accepts, then $\varepsilon _s$ is a safe upper bound on the effects of the unannotated code. This is the key result: when unannotated code is nested inside annotated code, capability-safety enables us to make a safe inference about its effects by examining what capabilities are being passed in by the annotated code.

2.1 Grammar ($\mathtt {CC}$)

The grammar of $\mathtt {CC}$ has rules for annotated code and analogous rules for unannotated code. To distinguish the two, we put a hat above annotated types, expressions, and contexts. $\hat{e}$, $\hat{\tau }$, and $\hat{\varGamma }$ are annotated, while e, $\tau$, and $\varGamma$ are unannotated. The rules for unannotated programs and their types are given in Fig. 4. Unannotated types $\tau$ are built using $\rightarrow$ and sets of resources $\{ \bar{r} \}$. An unannotated context $\varGamma$ maps variables to unannotated types. The syntax for invoking an operation on a resource is $e.\pi$. Resource literals and operations are drawn from fixed sets R (containing, e.g. $\mathtt {File}$, $\mathtt {Socket}$) and $\Pi$ (containing, e.g. $\mathtt {write}$, $\mathtt {read}$).

Fig. 4.

Unannotated programs and types in $\mathtt {CC}$.

Because our focus is on tracking what effects happen, i.e. whether particular operations are invoked on particular resources, we make the following simplifying assumptions: first, any operation may be called on any resource literal; and second, all operations take no inputs and return $\mathtt {unit}$.

Fig. 5.

Annotated programs and types in $\mathtt {CC}$.

Rules for annotated programs and their types are shown in Fig. 5. The first main difference is that the $\rightarrow _{\varepsilon }$ type constructor has a subscript $\varepsilon$, which is a set of effects that functions of that type may incur. The other main difference is the new expression form, $\mathtt {import}(\varepsilon _s)~x = \hat{e}~\mathtt {in}~ e$, where e is some unannotated code and $\hat{e}$ is a capability being passed to it; we call $\hat{e}$ an import. For simplicity, we assume there is only ever one import. Note the definition not only allows resource literals to be imported, but also effectful functions. Inside e, $\hat{e}$ is bound to the variable x. $\varepsilon _s$ is the maximum authority that e is allowed to exercise (its “selected authority”). For example, suppose an unannotated $\mathtt {Logger}$, which requires $\mathtt {File}$, is expected to only $\mathtt {append}$ to a file, but has an implementation which writes. This would be the expression $\mathtt {import}(\mathtt {File.append})~x = \mathtt {File}~\mathtt {in}~ \lambda y: \mathtt {Unit}.~\mathtt {x.write}$. The $\mathtt {import}$ expression is the only way to mix annotated and unannotated code, because it is the only situation in which we can say something interesting about the effects of unannotated code. For the rest of our discussion of $\mathtt {CC}$, we will only be interested in unannotated code when it is encapsulated by an $\mathtt {import}$ expression.

Capability safety prohibits ambient authority. $\mathtt {CC}$ meets this requirement by forbidding the use of resource literals directly inside an $\mathtt {import}$ expression (though they can still be passed in as a capability via the binding variable x). We could have enforced this syntactically, but we choose to do it using the typing rule for $\mathtt {import}$ in Sect. 2.3.

2.2 Semantics ($\mathtt {CC}$)

The rules for $\mathtt {CC}$ are natural extensions of the simply-typed lambda calculus, so for brevity we only give the rules for $\mathtt {import}$ (see Fig. 6). Reductions are defined on annotated expressions, using the notation $\hat{e} \longrightarrow \hat{e}'~|~ \varepsilon '$, which means that $\hat{e}$ is reduced to $\hat{e}'$ in a single step, incurring the set of effects $\varepsilon '$. To execute the unannotated code inside an $\mathtt {import}$ expression, we recursively annotate its components with the selected authority $\varepsilon _s$. While it is meaningful to execute unannotated code, we only care about it inside $\mathtt {import}$ expressions, so do not bother to give rules for this.

E-Import1 reduces the capability being imported. When it has been reduced to a value $\hat{v}$, E-Import2 annotates e with the selected authority $\varepsilon$—this is $\mathtt {annot}(e, \varepsilon )$—and substitutes the import $\hat{v}$ for its name x in e—this is $[\hat{v}/x]\mathtt {annot}(e, \varepsilon )$.

$\mathtt {annot}(e, \varepsilon )$ is the expression obtained by recursively annotating the parts of e with the set of effects $\varepsilon$. A definition is given in Fig. 7, with versions defined on expressions and types. Later we will need to annotate contexts, so the definition is given here. Note that $\mathtt {annot}$ operates on a purely syntatic level. Nothing prevents us from annotating a program with something unsafe, so any use of $\mathtt {annot}$ must be justified.

Fig. 6.

New single-step reductions in $\mathtt {CC}$.

Fig. 7.

Definition of $\mathtt {annot}$.

2.3 Static Rules ($\mathtt {CC}$)

Terms can be annotated or unannotated, so we need to be able to recognise when either is well-typed. We do not reason about the effects of unannotated code directly, so judgements involving them only ascribe a type to an expression, with the form $\varGamma \vdash e: \tau$. Subtyping judgements have the form $\tau <: \tau$. Because these rules are essentially those of the simply-typed lambda calculus, we do not list them here.

Judgements involving annotated terms have the form $\hat{\varGamma } \vdash \hat{e}: \hat{\tau }~\mathtt {with}~ \varepsilon$, meaning that when $\hat{e}$ is evaluated, it reduces to a value of type $\hat{\tau }$, incurring no more than the effects in $\varepsilon$. Most of the rules are analogous to those of the simply-typed lambda calculus; these ones are given in Fig. 8. Note that the rule for typing an operation call, $\varepsilon$ -OperCall, types the expression as $\mathtt {Unit}$, following our simplifying assumption that all operations return $\mathtt {Unit}$.

Fig. 8.

Type-and-effect and subtyping judgements in $\mathtt {CC}$.

There is one rule left, for typing $\mathtt {import}$. Since it is a complicated rule, we will start with a simplified (but incorrect) version, and spend the rest of the section building up to the final version.

To begin, typing $\mathtt {import}(\varepsilon _s)~x = \hat{e}~\mathtt {in}~ e$ in a context $\hat{\varGamma }$ requires us to know that $\hat{e}$ is well-typed, so we add the premise $\hat{\varGamma } \vdash \hat{e}: \hat{\tau }~\mathtt {with}~ \varepsilon _1$. e is only allowed to use what authority has been explicitly given to it (i.e. the capability $\hat{e}$, bound to x). To ensure this, we require that e can be typechecked using only one binding, $x: \hat{\tau }$, which binds x to the type of the capability being imported. Typing e in this restricted environment means it cannot use any other capabilities, thus prohibiting the exercise of ambient authority.

There is a problem though: e is unannotated, while $\hat{\tau }$ is annotated, and there is no rule for typechecking unannotated code in an annotated context. To get around this, we define a function $\mathtt {erase}$ in Fig. 9, which removes the annotations from a type. We can then add $x: \mathtt {erase}(\hat{\tau }) \vdash e: \tau$ as a premise.

Fig. 9.

Definition of $\mathtt {erase}$.

The first version of $\varepsilon$ -Import is given in Fig. 10. Since $\mathtt {import}(\varepsilon _s)~x = \hat{v}~\mathtt {in}~ e$ reduces to $[\hat{v}/x]\mathtt {annot}(e, \varepsilon _s)$ by E-Import2, its ascribed type is $\mathtt {annot}(\tau , \varepsilon )$, which is the type of the unannotated code e, annotated with its selected authority $\varepsilon _s$. The effects of reducing the $\mathtt {import}$ are $\varepsilon _1 \cup \varepsilon _s$—the former happens when the imported capability is reduced to a value, while the latter happens when the body of the $\mathtt {import}$ expression is annotated and executed.

Fig. 10.

A first (incorrect) rule for type-and-effect checking $\mathtt {import}$ expressions.

This first rule is incomplete, since any capability can be passed to the unannotated code e, even if it has effects that weren’t declared in $\varepsilon _s$. To avoid this, we define a function $\mathtt {effects}$, which collects the set of effects that an (annotated) type captures. For example, $\mathtt {\{File\}}$ captures every operation on $\mathtt {File}$, so $\mathtt {effects}(\{\mathtt {File}\}) = \mathtt {\{File.*\}}$. A first (but not yet correct) definition of this is given in Fig. 11. We then add the premise $\mathtt {effects}(\hat{\tau }) \subseteq \varepsilon _s$, which restricts imported capabilities to only those with effects selected in $\varepsilon _s$. The updated rule for typing $\mathtt {import}$ is given in Fig. 12.

Fig. 11.

A first (incorrect) definition of $\mathtt {effects}$.

Fig. 12.

A second (still incorrect) rule for type-and-effect checking $\mathtt {import}$ expressions.

Fig. 13.

Permitting multiple imports will break $\varepsilon$ -Import2.

There are still issues with this second rule, as the annotations on one import can be broken by another import. To illustrate, consider Fig. 13 where two⁴ capabilities are imported. This program imports a function $\mathtt {go}$ which, when given a $\mathtt {Unit}\rightarrow _{\varnothing } \mathtt {Unit}$ function with no effects, will execute it. The other import is $\mathtt {File}$. The unannotated code creates a $\mathtt {Unit}\rightarrow \mathtt {Unit}$ function which writes to $\mathtt {File}$ and passes it to $\mathtt {go}$, which subsequently incurs $\mathtt {File.write}$.

In the world of annotated code, it is not possible to pass a file-writing function to $\mathtt {go}$, but because the judgement $x: \mathtt {erase}(\hat{\tau }) \vdash e: \tau$ discards the annotations on $\mathtt {go}$, and since the file-writing function has type $\mathtt {unit}\rightarrow \mathtt {unit}$, the unannotated world accepts it. Although the unannotated code is allowed to incur this effect, since its selected authority is $\mathtt {\{File.*\}}$, this nonetheless violates the type signature of $\mathtt {go}$. We want to prevent this.

If $\mathtt {go}$ had the type $\mathtt {Unit}\rightarrow _{\{ \mathtt {File.write} \}} \mathtt {Unit}$, Fig. 13 would be safely rejected. However, a modified program where a file-reading function is passed to $\mathtt {go}$ would have the same issue. $\mathtt {go}$ is only safe when it expects every effect that the unannotated code might pass to it. To ensure this is the case, we shall require imported capabilities to have the authority to incur every effect in $\varepsilon _s$. To achieve greater control in how we say this, we split the definitions of $\mathtt {effects}$ into two separate functions, $\mathtt {effects}$ and $\mathtt {ho \hbox {-}effects}$. The latter is for higher-order effects, which are those effects not captured directly in the function body, but rather are possible because of what is passed into the function as an argument. If values of $\hat{\tau }$ possess a capability that can be used to incur the effect $r.\pi$, then $r.\pi \in \mathtt {effects}(\hat{\tau })$. If values of $\hat{\tau }$ can incur $r.\pi$, but need to be given the capability (as a function argument) by someone else to do so, then $r.\pi \in \mathtt {ho \hbox {-}effects}(\hat{\tau })$. Definitions are given in Fig. 14.

Fig. 14.

Effect functions (corrected).

Both $\mathtt {effects}$ and $\mathtt {ho \hbox {-}effects}$ are mutually recursive, with base cases for resource types. Any effect can be directly incurred by a resource on itself, hence $\mathtt {effects}(\{ \bar{r} \}) = \{ r.\pi \mid r \in \bar{r}, \pi \in \varPi \}$. A resource cannot be used to indirectly invoke some other effect, so $\mathtt {ho \hbox {-}effects}(\{ \bar{r} \}) = \varnothing$. The mutual recursion echoes the subtyping rule for functions: recall that functions are contravariant in their input type and covariant in their output; likewise, both functions recurse on the input-type using the other function, and recurse on the output-type using the same function.

In light of these new definitions, we still require $\mathtt {effects}(\hat{\tau }) \subseteq \varepsilon _s$—unannotated code must select any effect its capabilities can incur—but we add a new premise $\varepsilon _s \subseteq \mathtt {ho \hbox {-}effects}(\hat{\tau })$, which requires any higher-order effect of the imported capabilities to be declared in $\varepsilon _s$. Put another way, the imported capabilities must be expecting every effect they could be given by the unannotated code (which is at most $\varepsilon _s$). The counterexample from Fig. 13 is now rejected, because $\mathtt {ho \hbox {-}effects}((\mathtt {Unit}\rightarrow _{\varnothing } \mathtt {Unit}) \rightarrow _{\varnothing } \mathtt {Unit}) = \varnothing$, but $\mathtt {effects}(\mathtt {File}) = \{ \mathtt {File.*} \} \not \subseteq \varnothing$.

This is still not sufficient! Consider $\varepsilon _s \subseteq \mathtt {ho \hbox {-}effects}( \hat{\tau }_1 \rightarrow _{\varepsilon '} \hat{\tau }_2 )$. Expanding the definition of $\mathtt {ho \hbox {-}effects}$, this is the same as $\varepsilon _s \subseteq \mathtt {effects}(\hat{\tau }_1) \cup \mathtt {ho \hbox {-}effects}(\hat{\tau }_2)$. Let $r.\pi \in \varepsilon _s$ and suppose $r.\pi \in \mathtt {effects}(\hat{\tau }_1)$, but $r.\pi \notin \mathtt {ho \hbox {-}effects}(\hat{\tau }_2)$. Then $\varepsilon _s \subseteq \mathtt {effects}(\hat{\tau }_1) \cup \mathtt {ho \hbox {-}effects}(\hat{\tau }_2)$ is still true, but $\hat{\tau }_2$ is not expecting $r.\pi$. If $\hat{\tau }_2$ is a function, unannotated code could violate its annotations by passing it a capability for $r.\pi$, even though $r.\pi$ is not a higher-order effect of $\hat{\tau }_2$.

The cause of this issue is that $\subseteq$ does not distribute over $\cup$. We want a relation like $\varepsilon _s \subseteq \mathtt {effects}(\hat{\tau }_1) \cup \mathtt {ho \hbox {-}effects}(\hat{\tau }_2)$, which also implies $\varepsilon _s \subseteq \mathtt {effects}(\hat{\tau }_1)$ and $\varepsilon _s \subseteq \mathtt {effects}(\hat{\tau }_2)$. Figure 15 defines this: $\mathtt {safe}$ is a distributive version of $\varepsilon _s \subseteq \mathtt {effects}(\hat{\tau })$ and $\mathtt {ho \hbox {-}safe}$ is a distributive version of $\varepsilon _s \subseteq \mathtt {ho \hbox {-}effects}(\hat{\tau })$. An amended version of $\varepsilon$ -Import is given in Fig. 16, with a new premise $\mathtt {ho \hbox {-}safe}(\hat{\tau }, \varepsilon _s)$, capturing the notion that imported capabilities must be expecting the effects they could be passed by the unannotated code (which is at most $\varepsilon _s$).

Fig. 15.

Safety judgements in $\mathtt {CC}$.

Fig. 16.

A third (still incorrect) rule for type-and-effect checking $\mathtt {import}$ expressions.

The premises so far restrict what authority can be selected by unannotated code, but consider the example $\hat{e} = \mathtt {import}(\varnothing )~x = \mathtt {unit}~\mathtt {in}~ \lambda f: { \mathtt {File}}.~\mathtt {f.write}$. The unannotated code selects no capabilities and returns a function which takes $\mathtt {File}$ and incurs $\mathtt {File.write}$. This satisfies the premises in $\varepsilon$ -Import3, but its type would be the pure function $\{ \mathtt {File}\} \rightarrow _{\varnothing } \mathtt {Unit}$.

Speaking more generally, suppose the unannotated code evaluates to a function of type f, which is annotated to $\mathtt {annot}(f, \varepsilon _s)$. Suppose $\mathtt {annot}(f, \varepsilon _s)$ is invoked at a later point, back in the annotated world, incurring $r.\pi$. What is the source of $r.\pi$? If $r.\pi$ was selected by the $\mathtt {import}$ expression surrounding f, it is safe for $\mathtt {annot}(f, \varepsilon _s)$ to incur this effect. Otherwise, $\mathtt {annot}(f, \varepsilon _s)$ may have been passed, as an argument, a capability to do $r.\pi$, in which case $r.\pi$ is a higher-order effect of $\mathtt {annot}(f, \varepsilon _s)$. If the argument is a function, then $r.\pi \in \varepsilon _s$ by the soundness of our calculus. But if the argument is a resource literal r, then $\mathtt {annot}(f, \varepsilon _s)$ could exercise $r.\pi$ without declaring it in $\varepsilon _s$—this we do not yet account for.

To make $\varepsilon _s$ contain every effect captured by resources passed into $\mathtt {annot}(f, \varepsilon _s)$ as arguments, we inspect f for resource types. For example, if the unannotated code evaluates to a function of type $\mathtt { \{ File \} \rightarrow \mathtt {Unit}}$, we need $\mathtt { \{ File.* \} } \in \varepsilon _s$. To do this, we add a new premise $\mathtt {ho \hbox {-}effects}(\mathtt {annot}(\tau , \varnothing )) \subseteq \varepsilon _s$. Because $\mathtt {ho \hbox {-}effects}$ is only defined on annotated types, we first annotate $\tau$ with $\varnothing$, and since we are only inspecting the resources passed into f as arguments, our choice of annotation doesn’t matter.

Now we can handle the example from before. The unannotated code types via the judgement $x: \mathtt {Unit}\vdash \lambda f: \{ \mathtt {File}\}.~\mathtt {f.write}: \{ \mathtt {File}\} \rightarrow \mathtt {Unit}$. Its higher-order effects are $\mathtt {ho \hbox {-}effects}(\mathtt {annot}( \{ \mathtt {File}\} \rightarrow \mathtt {Unit}, \varnothing )) = \{ \mathtt {File.*} \}$, but $\{ \mathtt {File.*} \} \not \subseteq \varnothing$, so the example is safely rejected.

The final version of ${\varepsilon }$ -Import is given in Fig. 17. With it, we can now model the example from the beginning of this section, where the $\mathtt {Logger}$ selects the $\mathtt {File}$ capability and exposes an unannotated function $\mathtt {log}$ with type $\mathtt {Unit}\rightarrow \mathtt {Unit}$ and implementation e. The expected least authority of $\mathtt {Logger}$ is $\{ \mathtt {File.append} \}$, so its corresponding $\mathtt {import}$ expression would be $\mathtt {import}(\mathtt {File.append})~f = \mathtt {File}~\mathtt {in}~ \lambda x: \mathtt {Unit}.~e$. The imported capability is $f = \mathtt {File}$, which has type $\{ \mathtt {File} \}$, and $\mathtt {effects}(\{\mathtt {File}\}) = \{ \mathtt {File.*} \} \not \subseteq \{ \mathtt {File.append} \}$, so this example safely rejects: $\mathtt {Logger.log}$ has authority to do anything with $\mathtt {File}$, and its implementation e might be violating its stipulated least authority $\{ \mathtt {File.append} \}$.

Fig. 17.

The final rule for typing imports.

3 Applications

In this section, we examine a number of scenarios to show how capabilities can help developers reason about the effects and behaviour of code. In each story we will discuss some Wyvern code before translating it to $\mathtt {CC}$ and explaining how its rules apply. By doing this, we hope to convince the reader of the benefits of capability-based reasoning, and that $\mathtt {CC}$ captures the intuitive properties of capability-safe languages like Wyvern.

3.1 Unannotated Client

A $\mathtt {logger}$ module, when given $\mathtt {File}$, exposes a $\mathtt {log}$ function which incurs the effect $\mathtt {File.append}$. The $\mathtt {client}$ module, possessing the $\mathtt {logger}$ module, exposes an unannotated function $\mathtt {run}$. While $\mathtt {logger}$ has been annotated, $\mathtt {client}$ has not. If $\mathtt {client.run}$ is executed, what effects might it have? Code for this example is given below.

A translation into $\mathtt {CC}$ is given below. Lines 1–3 and 5–8 define $\mathtt {MakeLogger}$ and $\mathtt {MakeClient}$, which instantiate the $\mathtt {logger}$ and $\mathtt {client}$ modules respectively (represented as functions). Lines 10–14 define $\mathtt {MakeMain}$, which returns a function which, when executed, instantiates all other modules and invokes the code in the body of $\mathtt {main}$. Program execution begins on line 16, where $\mathtt {main}$ is given the initial capabilities (just $\mathtt {File}$ in this case).

The interesting part is on line 7, where the unannotated code selects $\{ \mathtt {File.append} \}$ as its authority. This matches the effects of $\mathtt {logger}$, i.e. $\mathtt {effects}(\mathtt {Unit}\rightarrow _{\{\mathtt {File.append}\}} \mathtt {Unit}) = \{ \mathtt {File.append} \}$. The unannotated code typechecks by $\varepsilon$ -Import, approximating its effects as $\mathtt {\{ \mathtt {File.append} \}}$.

3.2 Unannotated Library

The next example inverts the roles of the last scenario. Now, the annotated $\mathtt {client}$ wants to use the unannotated $\mathtt {logger}$, which captures $\mathtt {File}$ and exposes a single function $\mathtt {log}$, which incurs the $\mathtt {File.append}$ effect. The implementation of $\mathtt {client.run}$ executes $\mathtt {logger.log}$; it is annotated with $\varnothing$, so this violates its interface.

The translation is given below. On lines 3–4, the unannotated code is wrapped in an $\mathtt {import}$ expression selecting $\{ \mathtt {File.append} \}$ as its authority. The implementation of $\mathtt {logger}$ actually abides by this, but since it captures $\mathtt {File}$ it could, in general, do anything to $\mathtt {File}$; therefore, $\varepsilon$ -Import rejects this example. Formally, the imported capability has the type $\mathtt { \{ File \} }$, but $\mathtt {effects}(\{ \mathtt {File}\}) = \{ \mathtt {File}.* \} \not \subseteq \{ \mathtt { File.append } \}$. The only way for this to typecheck would be to annotate $\mathtt {client.run}$ as having every effect on $\mathtt {File}$.

3.3 Higher-Order Effects

Here, $\mathtt {Main}$ gains its functionality from a plugin. Plugins might be written by third-parties, so we may not be able to view their source code, but still want to reason about the authority they exercise. In this example, $\mathtt {plugin}$ has access to $\mathtt {File}$, but its interface does not permit it to perform any operations on $\mathtt {File}$. It tries to subvert this by wrapping $\mathtt {File}$ inside a function and passing it to $\mathtt {malicious}$, which invokes $\mathtt {File.read}$ in a higher-order manner in an unannotated context.

This example shows how higher-order effects can obfuscate potential security risks. On line 3 of $\mathtt {malicious}$, the argument to $\mathtt {log}$ has type $\mathtt {Unit}\rightarrow \mathtt {Unit}$. The body of $\mathtt {log}$ types with the T-rules, which do not approximate effects. It is not clear from inspecting the unannotated code that a $\mathtt {File.read}$ will be incurred. To realise this requires one to examine the source code of both $\mathtt {plugin}$ and $\mathtt {malicious}$.

A translation is given below. On lines 2–3, the $\mathtt {malicious}$ code selects its authority as $\varnothing$, to be consistent with the annotation on $\mathtt {plugin.run}$. $\varepsilon$ -Import safely rejects this: when the unannotated code is annotated with $\varnothing$, it has type $\{ \mathtt {File}\} \rightarrow _{\varnothing } \mathtt {Unit}$, but the higher-order effects of this type are $\mathtt { \{ File.* \} }$, which are not contained in the selected authority $\varnothing$.

To get this example to typecheck, the program would have to be rewritten to explicitly say that plugins can exercise arbitrary authority over $\mathtt {File}$, by changing the selected authority of $\mathtt {import}$ and the annotation on $\mathtt {plugin.run}$.

3.4 Resource Leak

This is another example which obfuscates an unsafe effect by invoking it in a higher-order manner. The setup is the same, except the function which $\mathtt {plugin}$ passes to $\mathtt {malicious}$ now returns $\mathtt {File}$ when invoked. $\mathtt {malicious}$ uses this function to obtain $\mathtt {File}$ and directly invokes $\mathtt {read}$ upon it, violating the declared purity of $\mathtt {plugin}$.

The translation is given below. The unannotated code in $\mathtt {malicious}$ is on lines 5–6. It has selected authority is $\varnothing$, to be consistent with the annotation on $\mathtt {plugin}$. Nothing is being imported, so the $\mathtt {import}$ binds $\mathtt {y}$ to $\mathtt {unit}$. This example is rejected by $\varepsilon$ -Import because the premise $\varepsilon = \mathtt {effects}(\hat{\tau }) \cup \mathtt {ho \hbox {-}effects}(\mathtt {annot}(\tau , \varepsilon ))$ is not satisfied. In this case, $\varepsilon = \varnothing$ and $\tau = \mathtt { (Unit \rightarrow \{ File \}) \rightarrow Unit }$. Then $\mathtt {annot}(\tau , \varepsilon ) = \mathtt { (Unit \rightarrow _{\varnothing } \{ File \}) \rightarrow _{\varnothing } Unit }$ and $\mathtt {ho \hbox {-}effects}(\mathtt {annot}(\tau , \varepsilon )) = \{ \mathtt {File.*} \}$. Thus, the premise cannot be satisfied and the example is safely rejected.

4 Conclusions

We introduced $\mathtt {CC}$, a lambda calculus with a simple notion of resources and their operations, which allows unannotated code to be nested inside annotated code with a new $\mathtt {import}$ construct. Its capability-safe design enables us to safely reason about the effects of unannotated code by inspecting what capabilities are passed into it by its annotated surroundings. Such an approach allows code to be incrementally annotated, giving developers a balance between safety and convenience, alleviating the verbosity that has discouraged widespread adoption of effect systems [19].

More broadly, our results demonstrate that the most basic form of capability-based reasoning—that you can infer what code can do based on what capabilities are passed to it—is not only useful for informal reasoning, but can improve formal reasoning about code by reducing the necessary annotation overhead.

4.1 Related Work

While much related work has already been discussed as part of the presentation, here we cover some additional strands related to capabilities and effects.

Capabilities were introduced by [3] to control which processes had permission to access which resources in an operating system. These ideas were adapted to the programming language setting, particularly by Miller [17], whose object-capability model constrains how permissions may proliferate among objects in a distributed system. [13] formalised the notion of a capability-safe language and showed that a subset of Caja (a Javascript implementation) is capability-safe. Miller’s object-capability model has been applied to more heavyweight systems, such as [6], which formalises the notion of trust in a Hoare logic. Capability-safety parallels have been explored in the operating systems literature, where similar restrictions on dynamic loading and resource access [7] enable static, lightweight analyses to enforce privilege separation [12].

The original effect system by [10] was used to determine what expressions could safely execute in parallel. Subsequent applications include determining what functions a program might invoke [21] and what regions in memory might be accessed or updated during execution [20]. In these systems, “effects” are performed upon “regions”; in ours, “operations” are performed upon “resources”. $\mathtt {CC}$ also distinguishes between unannotated and annotated code; only the latter will type-and-effect-check. Another capability-based effect system is the one by [4], who use effect polymorphism and possible world semantics to express behavioural invariants on data structures. $\mathtt {CC}$ is not as expressive, since it only inspects how capabilities are passed around a program, but the resulting formalism and theory is much more lightweight. Ongoing work with the Wyvern programming language includes an effect system which partially builds on ideas from this paper [15].

4.2 Future Work

Our system only models capabilities which manipulate system resources. This definition could be generalised to track other sorts of effects, such as stateful updates. Resources and their operations are fixed throughout runtime, but we could imagine them being created and destroyed at runtime. Finally, other future work could incorporate polymorphic types and effects.