#  Cocoon: Static Information Flow Control in Rust

Ada Barach  ,  Maxwell Taylor  ,  Vincent Beardsley  ,  Jacob Bambeck  ,
Michael D. Bond  and  Zhiqiang Lin  Ohio State UniversityUSA

###### Abstract.

Information flow control (IFC) ensures confidentiality by preventing secret
values from affecting non-secret values. Existing language-level IFC
approaches modify the language and use non-standard compilation tools, impose
run-time overhead, or report false leaks, all of which hinder adoption. This
paper presents Cocoon, a Rust library for static type-based IFC that uses the
unmodified Rust language and compiler. The key insight of Cocoon lies in
leveraging Rust’s type system and procedural macros to establish an effect
system that allows applications to safely compute arbitrary functions on
secret data. We integrated Cocoon into two popular Rust programs, the Spotify
TUI client and Mozilla’s Servo browser engine, to protect a secret value in
each program. The results show that applications can be retrofitted to use
Cocoon with limited modifications, at least to protect a single value, with
negligible or nonexistent impacts on run-time and compile-time performance.

##  1\. Introduction

Confidentiality is a fundamental property of secure computing systems.
Confidentiality, or secrecy, is usually achieved through _access control_ ,
which regulates _which_ entities may access _which_ data, but _not_ what
happens to the data after it is accessed, resulting in a large trusted
computing base. A robust alternative is _information flow control (IFC)_ ,
which ensures that high-secrecy values cannot flow to (i.e., cannot affect)
low-secrecy values (Rotenberg, 1973; Denning, 1976).111IFC generally also
ensures integrity, by ensuring that low-integrity values cannot flow to high-
integrity values, but this paper handles only confidentiality. IFC is
especially valuable as a _fine-grained_ , or language-level, mechanism that
protects the flow of data values within applications, ensuring they do not
misuse privileges. Consider, for example, a virus checker application with
privileges to read data from disk and to send requests to a server for
updates. Fine-grained IFC can ensure that application _cannot_ send the
contents of the disk to the server. Fine-grained IFC dramatically reduces the
trusted computing base to the relatively few operations that explicitly
violate IFC by _declassifying_ secret values.

Fine-grained IFC can be supported either dynamically at run time, which incurs
run-time overhead (Austin and Flanagan, 2009; Roy et al., 2009; Xiang and
Chong, 2021), or statically at compile time. Static IFC can be realized via
whole-program analysis or modular type-based analysis. _Whole-program static
analysis_ conservatively models the flow of values through expressions and
variables and ensures that high-secrecy values do not flow to low-secrecy
sinks (Balasubramanian et al., 2017; Zanioli et al., 2012; Hedin and
Sabelfeld, 2012; Hammer et al., 2006). However, whole-program analysis is non-
compositional, so it scales poorly and supports incremental deployment poorly.
A recent analysis called _Flowistry_ leverages Rust ownership constraints to
compute relatively precise function summaries without analyzing the functions’
bodies (Crichton et al., 2022). In _static type-based analysis_ by contrast,
variables and expressions are annotated with types that represent their
security labels, and a correctly typed program guarantees IFC (Russo, 2015;
Gregersen et al., 2019; Sabelfeld and Myers, 2003; Myers, 1999; Myers et al.,
2006; Myers and Liskov, 1997; Kozyri et al., 2016; Chong, 2008; Simonet, 2003;
Chapman and Hilton, 2004; Smith and Volpano, 1998; Volpano et al., 1996).
While this approach allows for modular checking and incremental deployment,
existing type-based solutions are either limited to functional languages, or
they modify mainstream imperative languages such as Java and C to be able to
support IFC. Modifying the language and compiler requires keeping the
modifications up to date, and programmers cannot use standard development
tools.

Prior work that targets an imperative language must _modify_ the language and
compiler because the language’s type system is not expressive enough to
statically ensure IFC. The key technical challenge is how to allow programs to
define and use functions on secret data without permitting unchecked side
effects that might leak data. In theory, an _effect system_ for encoding the
side effects of a computation would constrain the behaviors of functions on
secret data (Nielson and Nielson, 1999). Such an effect system has been used
by prior work in the context of certain functional languages (Russo, 2015;
Gregersen et al., 2019; Abadi et al., 1999). However, effect systems are not
supported by mainstream imperative languages including Java, C, C++, and Rust.

### Contributions

This paper introduces _Cocoon_ , the first static type-based IFC for a
mainstream imperative language. Cocoon is a Rust library for the unmodified
Rust language that works with the standard Rust compiler. It ensures that a
program compiles only if it does not leak secrets except by explicitly
_declassifying_ secrets or explicitly using unsafe Rust code. Cocoon provides
a rudimentary effect system that limits computations’ side effects using a
novel approach that leverages expressive Rust features including ownership,
traits, and procedural macros.

We evaluated Cocoon’s effectiveness and efficiency by retrofitting two popular
Rust applications, a Spotify client and the Servo web browser engine, to
protect a single secret value in each program. These case studies demonstrate
that Cocoon’s approach works in real applications and can be incrementally
deployed. The evaluation also shows Cocoon does not affect application run
time or memory usage, although it can affect compile time if a substantial
fraction of the program is annotated as dealing with secret values.

Cocoon thus advances the state of the art in language-level IFC support by
demonstrating a novel approach that requires no language or compiler
modifications. The current design has several limitations, including
supporting only static secrecy labels and placing restrictions on the
programming model (§ 4.6).

This paper makes the following contributions:

  * •

a language-level IFC approach that is the first to provide static type-based
IFC for a mainstream imperative language without language or compiler
modifications;

  * •

novel support for a rudimentary effect system that captures side effects that
could leak secrets;

  * •

two case studies on real Rust programs that demonstrate that Cocoon works for
real programs and adds negligible or nonexistent run-time and compile-time
overheads; and

  * •

a performance evaluation showing that Cocoon has no detectable run-time
impact, but can impact compile time significantly if a lot of code deals with
secret values.

##  2\. Motivating Example

Fig. 2 shows example Rust code that computes the number of overlapping days of
availability on two calendars, belonging to Alice and Bob. Each calendar is a
map from a day of the week, represented as a string, to a boolean indicating
whether Alice or Bob is available on that day. Suppose that Alice and Bob’s
calendars are secret. Specifically, the values (booleans) in their calendars
are secrets, although the keys (strings) are not. For simplicity we assume
that the calendars have identical key sets. The example computes and reveals
only the number of overlapping days in Alice and Bob’s availability.

The syntax for (day, available) in alice_cal iterates over all key–value pairs
in Alice’s calendar. Note that the types of day and available are &String and
&bool, meaning that they are actually (immutable) _references_ to the values.
The expression bob_cal.get(&day) calls HashMap::get(&self,&String) ->
Option<&bool>, which is a method that takes a reference to a String as a
parameter. Rust allows an unlimited number of immutable references, _or_ a
single mutable reference, to a value at a time. The get method returns a value
of type Option<&bool>, which represents a reference to a boolean, or an error
if the key was not found in bob_cal. The call to Option::unwrap(self) -> &bool
returns the reference to the inner boolean, or fails otherwise. Since unwrap()
returns &bool (reference to boolean), its result is dereferenced (and
implicitly copied) with the * operator. To be sure that the code in Fig. 2
does not leak more information about Alice or Bob’s schedule than the number
of overlapping days, we must trust the code or audit it carefully.

Alternatively, fine-grained (i.e., language-level) _information flow control
(IFC)_ provides a way to _ensure_ that code cannot leak secrets to untrusted
entities, by disallowing high-secrecy values from flowing to low-secrecy
values (Rotenberg, 1973; Denning, 1976). IFC can ensure both confidentiality
(secrecy) and integrity; for simplicity, this paper supports confidentiality
but not integrity.

Information flows can be explicit or implicit. In an _explicit flow_ , a data
dependency exists between the two values. In Fig. 2 the return value of
bob_cal.get(&day) flows to Option::unwrap()’s parameter via an explicit flow.
An implicit flow is a flow that involves control dependence. In Fig. 2, an
implicit flow exists from available’s value (and from the return value of
bob_cal.get(&day)) to count’s value.

⬇

let alice_cal: HashMap<String, bool> = /* { "Monday" -> true, ... } */

let bob_cal: HashMap<String, bool> = /* { "Monday" -> false, ...} */

let mut count = 0;

for (day, available) in alice_cal {

if available && *bob_cal.get(&day).unwrap() {

count += 1;

}

}

println!("Overlapping days: {}", count);

Figure 1. Rust code _without_ support for IFC that computes the overlapping
number of days in two calendars.

⬇

1let alice_cal: HashMap<String, Secret<lat::A,bool>> = /* { "Monday" ->
Secret(true), ... } */

2let bob_cal: HashMap<String, Secret<lat::B,bool>> = /* { "Monday" ->
Secret(false), ...} */

3let mut count = secret_block!(lat::AB { wrap_secret(0) });

4for (day, available) in alice_cal {

5 secret_block!(lat::AB {

6 if unwrap_secret(available) &&

7 *unwrap_secret_ref(::std::option::Option::unwrap(

8 ::std::collections::HashMap::get(&bob_cal, &day))) {

9 *unwrap_secret_mut_ref(&mut count) += 1;

10 }

11 });

12}

13println!("Overlapping days: {}", count.declassify());

Figure 2. Rust code that has the same functionality as Fig. 2 but uses Cocoon
to ensure IFC.

Consider Fig. 2, which has the same functionality as Fig. 2, but it ensures
IFC using this paper’s approach, Cocoon. The booleans in Alice and Bob’s
calendars are wrapped in a Secret type and have labels $\\{a\\}$ and
$\\{b\\}$, where $a$ and $b$ are _policies_ (also called _tags_) corresponding
to secrecy privileges. A label $L_{1}$ is _at least as secret as_ label
$L_{2}$ if and only if $L_{1}\supseteq L_{2}$.

Applications can only access secret values inside of lexically scoped regions
called _secret blocks_ , denoted by the macro call secret_block!. Before the
loop, the code uses a secret block to create a new secret value 0 (zero) with
label $\\{a,b\\}$, which is assigned to count. The secret block inside the
loop222One could instead wrap the whole loop in a single secret block, but in
the spirit of minimizing code in secret blocks—and to showcase more of
Cocoon—the code wraps only the loop’s body in a secret block. has label
$\\{a,b\\}$; Cocoon ensures that the block’s inputs must be no more secret
than $\\{a,b\\}$, and its output(s) must be no less secret than $\\{a,b\\}$,
thus preventing illegal flows.

The block uses calls to unwrap_secret, unwrap_secret_ref, and
unwrap_secret_mut_ref to access secret values. Cocoon ensures that these calls
are only allowed if the unwrapped value’s label is no more secret than the
secret block’s label. unwrap_secret_mut_ref() gets _mutable_ access to a
secret value, allowing both read and write access, requiring the value to have
the same label as the secret block.

The secret block uses fully qualified calls to Rust library functions (e.g.,
::std::option:Option::unwrap(...)), which Cocoon currently requires in order
to check that the callee cannot leak secrets.

After the loop completes, the program explicitly declassifies the secret value
count in order to print its value. Declassifications are part of the trusted
computing base and must be audited.

##  3\. Requirements and Assumptions

Fine-grained information flow control (IFC) is not used widely in practice
because it is not practical. A practical solution must provide sound and
precise IFC for programs written in a mainstream imperative language without
modifying the language or its compiler or incurring run-time overhead.

###  3.1. Assumptions and Non-requirements

This paper focuses on achieving language-level IFC for static secrecy labels
using an off-the-shelf language and compiler. This work does _not_ aim to
support integrity labels, dynamic labels, or OS integration.333Since OS
integration is outside our scope, the programming model assumes that every OS-
level entity is an untrusted entity. It is the programmer’s responsibility to
identify secrets coming from OS-level entities such as files and sockets, and
the program must declassify a value before sending it to any OS-level entity.
Our work aims to provide _termination-insensitive noninterference_ (explained
below); it does not protect side channels such as termination and timing
channels. Finally, although the programming model is pure Rust, it has several
restrictions, a challenge we leave for future work. § 4.5 and § 4.6 describe
Cocoon’s guarantees and limitations in more detail.

