Cryptographically Secure Information Flow Control on Key-Value Stores
The conference version of this paper appears in CCS 2017 <cit.>.

Lucas Waye

Harvard University

Pablo Buiras

Harvard University

Owen Arden

University of California, Santa Cruz$^\dagger$Work done while author was at Harvard University.
Santa Cruz

Alejandro Russo

Chalmers University of Technology

Stephen Chong

Harvard University

We present , an information flow control (IFC)
system that transparently incorporates cryptography
to enforce confidentiality and integrity policies on untrusted storage.

insulates developers from explicitly manipulating keys and cryptographic
primitives by leveraging the policy language of the IFC system to
automatically use the appropriate keys and correct cryptographic operations.

We prove that is secure with a novel proof technique that is
based on a proof style from cryptography together with standard programming
languages results.
We present a prototype implementation and a case study
that demonstrates 's practicality.

<concept_desc>Security and privacy Information flow control</concept_desc>
<concept_desc>Security and privacy Key management</concept_desc>
<concept_desc>Security and privacy Digital signatures</concept_desc>
<concept_desc>Security and privacy Public key encryption</concept_desc>
<concept_desc>Security and privacy Block and stream ciphers</concept_desc>
<concept_desc>Software and its engineering Domain specific languages</concept_desc>

§ INTRODUCTION

Cryptography is critical for applications that securely store
and transmit data.
It enables the authentication of remote hosts, authorization of
privileged operations, and the preservation of confidentiality and integrity of

However, applying cryptography is a subtle task, often involving setting up
configuration options and low-level details that users must get
right; even small mistakes can lead to major vulnerabilities <cit.>.

A common approach to address this problem is to raise the level of