We do not present a proof of correctness, which would be a notable research
contribution by itself. Other work has presented correctness proofs, but only
for small, toy languages (Zdancewic and Myers, 2000; Myers et al., 2004; Zheng
and Myers, 2005). As Zheng and Myers point out, “[p]roofs for noninterference
exist for numerous security-typed languages, but not for any language as
expressive as Jif” (Zheng and Myers, 2005). IFC solutions for larger-scale
languages do not include correctness proofs (Myers, 1999; Myers and Liskov,
1998; Zheng and Myers, 2005), with the authors of Viaduct (a compiler for
secure distributed programs) even noting that “a full correctness proof for
the Viaduct compiler would be a significant research achievement …” (Acay et
al., 2021).

###  3.2. Requirements

This paper aims to provide IFC support through a Rust library, without
modifying the Rust language or compiler. Here we motivate and describe the
requirements that our approach needs to meet.

#### Widely used, high-performance language

A drawback of many prior static IFC solutions is that they require the use of
an academic or non-mainstream language that inhibits their adoption (§ 6).
Thus, we aim to develop an IFC solution that uses a popular, high-performance
language: _Rust_. Rust was designed by Graydon Hoare at Mozilla Research in
2010 and had its first stable release in 2015 (Noel, 2010; Mozilla Research,
2020). Since then it has had 95 releases, over 3,500 contributors, and has
held the title of Stack Overflow’s “most loved language” by developers every
year since 2016 (Stack Overflow, 2022). Rust is commonly used in large-scale
applications; for example, many core features of Mozilla Firefox are primarily
written in Rust (The Rust Foundation, 2022).

#### Off-the-shelf language and compiler support

In contrast to prior solutions that extend a language and modify the compiler
or rely on a custom compiler (§ 6), we aim to enforce IFC without requiring a
customized language or compilation tools. In the context of the Rust language,
we aim to provide IFC entirely through a library. Programs are written in
unmodified Rust using the IFC library and compiled with the unmodified Rust
compiler. The library is trusted (i.e., is part of the trusted codebase) along
with the Rust compiler and standard library. The application is untrusted,
except for unsafe and declassify operations, which must be trusted or audited.
In Rust, unsafe operations already forgo guarantees of memory and type safety.

#### Soundness

We aim to provide _termination-insensitive noninterference_ : In the absence
of explicit declassification or explicitly unsafe code, high-secrecy values
cannot affect low-secrecy values, but may affect whether the program
terminates (Abadi et al., 1999; Askarov et al., 2008). This work does not
address side channels created by timing or microarchitectural states.

#### Incremental deployment

Converting large applications to use the IFC library could be time-consuming
and burdensome. Our goal is to provide an IFC library that can be
incrementally deployed. Developers should only need to modify parts of their
code that deal with secret values.

#### Run-time performance

Programs using the IFC library should perform indistinguishably from otherwise
equivalent programs that do not. The Rust compiler should be able to “optimize
away” the typing and scaffolding introduced by the application’s use of the
IFC library, reducing the compiled code so it performs the same as an
otherwise equivalent program.

##  4\. Cocoon: Static Information Flow Control in Rust

Cocoon is a static IFC approach that is implemented as a Rust library and
meets § 3.2’s requirements.

###  4.1. Cocoon’s Programming Model

Fig. 3 breaks down the Cocoon programming model into three foundational
components: secret data (3a) and their secrecy labels (3b), accessing secrets
(3c–3f), and declassification (3g).

⬇ struct Secret<Type: SecretValueSafe, SecrecyLabel: Label>

(a) Secret expressions and variables with non-empty secrecy have type
Secret<T,L>. The trait SecretValueSafe, defined in § 4.3.1, restricts what
values can be wrapped in Secret.

Struct |  Traits implementing struct
---|---
Label_Empty |  Label, MoreSecretThan<Label_Empty>
Label_A |  Label, MoreSecretThan<Label_Empty>, MoreSecretThan<Label_A>
Label_B |  Label, MoreSecretThan<Label_Empty>, MoreSecretThan<Label_B>
Label_AB |  Label, MoreSecretThan<Label_Empty>, MoreSecretThan<Label_A>, MoreSecretThan<Label_B>, MoreSecretThan<Label_AB>
(b) Labels, and traits defining a partial order of labels

⬇ secret_block!($\mathit{label}$ { $\mathit{body}$ })

(c) Secret block, which executes $\mathit{body}$ with secrecy label
$\mathit{label}$

Operation | Evaluates to | Type constraint
---|---|---
unwrap_secret($v$: Secret<T,$L$>) -> T | Inner value | $L\subseteq L_{B}$
unwrap_secret_ref($v$: &Secret<T,$L$>) -> &T | Immutable reference to value | $L\subseteq L_{B}$
unwrap_secret_mut_ref($v$: &mut Secret<T,$L$>) -> &mut T | Mutable reference to value | $L=L_{B}$
wrap_secret($v$) | Secret<_,$L_{B}$>::new($v$) | N/A
(d) Operations on Secret values in a secret block with secrecy label $L_{B}$

⬇ #[side_effect_free_attr] fn $\mathit{func}$($\mathit{params}$) ->
$\mathit{retType}$ { $\mathit{body}$ }

(e) Annotation for side-effect-free functions. Secret blocks may only
(transitively) call side-effect-free functions.

⬇ #[derive(InvisibleSideEffectFree)] struct $s$ { $\dots$ }

(f) Annotation for application types that are used in secret blocks

Operation | Evaluates to
---|---
Secret<T,$L$>::declassify(self) -> T | Inner value
Secret<T,$L$>::declassify_ref(&self) -> &T | Immutable reference to inner value
Secret<T,$L$>::declassify_ref_mut(&mut self) -> &mut T | Mutable reference to inner value
(g) Declassify operations on Secret values

Figure 3. Cocoon’s programming model.

#### Secret values and secrecy labels

Our work follows the decentralized IFC model introduced by Myers and Liskov
(1997). A secrecy _label_ , which describes the permissions for data, is a set
of secrecy _policies_ (also called _tags_). For example, a label $L=\\{a,b\\}$
contains the policies $a$ and $b$. These policies correspond to entities with
different secrecy privileges, such as users of a system. Labels form a partial
order on these policies, in which label $L_{1}$ is _at least as secret as_
label $L_{2}$ if and only if $L_{1}\supseteq L_{2}$.

Every expression and variable has a static secrecy label determined by its
static type. By default, expressions and variables have the empty secrecy
label (lowest secrecy). An expression or variable with higher secrecy is
represented by wrapping it in a Cocoon-provided type Secret<Type,Label>,
defined in Fig. 3a. Secret values are opaque and must be accessed through an
interface provided by Cocoon, discussed shortly. Note that wrapping values in
Secret incurs no run-time cost; a Secret<Type,Label> instance has the same
run-time representation as a Type instance.

Fig. 3b shows that labels are implemented as structs, and trait
implementations444Rust’s traits are similar to Java’s interfaces and C++’s
abstract methods, but traits allow more expressive type constraints. help
enforce legal flows. Specifically, a trait MoreSecretThan<$M$> is implemented
for label $L$ if and only if $M\subseteq L$.

#### Accessing secrets in secret blocks

To help restrict illegal flows and to limit the annotation burden, Secret-
wrapped values may be accessed only inside of lexically scoped blocks of code
called _secret blocks_ , as shown in Fig. 3c. A secret block is a macro
call555In Rust, every macro name ends with !. that specifies a static label
that restricts the values the block’s body may read and write—the body may
only read values with lower or same secrecy, and may only write values with
higher or same secrecy—preventing illegal explicit and implicit flows. The
block evaluates to a secret value with the the same label as the block.

The secret block’s body can call unwrap_secret($e$) on an expression $e$ with
type Secret<Type,$\mathit{label}$>, as long as $\mathit{label}$ is no more
secret than the block’s secrecy label. Cocoon also provides variants of
unwrap_secret that take and return references instead of values, called
unwrap_secret_ref and unwrap_secret_mut_ref. (§ 2 explained immutable and
mutable references briefly.) A secret block can call wrap_secret($e$) to
create a new Secret value with the same secrecy label as the block.

A secret block can call application-defined functions only if they have been
annotated as _side-effect free_ using a Cocoon-provided attribute macro,
#[side_effect_free_attr] (Fig. 3e). Side-effect-free functions in turn can
only call other side-effect-free functions.

To use a custom type in secret blocks, an application must annotate the type
as side-effect free by annotating it with #[derive(InvisibleSideEffectFree)]
(Fig. 3f).

#### Declassification

Cocoon allows high-secrecy values to flow to low-secrecy values through the
declassify() method and its variants (Fig. 3g), which return the unwrapped
value. Declassification is a trusted operation and should be audited by
developers.

#### Example

Fig. 2 in § 2 presented an example that uses most elements of the programming
model.

###  4.2. How Cocoon Restricts Accesses to Secret Values

This section describes how Cocoon restricts the flow of secret values inside
and outside of secret blocks, while § 4.3 describes how Cocoon restricts
arbitrary side effects in secret blocks. To support these features, Cocoon
leverages Rust _procedural macros_ , which are procedures that operate on Rust
_syntax_ at compile time—type information is not available at macro expansion
time, so macros operate on an untyped abstract syntax tree (AST).

Cocoon restricts accesses to Secret values inside of secret blocks using
transformations by the secret_block! procedural macro. Figs. 4a and 5a show
transformations performed on secret blocks to mediate accesses to secret
values. As Fig. 5a shows, secret_block! expands unwrap_secret($e$) to a call
to Secret::unwrap::<$L$>($e$) (similarly for unwrap_secret_ref and
unwrap_secret_mut_ref) where $L$ is the block’s label. Secret::unwrap($e$) has
a type constraint requiring that $e$’s label is no more secret than $L$. For
unwrap_secret_mut_ref($e$), the type constraint requires $e$’s label to be
_equal to_ $L$ because mutable references allow both writing and reading the
referent.

Application code: ⬇ secret_block!($L$, $\mathit{body}$) Macro-transformed
code: ⬇ if true { ::Cocoon::call_closure::<$L$,_,_>(|| -> _ {
::std::panic::catch_unwind(::std::panic::AssertUnwindSafe(|| {
$\tau(\mathit{body},\mathit{F})$ })) }.unwrap_or_default()) } else {
::Cocoon::call_closure::<$L$,_,_>(|| -> _ { $\tau(\mathit{body},\mathit{T})$
}) } Definition of call_closure: ⬇ fn call_closure<L, F, R>(clos: F) -> R
where F: FnOnce() -> R + VisibleSideEffectFree, R: SecretTrait<L> { clos() }
Note: SecretTrait<L> is a trait implemented by Secret<T,L> and tuples of
Secret<T,L>, allowing secret blocks to return multiple secret values.

(a) How the secret_block! macro expands secret blocks.

Application code: ⬇ #[side_effect_free_attr] fn $f$($\mathit{params}$) -> $r$
{ $\mathit{body}$ } Macro-transformed code: ⬇ fn
__$f$_secret_trampoline_unchecked($\mathit{params}$) -> $r$ {
$\tau(\mathit{body},\mathit{T})$ } fn
__$f$_secret_trampoline_checked($\mathit{params}$) -> $r$ {
$\tau(\mathit{body},\mathit{F})$ } #[inline(always)] unsafe fn
$f$($\mathit{params}$) -> ::Cocoon::Vetted<$r$> {
::Cocoon::Vetted::<$r$>::wrap(__$f$_secret_trampoline_unchecked($\mathit{args}$))
}

(b) How the #[side_effect_free_attr] macro expands side-effect-free functions.

Figure 4. Outer transformations performed by Cocoon’s procedural macros for
secret blocks and side-effect-free functions. The expressions
$\tau(\mathit{body},\mathit{F})$ and $\tau(\mathit{body},\mathit{T})$
represent syntax that is expanded by the macros; the expansions are detailed
in LABEL:fig:transf-all-exprs.

$\bm{\mathit{expr}}$ $\tau(\mathit{expr},\mathit{isExec})$ unwrap_secret($e$)
{ let tmp = $\tau(e,\mathit{isExec})$; unsafe { Secret::unwrap::<$L$>(tmp) } }
unwrap_secret_ref($e$) { let tmp = $\tau(e,\mathit{isExec})$; unsafe {
Secret::unwrap_ref::<$L$>(tmp) } } unwrap_secret_mut_ref($e$) { let tmp =
$\tau(e,\mathit{isExec})$; unsafe { Secret::unwrap_mut_ref::<$L$>(tmp) } }
wrap_secret($e$) { let tmp = $\tau(e,\mathit{isExec})$; unsafe {
Secret::new::<_,$L$>() } }

(a) Transformations performed by Cocoon’s procedural macros on secret blocks
only (not side-effect-free functions). $L$ is the secret block’s label. Secret
is an abbreviation for ::cocoon::Secret.

$\bm{\mathit{expr}}$ $\tau(\mathit{expr},\mathit{\mathit{isExec}})$
callee($e_{1}$, $e_{2}$, $\dots$) if callee is _not_ allowlisted let tmp1 =
$\tau(e_{1},\mathit{\mathit{isExec}})$; let tmp2 =
$\tau(e_{2},\mathit{\mathit{isExec}})$; $\dots$unsafe { callee(tmp1, tmp2,
$\dots$) as ::cocoon::Vetted<_> .unwrap() } callee($e_{1}$, $e_{2}$, $\dots$)
if callee is allowlisted
check_ISEF(callee($\tau(e_{1},\mathit{\mathit{isExec}})$,
$\tau(e_{2},\mathit{\mathit{isExec}})$, $\dots$))

(b) Transformations performed by Cocoon’s procedural macros on calls.

$\bm{\mathit{expr}}$ $\tau(\mathit{expr},\mathit{F})$
$\tau(\mathit{expr},\mathit{T})$ literal (constant) literal literal path (var.
name) { let tmp = &path; unsafe {check_ISEF_unsafe(tmp) } } path $e_{1}$ +
$e_{2}$ ::Cocoon::SafeAdd::safe_add($\tau(e_{1},\mathit{F})$,
$\tau(e_{2},\mathit{F})$) $\tau(e_{1},\mathit{T})$ + $\tau(e_{2},\mathit{T})$
$e_{1}$ && $e_{2}$ $\tau(e_{1},\mathit{F})$ && $\tau(e_{2},\mathit{F})$
$\tau(e_{1},\mathit{T})$ && $\tau(e_{2},\mathit{T})$ $e_{1}$ = $e_{2}$
*check_not_mut_secret(&mut $\tau(e_{1},\mathit{F})$)= $\tau(e_{2},\mathit{F})$
$\tau(e_{1},\mathit{T})$ = $\tau(e_{2},\mathit{T})$ &$e$
check_ISEF(&($\tau(e,\mathit{F})$ )) &$\tau(e,\mathit{T})$ *$e$
*($\tau(e,\mathit{F})$ ) *$\tau(e,\mathit{T})$ $e$.field
$\tau(e,\mathit{F})$.field $\tau(e,\mathit{T})$.field if $e_{1}$ { $e_{2}$
}else { $e_{3}$ } if $\tau(e_{1},\mathit{F})$ { $\tau(e_{2},\mathit{F})$ }else
{ $\tau(e_{3},\mathit{F})$ } if $\tau(e_{1},\mathit{T})$ {
$\tau(e_{2},\mathit{T})$ }else { $\tau(e_{3},\mathit{T})$ }

(c) Transformations performed by Cocoon’s procedural macros on secret blocks
and side-effect-free functions.

Code outside of a secret block cannot call unwrap_secret() because the
function does not exist (it is only recognized by secret_block!). Code cannot
call the unsafe function Secret::unwrap() directly without using the unsafe
keyword; code that uses unsafe forgoes Cocoon’s guarantees (and Rust’s safety
guarantees) and must be audited (§ 3). Application code cannot access
Secret’s value field directly because it is private.

A secret block must return a Secret with the same label as the block.
secret_block!($L$ { $\mathit{body}$ }) ensures that $\mathit{body}$ returns a
Secret value with label $L$ by using type constraints—specifically on the
return value of Cocoon::call_closure() as shown in Fig. 4a.

To prevent a secret block from assigning to a mutable Secret variable without
going through unwrap_secret_mut_ref (potentially leaking a more-secret value
through an implicit flow), secret_block! transforms every assignment
expression $e_{1}$ = $e_{2}$ by wrapping $e_{1}$ in a call to Cocoon function
check_not_mut_secret(), as Fig. 5c shows. The call requires statically that
$e_{1}$’s type is (transitively) not Secret, by using Rust auto traits and
negative implementations.

###  4.3. How Cocoon Restricts Side Effects that Could Leak Secrets

In addition to ensuring that secret blocks only access secret values through
legal flows, Cocoon must ensure that secret blocks do not have _side effects_
that might leak secret values. For example, if a secret block writes to a
mutable low-secrecy variable accessible outside of the block, or if a secret
block sends a value to an untrusted socket, then an illegal flow might exist.

Cocoon ensures that secret blocks are side-effect free by enforcing that
secret blocks (1) cannot write values that are visible outside of the block
and (2) may call only side-effect-free functions, which in turn may call only
side-effect-free functions. Collectively, secret blocks and side-effect-free
functions are _side-effect-free contexts_. Cocoon’s side-effect-free
restrictions constitute a rudimentary effect system that captures whether
operations have side effects that could leak secret values.

We classify side effects as either _syntactically visible or invisible_
depending on whether they are visible to Rust’s procedural macros, which
operate on an untyped AST (§ 4.2). § 4.3.1 and § 4.3.2 describe how Cocoon
restricts side effects that are syntactically visible and invisible,
respectively.

####  4.3.1. How Cocoon restricts syntactically visible side effects

Cocoon restricts two kinds of syntactically visible side effects: escaping
mutations and calls to functions with side effects.

##### Restricting mutation-based side effects

To ensure that a secret block cannot perform writes visible outside of the
block—except for writes to mutable Secret values, which are allowed—Cocoon
leverages Rust’s ownership and mutability constraints. Cocoon prevents a
secret block from modifying non-Secret variables in its surrounding
environment by forbidding the secret block’s body, which is implemented as a
closure, from capturing non-Secret variables by mutable reference. Cocoon
introduces the trait VisibleSideEffectFree (LABEL:fig:traits) to denote that
the block does not capture variables in its environment by mutable reference.
(In Rust, a closure implements a trait only if all the variables it captures
implement that trait.) Cocoon leverages Rust’s auto traits and negative
implementations to define VisibleSideEffectFree so that every type
automatically implements it except for types that (transitively) contain non-
Secret mutable references (&mut T except for &mut Secret<_,_>) or interior-
mutable cells (types that implement UnsafeCell, e.g., RefCell<T>). As a
result, a closure that implements VisibleSideEffectFree cannot mutably capture
non-Secret values. The only possible side effect of mutation is through Secret
values, which Cocoon mediates.

Trait |  Description |  Definition
---|---|---
VisibleSideEffectFree |  Limits mutably captured values of secret blocks |  $($Immutable$\,\lor\,($&mut Secret<_,_>$))\,\,\land$ &InvisibleSideEffectFree
SecretValueSafe |  Restricts T in Secret<T,L> to immutable, block-safe types |  Immutable $\land$ InvisibleSideEffectFree
Immutable |  Types without interior or regular mutability |  $\neg($UnsafeCell<_>)$\;\land\;\neg($&mut _$)$
InvisibleSideEffectFree |  Types that can be used in secret blocks |  Implemented individually for built-in and application types

Cocoon limits mutation in secret blocks but not in side-effect-free functions.
In Rust, functions cannot mutate memory accessible outside of the function
except through parameters to the function.

Cocoon must also ensure that values of type T wrapped in a Secret<T, Label>
are not interior mutable to avoid, for example, a secret block that reads
high-secrecy data using unwrap_secret() instead of unwrap_secret_mut() to
modify an interior-mutable value with low secrecy. Cocoon disallows interior
mutable types in a Secret by requiring that T implement a Cocoon-defined trait
SecretValueSafe (LABEL:fig:traits) that disallows mutable types.

##### Prohibiting calls to functions with side effects

To ensure that side-effect-free contexts call only side-effect-free functions,
Cocoon’s procedural macros ensure that every function called from a side-
effect-free context is also marked as side-effect free. Providing this
behavior is not straightforward because no type information is available at
macro expansion time (§ 4.2).

To address this challenge, the procedural macro #[side_effect_free_attr]
transforms the return type of the annotated function from R to Vetted<R>.
Cocoon’s procedural macros also rewrite all function calls within side-effect-
free contexts from f(...) to (f(...) as Vetted<R>).value, mandating that f
return Vetted<R>. As a result, every callee function must have been marked
side-effect free. Fig. 5b shows how the macros transform calls in side-effect-
free contexts.

Note that unverified functions cannot get around this requirement by directly
returning Vetted<R>. First, a function cannot simply construct a Vetted value
and return that function’s return value because the constructor of Vetted is
marked as unsafe to prevent unverified code from creating Vetted return
values. Second, a function cannot call another function that has been
transformed by the #[side_effect_free_attr] macro to obtain a Vetted value,
because the macro marks each function it generates as unsafe to disallow
calling the vetted function directly (without using unsafe).

Since the #[side_effect_free_attr] macro generates a function marked unsafe,
the untrusted function body could contain expressions that are only permitted
in unsafe Rust, although the original function was not marked unsafe. The
#[side_effect_free_attr] macro prevents this by generating a second function
that contains the function body. This second function omits the unsafe
modifier (assuming the original function did the same), thus preventing safety
violations.

Fig. 4b shows how the #[side_effect_free_attr] macro transforms marked
functions.

In addition to allowing side-effect-free contexts to call functions marked
side-effect free, the procedural macro allows calls to Rust Standard Library
functions that the Cocoon developers (i.e., us) have “allowlisted” as being
side-effect free. Cocoon’s procedural macro includes a list of functions that
we have determined to be side-effect free, which adds to the trusted codebase
and may be fragile (§ 4.5). Because the procedural macro operates on tokens
and has no type information, calls to allowlisted library functions from side-
effect-free contexts must be fully qualified (e.g.,
::std::string::String::len()) to prohibit calls to same-named functions with
side effects.

Thus, applications can mark any block or function as side-effect free, and the
compiler will check that the function is side-effect free (and generate a
compiler error if not). In order for a block or function to have a side
effect, e.g., by sending data to a network socket, it must ultimately call a
function _not_ marked side-effect free, which cannot pass the the procedural
macros’ checks.

####  4.3.2. How Cocoon restricts syntactically invisible side effects

So far we have described how Cocoon prevents side effects that are visible to
procedural macros. However, Rust provides a few ways to call functions in ways
that are syntactically _invisible_ —overloaded operators, deref coercion, and
custom destructors—which are difficult for Cocoon’s procedural macro to
detect.

Cocoon’s procedural macros transform every expression to ensure problematic
syntactically invisible side effects cannot compile. The procedural macros
actually generate _two versions_ of code in side-effect-free contexts: one
that executes and one that does not. In the _executed_ version, overloadable
operators and expressions are _not_ transformed by the procedural macro (but
unwrap_secret and wrap_secret calls are still expanded). This version is the
code that actually executes. In the _nonexecuted_ version, the procedural
macro _does_ transform operators and expressions as described below, but the
generated code is unreachable. As such, the expanded version causes compiler
errors if Cocoon’s requirements are violated, but it never executes. Fig. 4
shows the transformations performed on secret blocks and side-effect-free
functions to generate the executed and nonexecuted versions. The executed code
and nonexecuted code are generated by $\tau(\mathit{expr},\mathit{isExec})$,
which LABEL:fig:transf-all-exprs provides details of.

Cocoon uses this transformation strategy for two reasons. First, transforming
a _path expression_ (i.e., use of a variable) requires violating borrowing
rules: The transformation inserts a call to check_ISEF_unsafe, which needs to
take a reference to the path but return the expression, as Fig. 5c’s path row
shows. Second, avoiding transformations in the executed version potentially
reduces compile- and run-time costs of the transformations (depending on how
the compiler operates).

##### Restricting overloaded operators

Rust allows applications to overload certain operators (e.g., + and <) by
defining custom functions for their behavior. Should an application overload,
for example, the + operator, the expression a + b might no longer be side-
effect free. Cocoon’s procedural macro cannot detect whether a + b invokes an
overloaded operator because it operates on a parse tree without type
information. To address this problem, Cocoon’s procedural macro replaces all
calls to _overloadable_ operators with a call that implements the default
operator behavior.

Specifically, Cocoon provides a series of internal traits (e.g.,
cocoon::SafeAdd to replace std::ops::Add) that are essentially copies of the
standard Rust traits for each overloadable operator. Cocoon implements these
traits for all applicable standard Rust types. Cocoon’s procedural macros
replace $e_{1}$ + $e_{2}$ with ::Cocoon::SafeAdd::safe_add($e_{1}$, $e_{2}$)
in side-effect-free contexts. In this way, Cocoon allows the use of
overloadable operators only on standard Rust types, for which the behavior is
the original, Rust-standard side-effect-free behavior. Any use of these
operators on application-defined types within a side-effect-free context
results in a compilation error. Fig. 5c shows this transformation for $e_{1}$
+ $e_{2}$; the transformation is analogous for other overloadable operators.