For example, many libraries provide high-level interfaces for establishing
TLS <cit.> network connections (e.g.,
OpenSSL[<https://www.openssl.org/>]) that are very similar to the
interfaces for establishing unencrypted connections.

These libraries are useful (and popular) because they abstract many
configuration details, but they also make several assumptions about certificate
authorities, valid protocols, and client authentication.
Due in part to these assumptions, the interfaces
are designed for experienced cryptography programmers and as a result can be
used incorrectly by non-experts in spite of their high level of abstraction <cit.>.
Indeed, crypto library misuse is a more prevelant security issue than
Cross-Site Scripting (XSS) and SQL Injection <cit.>.

Information flow control (IFC) is an attractive approach to building
secure applications because it addresses some of these issues.

There has been extensive work in developing expressive information flow policy
languages <cit.> that help clarify
a programmer's intent.

Furthermore, many semantic guarantees offered by IFC languages are inherently
compositional from a security point of view
However, existing IFC languages (e.g., <cit.>) generally assume that critical components
of the system, such as persistent storage, are trustworthy—the components must enforce
the policies specified by the language abstraction.

This assumption makes most IFC systems a poor fit for many of the use-cases
that cryptographic mechanisms are designed for.

It is tempting to extend IFC guarantees to work with untrustworthy data
storage by simply “plugging-in” cryptography.

However, the task is not simple: the threat model of an IFC system extended
with cryptography differs from both
the standard cryptographic threat models and from standard IFC threat models.
Unlike most IFC security models, an attacker in this scenario may have
low-level abilities to access signatures and ciphertexts of sensitive data, and the ability to deny access to data by corrupting it (e.g.,
flipping bits in ciphertexts).

Attackers also have indirect access to the private cryptographic keys
through the trusted runtime.  An attacker may craft and run programs
that have access to the system's cryptographic keys in order to trick
the system into inappropriately decrypting or signing information.
Cryptographic security models often
account for the high-level actions of attackers using oracles that
mediate what information an active attacker can learn through
interactions with the cryptosystem.  These oracles abstractly represent implementation
artifacts that could be used by the attacker to distinguish ciphertexts.  Ensuring that an
actual implementation constrains its behavior to that modeled by an oracle
is typically left to developers.

An attacker's actual interactions with a system often extend beyond
the semantics of specific cryptographic primitives and into
application-specific runtime behavior such as how a server responds
when a message fails to decrypt or a signature cannot be verified.  If
an attacker can distinguish this behavior, it may provide them with
information about secrets.  Building real
implementations that provide no additional information to attackers
beyond that permitted by the security model can be very challenging.

Therefore, to give developers better tools for building secure applications, we
need to ensure that system security is not violated by
combining attackers' low-level abilities and their ability to craft
their own programs. This requires extending the attacker's power beyond that
typically considered by IFC models, and representing the attacker's interactions with
the system more precisely than typical cryptographic security models.

This paper presents ,

a programming language
that reconciles IFC and cryptography models to provide guarantees on both
ephemeral data within applications and persistent data on an untrusted
key-value store.

extends the IFC-tool LIO <cit.> with store
and fetch operations for interacting with a persistent key-value store.

Like LIO, expresses confidentiality and integrity requirements using
security labels: flows of information are
controlled throughout the execution of programs to ensure the policies
represented by the labels are enforced.

encrypts and signs data as it leaves the runtime,
and decrypts and verifies as it enters the system.

These operations are done automatically according to the security
labels—thus avoiding both the mishandling of sensitive data and the
misuse of cryptographic mechanisms.  Because the behavior of the
system is fully specified by the semantics of the language, an
attacker's interactions with the system can be characterized
precisely. This results in a strong connection between the power of
the attacker in our formal security model and in actual programs.

transparently maps security labels to cryptographic keys and leverages
the underlying IFC mechanisms to ensure that keys are not misused within the program.
Since we consider attackers capable of denying access to information
by corrupting data, extends labels with an availability policy that tracks who can deny
access to information (i.e., who may corrupt the data).

Figure <ref> presents an overview of the threat
model.  At a high-level, a program may be a malicious program written by the attacker.
All interactions between the runtime and the
store are visible to the attacker.  Only the (trusted) runtime
has access to the keys used to protect information from the attacker,
but the attacker may have access to other “low” keys.  The runtime never exposes keys directly to program code: they are only used
implicitly to protect or verify data as it leaves or enters the runtime.

Attackers may also perform low-level
and  operations directly on the key-value
store. Using these low-level operations, an attacker may corrupt ciphertexts to
make them invalid even when it does not possess the signing keys to make valid modifications.
We treat these actions as attacks on the availability of data, rather than
on its integrity.
A low-availability store is vulnerable to availability
attacks, and thus should be prevented from storing data that requires high-availability.
's information flow control mechanisms mediate the attacker's ability
to discover new information or modify signed values by interacting
with a program through s and s to a

threat model. Attackers write programs, read from and write to
the store, and observe the runtime's interactions.

This paper makes the following contributions:

* A formalization of the ideal semantics of ,
which models its security without
cryptography, and a real semantics, which enforces
security cryptographically.

* A novel proof technique that combines standard programming language
and cryptographic proof techniques.
Using this approach, we characterize the interaction between the
high-level security guarantees provided by information flow control
and the low-level guarantees offered by the cryptographic mechanisms.

* For confidentiality, we have formalized these guarantees as chosen-term attack (CTA)
security, an extension of chosen-plaintext attack (CPA) security to systems where an
attacker may choose arbitrary programs that encrypt
and decrypt information through the runtime.  Though CTA security is predicated on the relatively weak guarantees of CPA
crypto primitives, CTA security provides stronger guarantees since it applies to the end-to-end flow of
information through the system, including the interactions an active, adaptive attacker might use to distinguish

* For integrity, we have defined leveraged existential forgery, an
extension of existential forgery to systems where an attacker may choose and
execute a program to produce signed values.

* A prototype implementation in the form of a Haskell library extending LIO.

Our prototype system employs the DC labels model <cit.>,
previously used in practical systems (e.g., Hails <cit.> and
COWL <cit.>).

Our implementation extends DC-labels with an
availability component, which may be applicable to these existing
systems as well.

Our approach uses a computational model of cryptography.
However, we do not rely on a formal definition
of computational noninterference <cit.>.
Instead, we phrase security in terms
of an adversary-based game with a definition much closer to standard
cryptographic definitions of security such as CPA security <cit.>. This
approach helps to model an active adversary on the store, something that
computational noninterference can not easily capture. Furthermore, we
incorporate the semantics of programs and potential attacks
against them into the security model. This approach captures the power
of the attacker more precisely than cryptographic models for active
attackers like chosen-ciphertext attack (CCA)
security <cit.>.

Our CTA model applies a game-based definition of security in a
language setting and is a novel aspect of this work. Computational
noninterference and related approaches consider attackers that can
only provide different secret inputs to the program. Thus a key
contribution of our work is capturing the abilities of an active
attacker (that can both supply code to execute and directly manipulate
the store) in a crypto-style game that goes beyond CPA security
and standard IFC guarantees (noninterference, including
computational noninterference). Although our results are specific to
, we expect our approach to be useful in proving the security of
cryptographic extensions of other information flow languages.

The rest of the paper is structured as follows.
Section <ref> introduces and
Section <ref> describes the extensions to it in order to
interact with an untrusted store.
Section <ref> describes the computational model of
with cryptography, and Section <ref> shows the model's
formal security properties. Section <ref> describes
the prototype implementation of along with a case study.
And finally Section <ref> discusses related work.
and Section <ref> concludes.

§ BACKGROUND

In this section, we describe the programming model of .

is based on
LIO <cit.>, a dynamic IFC library
implemented in Haskell.

LIO uses Haskell features
to control how sensitive information is used and to restrict I/O
side-effects. In particular, it implements an embedded language and a
runtime monitor based on the notion of a monad, an abstract
data type that represents sequences of actions (also known as
computations) that may perform side-effects.

The basic interface of a monad consists in the fundamental operations
and $(\bindSymbol)$ (read as “bind”).

The expression $\return{x}$ denotes a computation that returns
the value denoted by $x$, performing no side-effects.

The function $(\bindSymbol)$ is used to sequence

Specifically, $\bind{t}{\lambda x.t'}$ takes the result produced by
$t$ and applies function $\lambda x.t'$ to it (which allows
computation $t'$ to depend on the value produced by $t$).  In order to
be useful, monads are usually extended with additional primitive
operations to selectively allow the desired side-effects. The  monad is a
specific instance of this pattern equipped with IFC-aware operations
that enforce security.

LIO, like many dynamic IFC approaches (e.g., <cit.>), employs a floating label.
Security concerns are represented by labels
which form a lattice, a partially-ordered ($\sqsubseteq$) set with
least upper bounds ($\sqcup$) and greatest lower bounds ($\sqcap$).

A runtime monitor maintains as part of its state a distinguished
label $\lcur$ known as the current label.

The current label is similar to the program
counter ($\mathit{pc}$) label of static IFC systems (e.g., <cit.>):
it restricts side-effects in the current
computation that may compromise the
confidentiality or integrity of data.
For example, a computation whose current label is secret cannot write to a public location.

LIO operations adjust this label when sensitive information enters the program
and use it to validate (or reject) outgoing flows.

When an LIO computation with current label $\lcur$ observes an
entity with label $l$, its current label is increased (if necessary)
to the least upper bound of the two labels, written
$\lcur \lub l$. Thus, the current label
“floats up” in the security lattice, so that it is always
an upper bound on the security levels of information in the computation.  Similarly, before performing a side-effect
visible to label $l$, LIO ensures the current label flows to
$l$ ($\lcur \flows l$).

Once the current label within a given computation is raised, it can
never be lowered. This can be very restrictive, since, for example, as
soon as confidential data is accessed by a computation, the
computation will be unable to output any public data. To address this
limitation, the $\textsf{toLabeled}$
operation allows evaluation of an LIO computation $m$ in a separate
compartment: $\toLabeled{l}{m}$ will run $m$ to completion,
and produce a labeled value $\LabeledO{l}{v}$, where $v$ is the result of
computation $m$, and $l$ is an over-approximation of the final current
label of $m$. Note that the current label of the enclosing computation
is not affected by executing $\toLabeled{l}{m}$.  In general, given a
labeled value $\LabeledO{l}{v}$, label $l$ is an upper bound on the information
conveyed by $v$. Labeled values can also be created from raw values
using operation , and a labeled value can be read into
the current scope with operation .

Creating a
labeled value with label $l$ can be regarded as writing into a channel
at security level $l$. Similarly, observing (i.e., unlabeling) a
labeled value at $l$ is analogous to reading from a channel at $l$.

security guarantees.

LIO provides a termination-insensitive noninterference-based
security guarantee <cit.>.
Intuitively, if a program is noninterfering with respect to
confidentiality, then the public outputs of a program reveal nothing
about the confidential inputs. More precisely, an attacker $\attacker$
that can observe inputs and outputs with confidentiality label at most
$l_\attacker$ learns nothing about any input to the program with label
$l$ such that $l \not\sqsubseteq l_\attacker$.  Similarly, a program
is noninterfering for integrity if an attacker that can control
untrusted inputs cannot influence trusted outputs.

\begin{align*}
\figCLioSyntaxMain
\end{align*}

Syntax for values, terms, and types.

is formalized as a typed $\lambda$-calculus with call-by-name
evaluation, in the same style as LIO <cit.>.

Figure <ref> gives the syntax of values, terms, and types.
In addition to standard $\lambda$-calculus features, includes several
security-related extensions that mirror those in LIO, and two
operations for interacting with the key-value store, namely
$\texttt{store}$ and $\texttt{fetch}$. As those primitives have nontrivial
semantics that involve the external storage, we defer their discussion
to Section <ref>.
Security labels have type $\LabelT$ and labeled values have type $\LabeledT{\tau}$.
Computation on labeled values occur in the $\CLIOT$ monad using the $\return{}$ and
$(\bindSymbol)$ monadic operators.
The nonterminals $\CLIO{t}$ and
$\block{l}{l'}{l''}{t}$ are only generated by intermediate reduction steps and are
not valid source-level syntax.
For convenience, we also distinguish values that can be easily
serialized as ground values, $\gv$. Ground values are all values
except functions and  computations. To facilitate our extension of LIO with cryptography, we require
labeled values to contain only ground values.

Static type checking is performed in the standard way.

We elide the typing rules $\vdash t : \tau$ since they are mostly
standard[Complete definitions given in <Ref>.].
LIO enforces information flow control dynamically, so it
does not rely on its type system to provide security guarantees.

The semantics is given by a small-step reduction relation $\lto$ over
configurations (Figure <ref>)[The rest can be found in <Ref>.]. Configurations are of the form
$\conf{\lcur}{\lclr}{t}$, where $\lcur$ is the current label and $t$
is the  term being evaluated.  Label $\lclr$ is the current
clearance and is an upper bound on the current label $\lcur$. The
clearance allows a programmer to specify an upper bound for
information that a computation is allowed to access. We write $c \lto
c'$ to express that configuration $c$ can take a reduction step to
configuration $c'$. We define $\lto^*$ as the reflexive and transitive
closure of $\lto$. Given configuration $c=\conf{\lcur}{\lclr}{t}$ we write $\pcOf{c}$ for $\lcur$, the current label of $c$.

language semantics (selected rules).

Rules $\rulename{return}$ and
$\rulename{bind}$ encode the core monadic operations. The intermediate
value $\CLIO{t}$ is used to represent a computation which produces
the term $t$, without any further effects on the configuration.  In
rule $\rulename{label}$, the operation $\llabel{l}{\gv}$ returns a
labeled value with label $l$ holding $\gv$ ($\LabeledO{l}{\gv}$), provided
that the current label flows to $l$ ($\lcur \flows l$) and
$l$ flows to the current clearance ($l \flows \lclr$). Note
that we force the second argument to be a ground value, i.e. it should
be fully normalized.

Rule $\rulename{unlabel}$ expresses that, given a labeled value
$\mathit{lv}$ with label $l$, the operation $\unlabel{\mathit{lv}}$
returns the value stored in $\mathit{lv}$ and updates the current
label to $\lcur \lub l$, to capture the fact that a value with label $l$ has been read, provided that this new label flows to the
current clearance ($l \flows \lclr$).

The operations $\textsf{getLabel}$ and $\textsf{getClearance}$ can be
used to retrieve the current label and clearance respectively.

Rules $\rulename{toLabeled}$ and $\rulename{reset}$ deserve special
attention. To evaluate $\toLabeled{l_1}{t}$, we first check that $l_1$
is a valid target label
($\lcur \flows l_1 \flows \lclr$) and then wrap
$t$ in a compartment using the special syntactic form
$\block{\lcur}{\lclr}{l_1}{t}$, recording the
current label and clearance at the time of entering
$\textsf{toLabeled}$ and the target label of the operation,
$l_1$. Evaluation proceeds by reducing $t$ in the context of
the compartment to a value of the form $\CLIO{t_1}$. Next,
the rule $\rulename{reset}$ evaluates the term $\block{\lcur}{\lclr}{l_1}{\CLIO{t_1}}$,
first checking that the current label
flows to the target of the current $\textsf{toLabeled}$
($\lcur \flows l_2$). Finally, the compartment is replaced
by a normal $\textsf{label}$ operation and the current label and
clearance are restored to their saved values.

DC Labels
LIO is parametric in the label format, but for the purposes of this
paper in  we use DC labels <cit.> with
three components to model confidentiality, integrity, and availability

A label $\ltrip{l_c}{l_i}{l_a}$ represents a policy with
confidentiality $l_c$, integrity $l_i$, and availability $l_a$.

Information labeled with $\ltrip{l_c}{l_i}{l_a}$ can be read by $l_c$,
is vouched for by $l_i$, and is hosted by $l_a$.  We write
$\projC{l}$, $\projI{l}$, $\projA{l}$ for the
confidentiality, integrity, and availability components of $l$,
respectively. Each component is a conjunction of disjunctions of
principal names, i.e., a formula in conjunctive normal form. A
disjunction $A\vee B$ in the confidentiality component means that
either $A$ or $B$ can read the data; in the integrity component, it
means that one of $A$ or $B$ vouch for the data, but none of them take
sole responsibility; in terms of
availability, it means that one of $A$ or $B$ can deny access to the
data. Conjunctions $A \wedge B$ mean that only $A$ and $B$ together
can read the data (confidentiality), that they jointly vouch for
the data (integrity), or that they can jointly deny access to the data (availability).

Data may flow between differently labeled entities, but only those with more restrictive policies:
those readable, vouched for, or hosted by fewer entities.

A label $\ltrip{l_c}{l_i}{l_{a}}$ can flow to any label where the
confidentiality component is at least as sensitive than $l_c$, the integrity
component is no more trustworthy than $l_i$, and the availability is no
than $l_a$,  i.e.  $l₁ \flows l₂$
if and only if $\projC{l_2} \Longrightarrow \projC{l_1}$,
$\projI{l_1} \implies \projI{l_2}$,
and  $\projA{l_1} \implies \projA{l_2}$. We use logical implication
because it matches the intuitive meaning of disjunctions and
conjunctions, e.g., data readable by $A\vee B$ is less confidential
than data readable only by $A$, and data vouched for by $A\wedge B$ is
more trustworthy than data vouched for only by $A$.

In the rest of the paper, we consider only  computations that
work on labels of this form.

§ INTERACTING WITH AN UNTRUSTED STORE

extends LIO with a key-value store. The language is extended with two new commands:
$\store{t_k}{t_v}$ puts a labeled value $t_v$ in the
store indexed by key $t_k$; $\fetch{t_k}{t_v}$ command fetches the entry with key $t_k$ and
if it cannot be fetched, returns the labeled value $t_v$.
In both commands, $t_k$ must evaluate to a ground value and the labeled value
$t_v$ must evaluate to a labeled ground value with type $\tau$.

language semantics (store and fetch rules).

Semantics for fetch and store are shown

in Figure <ref>.

We modify the semantics to be a labeled transition system, where step relation $\ltol{\alpha}$ is annotated with store events $\event$. Store event $\event$ is one of:

* $\skipcmd$ (representing no interaction
with the store, i.e., an internal step; we typically elide $\skipcmd$ for clarity),

* $\storecmd{\gv_k}{\Labeled{l}{\gv}}$ (representing putting a labeled ground value $\Labeled{l}{\gv}$ indexed by

* $\fetchcmd{\gv_k}{\Labeled{l}{\gv}}$ (representing reading
a labeled value from the store indexed by $\gv_k$), or

* $\missingcmd{\gv_k}$
representing no value is indexed by $\gv_k$.

Labeling transitions with store events allows us to cleanly factor out the implementation of the store, enabling us to easily use either an idealized (non-cryptographic) store, or a store that uses cryptography to help enforce security guarantees. We describe the semantics of store events in both these settings later.

We associate a label $\lowlabel$ with the store. Intuitively, store level $\lowlabel$ describes how trusted the store is: it represents the inherent protections provided
by the store and the inherent trust by the store in .
For example, the store may be behind an organization's firewall
so data is accessible only to organization members due to an external access control
mechanism (i.e., the firewall), so can safely store the organization's information there.

Dually, there may be integrity requirements that is trusted to uphold when
writing to the store. For example, the store may be used as part of a larger system that
uses the store to perform important operations (e.g., ship customer orders). Thus the integrity component of the store label is a bound on the untrustworthiness of information that should write to the store (e.g., should not put unendorsed shipping requests in the store).

The availability component of the store label specifies a bound on who is able to corrupt information in the store and thus make it unavailable. (Note that we are concerned with information availability rather than system availability.)
In general, this would describe all the principals who have direct and
indirect write-access to the store.

Rule Store (Figure <ref>) is used to put a labeled value l in the store, indexed by key $\gv_k$.

We require that the current label $\lcur$ is bounded above by store level $\lowlabel$. In terms of confidentiality, this means that any information that may be revealed by performing the store operation (i.e., $\lcur$) is permitted to be learned by users
of the store.
For integrity, the decision to place this value in the store (possibly overwriting
a previous value) should not be influenced by information below the integrity
requirements of the store. For availability, the information should not be derived
from less available sources than the store's availability level.

Additionally, we require the current label
to flow to $l$, the label of the value that is being stored (i.e., $\canFlowTo{\lcur}{l_1}$).
Intuitively, this is because an entity that learns the labeled value also learns
that the labeled value was put in the store. Current label $\lcur$ is an upper
bound on the information that led to the decision to perform the store, and
$l_1$ bounds who may learn the labeled value.

For command $\fetch{\gv_k}{\Labeled{l_d}{\gv_d}}$,
labeled value $\Labeled{l_d}{\gv_d}$ serves double duty. First, if
the store cannot return a suitable value (e.g., because there is no value indexed by key $\gv_k$, or because cryptographic signature verification fails), then the fetch command evaluates to the default labeled value $\Labeled{l_d}{\gv_d}$ (which might be an error value or a suitable default). Second, label $l_d$ specifies an upper bound on the label of any value that may be returned:

if the store wants to return a labeled value $\Labeled{l}{\gv}$ where $\cantFlowTo{l}{l_d}$, then the fetch command evaluates to
$\Labeled{l_d}{\gv_d}$ instead. This allows programmers to specify bounds on information they are willing to read from the store.

Rule Fetch-Valid is used when a labeled value is successfully
fetched from the store. Store event $\fetchcmd{\gv_k}{\Labeled{l}{\gv}}$
indicates that the store was able to return labeled value $\Labeled{l}{\gv}$ indexed by the key $\gv_k$.

Rule Fetch-Invalid is used when a labeled value cannot
be found indexed at the index requested or it does not safely flow
to the default labeled value (i.e., it is too secret, too untrustworthy
or not available enough), and causes the fetch to evaluate to the specified default labeled value.

Since the label of the default value $l_d$ will be used for the label
of the fetched value in general, the availability of the store level
should be bounded above by the availabiltiy of the label of the default value
(i.e., $\canFlowToA{\projA{\lowlabel}}{\projA{l_d}}$) in both rules,
as the label of the fetched value should reflect the fact that
anyone from the store could have corrupted the value.

§.§ Ideal Store Behavior

We informally describe the ideal behavior of an untrusted
store from the perspective of a program.[Complete formal definitions in <Ref>.]
The ideal store semantics provides a specification of the
behavior that
a real
implementation should strive for, and allows the programmer to focus on functionality and security properties of the store rather than the details of cryptographic enforcement of labeled values.

In Section <ref> we describe how
we use cryptography to achieve this ideal specification.

We use a small-step  relation $\iconf{c}{\istore}\ito\iconf{c'}{\istore'}$ where  $\iconf{c}{\istore}$ and $\iconf{c'}{\istore'}$ are pairs of
a configuration $c$
and an ideal store $\istore$.

An ideal store $\istore$
maps ground values $\gv_k$ to labeled ground values $\Labeled{l}{\gv}$. If a store doesn't contain a mapping for an index $\gv_k$, we represent that as mapping it to

the distinguished value

Store events
are used to communicate with the store. When a $\storecmd{\gv_k}{\Labeled{l}{\gv}}$ event is emitted, the store is updated appropriately. When the computation issues a fetch command, the store provides the appropriate event (i.e., either provides event
$\missingcmd{\gv_k}$ or
event  $\fetchcmd{\gv_k}{\Labeled{l}{\gv}}$ for an appropriate labeled value $\Labeled{l}{\gv}$). For computation steps that do not interact with the store, store event $\skipcmd$ is emitted, and the store is not updated.

§.§ Non-Interaction: Threat Model

We assume that programs other than computations may interact with the store

and may try to actively or passively subvert the security of programs.
Our threat model for these adversarial programs is as follows (and uses store level $\lowlabel$ to characterize some of the adversaries' abilities).

* All indices of the key-value store are public information, and an adversary can probe any index of the store and thus notice any and all updates to the store.

* An adversary can read labeled values $\Labeled{l_1}{\gv}$ in the store where the confidentiality level of label $l_1$ is at least as confidential as the store level $\lowlabel$ (i.e., $\canFlowToC{\projC{l_1}}{\projC{\lowlabel}}$).

* An adversary can put labeled values  $\Labeled{l_1}{\gv}$ in the store (with arbitrary ground value index $\gv_k$) provided the integrity level of store level $\lowlabel$ is at least as trustworthy as the integrity of label $l_1$ (i.e., $\canFlowToI{\projI{\lowlabel}}{\projI{l_1}}$).

An adversary can adaptively interact with the store. That is, the behavior of the adversary may depend upon (possibly probabilistically) changes the adversary detects or values in the store.

We make the following restrictions on adversaries.

* The adversary does not have access to timing information. That is, it cannot observe the time between updates to the store. We defer to orthorgonal techniques to mitigate the impact of timing channels <cit.>. For example, could generate store events on a fixed schedule.

* The adversary cannot observe termination of a program, including abnormal termination due to a failed label check. This assumption can be satisfied by requiring that all programs do not diverge and are checked to ensure normal termination, e.g., by requiring $\getLabel$ checks on the label of a labeled value before unlabeling it. Static program analysis can ensure these conditions, and in the rest of the paper we consider only programs that terminate normally.

Adversary Interactions and Low Steps

Note that even though the
adversary might have compromised the program, it can only
interact with it at runtime through the store. The adversary does not
automatically learn everything that the program learns, because data
in the runtime is still subject to semantics and the IFC
enforcement, which might prevent exfiltration to the store. Give
example here? Or later? Maybe when explaining fetch?  The semantics
thus gives a more precise characterization of the power of the adversary.  Rather
than proving the security in the presence of a decryption oracle
(e.g., CCA or CCA-2 <cit.>), the runtime prevents
system interactions from being used as a decryption oracle, by

We formally model the non-interactions with the store using
sequences of adversary interactions $I$, given in
Figure <ref>.

Adversary interactions are $\skipcmd$, $\storecmd{\gv'}{\Labeled{l_1}{\gv}}$
and $\corruptcmd{\gv_1, ... \gv_n}$, which, respectively: do nothing; put a labeled value in the store; and

delete the mappings
for entries at indices $\gv_1$ to $\gv_n$.

For storing labeled values, we restrict the integrity of the labeled value stored
by non-interactions to be at most at the store level.
Sequences of interactions $\iinteraction_1 \cdot ... \cdot \iinteraction_n$
are notated as $\iinteractions$.

To model the adversary actively updating the store, we define a step semantics
$\Lowstep{}$ that includes adversary interactions $\iinteractions$. We restrict
interactions to occur only at low steps, i.e., when the current label of the computation is less than or equal to the store level $\lowlabel$. (By contrast, a high step is when the current label can not flow to $\lowlabel$.)

This captures the threat model assumption that the attacker cannot observe timing.

Rules Low-Step
and Low-To-High-To-Low-Step in Figure <ref> express adversary interactions occurring only at low steps.

§ REALIZING

In this section we describe how uses cryptography to enforce
the policies on the labeled values through a formal model, called
the real store semantics. This model serves as the
basis for establishing strong, formally proven, computational
guarantees of the system.

We first describe how DC labels are enforced with
cryptographic mechanisms (Section <ref>),
and then describe the real store semantics (Section <ref>).

§.§ Cryptographic DC Labeled Values

This section is queueing up a lot of definitions, but it is hard to hold all of
this in memory.  maybe we need a summary table to refer to?

, like many systems,
identifies security principals
with the public key of a cryptographic key pair, and associates
the authority to act as a given principal with possession of the
corresponding private key. At a high level, ensures that only those with access to a principal's private key can access information confidential to that principal and vouch for information on behalf of that principal.

tracks key pairs in a keystore.

Formally, a keystore is a mapping
$\keystore : p \mapsto (\{0, 1\}^*, \{0, 1\}^*_{\bot}) $, where $p$ is the principal's well-known name, and the pair of bit strings contains the public and private keys for the principal.
In general, the private key for a principal may not be known—represented by $\bot$—which corresponds to knowing the identity of a principal, but not possessing its authority.
Keystores are the basis of authority and identity for computations.
We use meta-functions on keystores
to describe the authority of a keystore in terms of DC labels.[Complete
definitions for these functions are in <Ref>.]
Conceptually, a keystore can access and vouch for any information
for a principal for which it has the principal's
private key. Meta-function $\authorityOf{\keystore}$ returns a label where each component (confidentiality, integrity, and availability) is the conjunction of all principals for which keystore $\keystore$ has the private key.

We also use the keystore to determine the starting label of a program $\Start{\keystore}$
and the
least restrictive
clearance $\Clr{\keystore}$, which are, respectively, the
most public, trusted, and available label possible
and the
most confidential, least trusted, and least available data that the computation can compute on, given the keystore's authority.

Using the principal keystore as a basis for authority and identity
for principals,

derives a cryptographic protocol

that enforces the security policies of
safe information flows defined by DC labels.

In the DC label model, labels are made up of triples of formulas. Formulas are conjunctions of categories $\category_1 \wedge ... \wedge \category_n$.
Categories are disjunctions of principals $p_1 \vee ... \vee p_n$.
Any principal in a category can read (for confidentiality)
and vouch for (for integrity) information bounded above by the level of the category.
We enforce that ability cryptographically by ensuring that only principals
in the category have access to the private key for that category.
achieves this through the use of category keys.

A category key serves as the
cryptographic basis of authority and identity for a category.
Category keys are made up of the following components:
a category public key that is readable by all principals,
a category private key that is only readable by members of the category,
and a category key signature that is a signature on the category
public key and category private key to prove the category key's authenticity.
Category keys are created lazily by as needed and placed in
the store.

A category key is created using a randomized meta-function[Defined formally in <Ref>.] parameterized by the keystore.

The generated category private key is encrypted
for each member of the category separately using each member principal's
public key. To prevent illegitimate creation of category keys, the encrypted
category private key and category public key are together
signed using the private key of one of the category members.[The runtime ensures that the first time a category key for a given category is required, it will be because data confidential to the category or vouched for by the category is being written to the store, and thus the computation has access to at least one category member's private key. Note that any computation with the authority of a category member has the authority of the category.]

When a category key is created and placed in the store,
it can be fetched by anyone but decrypted only
by the members of the category.
When a computation fetches a category key,
it verifies the signature of the category key to ensure that a
category member actually vouches for it.[“Encrypt-then-sign”issues (e.g., <cit.>) do not apply here as the threat model (i.e., signed encrypted messages implying authorship) is different.]
(Failing to verify the signature would allow an adversary to trick a computation into using a category key that is readable by the adversary.)

A computation
encrypts data confidential to a formula $\category_1 \wedge ... \wedge \category_n$
by chaining the encryptions of the value.
It first encrypts  using $\category_1$'s category public key
and then encrypts the resulting ciphertext for formula $\category_2 \wedge ... \wedge \category_n$.

This form of layered encryption relies on a canonical ordering of categories;
we use a  lexicographic ordering of principals to ensure a canonical ordering of encryptions and decryptions.

A computation signs data for a formula by signing the data with each category's private key and then concatenating the signatures together.
Verification  succeeds only if every category signature
can be verified.

Equipped with a mechanism to encrypt and sign data for DC labels that
conceptually respects safe information flows in , we use this mechanism to serialize and deserialize labeled values to the store. Given a labeled ground value $\Labeled{\gv}{\ltrip{l_c}{l_i}{l_a}}$, the value $\gv$ is signed according to formula $l_i$. The value and signature are encrypted according to formula $l_c$, and the resulting bitstring is the serialization of the labeled value. Deserialization performs decryption and then verification.

If deserialization fails, then treats it like a missing entry, and

the fetch command that triggered the deserialization would evaluate to the default labeled value.

Replay Attacks
Unfortunately, using just encryption and signatures does not faithfully implement the ideal store semantics: the adversary is able to swap entries in the store, or re-use a previous valid serialization, and thus in a limited way modify high-integrity labeled values in the store. We prevent these attacks by requiring that the encryption of the ground value and signature also includes the index value (i.e., the key used to store the labeled value) and a version number.

The real
semantics keeps track of the last seen version of a labeled value
for each index of the store. When a value is serialized, the version of that
index is incremented before being put in the store. When the value is
deserialized the version is checked to ensure that the version is not
before a previously used version for that index. In a distributed setting, this version counter
could be implemented as a vector clock between computations to account
for concurrent access to the store. However, for simplicity, we use
natural numbers for versions in the real store semantics.

§.§ Store Semantics

reviewer: did not think store semantics accounted for category key creation
reviewer: puzzled by signing before encrypting, don't we need CCA2-security? what about malleability?

In this section we describe the real store semantics

in terms of
a small-step probabilistic relation $\rto{p}$.

The relation models a step taken from a real
configuration to a real configuration with probability $p$.
A real configuration is a triple
of a configuration $c$,
a distribution of sequences of real interactions
with the store $\interactionsdist$,
and a version map $\versions$.

The version map tracks version numbers for the store to prevent replay attacks, as described above. For technical reasons, instead of the configuration representing the key-value store as a map, we use
the history of store interactions (which includes interactions made both by the computation and the adversary). The sequence of interactions applied to the initial store gives the current store. Because the real store semantics are probabilistic (due to the use of a probabilistic cryptosystem and cryptographic-style probabilistic polynomial-time adversaries), configurations contain distributions over sequences of store interactions.

Real interactions $\interaction$ (and their sequences $\interactions$)  are defined
in Figure <ref> and are similar to interactions with the ideal store. However, instead of labeled values containing ground values, they contain
bitstrings $b$ (expressing the low-level details of the cryptosystem and the ability of the adversary to perform bit-level operations). Additionally,
the interaction $\storecmd{\category}{\categorykey}$ represents storing of a category key. These
interactions arise from the serialize metafunction, which may create new category keys.
Note that the interaction $\storecmd{\gv_k}{\LabeledO{l}{b}}$ does not need an integrity
side condition (as it did in the ideal semantics) in the real semantics since there is
no distinction between corruptions and valid store interactions.

We use notation

\randomExprL f(X_1, ..., X_n) ~|~ X_1 \drawnFrom D_1; ~ ... ~ X_n \drawnFrom D_n \randomExprR

to describe the probability distribution over the function $f$ with inputs of random variables $X_1, ...,  X_n$ where $X_i$ is distributed according to distribution $D_i$ for $1 \leq i \leq n$.

Real Semantics

Figure <ref> presents the inference rules for
Internal steps do not affect the interactions or versions. For storing
(rule Store),
the version of the entry is incremented using the $\incrementnm$ function and
the real configuration uses a new distribution of interactions
$\interactionsdist'$ containing the interactions to store the labeled value.
The new distribution contains the original interactions
(distributed according to the original distribution of interactions)
along with a concatenation of labeled ciphertexts and
any new category keys (distributed according to the distribution
given by serialization function). Note that the label of the stored value is
not encrypted as it is public information.
The configuration steps with probability $1$ as the Store rule
will be used for all $\textsf{store}$ operations.

When fetching a labeled value, there are three possible rules
that can be used depending on the
current state of the store:  Fetch-Exists,  Fetch-Missing,  Fetch-Replay.
The premise,

(\istore, p) \in \randomExprL \interactions(\emptyset) ~|~
\interactions \drawnFrom \interactionsdist \randomExprR

in each of these rules
means that store $\istore$ has probability $p$ of being produced (by drawing
interaction sequence $\interactions$ from distribution  $\interactionsdist$ and applying $\interactions$ to the empty store $\emptystore$ to give store $\istore$).

Which rule is used for a fetch operation depends on the state of the
store, and so the transitions may have probability less than one.

Rule Fetch-Exists is
used when the sequence of interactions drawn produces a store that has a
serialized labeled value indexed by $\gv_k$ that can be correctly deserialized
and whose version is not less than the last version seen at this index.
Rule Fetch-Missing is used when the sequence of interactions
produces a store that either does not have an entry indexed by $\gv_k$, or
has an entry that cannot be correctly deserialized. Finally, Fetch-Replay
rule is used when the sequences of interactions drawn produce a store
where an adversary has attempted to replay an old value:
the store has a labeled value that can be deserialized correctly, but whose
recorded index is not the same as the index requested by the computation
or whose version is less than the version last seen.

= λ.

|          = λ.   [↦]

|        _kl = λ.   [_k ↦l]

Strategies:           :        →

Real Low Step Semantics

Similar to the ideal store semantics, we use a low step relation $\Lowstep{p}$
to model adversary interactions, shown in Figure <ref>.
The low step relation is also probabilistic as it is based on the probabilistic
single step relation $\rto{p}$. Additionally, we use a distribution of sequences of adversarial
interactions $\interactionsdist_A$ to model an
adversary that behaves probabilistically. In rules Low-Step and
Low-To-High-To-Low-Step a new distribution of interactions, $\interactionsdist'$ is created by concatenating interaction sequences drawn from the existing distribution of interactions $\interactionsdist$ and the adversary distribution $\interactionsdist_A$. This is analogous to the application of adversary interactions to the current store in the ideal semantics.

The rest of the definitions of the rules
follow the same pattern as the ideal low step store semantics.

With the low step relation, we use metafunction $\multistepnm$ to describe
the distributions of real configurations resulting from taking $j$
low steps from configuration $c_0$, formally defined in
Figure <ref>. The $\multistepnm$ function
is parameterized by the keystore $\keystore$ and store level $\lowlabel$.

To provide a source of adversary interactions while
running the program, the $\multistepnm$ function also takes as input a
strategy $\strategy$ which is a function from
distributions of interactions to distributions of interactions, representing the
probabilities of interactions an active adversary would perform.
Before each low step, the strategy is invoked to produce a distribution of
interactions that will affect the store that the computation is using.

Strategy $\strategy$ expresses the ability of the attacker to modify the store. The
attacker chooses $\strategy$ (and $t$, $v_0$, and $v_1$), and $\strategy$
interacts with the store during
execution. $\strategy$ is a function from (distributions of) interaction sequences to
(distributions of) interaction sequences, i.e., a function from a history of
what has happened to the store so far to the attacker’s next modifications to
the store. Note that we do not explicitly model fetching from the store as an
adversary interaction.
There is no need for $\strategy$ to fetch values to determine the next
modification to the store since $\strategy$ effectively observes the entire history of store
interactions. At the end of the game when the adversary continuation ($\adversary_2$) needs
to pick $v_0$ or $v_1$, it observes the history of interactions with the store via
the interaction sequence $\interactionsvar{\interaction_b}$, and thus does not need to explicitly get or fetch values.

§ FORMAL PROPERTIES

§.§ Indistinguishability

A cryptosystem is semantically secure
if, informally, ciphertexts of messages of equal length
are computationally indistinguishable.
Two sequences of probability distributions
are computationally indistinguishable (written $\{X_n\}_n \approx \{Y_n\}_n$)
if for all non-uniform probabilistic polynomial time (ppt)
algorithms $\adversary$,

\big| ~ \probabilityOfCond{\adversary(x) = 1}{x \drawnFrom X_n}  - \probabilityOfCond{\adversary(y) = 1}{y \drawnFrom Y_n~ } ~ \big|

is negligible in $n$ <cit.>.

In modern cryptosystems, semantic security is defined as
indistinguishability under chosen-plaintext attacks (CPA)

Let the random variable $\mathrm{IND}_b(\mathcal{A}, n)$ denote
the output of the   experiment, where
$\mathcal{A}$ is non-uniform ppt, $n \in \varmathbb{N}$, $b \in \{0,1\}$ :

\figCPAGame

$\Pi = (\Gen, \Enc, \Dec)$ is Chosen-Plaintext Attack (CPA) secure if for all
non-uniform ppt $\mathcal{A}$:

\Big\{~\mathrm{IND}_0(\mathcal{A}, n)~\Big\}_n \approx \Big\{~\mathrm{IND}_1(\mathcal{A}, n)~\Big\}_n

This definition of indistinguishability phrases the security of the
cryptosystem in terms of a game where
an adversary receives the
public key and then produces two plaintext messages of equal length.

One of the two messages is encrypted and
the resulting ciphertext given to the adversary.
The cryptosystem is CPA Secure if no adversary exists that can
produce substantially different distributions of output
based on the choice
of message. In other words, no computationally-bounded adversary
is able to effectively distinguish which message was encrypted.

relies on a semantically secure cryptosystem, but this
is insufficient
for to protect the confidentiality of
secret information. This is because CPA Security provides guarantees
only for individually chosen plaintext messages.

In contrast, in our setting we consider terms (i.e., programs)
chosen by an adversary.

There are also many principals and as a
result many keys in a real system, so must protect arbitrarily many principals' information from the adversary. Additionally, the adversary may already have
access to some of the keys. Finally, the adversary is active: it can see interactions with the store and issue new interactions adaptively while the program is running.
It can attempt to leverage a computation
to illegitimately produce a value it should not have, or could try to trick the system into leaking secret information by interacting with the store.
Traditionally, these actions of the adversary are modeled by queries to a decryption oracle, as in CCA-2 <cit.>.
Here, they are modeled directly by the language and store semantics.

We chose to formulate a new definition of security that addresses these concerns,
as many previous classical definitions of security fall short in this setting:

* Noninterference does not permit the use of computationally secure mechanisms like

* CPA security considers only the semantics of the cryptographic
algorithms, not the system they are embedded within.

* CCA and CCA2 attempt to
model system behavior using oracles, but the connection between these oracles
and an actual system is too abstract.

In contrast, we chose to employ a computational
model of cryptography that accurately represents the power of the attacker precisely using
the semantics of the language and interactions with the store.

With these considerations in mind, we define indistinguishability
under a new form of attack: chosen-term attacks (CTA).

Let the random variable $\IND{b}{\keystore}{\adversary}{\principals}{j}{n}$ denote
the output of the following experiment, where
$\cryptosys = (\Gen, \Enc, \Dec, \Sign, \Verify)$,
$\adversary$ is non-uniform ppt, $n \in \nat$, $b \in \{0,1\}$:

\figCTAGame

using is CTA Secure if for all
non-uniform ppt $\adversary$, $j \in \varmathbb{N}$, keystores , and principals $\principals$:

\distfam{\IND{0}{\keystore}{\adversary}{\principals}{j}{n}} \cequiv
\distfam{\IND{1}{\keystore}{\adversary}{\principals}{j}{n}}

The CTA game follows the same structure as the CPA game.
In addition, we allow the adversary to know certain information (by fixing it in the game),
including some part of the keystore  ($\keystore_0$),
the set of principals that is protecting ($\principals$), and
the number of low steps the program takes ($j$).
Cryptosystem $\cryptosys$ is used implicitly in the CTA game to generate keys,
encrypt, decrypt, sign and verify[More formally, $\mathrm{IND}_b$, $\adversary$, and
the semantics are also parameterized on $\cryptosys$, and the uses of $\Gen, \Enc, \Dec, \Sign, \Verify$ should be explicitly taken from the tuple $\cryptosys$ though we elide their explicit usage in our notation for clarity.].

In this game setup, $\Gen(\principals, 1^n)$ generates a new keystore
containing private keys for each of the principals in $\principals$,
using the underlying cryptosystem's $\Gen$ function for each keypair.
Then, the adversary receives all public keys of the keystore

returns three well-typed terms: a function $t$, and two program inputs to the function
$v_0$ and $v_1$
that must be confidentiality-only low equivalent $\lowEquivC$
(i.e., they may differ only on secret values)[Complete definition of low equivalence is in <Ref>.]. It also returns a strategy
$\strategy$ that

models the behavior of the adversary on the store while the
computation is running.
Note that the strategy is also polynomial in the security parameter as it
is constructed from a non-uniform polynomial time algorithm.
The program $t$ is run with one of the inputs $v_0$ or $v_1$ for a fixed number of steps $j$.
The adversary receives the interactions resulting from a run
of the program and needs to use that information to determine which secret
input the program was run with.

Being secure under a chosen-term attack means that the sequences of interactions between two low-equivalent programs are indistinguishable and hence an adversary does not learn any secret information from the store despite actively interacting with it while the program it chose is running.

Note that the adversary receives the full trace of interactions on the store
(including its own interactions); this gives it enough information to reconstruct
the final state of the store and any intermediate state.

For any set of principals,
and any adversary store level, the interactions with the store contain
no efficiently extractable secret information for all well-typed terminating

If if CPA Secure, then using is CTA Secure.

We prove this theorem in part by induction over the low step relation
$\Lowstep{p}$, to show that two low equivalent configurations will
produce low equivalent configurations, including computationally
indistinguishable distributions over sequences of interactions. A
subtlety is that we must strengthen the inductive hypothesis to
show that sequences of interactions satisfy a stronger
syntactic relation (rather than  being just computationally

More concretely, the proof follows three high-level steps.
First, we show how a relation $\asymp$ on families of distributions of
sequences of interactions
preserves computational indistinguishability.
That is, if $\interactionsdist_1 \asymp \interactionsdist_2$ and $\cryptosys$ is CPA secure, then $\interactionsdist_1 \approx \interactionsdist_2$.
we show that as two low equivalent configurations step using the low step relation
$\Lowstep{p}$, low equivalence is preserved and the interactions
they produce satisfy the relation $\asymp$.
we show that the use of the $\multistepnm$ metafunction on two
low equivalent configurations will produce computationally indistinguishable distributions
over distributions of sequences of interactions.

Each step of the proof relies on the previous step and the
first step relies on the underlying assumptions on the cryptosystem. We
now describe each step of the proof in more detail.

Step 1: Interactions Relation

We consider pairs of arbitrary distributions of sequences of interactions
and show that, if they are both of a certain syntactic form then they are indistinguishable.
Importantly, the indistinguishability lemmas do not refer to the store semantics,
i.e., they merely describe the form of arbitrary interactions that may or may not
have come from . The invariants on pairs of indistinguishable distributions of
interactions implicitly require low equivalence of the programs that generated them,
and low equivalence circularly requires indistinguishable distributions of interactions.
As a result, we describe the lemmas free from the
store semantics to break the circularity.

We progressively define the relation $\asymp$ on a pair of interactions.
Initially, distributions of interactions only contain secret encryptions so that
we can appeal to a standard cryptographic argument of multi-message security.
for all keystores $\keystore_0$, and
$l_1, ..., l_k$, such that $\canFlowToC{\projC{l_i}}{\projC{\authorityOf{\keystore}}}$, and for all $m_{\{1,2\}}^1 ... m_{\{1,2\}}^n$ and all principals $\principals$, if $|m^i_1| = |m^i_2|$ for all $1 \leq i \leq k$ and $\cryptosys$ is CPA Secure, then

\[
\begin{array}{l}
\big\{ ~ \storecmd{\gv^1}{\Labeled{l^1}{b^1_1}} \cdot  ~...~ \cdot \storecmd{\gv^k}{\Labeled{l^{k}}{b^{k}_1}} ~\big|~ \\ \hspace*{1cm} \keystore \drawnFrom \Gen(1^n); \\ \hspace*{1cm} (pk^i, sk^i) \in rng(\keystore); \\ \hspace*{1cm}  b^i_1 \drawnFrom \Enc(pk^i, m^i_1); ~ 1 \leq i \leq k ~ \big\}_n \\
\multicolumn{1}{c}{\asymp} \\
\big\{ ~ \storecmd{\gv^1}{\Labeled{l^1}{b^1_2}} \cdot  ~...~ \cdot~ \storecmd{\gv^k}{\Labeled{l^{k}}{b^{k}_2}} ~\big|~ \\ \hspace*{1cm} \keystore \drawnFrom \Gen(1^n); \\ \hspace*{1cm} (pk^i, sk^i) \in rng(\keystore); \\ \hspace*{1cm}  b^i_2 \drawnFrom \Enc(pk^i, m^i_2); ~ 1 \leq i \leq k ~ \big\}_n
\end{array}
\]

Using multi-message security as a basis for indistinguishability,
we then expand the relation to contain readable encryptions (i.e.,
ones for which the adversary has the private key to decrypt) where the
values encrypted are the same.

In the complete definiton of $\asymp$, we expand it to also
contain interactions from a strategy,
forming the final relationship on interactions captured by the $\asymp$

We establish an invariant that must hold between pairs in the relation in
order for them to be indistinguishable. For example, in the first definition,
the lengths of each corresponding message between the pair must be the same.
Each intermediate definition of $\asymp$ is used
to show that a ppt can simulate the extra information in the more generalized
definition (thus providing no distinguishing power).
For the first definition of the relation containing only secret encryptions,
a hybrid argument is used similar to showing multi-message
CPA security <cit.>.

Step 2: Preservation of Low Equivalence

We show that as two low equivalent programs $t$ and $t'$ progress, they simultaneously
preserve low equivalence $t \lowEquivC t'$ and the distributions of sequences of interactions they produce $\interactionsdist$ and $\interactionsdist'$ are in the relation $\asymp$.

We first show that if $c_0 \ltol{\alpha} c_0'$ and $c_1 \ltol{\alpha} c_1'$ and $c_0 \lowEquivC c_1$ then $c_0' \lowEquivC c_1'$. This proof takes advantage of
the low equivalence preservation proofs for LIO in all cases except for the
storing and fetching rules. For store events, since all
values being stored will have the same type (due to type soundness), and will be ground values,
serialized values will have the same message lengths.

We then show that if

$$(\rconf{c_0}{\istoredist_0}{\interactionsdist_0}{\versions_0}, \interactionsdist) \Lowstep{p} \rconf{c_0'}{\istoredist_0'}{\interactionsdist_0'}{\versions_0'}$$

$$(\rconf{c_1}{\istoredist_1}{\interactionsdist_1}{\versions_1}, \interactionsdist) \Lowstep{p} \rconf{c_1'}{\istoredist_1'}{\interactionsdist_1'}{\versions_1'}$$

$$(c_0 \lowEquivC c_1) \wedge (\versions_0 = \versions_1) \wedge (\interactionsdist_0 \asymp \interactionsdist_1)$$

$$(c_0' \lowEquivC c_1') \wedge
(\versions_0' = \versions_1') \wedge
(\interactionsdist_0' \asymp \interactionsdist_1').$$

The proof on $\Lowstep{p}$ relies on the previous preservation proof on $\ltol{\alpha}$ and the indistinguishability results on $\asymp$.

Step 3: Indistinguishability of the step metafunction
We show that the $\multistepnm$ metafunction preserves low equivalence. More formally, we show that if

$c_0 \lowEquivC c_1$ and $\versions_0 = \versions_1$ and $\interactionsdist_0 \asymp \interactionsdist_1$

\begin{array}{c}
\{ (\interactionsdist_0', p_0 \cdot ... \cdot p) ~|~ \rconf{c_0}{\istoredist_0}{\interactionsdist_0}{\versions_0} \Lowstep{p_0} ... \Lowstep{p} \rconf{c_0'}{\istoredist_0'}{\interactionsdist_0'}{\versions_0'} \}_n\\
\approx \\
\{ (\interactionsdist_1', p_0' \cdot ...\cdot p') ~|~ \rconf{c_1}{\istoredist_1}{\interactionsdist_1}{\versions_1} \Lowstep{p_0'} ... \Lowstep{p'} \rconf{c_1'}{\istoredist_1'}{\interactionsdist_1'}{\versions_1'} \}_n
\end{array}

We prove this by showing that
the probabilities of traces taken by two low equivalent configurations
are equal with all but negligible probability.

As an example, Figure <ref> shows graphically how one step of the trace is handled.

We examine the result of $\multistepnm_{\keystore}(c_1, \strategy, 1)$ and $\multistepnm_{\keystore}(c_2,$ $\strategy, 1)$ where
$c_1 \lowEquivC c_2$. (Note that this setup matches the instantiation of
the CTA game where $j=1$.) The left rectangle shows the resulting distribution
over distributions of configurations after one step of the
$c_1$ configuration. The right circle
shows the resulting distribution over distributions of configurations
after one step of the $c_2$ configuration. Due to the results from Step 2,
we can reason that $c_1' \lowEquivC c_2'$ and that $c_1'' \lowEquivC c_2''$.
We can also conclude that $\interactionsdist_1 \asymp \interactionsdist_2$
and that $\interactionsdist_1' \asymp \interactionsdist_2'$. The final
step of the proof is to show that the interactions from the
resulting two distributions (i.e.,
the top circle and bottom circle) are computationally indistinguishable.

That is, we
show that $p_1$ is equal to $p_2$ and also $p_1'$ is equal to $p_2'$ with all
but negligible probability.

level 1=[level distance=0cm, sibling distance=4cm]
level 2=[level distance=1.5cm, sibling distance=1.9cm]

bag = [text width=1em, text centered, text width=3cm]
bag2 = [text width=1em, text centered, text width=1.3cm]
end = [circle, minimum width=2pt,fill, inner sep=0pt]

[grow=south, sloped,edge from parent/.style=draw,-latex]
node[bag] (c1 node) $\big(\rconf{c_1}{\emptyset}{\skipcmd}{\versions_0}, \strategy(\skipcmd)\big)$
node[bag2] (c1b node) $\rconf{c_1''}{\istoredist_1'}{\interactionsdist_1'}{\versions_1'}$

edge from parent
node[above=-2pt] $\Lowstep{p_1'}$

node[bag2] (c1a node) $\rconf{c_1'}{\istoredist_1}{\interactionsdist_1}{\versions_1}$

edge from parent
node[above=-2pt] $\Lowstep{p_1}$

edge from parent[draw=none]

node[bag] (c2 node) $\big(\rconf{c_2}{ \emptyset }{ \skipcmd }{\versions_0}, \strategy(\skipcmd)\big)$
node[bag2] (c2b node) $\rconf{c_2''}{\istoredist_2'}{\interactionsdist_2'}{\versions_2'}$

edge from parent
node[above=-2pt, rotate=0] $\Lowstep{p_2'}$

node[bag2] (c2a node) $\rconf{c_2'}{\istoredist_2}{\interactionsdist_2}{\versions_2}$

edge from parent
node[above=-2pt] $\Lowstep{p_2}$

edge from parent[draw=none]
[bend right,dashed]
(c2 node) to node[below=3pt, rotate=-0]  $\lowEquivC$  (c1 node);
[bend left=60,dashed]
(c2b node) to node[above=1pt, rotate=-0]  $\lowEquivC$   (c1b node);
[bend left=60,dashed]
(c2a node) to node[above=1pt, rotate=-0]  $\lowEquivC$   (c1a node);

[draw,fit=(c1b node) (c1a node) ,inner sep=2mm,rounded corners=1mm] (d1) ;
[below=8mm of d1] ${\multistepnm_{\keystore}(c_1, \strategy, 1)}$;
[draw,fit=(c2b node) (c2a node) ,inner sep=2mm,rounded corners=1mm] (d2) ;
[below=8mm of d2] ${\multistepnm_{\keystore}(c_2, \strategy, 1)}$;

Low equivalence is preserved in $\multistepnm_{\keystore}$ for two low
equivalent configurations $c_1$ and $c_2$ and a strategy $\strategy$.

§.§ Leveraged Forgery

Whereas in the previous subsection we considered the security of encryptions,
in this case we consider the security of the signatures.
We show that an adversary cannot leverage a computation to
illegitimately produce a signed value.

A digital signature scheme is secure if it is difficult
to forge signatures of messages.

requires its digital signature scheme to be secure against existential forgery under a chosen-message attack, where the adversary is a non-uniform ppt in the size of the key. Often stated informally
in the literature <cit.>,
a digital signature scheme is secure against
existential forgery if no adversary can succeed in forging the signature of one message, not necessarily of his choice. Further, the scheme is secure under a chosen-message attack if the adversary is allowed to ask the signer to sign a number of messages of the adversary’s choice. The choice of these messages may depend on previously obtained signatures.

Parallel to CPA and CTA,
we adapt the definition of existential forgery for , which
we call leveraged forgery.
Intuitively, it should not be the case that a high integrity signature can be produced for a value when it is influenced by low integrity information.
We capture this intuition in the following theorem:

For a principal $p$ and all keystores $\keystore_0$, non-uniform ppts $\adversary$, and labels $l_1$, integers $j, j'$, where $\lowlabel = \authorityOf{\keystore_0}$ and $\canFlowToI{\projI{l_1}}{p}$, if $\cryptosys$ is secure against existential forgery under chosen-message attacks, then

\figForgeryProb

Intuitively, the game is structured as follows.

First, an adversary chooses a term $t$ and strategy $\strategy$ that will be run with high integrity (i.e., $\Start{\keystore}$ where $\keystore$ has $p$'s authority). The adversary sees the interactions $\interactions$ produced by the high integrity computation (which in general will include high integrity signatures).

With that information, the adversary constructs a new term $t'$ and new strategy $\strategy'$ that will be run with low integrity (i.e., $\Start{\keystore_0}$). Note that the strategy may internally encode high integrity signatures learned from the high integrity run that it can place in the store.

The interactions produced by this low integrity computation should not contain any high integrity signatures (i.e., are signed by $p$). The adversary succeeds if it produces
a new valid labeled bitstring $\Labeled{l_1}{b}$
that did not exist in the first run.
In the experiment, the $\mathrm{Values}_{\keystore}$ metafunction
extracts the set of valid labeled bitstrings (i.e., can be deserialized
correctly) using the parameterized keystore $\keystore$ to perform
the category key decryptions.

The proof of this theorem is in two parts.
First we show that the label of a value being stored
by a computation is no more trustworthy than the current label of
computation. Second, we show that the current label never
becomes more trustworthy than the starting label.
This means that a low integrity execution (i.e., starting from
$\conf{\Start{\keystore_0}}{\Clr{\keystore}}{t}$) cannot
produce a high integrity value (i.e., a labeled value $\Labeled{l}{b}$
such that $\projI{l} \flows^I p$).

§.§ Soundness

A trivially secure but intuitively incorrect version of the crypto store semantics is to simply not
put anything in the store and just always return “missing” for fetch operations.

Indeed, cryptosystems have similar independence between security and correctness.
For example, a cryptosystem $(\Enc, \Dec)$ is only correct
if $\forall m.~\Dec(\Enc(m)) = m$. So we need to define an analogous
notion of “correctness.”

We define correctness in terms of the ideal semantics. That is, the ideal semantics is the “spec” of
what correct behavior should be. To do this, we must relate real interactions to ideal interactions.
We do that with the following translation function.

We describe the adversary in the ideal semantics through a simiplified language of adversary interactions $\iinteraction \Coloneqq \skipcmd~|~\storecmd{\gv}{\Labeled{l}{\gv}}~|~\corruptcmd{\gv, ..., \gv}$. The skip command has no effect on the store, the store command will replace the entries, and corrupt will replace the entry's value with the distinguished “corrupted” value $\missing$. That is,
$\corruptcmd{\gv_1, ..., \gv_n} = \lambda \istore. ~\istore[\gv_1 \mapsto \missing\; ... \gv_n \mapsto \missing]$

Note that CLIO does not protect against availability attacks (e.g., corrupt). As a result, corrupted entries are treated as “missing”. There are ways to combat this sort of corruption (e.g., replication, error correcting codes, etc.), which we do not model.

We can relate the real interactions $\interaction$ and ideal interactions $\iinteraction$ on a store $\istore$ using a translation function $\translate{\keystore}{\istore}{\versions}{\interaction} = \iinteraction$.

The translation function is parameterized by $\keystore$ (the power of the adversary; i.e., what it knows) and the current state of the store it is interacting on. It produces an ideal interaction with adversarial power equal to $\authorityOf{\keystore}$.
The definition of the translation function is given as follows:

For commands, the translation is straightforward: $\translate{\keystore}{\istore}{\versions}{\skipcmd} = \skipcmd$.

When a store is made, the real interaction corresponds to an ideal interaction when the bitstream can be properly deserialized and its version is not old. That is, $\translate{\keystore}{\istore}{\versions}{\storecmd{\gv_k}{\Labeled{l}{\bitstream}}} = \storecmd{\gv_k}{\Labeled{l}{\gv}}$
if $\Labeled{l}{(\gv, \version)} = \deserialize{\istore}{\Labeled{l}{\bitstream}}$ and $\version \not< \versions(\gv_k)$. If the value cannot be deserialized then we treat it as a corrupted entry, i.e., $\corruptcmd{\gv_k}$. Note that it could still be the case that bitstring was actually valid (e.g., the adversary may have guessed a correct ciphertext) and as a result this translation may not be morally equivalent to the real interaction. As we will formally show later, though, these discrepancies in the translation function between a real interaction and an ideal interaction will only occur with negligible probability.

Finally, an adversary may alter the category keys. $\translate{\keystore}{\istore}{\versions}{\storecmd{\category}{\categorykey}} = \skipcmd$ when
$\fetchck{\istore}{\category} = \fetchck{\istore[\category \mapsto \categorykey]}{\category}$. Otherwise,
$\translate{\keystore}{\istore}{\versions}{\storecmd{\category}{\categorykey}} = \corruptcmd{\gv_1, ..., \gv_j}$ for all $\gv_i \in \gv_1, ..., \gv_j$ and where $\LabeledO{l_i}{b_i} = \sigma(\gv_i)$ and $l_i$ contains category $\category$.

Note that this translation is conservative with respect to the possible ideal interactions corresponding to a real interaction. A real store interaction might not corrupt a key entry if the adversary had access to the private key beyond what is in $\mathcal{P}$ or if it is able to “replay” a previous value it saw. However, informally (which we will formalize and make more precise in our soundness theorem), if we assume that keys are difficult to guess and CLIO prevents replay attacks, then with all but a negligible probability the store interaction will not be a valid serialization and it will corrupt the key entry.

With this specification of correct terms with respect to real interactions, we can now state our soundness theorem:

For all ideal configurations $c_i$, real configurations $c_r$, and strategies drawn from a non-uniform ppt adversary, if $c_i ~\mathcal{R}~ c_r$ then,

\begin{array}{l}
\mathbf{Pr}\big[ (c_i', c_r') \not\in \mathcal{R} ~ \big| ~
\interactions \drawnFrom \strategy(\textsf{store}(c_r)); ~
\iinteractions = \mathcal{T}(c_r, \interactions); \\
\hspace*{22mm} (c_i, \iinteractions) \Lowstep{} c_i'; ~
(c_r, \interactions) \Lowstep{p} c_r'
\big]
\end{array}

is negligible in $n$.

\begin{array}{lll}
% (c_i, \iinteractions) & \mathcal{R} & (c_r, \interactions) \\
% \multicolumn{3}{r}{\mathrm{if~} c_i ~\mathcal{R}~ c_r \mathrm{~and~} \iinteractions = \mathcal{T}(c_r, \interactions)}\\
% (c_r, \interactions) & \mathcal{R} & (c_i, \iinteractions) \\
% \multicolumn{3}{r}{\mathrm{if~} c_i ~\mathcal{R}~ c_r \mathrm{~and~} \iinteractions = \mathcal{T}(c_r, \interactions)}\\
\iconf{\conf{\lcur}{\lclr}{t}}{\istore_i} & \mathcal{R} & \rconf{\conf{\lcur}{\lclr}{t}}{\istore_r}{\interactions}{\versions} \\
\multicolumn{3}{r}{\mathrm{if~} \istore_i ~\mathcal{R}~ \istore_r}
\end{array}

§ IN PRACTICE

§.§ Implementation

We implemented a prototype as a Haskell library, in the same
style as LIO. Building on the LIO code base, the library has
an API for defining and running programs embedded in
Haskell. The library also implements a monitor that oversees the
execution of the program and orchestrates three interdependent tasks:

* Information-flow control executes the usual LIO IFC
enforcement mechanism; in particular, it adjusts the current label
and clearance and checks that information flows according
to the DC labels lattice.

* External key-value store handles all interactions with the
store, realized as an external Redis <cit.> database. This is
accomplished by using the hedis <cit.> Haskell library, which
implements a Redis client.
reviewer B: I’m having a hard time imagining how a more realistic system would be used in practice. Do you imagine the Redis is simply outsourced to a generic remote service? What about practical details like distributing the public keys initially, or adding new participants?

* Cryptography takes care of managing and handling
cryptographic keys as well as invoking cryptographic operations to
protect the security of the principals' data as it crosses the
system boundary into/back from the untrusted store. Instead of
implementing our own cryptographic primitives, we leverage the
third-party cryptonite <cit.> library.

uses standard cryptographic schemes to protect the information in
the store. In particular, for efficiency reasons we use a hybrid
scheme that combines asymmetric cryptography with symmetric
encryption. The category keys in the store are encrypted and signed
with asymmetric schemes, while the entries stored by programs are
encrypted with symmetric encryption and signed with an asymmetric
signature scheme.

Asymmetric cryptography
We use cryptonite's implementation
of RSA, specifically OAEP mode for encryption/decryption and PSS for
signing/verification, both with 1024-bit keys and using SHA256 as a
hash. We get around the message size limitation by chunking the
plaintext and encrypting the chunks separately.

Symmetric encryption
We use cryptonite's implementation of
AES, specifically AES256 in Counter (CTR) mode for symmetric
encryption. We use randomized initialization vectors
for each
We can use AESNI if the
architecture supports it.

Storing and retrieving category keys and labeled values are
implemented as discussed in Section <ref>. Appendix <ref> has more

P:Maybe move this somewhere else?
LIO-style enforcement mechanisms have performed adequately in
practice, c.f. Hails <cit.>. We do not expect
combining this with off-the-shelf crypto to introduce more than a
constant time overhead for fetching and writing into the store. The
only additional concern is the overhead of the category key management
protocol, which is proportional to the number of distinct categories
and their size. Based on the experience obtained by Jif <cit.>,
Fabric <cit.>, and Hails, categories are
usually small in number and size. Furthermore, creating category keys
incurs a one-time cost which can be amortized over multiple runs and

§.§ Case Study

We have implemented a simple case study to illustrate how our
prototype implementation can be used to build an application. In
this case, we have built a system that models a tax preparation tool
and its interactions with a customer (the taxpayer) and the tax
reporting agency, communicating via a shared untrusted store. We model
these three components as principals $C$ (the customer), $P$ (the
preparer) and $\IRS$ (the tax reporting agency). The actions of each
of these three principals are modeled as separate computations
,  and ,
respectively. We assume that the store level $\lowlabel$ restricts writes to the store in confidential contexts,
i.e. $\ell = \ltrip{\bot}{\top}{S}$, where $S$ is the principal
running as the store.

In this scenario, we consider that the principals involved ($C$, $P$
and $\IRS$) trust each other and are trying to protect their data from
all other principals in the system (i.e., from $S$).

The customer $C$ initially makes a record with his/her personal
information, including his/her name, social security number (SSN),
declared income and bank account details, modeled as the type
.  Figure <ref> shows the customer
code on the left, modeled as a function that takes this record as an argument,
. The first step is to label  with the label
$\ltrip{C \vee P \vee \IRS}{C}{S}$.

The confidentiality component is a disjunction of all the principals
involved in the interaction, reflecting the fact that the customer
trusts both the preparer and the IRS with their the data and expects
them to be able to read it.

A more realistic example would also keep the customer's personal data
confidential (i.e. not readable by the IRS and to some extent by the
preparer). However, expressing those flows would require an IFC system
with declassification, a feature that we have not included in the
current version of since it would introduce additional
complexity in our model, and semantic security conditions for such
systems are still an active area of research <cit.>.  Without
declassification, if $\IRS$ was not in the label initially, the IFC
mechanism would not allow us to release this data (or anything derived
from it) to the IRS at a later time.

The integrity component of this label is just $C$ since this
data can be vouched for only by the customer at this point, while the
availability is trusted since these values haven't been exposed to (and potentially
corrupted by) the
adversary in the store yet. The final step of the customer is to store
their labeled  at key  for
the preparer to see. Note that in practice this operation creates a
category key for $C\vee P\vee \IRS$, stores it in the database and
uses it to encrypt the data, which gets signed by $C$.

\begin{array}{l}
\texttt{customerCode} :: \texttt{TaxpayerInfo} \to \CLIOT{()}  \\
\texttt{customerCode}\;\;\; \mathit{tpi} = \mathbf{do}  \\
\begin{array}{ll}
\quad &\mathit{info} \leftarrow \llabel{\ltrip{C\vee P\vee \IRS}{C}{S}}{\mathit{tpi}} \\
& \store{\texttt{"taxpayer\_info"}}{\mathit{info}} \\
& \return{()}
\end{array}
\end{array}

\begin{array}{l}
\texttt{preparerCode} :: \CLIOT{()}  \\
\texttt{preparerCode} = \mathbf{do}  \\
\begin{array}{ll}
\quad & \mathit{default} \leftarrow
\llabel{\ltrip{P\vee\IRS}{P\vee
C}{S}}{\mathit{notFound}} \\
& \mathit{info} \leftarrow
\fetch{\texttt{"taxpayer\_info"}}{\mathit{default}} \\
& r \leftarrow \toLabeled{\ltrip{P\vee\IRS}{P\vee
C}{S}} \$\;\; \mathbf{do} \\
& \begin{array}{ll}
& i \leftarrow \unlabel{\mathit{info}} \\
& \return{(\texttt{prepareTaxes}\;\; i)}
\end{array} \\
&  \store{\texttt{"tax\_return"}}{r}
\end{array}
\end{array}

\begin{array}{l}
\texttt{irsCode} :: \CLIOT{\BoolT}  \\
\texttt{irsCode} = \mathbf{do}  \\
\begin{array}{ll}
\quad & \textbf{let}\;\; \mathit{l} = \ltrip{\IRS}{P\vee C\vee
\IRS}{S} \\
& \mathit{default}\leftarrow
\llabel{l}{\mathit{emptyTR}} \\
& \mathit{lv} \leftarrow
\fetch{\texttt{"tax\_return"}}{\mathit{default}} \\
& \mathit{tr}  \leftarrow \unlabel{\mathit{lv}} \\
& \return{(\texttt{verifyReturn}\;\; \mathit{tr})}
\end{array}
\end{array}

Customer code (left), Preparer code (middle), and IRS code (right)

The next step is to run the preparer code, shown in the middle of
Figure <ref>. The preparer starts by fetching the
taxpayer data at key , using a default empty
record labeled with $l_1 = \ltrip{P\vee\IRS}{P\vee C}{S}$. The
entry in the database is labeled differently with
$l_2 =\ltrip{C\vee P\vee \IRS}{C}{S}$, but the operation succeeds
because $l_2 \sqsubseteq l_1$ and the availability
in $l_2$ is $S$, i.e., it reflects the fact that the adversary $S$ might have
corrupted this data.

The code then starts a $\texttt{toLabeled}$
sub-computation to securely manipulate the labeled taxpayer record
without raising its current label. In the subcomputation, we unlabel
this labeled record and use function  to prepare
the tax return. Since we are only concerned with the information-flow
aspects of the example, we elide the details of how this function
works; our code includes a naive implementation but it would be
straightforward to extend it to implement a real-world tax preparation
operation. The $\text{toLabeled}$ block wraps the result in a labeled
value $r$ with label $l_1$, the argument to
$\text{toLabeled}$. Finally, the preparer stores the labeled tax
return $r$ at key . Note that this operation would
fail if we had not used $\text{toLabeled}$, since in that case the
current label, raised by the $\text{unlabel}$ operation, would not
flow to $\ell$, the label of the adversary.

Figure <ref> shows the tax agency code
on the right. This code fetches the
tax return made by the preparer and stored at key
. Analogously to the preparer code, we use the
default value of the fetch operation to specify the target label of
the result, namely $\ltrip{\IRS}{P\vee C\vee \IRS}{S}$, which in this case is
once again more restrictive than what is stored in the
database. Thereafter the labeled tax return gets unlabeled and the
information is audited in function , which
returns a boolean that represents whether the declaration is
correct. In a more realistic application, this auditing would be
performed inside a $\text{toLabeled}$ block too, but since we are not
doing any further $\text{store}$ operations we let the current label
get raised for simplicity.

These three pieces of code are put together in the main function of
the program, which we elide for brevity. This function simply
generates suitable keystores for the principals involved (using the
library function ) and then runs the
code for each principal using the  function.

§ RELATED WORK

reviewer: expected more technical comparison to prior systems providing crypto soundness for lang-based IFC
reviewer: proof technique seems similar to CoSP by Backes, Hofheinz, and Unruh
Language-based approaches.  Combining cryptography and IFC languages is
not new.

The Decentralized Label Model (DLM) <cit.> has been
extended with cryptographic
operations <cit.>. These
extensions, however, either use only symbolic models of cryptography
or provide no security properties for their system.

Models for secure declassification are an active area of research in the IFC
community (e.g., <cit.>).
It is less clear, though, how such models compose with cryptographic attacker
models. Exploring the interactions between declassification and
cryptography is very interesting, but a rigorous treatment of it is beyond the
scope of this work.

Cryptographically-masked flows <cit.>

account for
covert information-flow channels due to the cryptosystem (e.g., an observer may
distinguish different ciphertexts for the same message).

However, this approach ignores the probability distributions for ciphertexts, which might
compromise security in some scenarios <cit.>.

Laud <cit.> establishes conditions under which secure
programs with cryptographically-masked flows

satisfy computational noninterference <cit.>.

Fournet and Rezk <cit.> describe a language that directly embeds
cryptographic primitives and provide a language-based model of correctness,
where cryptographic games are encoded in the language itself so that security
can range from symbolic correctness to computational noninterference.

Information-flow availability has not been extensively studied.

Li et al. <cit.> discuss the relationship between availability and
and state a (termination- and
progress-insensitive) noninterference property for availability.

Zheng and Myers <cit.> extend the DLM with availability policies, which
express which principals are trusted to make data available.

In their setting, availability is, in essence, the integrity of
progress <cit.>: low-integrity
inputs should not affect the availability of high-availability outputs.

In our work, availability tracks the successful verification of signatures and
decryption of ciphertexts, and has analogies with Zheng and Myers' approach.

The problem of conducting proofs of trace-based properties of
languages with access to cryptographic operations in a computational
setting has been studied before.
CoSP <cit.> is
a framework for writing computational soundness proofs
of symbolic models. Their approach abstracts details such as
message scheduling and corruption models and allows for proofs of
preservation of trace properties to be developed in a modular fashion. What do we have to say about the comparison?

Cryptographic approaches. There is much work on how to
map principals and access policies to cryptographic keys.
Attribute-Based Encryption <cit.> could be used to protect the confidentiality
of data for categories and would avoid the need for category keys
when encrypting and decrypting.
Ring signatures <cit.> could be used to protect the integrity
of data for categories and would similarly avoid the need for category
keys when signing and verifying. We take the approach
of using simpler cryptographic primitives as they are more
amenable to our proofs. Additionally, as a benefit of taking a
language-based approach, 's ideal semantics is agnostic
to the choice of cryptosystem used.
From a user's perspective
the underlying cryptographic operations could be swapped out in favor of more
efficient cryptosystems without changing the semantics of the system
(provided the real semantics was shown separately
to provide CTA security and security against leveraged forgery).

There is also work on strengthening the guarantees of existing cryptosystems
to protect against more powerful adversaries, e.g.,
Chosen Ciphertext Attack (CCA) <cit.> security for adversaries that can
observe decryptions of arbitrary ciphertexts. CCA security is needed in systems where an adversary can
observe (some of) the effects of decrypting arbitrary ciphertexts.

In contrast,
's security guarantees are based on a very precise definition of the
adversary's power over the system. In particular it captures
that an adversary cannot observe anything about the decryptions
of confidential values due to IFC mechanisms, since the results of
such a decryption would be
protected by a label that is more confidential than an adversary would have
access to.
As a result, requires only a CPA secure cryptosystem to be CTA secure.

DStar <cit.> extends decentralized IFC in a distributed system.

Every DStar node has an exporter that is responsible for communicating
over the network.

Exporters also establish the security categories trusted by a node via
private/public keys.

Fabric <cit.> is a platform and statically-checked fine-grained IFC language.  Fabric
supports the secure transfer of data as well as code <cit.>
through, in part, the use of cryptographic mechanisms.

In contrast to Fabric, provides coarse-grained IFC and uses DC labels
instead of the DLM.

In contrast to both DStar and Fabric, this work establishes a formal basis for
security of the use of cryptography in the system.

The lack of a formal proof in both DStar and Fabric is not surprising, given
that they target more ambitious and complex scenarios
decentralized information-flow control for distributed systems).

Remote storage.

While data can be stored and fetched cryptographically, information
can be still leaked through access patterns.

Private Information Retrieval protocols aim to avoid such leaks by hiding
queries and answers from a potentially malicious server <cit.>
similar to 's threat model.

For performance reasons <cit.>,
some approaches rely on a small trusted execution
environment provided by hardware <cit.> that
provides the cryptographic support needed to obliviously query the data
store <cit.>.

This technique can be seen in oblivious computing
<cit.>, online advertising <cit.>, and credit networks

for clients which are benign or follow an strict access protocol.

If clients are malicious, however,
attacker's code may leak information though access patterns.

We force communication with the store to occur in non-sensitive contests. In addition,

language-based techniques could be extended to require
untrusted code to follow an oblivious protocol.

§ CONCLUSION

is a computationally secure coarse-grained dynamic information-flow control
library that uses cryptography to protect the confidentiality and integrity of
data. The use of cryptography is hidden from the language operations and is controlled
instead through familiar language constructs in an existing IFC library, LIO. Further,
we present a novel proof technique that combines standard programming language
and cryptographic proof techniques to show the interaction between the
high-level security guarantees provided by information flow control
and the low-level guarantees offered by the cryptographic mechanisms are secure.
We also provide a prototype implementation in the form of a Haskell library extending LIO to evaluate its practicality. We see as a way for
programmers that are non-expert cryptographers
to use cryptography securely.

This material is based upon work supported by the National Science Foundation under Grant No.s 1421770 and 1524052. Any opinions, findings, and conclusions or recommendations expressed in this material are those of the authors and do not necessarily reflect the views of the National Science Foundation. This research is also supported by the Air Force Research Laboratory and the Swedish research agencies VR and STINT.

#1     #1#1#1     #1     #1     #1     #1#1          #1#1

[Anderson and NeedhamAnderson and
authorpersonRoss Anderson and personRoger
Needham. year1995.
Robustness Principles for Public Key Protocols. In
booktitleAnnual International Cryptology Conference.

[Arden, George, Liu, Vikram, Askarov, and
MyersArden et al2012]
authorpersonOwen Arden, personMichael D.
George, personJed Liu, personK. Vikram,
personAslan Askarov, and personAndrew C. Myers.
Sharing Mobile Code Securely with Information Flow
Control. In booktitleProceedings of the 2012 IEEE Symposium
on Security and Privacy. pages191–205.

[Arden, Liu, and MyersArden
et al2015]
authorpersonOwen Arden, personJed Liu,
and personAndrew C. Myers. year2015.
Flow-Limited Authorization. In
booktitleProceedings of the IEEE 28th Computer Security
Foundations Symposium. pages569–583.

[Askarov and ChongAskarov and Chong2012]
authorpersonAslan Askarov and
personStephen Chong. year2012.
Learning is Change in Knowledge: Knowledge-based
Security for Dynamic Policies. In booktitleProceedings of
the IEEE Computer Security Foundations Symposium.

[Askarov, Hedin, and SabelfeldAskarov
et al2006]
authorpersonAslan Askarov, personDaniel
Hedin, and personAndrei Sabelfeld.
Cryptographically-Masked Flows. In
booktitleProceedings of the 13th International Static
Analysis Symposium.

[Askarov, Hunt, Sabelfeld, and SandsAskarov
et al2008]
authorpersonAslan Askarov, personSebastian
Hunt, personAndrei Sabelfeld, and personDavid
Sands. year2008.
Termination-Insensitive Noninterference Leaks More
Than Just a Bit. In booktitleProceedings of the 13th
European Symposium on Research in Computer Security: Computer Security.

[Askarov and SabelfeldAskarov and
authorpersonAslan Askarov and personAndrei
Sabelfeld. year2007.
Gradual Release: Unifying Declassification,
Encryption and Key Release Policies. In booktitleProceedings
of the IEEE Symposium on Security and Privacy. pages207–221.

[Askarov, Zhang, and MyersAskarov
et al2010]
authorpersonAslan Askarov, personDanfeng
Zhang, and personAndrew C. Myers.
Predictive black-box mitigation of timing
channels. In booktitleProceedings of the 17th ACM
Conference on Computer and Communications Security.

authorpersonD. Asonov.
booktitleQuerying Databases Privately: A New Approach
to Private Information Retrieval.

[Backes, Hofheinz, and UnruhBackes
et al2009]
authorpersonMichael Backes, personDennis
Hofheinz, and personDominique Unruh.
CoSP: A General Framework for Computational
Soundness Proofs. In booktitleProceedings of the 16th ACM
Conference on Computer and Communications Security.

[Backes, Kate, Maffei, and PecinaBackes
et al2012]
authorpersonMichael Backes, personAniket
Kate, personMatteo Maffei, and personKim Pecina.
ObliviAd: Provably Secure and Practical Online
Behavioral Advertising. In booktitleProceedings of the 2012
IEEE Symposium on Security and Privacy.

[Bethencourt, Sahai, and WatersBethencourt
et al2007]
authorpersonJohn Bethencourt, personAmit
Sahai, and personBrent Waters.
Ciphertext-policy attribute-based encryption. In
booktitleProc. of the 2007 IEEE Symposium on Security and
Privacy. pages321–334.

[Broberg and SandsBroberg and Sands2010]
authorpersonNiklas Broberg and personDavid
Sands. year2010.
Paralocks: Role-based Information Flow Control and
Beyond. In booktitleProceedings of the ACM SIGPLAN-SIGACT
Symposium on Principles of Programming Languages.

[Cheng, Ports, Schultz, Popic, Blankstein,
Cowling, Curtis, Shrira, and LiskovCheng et al2012]
authorpersonWinnie Cheng, personDan R.K.
Ports, personDavid Schultz, personVictoria Popic,
personAaron Blankstein, personJames Cowling,
personDorothy Curtis, personLiuba Shrira, and
personBarbara Liskov. year2012.
Abstractions for Usable Information Flow Control in
Aeolus. In booktitleProceedings of the 2012 USENIX Annual
Technical Conference. pages139–151.

[Chong and MyersChong and Myers2006]
authorpersonStephen Chong and
personAndrew C. Myers. year2006.
Decentralized Robustness. In
booktitleProceedings of the 19th IEEE Workshop on Computer
Security Foundations. pages242–256.

[Chor, Goldreich, Kushilevitz, and SudanChor
et al1995]
authorpersonB. Chor, personO. Goldreich,
personE. Kushilevitz, and personM. Sudan.
Private Information Retrieval. In
booktitleProceedings of the 36th Annual Symposium on
Foundations of Computer Science.

[Chothia, Duggan, and VitekChothia
et al2003]
authorpersonTom Chothia, personDominic
Duggan, and personJan Vitek. year2003.
Type-Based Distributed Access Control. In
booktitleProceedings of the 16th IEEE Computer Security
Foundations Workshop. pages170–186.

[De Groef, Devriese, Nikiforakis, and
PiessensDe Groef et al2012]
authorpersonWillem De Groef, personDominique
Devriese, personNick Nikiforakis, and personFrank
Piessens. year2012.
FlowFox: a web browser with flexible and precise
information flow control. In booktitleProceedings of the
2012 ACM Conference on Computer and communications security.

authorpersonTim Dierks.
titleThe Transport Layer Security (TLS) Protocol Version
howpublishedRFC 5246.   (year2008).

[Ding, Yang, Deng, and WangDing
et al2010]
authorpersonXuhua Ding, personYanjiang
Yang, personRobert H. Deng, and personShuhong
Wang. year2010.
A new hardware-assisted PIR with O(n) shuffle
journalInternational Journal of Information
Security volume9, number4 (year2010).

[Fournet and RezkFournet and Rezk2008]
authorpersonCédric Fournet and
personTamara Rezk. year2008.
Cryptographically Sound Implementations for Typed
Information-flow Security. In booktitleProceedings of the
35th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming
Languages. pages323–335.

[Gazeau, Chothia, and DugganGazeau
et al2017]
authorpersonIvan Gazeau, personTom Chothia,
and personDominic Duggan. year2017.
Types for Location and Data Security in Cloud
Environments. In booktitleProceedings of the IEEE Computer
Sec. Foundations Symposium.

[Giffin, Levy, Stefan, Terei, Mazières,
Mitchell, and RussoGiffin et al2012]
authorpersonDaniel B. Giffin, personAmit
Levy, personDeian Stefan, personDavid Terei,
personDavid Mazières, personJohn Mitchell, and
personAlejandro Russo. year2012.
Hails: Protecting Data Privacy in Untrusted Web
Applications. In booktitleProceedings of the Symposium on
Operating Systems Design and Implementation.

[Goguen and MeseguerGoguen and
authorpersonJ. A. Goguen and personJ.
Meseguer. year1982.
Security Policies and Security Models. In
booktitleProceedings of the IEEE Symposium on Security and
Privacy. pages11–20.

[Goldwasser and BellareGoldwasser and
authorpersonShafi Goldwasser and
personMihir Bellare. year2001.
booktitleLecture Notes on Cryptography.
Chapter 10.

[Goldwasser and MicaliGoldwasser and
authorpersonShafi Goldwasser and
personSilvio Micali. year1982.
Probabilistic Encryption & How to Play Mental
Poker Keeping Secret All Partial Information. In booktitleProceedings of the 14th Annual ACM Symposium on Theory of Computing.

authorpersonVincent Hanquez.
titleThe cryptonite library.

[Hedin, Birgisson, Bello, and SabelfeldHedin
et al2014]
authorpersonDaniel Hedin, personArnar
Birgisson, personLuciano Bello, and personAndrei
Sabelfeld. year2014.
JSFlow: Tracking information flow in JavaScript
and its APIs. In booktitleProceedings of the 29th ACM
Symposium on Applied Computing.

authorpersonRedis Labs.

authorpersonPeeter Laud.
Semantics and Program Analysis of Computationally
Secure Information Flow. In booktitleProceedings of the 10th
European Symposium on Programming Languages and Systems.

authorpersonPeeter Laud.
On the Computational Soundness of Cryptographically
Masked Flows. In booktitleProceedings of the 35th Annual ACM
SIGPLAN-SIGACT Symposium on Principles of Programming Languages.

[Li, Mao, and ZdancewicLi
et al2003]
authorpersonPeng Li, personYun Mao, and
personSteve Zdancewic. year2003.
Information integrity policies. In
booktitleProceedings of the Workshop on Formal Aspects in
Security and Trust.

[Liu, George, Vikram, Qi, Waye, and MyersLiu
et al2009a]
authorpersonJed Liu, personMichael D.
George, personK. Vikram, personXin Qi,
personLucas Waye, and personAndrew C. Myers.
Fabric: A Platform for Secure Distributed
Computation and Storage. In booktitleProceedings of the ACM
SIGOPS Symposium on Operating Systems Principles.

[Liu, George, Vikram, Qi, Waye, and MyersLiu
et al2009b]
authorpersonJed Liu, personMichael D.
George, personK. Vikram, personXin Qi,
personLucas Waye, and personAndrew C. Myers.
Fabric: A Platform for Secure Distributed
Computation and Storage. In booktitleProceedings of the ACM
SIGOPS 22nd Symposium on Operating Systems Principles.

[Maas, Love, Stefanov, Tiwari, Shi, Asanovic,
Kubiatowicz, and SongMaas et al2013]
authorpersonMartin Maas, personEric Love,
personEmil Stefanov, personMohit Tiwari,
personElaine Shi, personKrste Asanovic,
personJohn Kubiatowicz, and personDawn Song.
PHANTOM: Practical Oblivious Computation in a
Secure Processor. In booktitleProceedings of the ACM
SIGSAC Conference on Computer & Communications Security.

authorpersonJohn McLean.
Security Models and Information Flow. In
booktitleProceedings of the IEEE Symposium On Security And
Privacy. pages180–187.

authorpersonMichael Mimoso.
titleD-Link Accidentally Leaks Private Code-Signing
(dateSept. year2015).

[Moreno-Sanchez, Kate, Maffei, and
PecinaMoreno-Sanchez et al2015]
authorpersonPedro Moreno-Sanchez,
personAniket Kate, personMatteo Maffei, and
personKim Pecina. year2015.
Privacy Preserving Payments in Credit Networks:
Enabling trust with privacy in online marketplaces. In
booktitleProceedings of the Network and Distributed System
Security Symposium.

[Myers and LiskovMyers and Liskov1998]
authorpersonAndrew C. Myers and
personBarbara Liskov. year1998.
Complete, Safe Information Flow with Decentralized
Labels.. In booktitleProceedings of the IEEE Symposium on
Security and Privacy.

[Myers, Sabelfeld, and ZdancewicMyers
et al2006]
authorpersonAndrew C. Myers, personAndrei
Sabelfeld, and personSteve Zdancewic.
Enforcing Robust Declassification and Qualified
journalJournal of Computer Security
volume14, number2 (dateApril
year2006), pages157–196.

[Myers, Zheng, Zdancewic, Chong, and
NystromMyers et al01  ]
authorpersonA. C. Myers, personL. Zheng,
personS. Zdancewic, personS. Chong, and
personN. Nystrom. year2001–.
titleJif: Java Information Flow.
Software release. <http://www.cs.cornell.edu/jif>.

[Olumofin and GoldbergOlumofin and
authorpersonFemi G. Olumofin and personIan
Goldberg. year2011.
Revisiting the Computational Practicality of
Private Information Retrieval. In booktitleProceedings of
the 15th International Conference on Financial Cryptography and Data

[Pass and ShelatPass and Shelat2010]
authorpersonRafael Pass and personAbhi
Shelat. year2010.
booktitleA Course in Cryptography
(edition3rd ed.).
Chapter 7.

authorpersonFalko Peters.
titleThe hedis library.

[Rivest, Shamir, and TaumanRivest
et al2006]
authorpersonRonald L Rivest, personAdi
Shamir, and personYael Tauman.
How to leak a secret: Theory and applications of
ring signatures.
In booktitleTheoretical Computer Science.

[Roy, Porter, Bond, McKinley, and WitchelRoy
et al2009]
authorpersonIndrajit Roy, personDonald E.
Porter, personMichael D. Bond, personKathryn S.
McKinley, and personEmmett Witchel.
Laminar: Practical Fine-grained Decentralized
Information Flow Control. In booktitleProceedings of the ACM
SIGPLAN Conference on Programming Language Design and Implementation.

authorpersonAlejandro Russo.
Functional Pearl: Two Can Keep a Secret, if One
of Them Uses Haskell. In booktitleProceedings of the 20th
ACM SIGPLAN International Conference on Functional Programming.

authorpersonRafia Shaikh.
titleMicrosoft Accidentally Leaks Xbox Live Keys, User
Data at Risk of Man-in-the-Middle Attacks.
(dateDec. year2015).

authorpersonV. Simonet.
titleThe Flow Caml System.  (dateJuly
Software release at
<http://cristal.inria.fr/ simonet/soft/flowcaml/>.

[Sion and CarbunarSion and Carbunar2007]
authorpersonRadu Sion and personBogdan
Carbunar. year2007.
On the Computational Practicality of Private
Information Retrieval. In booktitleProceedings of the
Network and Distributed Systems Security Symposium. Stony Brook Network
Security and Applied Cryptography Lab Tech Report.

[Smith and AlpízarSmith and
authorpersonGeoffrey Smith and
personRafael Alpízar. year2006.
Secure Information Flow with Random Assignment and
Encryption. In booktitleProceedings of the 4th ACM Workshop
on Formal Methods in Security. pages33–44.

[Smith and SaffordSmith and Safford2001]
authorpersonS. W. Smith and personD.
Safford. year2001.
Practical Server Privacy with Secure Coprocessors.
journalIBM Systems Journal volume40,
number3 (dateMarch year2001).

[Stefan, Russo, Mazières, and
MitchellStefan et al2011a]
authorpersonDeian Stefan, personAlejandro
Russo, personDavid Mazières, and personJohn C.
Mitchell. year2011a.
Disjunction Category Labels. In
booktitleProceedings of the 16th Nordic Conference on
Security IT Systems. pages223–239.

[Stefan, Russo, Mitchell, and
MazièresStefan et al2011b]
authorpersonDeian Stefan, personAlejandro
Russo, personJohn C. Mitchell, and personDavid
Mazières. year2011b.
Flexible Dynamic Information Flow Control in
Haskell. In booktitleProceedings of the 4th ACM symposium
on Haskell. pages95–106.

[Stefan, Yang, Marchenko, Russo, Herman, Karp,
and MazièresStefan et al2014]
authorpersonDeian Stefan, personEdward Z.
Yang, personPetr Marchenko, personAlejandro Russo,
personDave Herman, personBrad Karp, and
personDavid Mazières. year2014.
Protecting Users by Confining JavaScript with
COWL. In booktitleProceedings of the 11th Symposium on
Operating Systems Design and Implementation.

[Vaughan and ZdancewicVaughan and
authorpersonJeffrey A. Vaughan and
personSteve Zdancewic. year2007.
A Cryptographic Decentralized Label Model. In
booktitleProceedings of the 2007 IEEE Symposium on Security
and Privacy. pages192–206.

authorpersonVeracode. year2015.
booktitleState of Software Security.
Vol. volume6.

[Wang, Ding, Deng, and BaoWang
et al2006]
authorpersonShuhong Wang, personXuhua Ding,
personRobert H. Deng, and personFeng Bao.
Private Information Retrieval Using Trusted
Hardware. In booktitleProceedings of the 11th European
Symposium on Research in Computer Security. pages49–64.

[Waye, Buiras, Arden, Russo, and ChongWaye
et al2017]
authorpersonLucas Waye, personPablo Buiras,
personOwen Arden, personAlejandro Russo, and
personStephen Chong. year2017.
Cryptographically Secure Information Flow Control
on Key-Value Stores. In booktitleProceedings of the ACM
SIGSAC Conference on Computer and Communications Security.

[Waye, Buiras, King, Chong, and RussoWaye
et al2015]
authorpersonLucas Waye, personPablo Buiras,
personDan King, personStephen Chong, and
personAlejandro Russo. year2015.
It's My Privilege: Controlling Downgrading in
DC-Labels. In booktitleProceedings of the 11th
International Workshop on Security and Trust Management.

[Whitten and TygarWhitten and Tygar1999]
authorpersonAlma Whitten and personJ. D.
Tygar. year1999.
Why Johnny Can't Encrypt: A Usability Evaluation
of PGP 5.0. In booktitleProceedings of the 8th Conference
on USENIX Security Symposium.

[Williams and SionWilliams and Sion2008]
authorpersonPeter Williams and personRadu
Sion. year2008.
Usable PIR. In booktitleProceedings of the Network and Distributed System Security Symposium.

[Yip, Narula, Krohn, and MorrisYip
et al2009]
authorpersonAlexander Yip, personNeha
Narula, personMaxwell Krohn, and personRobert
Morris. year2009.
Privacy-preserving browser-side scripting with
BFlow. In booktitleEuroSys.

[Zdancewic and MyersZdancewic and
authorpersonSteve Zdancewic and
personAndrew C. Myers. year2001.
Robust Declassification. In
booktitleProceedings of the 14th IEEE Computer Security
Foundations Workshop. pages15–23.

[Zeldovich, Boyd-Wickizer, and
MazièresZeldovich et al2008]
authorpersonNickolai Zeldovich, personSilas
Boyd-Wickizer, and personDavid Mazières.
Securing Distributed Systems with Information Flow
Control. In booktitleProceedings of the 5th USENIX Symposium
on Networked Systems Design and Implementation. pages293–308.

[Zheng and MyersZheng and Myers2005]
authorpersonLantian Zheng and
personAndrew C. Myers. year2005.
End-to-End Availability Policies and
Noninterference. In booktitleProceedings of the 18th IEEE
Computer Security Foundations Workshop. pages272–286.

§ COMPLETE DEFINITIONS

§.§ Security Lattice Orderings and Operators

We use three lattices (Confidentiality, Integrity, and Availability)
whose domains (named C, I, and A) are formulas of principals in conjuctive normal form.
define an information flow ordering $\flows$ (read as “can flow to”). We
give the definitions of each below, where $\Rightarrow, \wedge, \vee$ are the usual classical logical connectives:

§.§.§ Confidentiality

\[
\begin{array}{r@{\,}c@{\;\;}l}
\canFlowToC{C}{C'}      &\iff&     C' \Rightarrow C \\
\canFlowToStrictC{C}{C'}      &\iff&     \canFlowToC{C}{C'} \textand C \neq C' \\
\cjoin{C}{C'}     &\iff&     C \wedge      C' \\
\cmeet{C}{C'}     &\iff&     C \vee        C' \\
\bot_C \equiv True    &    &     \top_C \equiv False
\end{array}
\]

§.§.§ Integrity

\[
\begin{array}{r@{\,}c@{\;\;}l}
\canFlowToI{I}{I'}      &\iff&     I \Rightarrow I' \\
\canFlowToStrictI{I}{I'}      &\iff&     \canFlowToI{I}{I'} \textand I \neq I' \\
\ijoin{I}{I'}     &\iff&     I \vee        I' \\
\imeet{I}{I'}     &\iff&     I \wedge      I' \\
\bot_I \equiv False   &    &     \top_I \equiv True
\end{array}
\]

§.§.§ Availability

\[
\begin{array}{r@{\,}c@{\;\;}l}
\canFlowToA{A}{A'}      &\iff&     A \Rightarrow A' \\
\canFlowToStrictA{A}{A'}      &\iff&     \canFlowToA{A}{A'} \textand A \neq A' \\
\ajoin{A}{A'}     &\iff&     A \vee        A' \\
\ameet{A}{A'}     &\iff&     A \wedge      A' \\
\bot_A \equiv False   &    &     \top_A \equiv True
\end{array}
\]

We define the security lattice of DC labels as a product lattice of the three individual lattices to form a security lattice whose domain is a triple of principal formulas ($l = \ltrip{C}{I}{A}$) and whose ordering is based on safe information flows. We also define a trust ordering $\trusts$ (read as “at least as trustworthy as”):

\[
\begin{array}{r@{\,}c@{\;\;}l}
\canFlowTo{\ltrip{C}{I}{A}}{\ltrip{C'}{I'}{A'}}      &\iff&
\canFlowToC{C}{C'} \textand \canFlowToI{I}{I'} \textand \canFlowToA{A}{A'}  \\
\canFlowToStrict{\ltrip{C}{I}{A}}{\ltrip{C'}{I'}{A'}}      &\iff&
\canFlowToStrictC{C}{C'} \textor \canFlowToStrictI{I}{I'} \textor \canFlowToStrictA{A}{A'}  \\

\canTrustTo{\ltrip{C}{I}{A}}{\ltrip{C'}{I'}{A'}}      &\iff&
\canFlowToC{C}{C'} \textand \canFlowToI{I'}{I} \textand \canFlowToA{A'}{A}  \\

\join{\ltrip{C}{I}{A}}{\ltrip{C'}{I'}{A'}}     &\iff&
\ltrip{~\cjoin{C}{C'}~}{~\ijoin{I}{I'}~}{~\ajoin{A}{A'}~} \\
\meet{\ltrip{C}{I}{A}}{\ltrip{C'}{I'}{A'}}     &\iff&
\ltrip{~\cmeet{C}{C'}~}{~\imeet{I}{I'}~}{~\ameet{A}{A'}~} \\
\bot \equiv \ltrip{\bot_C}{\bot_I}{\bot_A}   &    &     \top \equiv \ltrip{\top_C}{\top_I}{\top_A}
\end{array}
\]

For convenience of avoiding pattern matching over the components of a label when needing to inspect an individual component, we define the following projection functions:

\[
\begin{array}{r@{\,}c@{\;\;}l}
\projC{\ltrip{C}{I}{A}} &=& C \\
\projI{\ltrip{C}{I}{A}} &=& I \\
\projA{\ltrip{C}{I}{A}} &=& A
\end{array}
\]

§.§ Cryptography Background Definitions

* Distribution Ensemble: An ensemble of probability distributions is a sequence $\{X_n\}_{n \in \mathcal{N}}$ of probability distributions.

* Negligible Function: A negligible function is a function $f(x) : \mathbb{N} \rightarrow \mathbb{R}$ such that for every positive integer $c \in \mathbb{Z}^+$ there exists an integer $N_c$ such that for all $x > N_c$:

\big| f(x) \big| < \frac{1}{x^c}

* Computationally Indistinguishable: Let $\{X_n\}_n$ and $\{Y_n\}_n$ be distribution ensembles. Then we say that they are computationally indistinguishable $\approx$ if for any non-uniform PPT $\adversary$ the following function is negligible in $n$:

\big| \probabilityOfCond{\adversary(x) = 1}{x \drawnFrom X_n}  - \probabilityOfCond{\adversary(y) = 1}{y \drawnFrom Y_n} \big|

* Hybrid Argument:  Let $X_1, ..., X_m$ be a sequence of probability distributions, where $m$ is polynomial in $n$. Suppose
there exists a distinguisher $D$ that distinguishes $X_1$ and $X_m$ with probability $\epsilon$. Then there exists $i \in [1, m - 1]$ such that $D$ distinguishes $X_i$ and $X_{i+1}$ with probability $\frac{\epsilon}{m}$. (Proof uses Triangle Inequality)

* Cryptosystem: We consider a asymmetric encryption system and signature scheme $\Pi = (\Gen, \Enc, \Dec, \Sign, \Verify)$ such that $\Gen : 1^n \rightarrow (\{0, 1\}^n, \{0, 1\}^n)$ representing the public key and private key to use in the assymetric cryptographic functions.

* Correctness of Cryptosystem For correctness of our encryption system, we require that if $p \in \{0, 1\}^*$ and $(pk, sk) \drawnFrom \Gen(1^n)$ and $c = \Enc(pk, p)$ then $p = \Dec(sk, c)$.

For correctness of our signature scheme, we require that if $p \in \{0, 1\}^*$ and $(pk, sk) \drawnFrom \Gen(1^n)$ and $s = \Sign(sk, p)$ then $1 = \Verify(pk, s)$.

To simplify the notation while mainting easy-to-prove security properties, we require that the encryption and signature functions operate on independent parts of the key; that is, they internally use a key derivation function (e.g., encryption uses the first half, and signing uses the second half).

* Security of Cryptosystem: For our encryption functions, we assume the cryptosystem is CPA secure, defined as follows <cit.>.

Let the random variable $\mathrm{IND}_b(\adversary, n)$ denote
the output of the   experiment, where
$\adversary$ is a non-uniform p.p.t., $n \in \varmathbb{N}$, $b \in \{0,1\}$ :

\figCPAGame

Then we say that $\Pi$ is CPA (Chosen-Plaintext Attack) secure if for all
non-uniform p.p.t. $\adversary$:

\Big\{~\mathrm{IND}_0(\adversary, n)~\Big\}_n \approx \Big\{~\mathrm{IND}_1(\adversary, n)~\Big\}_n

Note that we consider the cryptographic functions themselves to be public.

For security of the signature scheme, we assume $\Pi$ is secure against existential forgery.

* Indistinguishability Corrollary: The CPA definition may be difficult to understand to some as it is phrased in the form of a game. An alternative definition of security (that is a fairly direct consequence of CPA security) is: For all $p_0, p_1$, if $|p_0| = |p_1|$ then,

\Big\{ ~\Enc(pk, p_0) ~|~ (pk, sk) \drawnFrom \Gen(1^n)~ \Big\}_n \approx
\Big\{ ~\Enc(pk, p_1) ~|~ (pk, sk) \drawnFrom \Gen(1^n)~ \Big\}_n

Informally, the results of encrypting of equal-length plaintexts are computationally indistinguishable.

* Digital Signature Forgery: We require our digital signature scheme to be secure against existential forgery under a Chosen-Message Attack, where the adversary is a non-unfiorm ppt in the size of the key <cit.>:

* Existential Foregery: The adversary succeeds in forging the signature of one message, not necessarily of his choice.

* Chosen-Message Attack: The adversary is allowed to ask the signer to sign a number of messages of the adversary’s choice. The choice of these messages may depend on previously obtained signatures. For example, one may think of a notary public who signs documents on demand.

§.§ Complete Syntax and Typing Rules

\begin{align*}
\figLioSyntaxFull
\end{align*}

§.§ Remaining Step Rules

The program state is $c = \conf{\lcur}{\lclr}{t}$ where $\lcur$ is the
current label, $\lclr$ is the current clearance.
Computation is modeled as a small-step semantics $c \ltol{\event~} c'$.
We use labels $\event$ to represent interaction with the store.

Where $\lowlabel$ is the store adversary level.

§.§ Complete Low Equivalence Relation

§.§.§ Confidentiality Low Equivalence

Define to be the low equivalence relation with respect to
only confidentiality. The integrity and availability parts of
the label are ignored.

$\gv_1$     $\lowEquivC$     $\gv_2$     if $\gv_1 = \gv_2$

$\LabeledO{l_1}{\gv_1}$     $\lowEquivC$     $\LabeledO{l_1}{\gv_2}$    where

\left\{
\begin{array}{lll}
\gv_1 = \gv_2 & \mathrm{if} & \projC{l_1} \flows^C \projC{\lowlabel} \\
\typeOf{\gv_1} = \typeOf{\gv_2} & \multicolumn{2}{l}{\mathrm{otherwise} }
\end{array}
\right.

$(v_1, v_2)$     $\lowEquivC$     $(v_1', v_2')$    if $v_1 \lowEquivC v_1'$ and $v_2 \lowEquiv v_2'$

$t_1\ t_2$     $\lowEquivC$     $t_1'\ t_2'$    if $t_1 \lowEquivC t_1'$ and $t_2 \lowEquiv t_2'$

$\conf{\lcur}{\lclr}{t}$     $\lowEquivC$     $\conf{\lcur'}{\lclr'}{t'}$     if $t \lowEquivC t'$ and
$\lcur = \lcur'$ and  $\lclr = \lclr'$

$\conf{\lcur}{\lclr}{t}$     $\lowEquivC$     $\conf{\lcur'}{\lclr'}{t'}$     if $\projC{\lcur} \not\flows^C \projC{\lowlabel}$ and $\projC{\lcur'} \not\flows^C \projC{\lowlabel}$  and $\projC{\lclr} \not\flows^C \projC{\lowlabel}$ and $\lclr' \not\flows^C \projC{\lowlabel}$

§.§ Ideal Complete Syntax and Semantics

The ideal state is $\iconf{c}{\istore}$ where $c$ is the
configuration and $\istore$ is a mapping
$\istore : \gv \rightarrow \Labeled{l}{\gv}_{\missing}$, where $\missing$
represents a corrupted entry.

Ideal interactions $\iinteraction$ are given by the following syntax:

The low-step relation $\Lowstep{\iinteractionsvar{\iinteraction}}{}$ from
ideal configurations to configurations using adversary interaction $\iinteractions$.

§.§ Complete Definitions for Labeled Value Serialization

reviewer: doesn't account for version indexes, which should be needed for Theorem 2

* $\initializecknm(\istore, C) = (\fetchcknm(\istore, C), \skipcmd)$ if $\fetchcknm(\istore, C)$ defined

* $\initializecknm(\istore, C) = (\fetchcknm(R(\istore), C), R)$ if $\fetchcknm(\istore, C)$ undefined and $R = \createcknm(\istore, C)$

* $\createcknm(\istore, p_1  \vee ... \vee p_n) = \mathrm{store}~(p_1 \vee ... \vee  p_i \vee ... \vee p_n)~(pk, m_n, s)$ where

$(pk, sk) \drawnFrom \mathrm{Gen}(1^n)$

$m_0 = \emptyset$

for $i$ from $1$ to $n$:

$(pk_i, sk_i) = \keystore(p_i)$

$m_i \drawnFrom m_{i-1}[p_i \mapsto \Enc(pk_i, sk)]$

$s \drawnFrom \Sign(sk_i, (pk, m))$ if $sk_i \neq \bot$

* $\fetchcknm(\istore, p_1 \vee ... \vee p_i \vee ... \vee p_n) = (pk, sk)$ where

$(pk, m, s) = \istore(p_1 \vee ... \vee p_i \vee ... \vee p_n)$

$(pk_i, sk_i) = \keystore(p_i)$ where $i$ chosen s.t. $sk_i \neq \bot$

$sk = \Dec(sk_i, m(p_i))$

$\Verify(pk_j, (pk, m), s) = 1$ for some $pk_j$ in the category.

* $\Enc_{\keystore}(\istore_0, \langle C_1 \wedge ... \wedge C_i \wedge ... \wedge C_n, l_i \rangle, v_0) = (R_n \cdot ... \cdot R_1, v_n)$ where

for $i$ from $1$ to $n$:

$((pk_i, sk_i), R_i) \drawnFrom \initializecknm(\istore_{i-1}, C_i)$

$\istore_i = R_i(\istore_{i-1})$

$v_i \drawnFrom \Enc(pk_i, v_{i-1})$

* $\Sign_{\keystore}(\istore_0, \langle l_c, C_1 \wedge ... \wedge C_n \rangle, v) = (R_n \cdot ... \cdot R_1, s_1, ..., s_n)$ where

for $i$ from $1$ to $n$:

$((pk_i, sk_i), R_i) \drawnFrom \initializecknm(\istore_{i-1}, C_i)$

$\istore_i = R_i(\istore_{i-1})$

$s_i \drawnFrom \Sign(sk_i, v)$

* $\Dec_{\keystore}(\istore, \langle C_1  \wedge ... \wedge C_n, l_i \rangle, v_n) = v_0$ where

for $i$ from $n$ to $1$:

$(pk_i, sk_i) = \fetchcknm(\istore, C_i)$

$v_{i-1} = \Dec(sk_i, v_{i})$

* $\Verify_{\keystore}(\istore, \langle l_c, C_1  \wedge ... \wedge C_n \rangle, v, s_1, ..., s_n) = 1$ if

for $i$ from $n$ to $1$:

$(pk_i, sk_i) = \fetchcknm(\istore, C_i)$

$1 = \Verify(pk_i, v, s_i)$

Similar to the category key meta-functions, we also annotate the results of the meta-functions with the interactions made on the store so that we can track what actions are being taken on the crypto store.

With these cryptographic functions operating on labels, we are now ready to describe the meta-functions which convert a labeled value to a bit string and vice-versa.

* $\serializenm_{\keystore}(\istore, \LabeledO{l}{\gv}) = \randomExpr{(\overline{R_2} \cdot \overline{R_1} , \LabeledO{l}{\bitstream})}{(\overline{R}, b) \drawnFrom \Enc_{\keystore}(\overline{R_1}(\istore), l, (\gv, s_1, ..., s_n));~ (\overline{R_1}, s_1, ..., s_n) \drawnFrom \Sign_{\keystore}(\istore, l, \gv) }$

* $\deserializenm_{\keystore}(\istore, \LabeledO{l}{\bitstream}, \tau) =  \LabeledO{l}{\gv}$ if $\Verify_{\keystore}(\istore, l, \gv, s_1, ..., s_n) = 1$ and $\Dec_{\keystore}(\istore, l, b) = (\gv, s_1, ..., s_n)$ and $\typeOf{\gv} = \tau$

We use the convenience function $\mathrm{pub}(\keystore)$ to represent the projection of the keystore that only contains the public key parts of the keystores, and no private keys.

§.§ Real Complete Syntax and Semantics

The interaction concatenation operation $\concat{\interaction}{\interaction}$ sequences interactions. We use the notation $\interactions = \concat{\interaction}{\concat{...}{\interaction}}$ to denote a sequence of interactions.

The real state is $\rconf{c}{\istore}{\interactionsdist}{\versions}$
where $c$ is the configuration, $\istore$ is the store.

The low-step relation $\Lowstep{p}$ from
real configurations and adversary interactions to configurations with probability $p$.

The step function encodes the distribution of real states after taking $j$ low steps:

Note that, we consider only configurations and strategies that can and always will take at least $j$ low steps for all strategies. That is, there is no possibility for a trace to fail to make a low step before $j$ low steps. As a result, the step function will always produce a distribution (i.e., their probabilities will add up to 1). The program should be written in such a way that it is defensively written to ensure that it can take at least $j$ low steps.

§ COMPLETE THEOREMS AND PROOFS

§.§ Interaction Indistinguishability Lemmas

For all $m_{\{1,2\}}^1 ... m_{\{1,2\}}^n$ and all principals
$\principals$, if $|m^0_i| = |m^1_i|$ for all $1 \leq i \leq k$, and
$\cryptosys$ is CPA Secure, then

\[
\begin{array}{c}
% \big\{ ~ \Enc_\keystore(\istore^1_1, l^1, \gv^1_1);  ~...~ \Enc_\keystore(\istore^{\,i}_1, l^{\,i}, \gv^{\,i}_1); ~  ...; ~\Enc_\keystore(\istore^k_1, l^k, \gv^k_1) ~|~ \keystore \drawnFrom \Gen(1^n) ~ \big\} \\
% \approx \\
% \big\{ \Enc_\keystore(\istore^1_2, l^1, \gv^1_2);  ~...~ \Enc_\keystore(\istore^{\,i}_2, l^{\,i}, \gv^{\,i}_2); ~  ...; ~\Enc_\keystore(\istore^k_2, l^k, \gv^k_2) ~|~ \keystore \drawnFrom \Gen(1^n) ~  \big\}
\big\{ \Enc(pk^1_1, m^1_1),  ~...,~ \Enc(pk^{\,i}_1, m^{\,i}_1), ~  ..., ~\Enc(pk^k_1, m^k_1) ~\big|~ \keystore \drawnFrom \Gen(\principals, 1^n); ~ (pk^i_2, sk^i_2) \in rng(\keystore);  ~ 1 \leq i \leq k \big\}_n \\
\approx \\
\big\{ \Enc(pk^1_2, m^1_2),  ~...,~ \Enc(pk^{\,i}_2, m^{\,i}_2), ~  ..., ~\Enc(pk^k_2, m^k_2) ~\big|~ \keystore \drawnFrom \Gen(\principals, 1^n); ~ (pk^i_2, sk^i_2) \in rng(\keystore); ~ 1 \leq i \leq k \big\}_n \\
\end{array}
\]

We perform a proof by contradiction: we assume the consequent does not hold
and construct a counter-example to the CPA-security of $\cryptosys$.

The lengths of the sequences of encryptions are equal by setup. The sequences are also polynomial in $n$ as each low step produces a polynomial number of messages and the number of low steps is polynomial in $n$ as $k$ is fixed.

This setup is equivalent to the multi-message CPA security problem. We use the same general technique to show that single-message CPA security. gives rise to multi-message CPA security by using a hybrid argument.

We can define a hybrid sequence of messages

H_i = \big\{ m^1_1;  ~...;~ m^{\,i}_1; ~   m^{\,i+1}_2; ~  ...; ~m^k_2 \}

such that at the point $i$ we switch from using the sequence of messages from the first run to using the sequence of messages from the second run. By the hybrid argument, there must exist an $i$ that distinguishes $H_i$ and $H_{i+1}$ with non-negligible probability in $n$. We will fix on that $i$. So we can now construct the following CPA adversary:

* By assumption of our proof by contradiction, there exists a Round 1 adversary that can distinguish $H_i$ and $H_{i+1}$ for a particular $i$ and particular $m^{\{0,1\}}_1, ..., m^{\{0,1\}}_n$, and call it $\adversary_{R1}$.

* In our construction, we generate a new keystore $\keystore$ as defined in the lemma statement and give the plaintext messages $m^{i+1}_2$ and $m^{i+1}_1$ to the CPA game and it will then provide us back a ciphertext $c$ of one of the messages.

* We create a new sequence of encrypted messages in the following way:

H = \big\{ \Enc(pk^1_1, m^1_1);  ~...;~ \Enc(pk^i_1, m^{\,i}_1); ~  c; ~ \Enc(pk^{i+2}_2, m^{\,i+2}_2); ~  ...; ~\Enc(pk^k_2, m^k_2) ~\big|~ pk^o_{\{1,2\}} \drawnFrom \Gen(1^n); 1 \leq o \leq k \} \}

In the case where the CPA game chose message $m^{i+1}_2$ we have that $H = H_i$ and in the other case where $m^{i+1}_1$ we have that $H = H_{i+1}$. Since $\adversary_{R1}$ can distinguish exactly this case and that the choice of message encrypted determines which sequence of messages was used, we can as a result distinguish which plain-text message was chosen by the CPA game with non-negligible probability.

As a result of constructing a CPA adversary that can distinguish plain-text messages with non-negligible probability, we have shown a contradiction, and can conclude that the above sequences of encryptions is indistinguishable.

Let $L_{\keystore}(\interactions)$ to be a fixed function (i.e., it does not change its behavior based on its inputs) from interactions to interactions such that the result contains the original sequence of interactions
with low interactions added at statically fixed locations in the sequence. Let the resulting sequences of interactions be called low equivalent interactions.

A low interaction is a $\skipcmd$ command or a $\storecmd{\gv_k}{\Labeled{l_1}{b}}$ such that
$\projC{l_1} \flows^C \projC{\authorityOf{\keystore}} \textand
\Labeled{l_1}{(\gv, \gv_k, n)} = \deserializenm_{\keystore}({\interactions},{\Labeled{l_1}{b}})$ or $\storecmd{\category}{\principals'}$.

For all keystores $\keystore_0$, and
$l_1, ..., l_k$, such that $\canFlowToC{\projC{l_i}}{\projC{\authorityOf{\keystore}}}$, and for all $m_{\{1,2\}}^1 ... m_{\{1,2\}}^n$ and all principals $\principals$, if $|m^i_1| = |m^i_2|$ for all $1 \leq i \leq k$ and $\cryptosys$ is CPA Secure, then

\[
\begin{array}{c}
\big\{ ~ L_{\keystore_0}\Big(\storecmd{\gv^1}{\Labeled{l^1}{b^1_1}} \cdot  ~...~ \cdot \storecmd{\gv^k}{\Labeled{l^{k}}{b^{k}_1}} \Big) ~|~ \keystore \drawnFrom \Gen(1^n); ~ (pk^i, sk^i) \in rng(\keystore); ~ b^i_1 \drawnFrom \Enc(pk^i, m^i_1); ~ 1 \leq i \leq k ~ \big\}_n \\
\approx \\
\big\{ ~ L_{\keystore_0}\Big(\storecmd{\gv^1}{\Labeled{l^1}{b^1_2}} \cdot  ~...~ \cdot~ \storecmd{\gv^k}{\Labeled{l^{k}}{b^{k}_2}} \Big) ~|~ \keystore \drawnFrom \Gen(1^n); ~ (pk^i, sk^i) \in rng(\keystore); ~ b^i_2 \drawnFrom \Enc(pk^i, m^i_2); ~ 1 \leq i \leq k ~ \big\}_n
\end{array}
\]

We perform a reduction to the Round 1 adversary. That is, if there exists a Round 2 adversary $\adversary_{R2}$ then there also exists a Round 1 adversary, which will provide a contradiction.

We construct our adversary as follows. Given a sequence of secret encryptions (from Round 1), we can construct the input to the $L$ function by constructing a constant set of labels $l_1$ to $l_n$ arbitrarily so long as they flow to $\projC{\authorityOf{\keystore}}$, which is a static property and also arbitrary input keys. We can then also construct the entry keys $v^i$ in the same static fashion. When then just apply the deterministic $L$ function and pass that to $\adversary_{R2}$.

Since we have shown how to construct a Round 1 adversary from a Round 2 adversary, we have a contradiction of the Round 1 lemma, so we conclude our proof.

Let $m^1_{\{1,2\}}, ..., m^k_{\{1,2\}}$ be sequences of messages such that $|m^i_1| = |m^i_2|$. Further, let $\interactions^1_{\{1,2\}}, ..., \interactions^j_{\{1,2\}}$ be sequences of low equivalent interactions (from Definition 2) whose ciphertexts are based on slices of the underlying message. For example

\[
\begin{array}{lcl}
\interactions^1_1 &=& \storecmd{\category}{(b, \{ p \mapsto \Enc(pk, m^1_1) \}, b_s)}  ~ \cdot ~ \storecmd{\gv_1}{\Enc(pk, m^2_1)} \\
\interactions^2_1 &=& \skipcmd \\
\interactions^3_1 &=& \storecmd{\gv_3}{\Enc(pk', m^3_1)} \\
\multicolumn{2}{c}{...} \\
\interactions^j_1 &=& \storecmd{\gv_j}{\Enc(pk'', m^k_1)}
\end{array}
\]

Then we say two sequences of interactions are equivalent $\asymp$ iff they are of the form, with all but negligible probability,

\[
\begin{array}{rcl}
\big\{ ~ \interactions^{1}_{1} ~ \cdot ~ \interactions'^{2}_{1} \cdot ... \cdot ~
\interactions^{j}_{1}  ~ \cdot ~ \interactions'^j_1
& ~\Big|~ & \keystore \drawnFrom \Gen(1^n); ~ (pk^i, sk^i) \in rng(\keystore); ~ b^i_1 \drawnFrom \Enc(pk^i, m^i_1); ~ 1 \leq i \leq k; ~ \\
&& t, v_{\{0,1\}}, \strategy \drawnFrom \adversary(1^n); ~
\interactions'^{s}_1 \drawnFrom \strategy(\interactions^{s}_1 \cdot ... \cdot \interactions^{j}_1 \cdot \interactions'^{j}_1); ~ 1 < s < j; ~ \interactions'^{j}_1 \drawnFrom \strategy(\skipcmd)
~ \big\}_n \\
\multicolumn{3}{c}{\asymp} \\
\big\{ ~ \interactions^{1}_{2} ~ \cdot ~ \interactions'^{2}_{2} \cdot ... \cdot ~