Code cannot circumvent this restriction by overloading operators on built-in
Rust types (e.g., numeric types): Overloadable operators are defined by built-
in Rust traits, and Rust does not permit a crate to implement a trait for a
type unless the crate defines the trait or the type (or both).

##### Restricting deref coercion and custom destructors

One of Rust’s features is that, in attempting to find a match for a function
or struct signature, the Rust compiler performs _deref coercion_ ,
automatically inserting dereference calls until it finds a match for the
signature or cannot dereference any further. The compiler will automatically
convert s.area() to s.deref().area() if s has type &Shape and method
Shape::area() exists. It will convert b.area() to b.deref().deref().area() if
b has type &Box<Shape> and method Shape::area() exists. This situation
presents a challenge because a call to s.area() can implicitly invoke
s.deref() or s.deref().deref() in a way that is invisible to Cocoon’s
procedural macro. Deref::deref() and DerefMut::deref_mut() for built-in types
have no side effects, but an application could define a deref() or deref_mut()
method that has side effects.

Another problematic Rust feature is that applications can define custom
destructor behavior. The compiler inserts a _drop_ (i.e., deallocation) of a
value in the code where the value dies. The application can provide custom
behavior on drop by implementing the Drop trait on an application type and
providing an implementation of Drop::drop()—which could have a syntactically
invisible side effect.

To handle these operations, the procedural macros insert code to ensure that
_every value used by or created in_ a side-effect-free context does not
provide a custom implementation of Deref, DerefMut, or Drop. Cocoon provides a
trait InvisibleSideEffectFree that can be implemented by any type that (1)
does not provide a custom implementation of Deref::deref(),
DerefMut::deref_mut(), or Drop::drop() and (2) contains only
InvisibleSideEffectFree values (LABEL:fig:traits). Cocoon implements
InvisibleSideEffectFree for conforming Standard Rust types, e.g., i64 and
Box<T: InvisibleSideEffectFree> implement InvisibleSideEffectFree, among many
others. Conforming application types do not automatically implement
InvisibleSideEffectFree, but an application type can be annotated with
#[derive(InvisibleSideEffectFree)] (Fig. 3f), which invokes a procedural macro
that transforms the type’s definition to ensure that (1) it does not implement
Deref, DerefMut, or Drop (by generating negative implementations of these
traits) and (2) all of the type’s contained values have types that implement
InvisibleSideEffectFree (by generating type constraints on the contained
values).

To ensure that side-effect-free contexts only use and create
InvisibleSideEffectFree values, Cocoon’s procedural macro transforms several
kinds of expressions $e$ to check_ISEF($e$) as Figs. 5b and 5c show. The
expression check_ISEF($e$) simply returns the value $e$ evaluates to, but
$e$’s type must be InvisibleSideEffectFree to compile.

Not every expression needs to be wrapped in check_ISEF(), as Fig. 5c shows.
For example, the field expression $e$.field does not need to be wrapped
because it is InvisibleSideEffectFree as long as $e$ is
InvisibleSideEffectFree ($e$ still needs to be wrapped in check_ISEF() in
general).

Note that secret blocks are not prevented from _capturing_ all non-
InvisibleSideEffectFree types, but it is sufficient for secret blocks to be
prevented from creating _creating_ or _using_ such types. Specifically,
VisibleSideEffectFree, which defines types that can be captured by secret
blocks, does _not_ negatively implement all InvisibleSideEffectFree types
(because it does not seem possible due to limitations of auto traits and
negative implementations). Instead, VisibleSideEffectFree excludes
implementation of all &T where T does _not_ implement InvisibleSideEffectFree
(LABEL:fig:traits), which disallows captures of non-InvisibleSideEffectFree
variables by reference, but not by value.

##### Handling exceptional flow

To avoid implicit flows, a secret block must have a single static exit. Even
if the block’s body executes return, continue, or break, control always
continues immediately after the block, since a secret block’s body is wrapped
in a closure (Fig. 4a).

A remaining problem are _panics_ , which Rust generates for unexpected or
unrecoverable errors. By default, a panic aborts the execution, creating a
termination channel if a secret block (or code it calls) panics. Worse yet,
the application might _catch_ a panic outside of a secret block, creating an
implicit flow. To avoid this, every secret block catches any panics (using
std::panic::catch_unwind), which it handles by returning a Secret-wrapped
default value (Secret-wrapped types must implement std::default::Default) and
continuing execution after the block normally, as Fig. 4a shows.

####  4.3.3. Example transformation

Expansion of secret_block!(lat::AB { wrap_secret(0) }):

⬇

if true {

/* Expansion by $\tau(e,\mathit{T})$ */

::cocoon::call_closure::<lat::AB, _, _>(

(|| -> _ {

let result = ::std::panic::catch_unwind(::std::panic::AssertUnwindSafe(|| {

/* Expansion of wrap_secret(0) */

let tmp = 0; unsafe { ::cocoon::Secret::<_, lat::AB>::new(tmp) }

})).unwrap_or_default();

result

}))

} else {

/* Expansion by $\tau(e,\mathit{F})$ */

::cocoon::call_closure::<lat::AB, _, _>(

(|| -> _ {

/* Expansion of wrap_secret(0) */

unsafe { ::cocoon::Secret::<_, lat::AB>::new(0) }

}))

}

Figure 7. The secret block at line 3 of Fig. 2, after expansion by Cocoon’s
procedural macro secret_block!.

⬇

if true {

/* Expansion by $\tau(e,\mathit{T})$ */

::cocoon::call_closure::<lat::AB, _, _>(

(|| -> _ {

let result = ::std::panic::catch_unwind(::std::panic::AssertUnwindSafe(|| {

if /* Expansion of unwrap_secret(available) */

{ let tmp = available;

unsafe { ::cocoon::Secret::unwrap::<lat::AB>(tmp) } } &&

/* Expansion of unwrap_secret_ref(::std::option::Option::unwrap(

::std::collections::HashMap::get(&bob_cal, &day))) */

*{ let tmp = ::std::option::Option::unwrap(

::std::collections::HashMap::get(&bob_cal, &day));

unsafe { ::cocoon::Secret::unwrap_ref::<lat::AB>(tmp) } }

{

/* Expansion of *unwrap_secret_mut_ref(&mut count) += 1; */

*{ let tmp = &mut count;

unsafe { ::cocoon::Secret::unwrap_mut_ref::<lat::AB>(tmp) } } += 1;

}

}))

.unwrap_or_default();

result

})

)

} else {

/* Expansion by $\tau(e,\mathit{F})$ */

::cocoon::call_closure::<lat::AB, _, _>(

|| -> _ {

if /* Expansion of unwrap_secret(available) */

unsafe {

::cocoon::Secret::unwrap::<lat::AB>(

{ let tmp = &(available); unsafe { ::cocoon::check_ISEF_unsafe(tmp) } }) } &&

/* Expansion of unwrap_secret_ref(::std::option::Option::unwrap(

*unsafe {

::cocoon::Secret::unwrap_ref::<lat::AB>({

::cocoon::check_ISEF(::std::option::Option::unwrap({

::cocoon::check_ISEF(::std::collections::HashMap::get(

{ ::cocoon::check_ISEF_ref(&bob_cal) },

{ ::cocoon::check_ISEF_ref(&day) })) })) }) }

{

/* Expansion of *unwrap_secret_mut_ref(&mut count) += 1; */

::cocoon::SafeAddAssign::safe_add_assign(

&mut *(unsafe { ::cocoon::Secret::unwrap_mut_ref::<lat::AB>(

{ ::cocoon::check_ISEF((&mut count)) })

}), 1);

}

})

}

Figure 8. The secret block at lines 5–11 of Fig. 2, after expansion by
Cocoon’s procedural macro secret_block!.

Figs. 7 and 8 show how the secret_block! procedural macro transforms Fig. 2’s
first and second secret blocks, respectively.

###  4.4. Implementation Details

Our prototype implementation of Cocoon is divided into two Rust crates—one
that defines the procedural macros and another that provides all other Cocoon
functionality—since procedural macros must be defined in their own crate. The
implementation depends on a _nightly_ version of Rust (1.69.0-nightly) since
it uses a few Rust features that are not yet stable: auto traits, negative
traits, function traits, and unboxed closures. We will release Cocoon’s source
code publicly upon paper publication.

###  4.5. Security Guarantees and Threats

Cocoon aims to provide termination-insensitive noninterference, excepting
declassify operations and unsafe Rust code (§ 3.2). Here we discuss a few
additional caveats of Cocoon’s guarantees.

#### Trusted codebase

Allowlisted Rust Standard Library functions must be trusted to be side-effect
free. Identifying side-effect-free library functions accurately is potentially
error prone: A function with a side-effect-free specification might have
(externally detectable) side effects internally, or an update to the library
implementation could introduce side effects.

In general, every component of an application (whether part of the
application’s crate or an external crate) must be ported to Cocoon, or it must
be trusted to be side-effect free. Porting components to Cocoon provides an
incremental mechanism for reducing the trusted codebase.

Programmers must audit not only any declassify operations or unsafe Rust code
in their applications, but also the application’s Cargo.toml file, which
specifies the names and locations of external crates and could potentially
point to untrusted versions of Cocoon or the Rust Standard Library.

#### Macros

What if application code calls an untrusted macro that transforms a secret
block (e.g., evil_macro!(secret_block!(...)))? Fortunately, the Rust
compiler’s macro expansion algorithm iteratively expands macros, starting from
the outermost macro. The resulting expansion is repeatedly expanded, until no
macros are left in the expansion. If an application macro expands to contain a
call to Cocoon’s macro, Cocoon’s macro’s expansion is opaque to the
application macro.

All accesses to secret values must occur in macros—except for calls to
declassify() methods. However, the potential threat is mitigated by the fact
that declassify() calls must be audited. Alternatively, one could change
Cocoon so values are declassified with a macro instead of a method.

###  4.6. Limitations

Cocoon’s current design has some drawbacks that limit its practicality as a
full-featured language-level IFC approach. It may be possible to remove these
limitations in future work.

Cocoon’s current design supports only static secrecy labels, not integrity
labels or dynamic labels (i.e., labels as run-time values). We are not aware
of any properties of Cocoon that would preclude adding support for dynamic
labels and integrity labels while continuing to meet the requirements
described in § 3.2, except that dynamic labels would impact run-time
performance.

The current design does not allow the use of overloaded operators in secret
blocks. Likewise, the current design disallows application types that
implement custom dereference (Deref and DerefMut) and destructor (Drop)
operations. We believe that this is not very restrictive because these traits
are most useful for implementing abstract data types (ADTs) (in fact, the Rust
documentation666https://doc.rust-lang.org/1.23.0/std/ops/trait.Deref.html
emphasizes that Deref should only be implemented by programmers when defining
smart pointers). As a result, only a few “kernel” ADTs are needed for most
software.

Secret blocks cannot use macros. Due to the Rust compiler’s macro expansion
algorithm, which expands the outermost macro first and iteratively works its
way through the resulting expansion (§ 4.5), Cocoon cannot inspect a macro’s
expansion within a secret block and thus cannot certify that it is side-effect
free. It may be possible to extend Cocoon’s macro to recognize known macros
such as vec! and generate code using the appropriate macro expansion, but we
have not done so.

Secret blocks cannot use interior mutability. In our experience, interior
mutability is rare in real code: None of the case studies or performance
benchmarks in § 5.4 use interior mutability in secret blocks.

Calls from side-effect-free code to allowlisted Rust Standard Library
functions must be fully qualified (§ 4.3.1). A future implementation could
eliminate this requirement by automatically rewriting function calls to match
their fully qualified names. To avoid ambiguity of function names, Cocoon
could disallow side-effect-free application functions from having the same
name as allowlisted library functions, or it could require the application to
disambiguate ambiguous calls.

##  5\. Evaluation

This section evaluates the performance and usability of Cocoon. We integrated
Cocoon with two applications (Spotify TUI and Servo), finding that
applications can start reaping the benefits of the library with limited
modifications. We also wrote Cocoon and non-Cocoon versions of a Battleship
program. Using performance benchmarks, we evaluated the worst case for
performance—all application code accesses secret values—and found that Cocoon
increases compile times by 7–53% but has no detectable impact on executable
size or run-time performance.

All experiments were executed on a quiet machine with a 16-core Intel Xeon
Gold 5218 at 2.3 GHz with 18 GB RAM running Linux.

###  5.1. Case Study: Spotify TUI

Spotify TUI (text-based user interface) is a Spotify client written in Rust
that allows an end user to interact with Spotify from a terminal. We chose it
as a case study because it is a popular project on
GitHub777https://github.com/Rigellute/spotify-tui with over 13,000 “stars.”

We modified Spotify TUI to use Cocoon to protect a value called the _client
secret_ , which is akin to a user password. The client secret is a 32-digit
hexadecimal string that Spotify TUI uses to authenticate with the Spotify API
server. Leaking the client secret to an adversary would allow the adversary to
make Spotify API calls on behalf of the victim user.

Spotify TUI receives the client secret from the command line, or from a file
that a previous execution of Spotify TUI wrote the client secret to. We
modified these code locations to wrap the client secret as a
Secret<String,Label_A>. (For this application we use a simple label scheme in
which $\\{A\\}$ and $\emptyset$ are the only labels, representing secret and
non-secret values, respectively.) Spotify TUI must send the client secret
outside of the application in two different ways: (1) writing the client
secret to a file; or (2) sending the client secret to two external Rust
libraries, RSpotify (a Rust wrapper for the Spotify Web API) and Serde (a Rust
serialization library).

By retrofitting the Spotify TUI application to use Cocoon, we implicitly treat
Spotify TUI as untrusted (except for its declassify calls and any unsafe
blocks). Spotify TUI must declassify the client secret in order to write it to
a file and to send it to RSpotify and Serde (because these components do not
integrate with Cocoon), implicitly treating the OS and the separate libraries
as part of the trusted codebase. Removing RSpotify and Serde from the trusted
codebase would require retrofitting them with Cocoon by annotating their side-
effect-free functions (§ 4.5).

⬇

1fn validate_client_key(key: &str) -> Result<()> {

2 if key.len() != EXPECTED_LEN {

3 Err(Error::from(std::io::Error::new(

4 std::io::ErrorKind::InvalidInput,

5 format!("invalid length: {} (must be {})", key.len(), EXPECTED_LEN,),

6 )))

7 } else if !key.chars().all(|c| c.is_digit(16)) {

8 Err(Error::from(std::io::Error::new(

9 std::io::ErrorKind::InvalidInput,

10 "invalid character found (must be hex digits)",

11 )))

12 } else {

13 Ok(())

14 }

15}

(a) Original code

⬇

1fn validate_client_key(key: &Secret<String, Label_A>) -> Result<()> {

2 const EXPECTED_LEN: usize = 32;

3 let sec_error_string = secret_block!(Label_A {

4 let u_key = unwrap_secret_ref(key);

5 let mut is_hex = true;

6 for c in ::str::chars(&u_key) {

7 if !::char::is_digit(c, 16) {

8 is_hex = false;

9 }

10 }

11 let mut error_string = ::std::string::String::from("");

12 if ::std::string::String::len(&u_key) != EXPECTED_LEN {

13 error_string = /* create string "invalid length: {key.len()} (must be
{EXPECTED_LEN})" */;

14

15 } else if !is_hex {

16 error_string = ::std::string::String::from("invalid character found (must
be hex digits)");

17 }

18 wrap_secret(error_string)

19 });

20

21 let error_string = sec_error_string.declassify();

22 if !error_string.is_empty() {

23 Err(::std::error::Error::from(::std::io::Error::new(

24 ::std::io::ErrorKind::InvalidInput,

25 error_string,

26 )))

27 } else {

28 Ok(())

29 }

30}\end{lstlisting}

31 {\small \sf (b) \Ifclib-retrofitted code}

32 %\\\\\mike{Code needs some changes to match the \ifclib usage in the rest
of the paper.} \ada{I updated the labels and declassify call - that looks like
the only necessary changes to me} \mike{Yeah I think that’s it. Can you check
the next two figures?} \ada{yep}

33 \caption{Spotify TUI code that validates that the client secret is a
32-digit hexadecimal string.}

34 \label{fig:Spotify-Validation}

35\end{figure}

36

37% Commented out from if block in above figure

38%::str::to_string("invalid length: ")

39% + &*::usize::to_string(&::std::string::String::len(&u_key))

40% + &*::str::to_string(" (must be ") + &*::usize::to_string(&EXPECTED_LEN)

41% + &*::str::to_string(")");

42

43%\subsubsection*{Code excerpts}

44

45Next, we show a snippet of Spotify TUI code before and after retrofitting it
to use \ifclib.

46% to make the client secret be a \code{Secret<String,Label_A>}.

47%\ada{TODO: Rewrite to remove \autoref{fig:Spotify-Validation} and
\autoref{fig:Spotify-Write} I don’t think these changes are particularly
relevant. We should instead present the modification to
\lstinline|client_secret|, not how it’s used. Readers will have access to the
code if they want to see the code in \autoref{fig:Spotify-Validation}. This
change will bring the spotify-tui section in line with servo and reduce
space.}

48%

49%\paragraph{Validation of the client secret}

50%

51\autoref{fig:Spotify-Validation} shows a Spotify TUI function that validates
that the client secret

52% an input ‘‘key,’’ which could be either the client ID or client secret,

53is 32 hexadecimal digits. The function returns a \code{Result} indicating
either \code{Ok} or \code{Err}.

54\autoref{fig:Spotify-Validation}(a) shows the original code and
\autoref{fig:Spotify-Validation}(b) shows how we changed the code to account
for the client secret being a \code{Secret} value.

55% The retrofitted code shows a differently named function,
\code{validate_client_secret}, which it uses only for validating the client
secret; it continues to use \code{validate_client_key} for the (non-secret)
client ID, which has the same format requirements.

56%\mike{I thought the differently named functions was a confusing detail, so
I removed it and gave the function the same name in the figure. Note that we
could actually make the presented code work by assigning a different name to
the non-\ifclib version of the function.} \ada{sounds good.}

57% retrofitted with \ifclib after marking the client secret as a achieve the
same result for the client secret, a \code{Secret} type.

58

59To perform the validation logic,

60%the retrofitted code creates a secret block that processes the block’s code
with a procedural macro.

61the modified code creates a secret block to check that each digit within the
client secret is a hexadecimal character. Note that we had to manually
implement the string formatting and hexadecimal character check, as opposed to
using \code{|c| c.isdigit(16)}, since the \ifclib implementation does not
support

62% function or

63% \mike{?}

64closure calls within secret blocks.

65

66%Because our prototype implementation’s procedural macro does not currently
support functions containing macro calls or closure invocations, we had to
write the retrofitted code to perform the logic using expanded code that does
not call the macro \code{format!} or use the inlined closure (\code{|c|
c.isdigit(16)}). %The secret block calls only allowlisted side-effect-free
functions in the Rust Standard Library; it always uses the fully qualified
name (e.g., \code{::std::string::String::len}) to eliminate any ambiguity
(\autoref{sec:application-defined-functions-visible}).

67

68% In theory, the block could return a \code{Result}. However, the
implementation of \code{Result} uses interior mutability, so
\code{Secret<Result,Label_A>} is disallowed (\autoref{sec:application-defined-
functions-visible}).

69% Instead, we wrote

70%\mike{Correction to text that was previously here: \lstinline{Result} isn’t
interior mutable. Or at least I was able to use \lstinline{Result} in a secret
block just by implementing \lstinline{InvisibleSideEffectFree} for
\lstinline{Result}. So I think using \lstinline{Result} in this case would be
an option. But for now I revised the text to just say what the code does, not
that we’re avoiding using \lstinline{Result}.}%

71The secret block populates an error string, which it leaves empty in the
event of no error, and

72%The retrofitted code passes the string as the mutable parameter to
\code{apply_ternary_mut_ref}.

73the retrofitted code declassifies the error string because in the event of
an error, it must report the error. Declassifying the error string is
acceptable leakage because knowing \emph{whether} the client secret is
correctly formatted is not security sensitive. The retrofitted code in
\autoref{fig:Spotify-Validation}(b) ultimately returns a \code{Result}, just
as in \autoref{fig:Spotify-Validation}(a). Thus, \autoref{fig:Spotify-
Validation}(b) achieves the same behavior for the client secret without
declassifying the secret\---but rather by declassifying only whether the input
client secret is not in the correct format, which is not exploitable
information.

74

75\iffalse

76\begin{figure}[t]

77 \centering

78 \lstset{numbers=left,basicstyle=\ttfamily\scriptsize}

79 \begin{lstlisting}

80pub fn load_config(&mut self) -> Result<()> {

81 ... /* Includes initialization of config_yml: ClientConfig */

82 let content_yml = serde_yaml::to_string(&config_yml)?;

83

84 let mut new_config = fs::File::create(&paths.config_file_path)?;

85 write!(new_config, "{}", content_yml)?;

86

87 self.client_id = config_yml.client_id;

88 self.client_secret = config_yml.client_secret;

89 self.device_id = config_yml.device_id;

90 self.port = config_yml.port;

91}

(a) Original code

⬇

1pub fn load_config(&mut self) -> Result<()> {

2 ... /* Includes initialization of serializable_config_yml:

3 Secret<SerializableClientConfig, Label_A> */

4 let content_yml: Secret<String, Label_A> =

5
Secret::new(serde_yaml::to_string(serializable_config_yml.declassify_ref())?);

6

7 let mut new_config = fs::File::create(&paths.config_file_path)?;

8 let serde_yaml_str =
serde_yaml::to_string(serializable_config.declassify_ref())?

9 let content: Secret<String, Label_A> = secret_block!(Label_A {
wrap_secret(serde_yaml_str) });

10 write!(new_config, "{}", content.declassify())?;

11

12 let (all_but_secret, client_secret) = secret_block!(Label_A {

13 let u_config = unwrap_secret(serializable_config);

14 (wrap_secret((u_config.client_id, u_config.device_id, u_config.port)),

15 wrap_secret(u_config.client_secret))

16 });

17 let (client_id, device_id, port) = all_but_secret.declassify();

18

19 self.client_id = client_id;

20 self.client_secret = client_secret;

21 self.device_id = device_id;

22 self.port = port;

23}

(b) Cocoon-retrofitted code

Figure 9. Spotify TUI code that writes client configuration values, including
the client secret, and assigns them to a ClientConfig (self).

##### Writing the client secret to a file

Fig. 9 shows a function from Spotify TUI that writes a client configuration,
including the client secret, to a configuration file. The code first
serializes the client configuration to a string using the Serde serialization
library. It then writes the string to a file. Finally it transfers the
configuration from config_yml to self, both of which have type ClientConfig.

Fig. 9(b) shows how we modified this code to handle the client secret being
Secret. Because serializable structs cannot easily contain Secret—the Serde
serialization library cannot properly serialize a Secret—we replace
config_yml, which contains the client secret as a member with type
Secret<String,Label_A>, with serializable_config_yml, which has type
Secret<SerializableClientConfig,Label_A>. SerializableClientConfig is a new
type that is serializable because all of its member fields are non-secrets.
The retrofitted code thus declassifies serializable_config_yml and sends it to
Serde, the trusted serialization library, and writes the resulting string to a
file. (The code actually first wraps the resulting string in a Secret and then
immediately declassifies it, pedantically following our discipline of both
wrapping secret values from outside Spotify TUI as Secrets and declassifying
secret values before sending them to trusted libraries or files.)

Next, the retrofitted code needs to copy the client configuration from
serializable_config_yml, which is a Secret<SerializableClientConfig,Label_A>,
to self, which is a ClientConfig that contains a Secret<String,Label_A>. To
perform this copy _without declassifying the client secret_ , we define and
use a secret block that extracts the secret and non-secret fields into two
separate parts of its return value. The code then safely declassifies the non-
secret fields (all_but_secret) and stores all fields into self, an instance of
ClientConfig.

#### Empirical results

Table 2 shows that the annotation burden of protecting the client secret with
Cocoon is small: To retrofit Spotify TUI, we inserted 167 lines of code and
removed 54 lines in a codebase of over 12,000 lines.

Table 2’s last column shows how many times a call to a Secret::declassify
method appears in the retrofitted code of Spotify TUI. In 14 out of 17 cases,
the code declassifies secret data because the data needs to be sent outside of
the Spotify TUI codebase. In these cases, the client secret leaves the
codebase to be passed to RSpotify or Serde, or to be written to the
configuration file, all as intended. In the other 3 out of 17 cases, the code
declassifies secret values in ways that should not leak sensitive information.
For example, revealing the Result in LABEL:fig:Spotify-Validation(b) should
not present a security risk.

| Lines of source code |
---|---|---
Program | Original | Cocoon | Inserted | Deleted | Declassify calls
Spotify TUI | 12,169 | 12,282 | 167 | 54 | 17
Servo | 397,141 | 397,174 | 77 | 44 | 1
Battleship | 383 | 410 | 47 | 20 | 2

Table 1. Programmer burden for integrating three applications with Cocoon, in
terms of lines of code modified, and number of calls to declassify methods.

| Compile time (s) | Run time | Executable size (bytes)
---|---|---|---
Program | Original | Cocoon | Original | Cocoon | Original | Cocoon
Spotify TUI |  14.395 $\,\\!\pm\,\\!$ 0.031 |  14.395 $\,\\!\pm\,\\!$ 0.053 |  2868.711 $\,\\!\pm\,\\!$ 5.612 ns |  2822.784 $\,\\!\pm\,\\!$ 5.662 ns | 15,779,320 | 15,779,088
Servo |  312.579 $\,\\!\pm\,\\!$ 4.354 |  309.983 $\,\\!\pm\,\\!$ 4.262 |  183.817 $\,\\!\pm\,\\!$ 0.540 s |  184.086 $\,\\!\pm\,\\!$ 0.529 s | 403,548,416 | 403,547,984
Battleship |  2.068 $\,\\!\pm\,\\!$ 0.003 |  2.321 $\,\\!\pm\,\\!$ 0.002 |  30.240 $\,\\!\pm\,\\!$ 0.254 ms |  29.490 $\,\\!\pm\,\\!$ 0.272 ms | 6,727,464 | 6,740,248

Table 2. Comparison of performance costs for applications without Cocoon and
versions that use Cocoon. Execution times include 95% confidence intervals
based on multiple trials.

Table 2 shows the performance cost of retrofitting Spotify TUI to use Cocoon.
We compiled Spotify TUI 10 times, without and with integration with Cocoon,
using the “release” optimization level. According to the results, Cocoon has
no detectable impact on compile time. Cocoon has a modest impact on the size
of the compiled binary; in fact, Cocoon’s code size is actually smaller than
the original’s by 232 bytes, for reasons that are unclear to us. In theory,
the compiled code should be identical, but the additional code generated by
Cocoon’s macros could affect compiler decisions such as how aggressively to
inline.

To measure run time, we timed just the part of the code—configuration and
authentication—that deals with the client secret, in both the original and
retrofitted Spotify TUI. As the results show, the measured time is around
2,800 nanoseconds. We ran and timed this part of the code 100,000 times for
each version of Spotify TUI to account for high run-to-run variability. The
Cocoon version actually outperforms the original version by about 1%. We are
unsure of the reason for this (statistically significant and repeatable)
performance difference. Like the executable code size differences, the
performance difference could be the result of compiler decisions impacted by
the extra code generated by Cocoon’s macros.

###  5.2. Case Study: Servo

Servo is Mozilla’s browser engine written in Rust (Linux Foundation, 2022). We
selected Servo as an evaluation subject for two reasons. First, Servo is the
sixth-most popular Rust project on GitHub, with over 20,000 “stars.” Second,
Servo is an influential project, e.g., Rust’s early design was informed by
Mozilla’s experiences creating Servo. We used Cocoon in Servo to help enforce
a security policy that prevents different JavaScript programs from reading
each others’ user data.

To make an HTTP request, JavaScript programs call the Fetch API, which the
JavaScript engine implements by calling into Servo’s implementation to perform
the request and return a response. Critically, JavaScript programs are only
allowed to read HTTP responses if the programs share the same origin web
server, unless the response explicitly allows cross-origin sharing. Otherwise
a malicious JavaScript program such as a malicious advertisement could read
sensitive user data such as a password field from a login form from a trusted
JavaScript program originating from a different web server. This policy is
called the _same-origin policy_. Responses from different origin servers are
considered _opaque_ and cannot be read by JavaScript programs.

Fig. 10 shows how we modified Servo to use Cocoon. First, we modified the
Response type, which is instantiated after the client receives an HTTP
response from an origin server following an HTTP request, to use Cocoon’s
Secret type to protect the response body from being read without
declassification (lines 2 and 3).

⬇

1pub struct Response {

2\- pub body: Arc<Mutex<ResponseBody>>,

3\+ pub body: Arc<Mutex<Secret<ResponseBody,Label_A>>,

4 ...

5}

6

7pub fn get_body(&self) -> Arc<Mutex<ResponseBody>> {

8 if self.response_type == ResponseType::Opaque {

9 Arc::new(Mutex::new(ResponseBody::Empty))

10 } else {

11 secrets::declassify_transmute(self.body)

12 }

13}

Figure 10. Servo’s response structure. We modified the structure to use Cocoon
to enforce the same-origin policy.

Following this change, the application can read the response body only by
declassifying it. To implement the same-origin policy, the code should only
return the declassified value if the response type is not opaque, as shown in
lines 8–12 of Fig. 10. If the response is opaque, the code returns an empty
body (line 9), in accordance with the Fetch API specification. To return an
Arc<Mutex<ResponseBody>>, the code calls a declassify_transmute() method (line
11) provided by the Cocoon implementation; it is like other declassify methods
but returns a T<Secret<U>> value as a T<U>. Cocoon implements
declassify_transmute() safely without creating new data because T<Secret<U>>
is guaranteed to have the same layout as T<U>.

Instead of adding this same logic at the dozens of locations in Servo’s source
code that read Response::body, we changed all such locations to instead call
Response::get_body() (line 7).

Following this change, an opaque response’s body is not readable without a
declassify operation (or an unsafe block). Our changes explicitly reflect
developers’ intentions and prevent future changes from accidentally allowing
reads when the response body is opaque.

#### Empirical results

Table 2 (page 2) shows the effort to integrate Servo with Cocoon to protect
the response body. We modified dozens of lines of code to integrate Servo with
Cocoon. A significant number of the lines we modified reside in Servo’s test
suite (55). Many edits were made by our IDE’s search and replace feature. At
other source code locations, we had to introduce temporary variables because
of Rust’s lifetime analysis: Normally, the value returned by get_body
immediately dies (i.e., it is not usable by expressions later in the program).
Storing the return value in a temporary variable keeps the value alive while
the body is read.

Table 2 compares performance before and after integration with Cocoon. As for
Spotify TUI, we compiled Servo 10 times, with and without integration with
Cocoon. We observe that there is no statistically significant compile-time
overhead imposed.888For Servo, compile time includes the time for compiling
all dependent crates because Servo does not use the standard Rust build tools.
For all of our other evaluated programs, compile time includes only the time
to compile the target application. We ran Servo’s provided tests 20 times,
with and without integration with Cocoon. We find that Cocoon imposes no run-
time burden that is statistically significant (the confidence intervals
overlap). The executable code sizes differ by 432 bytes; as for Spotify TUI,
the exact reasons are unclear to us because of the substantial amount of code
involved and the complexity of the compiler.

###  5.3. Case Study: Battleship

Battleship is a classic game in which two players place ships at secret
locations on a grid. The object of the game is to sink the opponent’s ships by
correctly guessing their locations. A player wins by sinking all of the other
player’s ships first.

JRIF and Jif each employed Battleship as a case study; it is interesting as a
case study not only because confidentiality is needed to prevent cheating, but
also because secret data (ship placements) are revealed throughout the game
(Kozyri et al., 2016; Myers et al., 2006). An implementation of Battleship
should not reveal any of the locations of a player’s ships unless the opponent
correctly guesses it first. We implemented a multithreaded implementation of
Battleship that uses Cocoon to enforce this secrecy policy.

⬇

1#[derive(InvisibleSideEffectFree)]

2struct Player<L: Label> {

3 ship_positions: Secret<Grid<bool>, L>,

4 guesses: Grid<CellStatus>,

5}

Figure 11. Data structure representing each Battleship player’s game state.

⬇

1impl<L: Label> Player<L> {

2 fn new() -> Player<L> {

3

4 let ship_positions = secret_block!(L {

5 let ships = [Ship::Carrier, Ship::Battleship, Ship::Cruiser,
Ship::Submarine, Ship::Destroyer];

6 let mut ship_positions: Grid<bool> = [[false; GRID_SIZE]; GRID_SIZE];

7 for ship in ships {

8 let placement: Placement = random_placement(&ship_positions, &ship);

9 place_ship(&mut ship_positions, &ship, &placement);

10 }

11 wrap_secret(ship_positions)

12 });

13

14 Player {

15 ship_positions,

16 guesses: [[CellStatus::Unguessed; GRID_SIZE]; GRID_SIZE],

17 }

18 }

19}

20#[side_effect_free_attr]

21fn random_placement(grid: &Grid<bool>, ship: &Ship) -> Placement {

22 let mut ship_placement: Placement = random_maybe_illegal_placement(grid,
ship);

23 while !legal_placement(&grid, ship_placement) {

24 ship_placement = random_maybe_illegal_placement(grid, ship);

25 }

26 ship_placement

27}

Figure 12. Battleship player initialization routines.

⬇

1fn game_loop_a(mut player: Player<lat::Label_A>, chan:
session_types::Chan<(), PlayerA>) {

2 let mut c = chan.enter();

3 let mut player_b_guesses = [[CellStatus::Unguessed; GRID_SIZE]; GRID_SIZE];

4 loop {

5 // Not shown: Display user’s previous guesses, prompt user to make new
guess, send guess to opponent.

6

7 // Receive opponent’s guess.

8 let (c3, guess) = c.recv();

9

10 // Decide if the opponent hit our ship.

11 let is_hit: bool = secret_block!(lat::Label_A {

12 wrap_secret(is_occupied(unwrap_secret_ref(&player.ship_positions), guess.0,
guess.1))

13 }).declassify();

14

15 // Not shown: Update opponent’s guesses. Exit loop if guess won the game.

16 }

17}

18

19#[side_effect_free_attr]

20fn is_occupied(grid: &Grid<bool>, row: usize, col: usize) -> bool {
(&grid[row])[col] }

Figure 13. Main Battleship game loop.

Fig. 13 shows the data structure that represents each player’s game state.
Line 1 uses the #[derive(InvisibleSideEffectFree)] macro to assert that the
data structure is safe to use from within side-effect-free contexts. The
struct uses a generic secrecy label (line 2) so that the Player data structure
can represent both players using distinct labels. Line 3 shows how the
ship_positions field, which stores secret ship placement values, has Secret
type. The player’s guesses are low-secrecy values since they are announced to
their opponent, and thus the value of guesses is not wrapped in Secret.

Fig. 13 shows the Player initialization routine, which preserves the
confidentiality of Player::ship_positions. Line 4 begins the secret block that
initializes a player’s ship placements. The secret block iterates through the
ships in the game and places them onto a grid. The secret block calls
random_placement, which is annotated with #[side_effect_free_attr],
demonstrating Cocoon’s effect system. Note that random_placement calls more
application functions (legal_placement and
random_maybe_illegal_placement—definitions not shown).

The main game logic is shown in Fig. 13. The players communicate over the
channel chan. This code prints Player A’s guesses (public information), then
prompts Player A to make a new guess (public information). The code then sends
the guess to Player B over chan. Player B uses the same channel to communicate
if the guess hit a ship or ended the game. Next, Player A receives Player B’s
guess (line 8). The game loop uses a secret block on line 11 to decide if
Player B scored a hit. This is necessary because the player’s ship placements
are secret.

#### Empirical results

Table 2 compares two versions of the Battleship implementation: one with
Cocoon, and one without it. The Cocoon changes affect a significantly larger
fraction of the code than for Spotify TUI and Servo. There are two calls to
declassify in Battleship. Both occur in a player’s game loop to decide if
their opponent correctly guessed a ship location.

Table 2 shows the effect of Cocoon on compilation times, run times, and
executable sizes, using the same methodology as for Spotify TUI and Servo.
Cocoon slows compilation time by 12%—more than for Spotify TUI and Servo,
which makes sense because a larger fraction of Battleship’s code is in secret
blocks and side-effect-free functions. Cocoon adds no run-time overhead—in
fact, as for Spotify TUI, it decreases run time inexplicably, perhaps as a
result of different compiler optimization decisions—showing that the compiler
effectively optimizes away the type-checking scaffolding added by Cocoon.
Finally, Cocoon increases executable size by 0.1%, for unknown reasons,
possibly again due to compiler optimization differences.

###  5.4. Performance-Focused Evaluation

To measure the worst-case performance impact of Cocoon, we evaluated wrapping
entire programs in secret blocks. We used benchmarks from The Computer
Language Benchmarks Game (Debian benchmarksgame-team, 2022), for which
developers create the most efficient implementations possible, in order to
compare the performance of different programming languages. We modified the
best-performing Rust implementations to perform all of their computations with
the primitives Cocoon introduces. In each case, we can conclude with high
cofidence that Cocoon adds negligible (¡1%) or nonexistent runtime overhead
and increases compile time by 7–16% with the exception of n-body, which
increased compile time by 53%. See Appendix A for details.

##  6\. Related Work

In the mid-1970s, Lampson first discussed information confinement as
preventing even the partial leak of confidential information (1973), while
Rotenberg introduced a mechanism to constrain systems from allowing secret
data to flow to untrusted entities (1973); these works became the concept of
information flow control (IFC). Denning first defined a lattice structure for
applying information flow policies (1976) and later observed that static
analysis can be used for IFC (Denning and Denning, 1977). Building on the
static analysis models of the 1970s, Myers and Liskov introduced a
decentralized model in which applications declassify their own data as opposed
to relying on a third-party authority to do so (1997).

Prior systems have provided coarse-grained, inter-process IFC between
processes, sockets, files, and other OS-level entities using dynamic tracking
(Zeldovich et al., 2008; Krohn et al., 2007). In contrast, fine-grained IFC at
the programming language level presents unique challenges. First,
communication within a process, which involves the flow of data and control
between program-level elements such as values and expressions, is less
explicit than the flow between processes and other OS-level entities, making
it difficult to track information flow soundly and precisely. Second,
language-level flow has higher bandwidth, so the cost of tracking it at run
time can be substantial.

Existing language-level IFC operates either dynamically at run time or
statically at compile time.

###  6.1. Dynamic IFC

Dynamic IFC tracks and checks labels of variables and values at run time.
Austin and Flanagan showed how to speed up dynamic tracking of labels for
JavaScript programs, but their approach still adds significant run-time
overhead (2009). Laminar tracks labels at run time for Java programs and
handles implicit flows by consigning secret operations to lexically scoped
regions, but still adds up to 56% run-time overhead (Roy et al., 2009). Co-
Inflow provides dynamic coarse-grained IFC for Java programs through the use
of implicitly inserted labels (Xiang and Chong, 2021). Converting a Java
program to use Co-Inflow requires few annotations and achieves relatively high
precision, but introduces an average run-time overhead of 15%.

###  6.2. Static IFC

Static IFC can be provided by whole-program analysis or modular type-based
analysis.

#### Whole-program static analysis

Whole-program static analysis computes information flow conservatively by
abstracting data and control flow across program expressions and variables
(Hammer et al., 2006; Zanioli et al., 2012; Balasubramanian et al., 2017;
Hedin and Sabelfeld, 2012). It minimizes programmer effort by eschewing the
need for type annotations, but it is non-compositional: Precision loss
analyzing one part of the program affects precision analyzing other parts of
the program. Non-compositionality makes it hard to scale to large programs and
hard to deploy incrementally.

Recent work introduces whole-program static analysis for information flow in
Rust called Flowistry (Crichton et al., 2022). Flowistry leverages Rust’s
ownership constraints to compute relatively precise function summaries without
actually analyzing the functions’ bodies. As such, Flowistry is scalable
enough to use interactively, and it naturally handles calls to functions for
which source code is unavailable. However, Flowistry is inherently
intraprocedural; Crichton et al. suggest that future work “could build an
interprocedural analysis by using Flowistry’s output as procedure summaries in
a larger information flow graph” (Crichton et al., 2022). As an
intraprocedural analysis, Flowistry is not applicable to checking for illegal
flows in our evaluated programs, which have secret values that flow
interprocedurally. As a static analysis approach, Flowistry may report false
flows, which are hard for programmers to deal with. In contrast, Cocoon uses
static type-based analysis, which requires program modifications but provides
a way to ensure that no illegal flows exist. Flowistry and Cocoon are
potentially complementary: Because Flowistry targets Rust and is fairly
precise, it could potentially be adapted as a tool to help automatically infer
labels in applications using Cocoon. But Flowistry cannot replace Cocoon
because Flowistry is a conservative, intraprocedural static analysis.

#### Modular static type-based analysis

Static type-based approaches extend the type system with IFC labels, so the
static type of every expression and variable includes an IFC label. In
contrast with whole-program static analysis, static type-based analysis is
compositional because typing rules can be checked locally (i.e., one
expression at a time) instead of globally. As a result, type-based analysis
offers the potential to allow large programs to provide IFC without false leak
reports or run-time overhead. A downside of type-based analysis is that it
creates extra work for programmers to express types, although this burden can
be limited to parts of the program that touch data with non-empty labels. A
key drawback of type-based analysis is that mainstream imperative languages
such as Java, C, C++, C#, and Rust do not provide type systems that are
expressive enough to ensure that operations on secret values do not have
unchecked side effects. As a result, existing solutions either use a
functional language (Russo, 2015; Gregersen et al., 2019) or extend an
imperative language (Myers, 1999; Myers et al., 2006; Myers and Liskov, 1997;
Kozyri et al., 2016; Chong, 2008; Simonet, 2003; Chapman and Hilton, 2004;
Smith and Volpano, 1998; Volpano et al., 1996).

MAC is a static type-based IFC library for Haskell that leverages the fact
that operations in pure functional languages are side-effect free (Russo,
2015). Likewise, DepSec is a dependently typed static IFC library for Idris
(Gregersen et al., 2019), a dependently typed language influenced by Haskell
(Brady, 2007). High-performance programs are typically not written in these
languages.

To add static type-based IFC to imperative languages, prior work extends the
language and provides a separate compiler. Jif is an extension of Java that
provides static type-based IFC (Myers, 1999; Myers et al., 2006; Myers and
Liskov, 1997). Jif introduces types that represent secrecy and integrity
labels, which programs use to annotate variables and expressions. Jif provides
a compiler for the Jif language that checks types and flows, including
implicit flows, and produces pure Java code with the same functionality as the
original program. Jif includes a variety of features such as support for
dynamic labels and automatic inference. Follow-on research has extended Jif to
solve a wide variety of IFC-related problems, such as erasure policies and
reactive information flow (Chong, 2008; Kozyri et al., 2016). The key drawback
of Jif is that it requires programs to be written in a non-mainstream language
and to be processed with a non-mainstream compiler, hampering adoption.

Flow Caml extends Objective Caml with a type system to track variable secrecy
levels without requiring programmers to annotate the source code (Simonet,
2003). While Flow Caml has full type inference, it does not support many of
the object-oriented features of Objective Caml, such as polymorphic variables
or labels. Chapman and Hilton similarly extended SPARK Ada and the SPARK
Examiner to include variable annotations (2004). This extension does not
support concurrency, and their declassification mechanism requires hiding the
body of the declassifying subprogram from the Examiner. Volpano, Smith, et al.
developed a model for IFC type systems in imperative languages that they later
extended to support multithreading and non-interference, but (as far as we
know) this model has not been implemented (1998; 1996).

RLBox is an approach for sandboxing libraries to prevent cross-library leaks
(Narayan et al., 2020). It uses a combination of static type-based analysis
and run-time isolation to prevent data and control from transferring between
libraries. RLBox, which targets C++ libraries, cannot provide a guarantee of
side-effect freedom, but rather requires programmers to write a validation
check when handling tainted values. RLBox adds run-time and space overheads,
unlike Cocoon. Another difference is that Cocoon’s secrecy labels allow a
hierarchy of labels, while RLBox only has a binary label: A value is “tainted”
or it is not.

##  7\. Conclusion

Cocoon is the first static type-based IFC approach for an imperative language
that uses the standard language and compiler. The key technical contribution
of Cocoon is its establishment of an effect system that tracks whether Rust
functions have side effects. As a result, Cocoon allows programmers to define
and perform arbitrary operations on secret data while ensuring that these
operations do not violate IFC rules, all in pure Rust. Cocoon can be
incrementally deployed on existing systems without significantly affecting
performance.

###### Acknowledgements.

Thanks to Ethar Qawasmeh for help in the early stages of the project, Chris
Xiong for help with code and ideas, and Chujun Geng for helpful feedback and
discussions. Thanks to the anonymous reviewers for valuable feedback.

##  Appendix A Details: Performance-Focused Evaluation

This section provides full details for the performance-focused evaluation (§
5.4). To place all of a benchmark’s computation in a secret block, we placed
the subroutines that perform the benchmark’s primary calculations inside of a
secret block, and annotated the blocks’ transitive callees as side-effect-free
functions. Meanwhile, we directed Cocoon’s procedural macros to ignore calls
to functions in external crates.

We evaluated 9 out of 10 available benchmarks (Debian benchmarksgame-team,
2022),excluding reverse-complement because it concurrently modifies a shared
mutable buffer, which constitutes a side effect.

Table 3 shows results of each benchmark with and without our modifications to
use Cocoon. We observe that there are few statistically significant
differences in run time (wall clock time) between the original and Cocoon
versions, and confidence intervals are tight enough that we can conclude with
high confidence that Cocoon adds negligible ($<\,$1%) or nonexistent
overhead—and speeds up programs as often as it slows them down, suggesting
that run-time differences are due to indirect effects such as compiler
decisions or microarchitectural sensitivities.

Cocoon increases compile time because its procedural macro adds significant
“scaffolding” code for type checking, which is generally “compiled away,” so
it does not translate to an increase in run time. The table shows that
compile-time overhead ranges from 7% to 16% for all programs except n-body,
which has 53% compile-time overhead. These overheads represent an extreme case
in which all code is transformed by Cocoon’s procedural macros. In practice,
only a program’s computations on secret values need to be transformed, which
is why the compile-time overheads for Spotify TUI and Servo are significantly
lower (Table 2).

The benchmark suite additionally reports run-time memory usage (maximum
resident set size). The results, which we omit for brevity, show that space
overhead is negligible or nonexistent for all programs, i.e., confidence
intervals are consistently small and overlapping.

| Run time (s) | Compile time (s) | Executable size (bytes)
---|---|---|---
Benchmark | Original | Cocoon | Original | Cocoon | Original | Cocoon
binary-trees | $0.364\pm 0.023$ | $0.365\pm 0.023$ | $0.608\pm 0.010$ | $0.647\pm 0.003$ | 4,560,608 | 4,560,640
fannkuch-redux | $1.828\pm 0.027$ | $1.821\pm 0.011$ | $0.489\pm 0.147$ | $0.545\pm 0.002$ | 4,488,712 | 4,489,800
fasta | $1.116\pm 0.070$ | $1.093\pm 0.049$ | $0.417\pm 0.008$ | $0.468\pm 0.004$ | 4,339,184 | 4,339,640
k-nucleotide | $1.539\pm 0.007$ | $1.559\pm 0.007$ | $0.464\pm 0.003$ | $0.503\pm 0.003$ | 4,355,808 | 4,360,544
mandelbrot | $0.352\pm 0.003$ | $0.352\pm 0.003$ | $0.603\pm 0.030$ | $0.699\pm 0.006$ | 4,546,848 | 4,548,456
n-body | $46.657\pm 0.008$ | $46.335\pm 0.005$ | $0.386\pm 0.007$ | $0.591\pm 0.007$ | 4,305,872 | 4,318,312
pidigits | $0.554\pm 0.005$ | $0.556\pm 0.004$ | $0.334\pm 0.004$ | $0.382\pm 0.002$ | 4,528,080 | 4,529,800
regex-redux | $0.957\pm 0.003$ | $0.967\pm 0.003$ | $0.644\pm 0.005$ | $0.686\pm 0.010$ | 6,114,664 | 6,115,904
spectral-norm | $0.111\pm 0.002$ | $0.112\pm 0.003$ | $0.426\pm 0.005$ | $0.477\pm 0.005$ | 4,514,568 | 4,515,176
Table 3. Performance of nine benchmarks whose entire computation is wrapped in
a secret block, compared with the originals. Performance results include the
mean and a 95% confidence interval from at least 10 trials.

## References

  * (1)
  * Abadi et al. (1999) Martín Abadi, Anindya Banerjee, Nevin Heintze, and Jon G. Riecke. 1999.  A Core Calculus of Dependency. In _Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_ (San Antonio, Texas, USA) _(POPL ’99)_. Association for Computing Machinery, New York, NY, USA, 147–160.  https://doi.org/10.1145/292540.292555
  * Acay et al. (2021) Coşku Acay, Rolph Recto, Joshua Gancher, Andrew C. Myers, and Elaine Shi. 2021.  Viaduct: An Extensible, Optimizing Compiler for Secure Distributed Programs. In _Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation_ (Virtual, Canada) _(PLDI 2021)_. Association for Computing Machinery, New York, NY, USA, 740–755.  https://doi.org/10.1145/3453483.3454074
  * Askarov et al. (2008) Aslan Askarov, Sebastian Hunt, Andrei Sabelfeld, and David Sands. 2008.  Termination-Insensitive Noninterference Leaks More Than Just a Bit. In _Proceedings of the 13th European Symposium on Research in Computer Security: Computer Security_ (Málaga, Spain) _(ESORICS ’08)_. Springer-Verlag, Berlin, Heidelberg, 333–348.  https://doi.org/10.1007/978-3-540-88313-5_22
  * Austin and Flanagan (2009) Thomas H. Austin and Cormac Flanagan. 2009.  Efficient Purely-Dynamic Information Flow Analysis. In _Proceedings of the ACM SIGPLAN Fourth Workshop on Programming Languages and Analysis for Security_ (Dublin, Ireland) _(PLAS ’09)_. Association for Computing Machinery, New York, NY, USA, 113–124.  https://doi.org/10.1145/1554339.1554353
  * Balasubramanian et al. (2017) Abhiram Balasubramanian, Marek S. Baranowski, Anton Burtsev, Aurojit Panda, Zvonimir Rakamari, and Leonid Ryzhyk. 2017.  System Programming in Rust: Beyond Safety.  _SIGOPS Oper. Syst. Rev._ 51, 1 (sep 2017), 94–99.  https://doi.org/10.1145/3139645.3139660
  * Brady (2007) Edwin Brady. 2007\.  Idris.  Archived from http://www-fp.cs.st-and.ac.uk/ eb/darcs/Idris/.
  * Chapman and Hilton (2004) Roderick Chapman and Adrian Hilton. 2004.  Enforcing Security and Safety Models with an Information Flow Analysis Tool. In _Proceedings of the 2004 Annual ACM SIGAda International Conference on Ada: The Engineering of Correct and Reliable Software for Real-Time & Distributed Systems Using Ada and Related Technologies_ (Atlanta, Georgia, USA) _(SIGAda ’04)_. Association for Computing Machinery, New York, NY, USA, 39–46.  https://doi.org/10.1145/1032297.1032305
  * Chong (2008) Stephen Nathaniel Chong. 2008\.  _Expressive and Enforceable Information Security Policies_.  Ph. D. Dissertation. Cornell University.  "http://people.seas.harvard.edu/~chong/pubs/chong_dissertation.pdf"
  * Crichton et al. (2022) Will Crichton, Marco Patrignani, Maneesh Agrawala, and Pat Hanrahan. 2022.  Modular Information Flow through Ownership. In _Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation_ (San Diego, CA, USA) _(PLDI 2022)_. Association for Computing Machinery, New York, NY, USA, 1–14.  https://doi.org/10.1145/3519939.3523445
  * Debian benchmarksgame-team (2022) Debian benchmarksgame-team. 2022\.  The Computer Language 22.05 Benchmarks Game.  https://benchmarksgame-team.pages.debian.net/benchmarksgame/index.html.  Accessed 2 November 2022.
  * Denning (1976) Dorothy E. Denning. 1976\.  A Lattice Model of Secure Information Flow.  _Commun. ACM_ 19, 5 (may 1976), 236–243.  https://doi.org/10.1145/360051.360056
  * Denning and Denning (1977) Dorothy E. Denning and Peter J. Denning. 1977.  Certification of Programs for Secure Information Flow.  _Commun. ACM_ 20, 7 (jul 1977), 504–513.  https://doi.org/10.1145/359636.359712
  * Gregersen et al. (2019) Simon Gregersen, Søren Eller Thomsen, and Aslan Askarov. 2019.  A Dependently Typed Library for Static Information-Flow Control in Idris. In _Principles of Security and Trust_ , Flemming Nielson and David Sands (Eds.). Springer International Publishing, Prague, Czech Republic, 51–75.
  * Hammer et al. (2006) Christian Hammer, Jens Krinke, and Gregor Snelting. 2006\.  Information Flow Control for Java Based on Path Conditions in Dependence Graphs. In _Proceedings IEEE International Symposium on Secure Software Engineering_. IEEE, Arlington, Virginia, USA, 10 pages.
  * Hedin and Sabelfeld (2012) Daniel Hedin and Andrei Sabelfeld. 2012.  A Perspective on Information-Flow Control.  In _Software Safety and Security - Tools for Analysis and Verification_ , Tobias Nipkow, Orna Grumberg, and Benedikt Hauptmann (Eds.). NATO Science for Peace and Security Series - D: Information and Communication Security, Vol. 33. IOS Press, Amsterdam, 319–347.  https://doi.org/10.3233/978-1-61499-028-4-319
  * Kozyri et al. (2016) Elisavet Kozyri, Owen Arden, Andrew C. Myers, and Fred B. Schneider. 2016.  _JRIF: reactive information flow control for Java_.  Technical Report 1813–41194. Cornell University Computing and Information Science.  https://ecommons.cornell.edu/handle/1813/41194
  * Krohn et al. (2007) Maxwell Krohn, Alexander Yip, Micah Brodsky, Natan Cliffer, M. Frans Kaashoek, Eddie Kohler, and Robert Morris. 2007.  Information Flow Control for Standard OS Abstractions. In _Proceedings of Twenty-First ACM SIGOPS Symposium on Operating Systems Principles_ (Stevenson, Washington, USA) _(SOSP ’07)_. Association for Computing Machinery, New York, NY, USA, 321–334.  https://doi.org/10.1145/1294261.1294293
  * Lampson (1973) Butler W. Lampson. 1973\.  A Note on the Confinement Problem.  _Commun. ACM_ 16, 10 (oct 1973), 613–615.  https://doi.org/10.1145/362375.362389
  * Linux Foundation (2022) Linux Foundation. 2022\.  Servo.  https://servo.org
  * Mozilla Research (2020) Mozilla Research. 2020\.  The Rust Language.  Archived from https://research.mozilla.org/rust/.
  * Myers and Liskov (1998) A.C. Myers and B. Liskov. 1998.  Complete, safe information flow with decentralized labels. In _Proceedings. 1998 IEEE Symposium on Security and Privacy (Cat. No.98CB36186)_. IEEE, New York City, NY, USA, 186–197.  https://doi.org/10.1109/SECPRI.1998.674834
  * Myers et al. (2004) A.C. Myers, A. Sabelfeld, and S. Zdancewic. 2004.  Enforcing robust declassification. In _Proceedings. 17th IEEE Computer Security Foundations Workshop, 2004._ (Pacific Grove, CA, USA). IEEE, New York City, NY, USA, 172–186.  https://doi.org/10.1109/CSFW.2004.1310740
  * Myers (1999) Andrew C. Myers. 1999\.  JFlow: Practical Mostly-Static Information Flow Control. In _Proceedings of the 26th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_ (San Antonio, Texas, USA) _(POPL ’99)_. Association for Computing Machinery, New York, NY, USA, 228–241.  https://doi.org/10.1145/292540.292561
  * Myers and Liskov (1997) Andrew C. Myers and Barbara Liskov. 1997.  A Decentralized Model for Information Flow Control. In _Proceedings of the Sixteenth ACM Symposium on Operating Systems Principles_ (Saint Malo, France) _(SOSP ’97)_. Association for Computing Machinery, New York, NY, USA, 129–142.  https://doi.org/10.1145/268998.266669
  * Myers et al. (2006) Andrew C. Myers, Lantian Zheng, Steve Zdancewic, Stephen Chong, and Nathaniel Nystrom. 2006.  Jif 3.0: Java information flow.  http://www.cs.cornell.edu/jif
  * Narayan et al. (2020) Shravan Narayan, Craig Disselkoen, Tal Garfinkel, Nathan Froyd, Eric Rahm, Sorin Lerner, Hovav Shacham, and Deian Stefan. 2020\.  Retrofitting Fine Grain Isolation in the Firefox Renderer. In _Proceedings of the 29th USENIX Conference on Security Symposium_ _(SEC’20)_. USENIX Association, USA, Article 40, 18 pages.
  * Nielson and Nielson (1999) Flemming Nielson and Hanne Riis Nielson. 1999.  _Type and Effect Systems_.  Springer Berlin Heidelberg, Berlin, Heidelberg, 114–136.  https://doi.org/10.1007/3-540-48092-7_6
  * Noel (2010) Noel. 2010.  The Rust Language.  http://lambda-the-ultimate.org/node/4009.
  * Rotenberg (1973) Leo J. Rotenberg. 1973\.  _Making Computers Keep Secrets_.  Ph. D. Dissertation. Massachusetts Institute of Technology, Boston, MA.
  * Roy et al. (2009) Indrajit Roy, Donald E. Porter, Michael D. Bond, Kathryn S. McKinley, and Emmett Witchel. 2009\.  Laminar: practical fine-grained decentralized information flow control. In _Proceedings of the 2009 ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2009_ , Michael Hind and Amer Diwan (Eds.). ACM, Dublin, Ireland, 63–74.  https://doi.org/10.1145/1542476.1542484
  * Russo (2015) Alejandro Russo. 2015\.  Functional Pearl: Two Can Keep a Secret, If One of Them Uses Haskell. In _Proceedings of the 20th ACM SIGPLAN International Conference on Functional Programming_ (Vancouver, BC, Canada) _(ICFP 2015)_. Association for Computing Machinery, New York, NY, USA, 280–288.  https://doi.org/10.1145/2784731.2784756
  * Sabelfeld and Myers (2003) Andrei Sabelfeld and Andrew C. Myers. 2003.  Language-Based Information-Flow Security.  _IEEE Journal on Selected Areas in Communications_ 21, 1 (2003), 5–19.
  * Simonet (2003) Vincent Simonet. 2003\.  _The Flow Caml System: documentation and user’s manual_.  Technical Report 0282. Institut National de Recherche en Informatique et en Automatique (INRIA).  ©INRIA.
  * Smith and Volpano (1998) Geoffrey Smith and Dennis Volpano. 1998.  Secure Information Flow in a Multi-Threaded Imperative Language. In _Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages_ (San Diego, California, USA) _(POPL ’98)_. Association for Computing Machinery, New York, NY, USA, 355–364.  https://doi.org/10.1145/268946.268975
  * Stack Overflow (2022) Stack Overflow. 2022\.  Annual Developer Survey.  https://survey.stackoverflow.co/2022/.
  * The Rust Foundation (2022) The Rust Foundation. 2022\.  Prodution Users — Rust Programming Language.  https://www.rust-lang.org/production/users
  * Volpano et al. (1996) Dennis Volpano, Cynthia Irvine, and Geoffrey Smith. 1996\.  A Sound Type System for Secure Flow Analysis.  _J. Comput. Secur._ 4, 2–3 (jan 1996), 167–187.
  * Xiang and Chong (2021) Jian Xiang and Stephen Chong. 2021.  Co-Inflow: Coarse-grained Information Flow Control for Java-like Languages. In _2021 IEEE Symposium on Security and Privacy (SP)_. IEEE, San Francisco, CA, USA, 18–35.  https://doi.org/10.1109/SP40001.2021.00002
  * Zanioli et al. (2012) Matteo Zanioli, Pietro Ferrara, and Agostino Cortesi. 2012\.  SAILS: Static Analysis of Information Leakage with Sample. In _Proceedings of the 27th Annual ACM Symposium on Applied Computing_ (Trento, Italy) _(SAC ’12)_. Association for Computing Machinery, New York, NY, USA, 1308–1313.  https://doi.org/10.1145/2245276.2231983
  * Zdancewic and Myers (2000) Steve Zdancewic and Andrew C. Myers. 2000.  _Confidentiality and Integrity with Untrusted Hosts: Technical Report_.  technical report. Cornell University.
  * Zeldovich et al. (2008) Nickolai Zeldovich, Silas Boyd-Wickizer, and David Mazières. 2008\.  Securing Distributed Systems with Information Flow Control. In _Proceedings of the 5th USENIX Symposium on Networked Systems Design and Implementation_ (San Francisco, California) _(NSDI’08)_. USENIX Association, USA, 293–308.
  * Zheng and Myers (2005) Lantian Zheng and Andrew C. Myers. 2005.  Dynamic Security Labels and Noninterference (Extended Abstract). In _Formal Aspects in Security and Trust_ , Theo Dimitrakos and Fabio Martinelli (Eds.). Springer US, Boston, MA, 27–40.