Flame is a library and plugin for GHC
that enforces information security
policies in Haskell programs. In Flame, sensitive
information is protected by monad-like types that specify
how information may flow according to the Flow-Limited Authorization Model. The operations of these
Flame monads implement the type system constraints of the
Flow-Limited Authorization Calculus (FLAC).
Applying consensus and replication securely with FLAQR
A formal language for building application-level consensus and replication protocols
that are secure by construction.
CSF’22
Distinguished paper award
Mondal, Priyanka and Algehed, Maximilian and Arden, Owen
@inproceedings{flaqr,
author = {Mondal, Priyanka and Algehed, Maximilian and Arden, Owen},
booktitle = {35\textsuperscript{th} {IEEE} Computer Security Foundations Symp. (CSF)},
title = {Applying consensus and replication securely with FLAQR},
series = {CSF'22},
year = {2022},
month = aug,
doi = {10.1109/CSF54842.2022.9919637},
volume = {},
number = {},
month_numeric = {8}
}
Availability is crucial to the security of distributed systems, but
guaranteeing availability is hard, especially when participants in the system
may act maliciously. Quorum replication protocols provide both integrity and
availability: data and computation is replicated at multiple independent hosts,
and a quorum of these hosts must agree on the output of all operations applied
to the data. Unfortunately, these protocols have high overhead and can be
difficult to calibrate for a specific application’s needs. Ideally, developers
could use high-level abstractions for consensus and replication to write
fault-tolerant code by that is secure by construction.
%
This paper presents Flow-Limited Authorization for Quorum Replication (FLAQR),
a core calculus for building distributed applications with heterogeneous quorum
replication protocols while enforcing end-to-end information security. Our type
system ensures that well-typed FLAQR programs cannot fail (experience an
unrecoverable error) in ways that violate their typelevel specifications. We
present noninterference theorems that characterize FLAQR’s confidentiality,
integrity, and availability in the presence of consensus, replication, and
failures, as well as a liveness theorem for the class of majority quorum
protocols under a bounded number of faults.
A Calculus for Flow-Limited Authorization: Expanded Technical Report
A core programming model that uses flow-limited authorization to provide end-to-end
information security to dynamic authorization mechanisms and programs that use them.
Technical Report
Revised, corrected, and expanded version of CSF’16 paper
Arden, Owen and Gollamudi, Anitha and Cecchetti, Ethan and Chong, Stephen and Myers, Andrew C
@techreport{jflac,
title = {A Calculus for Flow-Limited Authorization: Expanded Technical Report},
author = {Arden, Owen and Gollamudi, Anitha and Cecchetti, Ethan and Chong, Stephen and Myers, Andrew C},
journal = {arXiv preprint arXiv:2104.10379},
doi = {10.48550/arXiv.2104.10379},
year = {2021}
}
Real-world applications routinely make authorization decisions
based on dynamic computation. Reasoning about dynamically computed authority is
challenging. Integrity of the system might be compromised if attackers can
improperly influence the authorizing computation. Confidentiality can also be
compromised by authorization, since authorization decisions are often based on
sensitive data such as membership lists and passwords. Previous formal models
for authorization do not fully address the security implications of permitting
trust relationships to change, which limits their ability to reason about
authority that derives from dynamic computation. Our goal is an approach to
constructing dynamic authorization mechanisms that do not violate
confidentiality or integrity. The Flow-Limited Authorization Calculus (FLAC)
is a simple, expressive model for reasoning about dynamic authorization as well
as an information flow control language for securely implementing various
authorization mechanisms. FLAC combines the insights of two previous models: it
extends the Dependency Core Calculus with features made possible by the
Flow-Limited Authorization Model. FLAC provides strong end-to-end information
security guarantees even for programs that incorporate and implement rich
dynamic authorization mechanisms. These guarantees include noninterference and
robust declassification, which prevent attackers from influencing information
disclosures in unauthorized ways. We prove these security properties formally
for all FLAC programs and explore the expressiveness of FLAC with several
examples.
First-Order Logic for Flow-Limited Authorization
A logic for reasoning about authorization decisions in the presence of information-flow policies.
CSF’20
Hirsch, Andrew K. and Azevedo de Amorim, Pedro Henrique and Cecchetti, Ethan and Tate, Ross and Arden, Owen
@inproceedings{flafol,
author = {{Hirsch, Andrew K.} and {Azevedo de Amorim, Pedro Henrique} and {Cecchetti, Ethan} and {Tate, Ross} and {Arden, Owen}},
booktitle = {33\textsuperscript{rd} {IEEE} Computer Security Foundations Symp. (CSF)},
title = {First-Order Logic for Flow-Limited Authorization},
year = {2020},
volume = {},
number = {},
pages = {123-138},
doi = {10.1109/CSF49147.2020.00017},
series = {CSF'20}
}
We present the Flow-Limited Authorization First-Order Logic
(FLAFOL), a logic for reasoning about authorization decisions in the presence
of information-flow policies. We formalize the FLAFOL proof system, characterize
its proof-theoretic properties, and develop its security guarantees. In
particular, FLAFOL is the first logic to provide a non-interference guarantee
while supporting all connectives of first-order logic. Furthermore, this
guarantee is the first to combine the notions of noninterference from both
authorization logic and information-flow systems. All the theorems in this paper
are proven in Coq.
Information flow control for distributed trusted execution environments
DFLATE offers high-level security abstractions that reflect both the guarantees
and limitations of the TEE security mechanisms.
CSF’19
Gollamudi, Anitha and Chong, Stephen and Arden, Owen
@inproceedings{dflate,
title = {Information flow control for distributed trusted execution environments},
author = {Gollamudi, Anitha and Chong, Stephen and Arden, Owen},
year = {2019},
booktitle = {32\textsuperscript{nd} {IEEE} Computer Security Foundations Symp. (CSF)},
month = jun,
series = {CSF'19},
doi = {10.1109/CSF.2019.00028},
month_numeric = {6}
}
Distributed applications cannot assume that their security
policies will be enforced on untrusted hosts. Trusted execution environments
(TEEs) combined with cryptographic mechanisms enable execution of known code on
an untrusted host and the exchange of confidential and authenticated messages
with it. TEEs do not, however, establish the trustworthiness of code executing
in a TEE. Thus, developing secure applications using TEEs requires specialized
expertise and careful auditing.
This paper presents DFLATE, a core security calculus for distributed
applications with TEEs. DFLATE offers high-level abstractions that reflect both
the guarantees and limitations of the underlying security mechanisms they are
based on. The accuracy of these abstractions is exhibited by asymmetry between
confidentiality and integrity in our formal results: DFLATE enforces a strong
form of noninterference for confidentiality, but only a weak form for integrity.
This reflects the asymmetry of the security guarantees of a TEE: a malicious
host cannot access secrets in the TEE or modify its contents, but they can
suppress or manipulate the sequence of its inputs and outputs. Therefore DFLATE
cannot protect against the suppression of high-integrity messages, but when
these messages are delivered, their contents cannot have been influenced by an
attacker.
Nonmalleable Information Flow Control
A new 4-safety hyperproperty for secure declassification and endorsement and a
type system for enforcing it.
CCS’17
Best paper finalist (11 finalists out of 151 accepted papers).
Cecchetti, Ethan and Myers, Andrew C. and Arden, Owen
@inproceedings{nmifc,
author = {Cecchetti, Ethan and Myers, Andrew C. and Arden, Owen},
title = {Nonmalleable Information Flow Control},
booktitle = {24\textsuperscript{th} ACM Conf.~on Computer and Communications Security (CCS)},
year = {2017},
month = oct,
pages = {1875--1891},
location = {Dallas, TX},
series = {CCS'17},
doi = {10.1145/3133956.3134054},
month_numeric = {10}
}
Noninterference is a popular semantic security condition
because it offers strong end-to-end guarantees, it is inherently compositional,
and it can be enforced using a simple security type system. Unfortunately, it
is too restrictive for real systems. Mechanisms for downgrading information are
needed to capture real-world security requirements, but downgrading eliminates
the strong compositional security guarantees of noninterference.
We introduce nonmalleable information flow, a new formal security condition
that generalizes noninterference to permit controlled downgrading of both
confidentiality and integrity. While previous work on robust declassification
prevents adversaries from exploiting the downgrading of confidentiality, our
key insight is transparent endorsement, a mechanism for downgrading integrity
while defending against adversarial exploitation. Robust declassification
appeared to break the duality of confidentiality and integrity by making
confidentiality depend on integrity, but transparent endorsement makes
integrity depend on confidentiality, restoring this duality. We show how to
extend a security-typed programming language with transparent endorsement and
prove that this static type system enforces nonmalleable information flow, a
new security property that subsumes robust declassification and transparent
endorsement. Finally, we describe an implementation of this type system in the
context of Flame, a flow-limited authorization plugin for the Glasgow Haskell
Compiler.
A Calculus for Flow-Limited Authorization
A core programming model that uses flow-limited authorization to provide end-to-end information security to dynamic authorization mechanisms and programs that use them.
CSF’16
Arden, Owen and Myers, Andrew C.
@inproceedings{flac,
author = {Arden, Owen and Myers, Andrew C.},
booktitle = {2016 IEEE 29th Computer Security Foundations Symposium (CSF)},
title = {A Calculus for Flow-Limited Authorization},
year = {2016},
doi = {10.1109/CSF.2016.17},
month = jun,
series = {CSF'16},
month_numeric = {6}
}
Real-world applications routinely make authorization decisions
based on dynamic computation. Reasoning about dynamically computed authority is
challenging. Integrity of the system might be compromised if attackers can
improperly influence the authorizing computation. Confidentiality can also be
compromised by authorization, since authorization decisions are often based on
sensitive data such as membership lists and passwords. Previous formal models
for authorization do not fully address the security implications of permitting
trust relationships to change, which limits their ability to reason about
authority that derives from dynamic computation. Our goal is a way to construct
dynamic authorization mechanisms that do not violate confidentiality or
integrity. We introduce the Flow-Limited Authorization Calculus (FLAC), which
is both a simple, expressive model for reasoning about dynamic authorization
and also an information flow control language for securely implementing various
authorization mechanisms. FLAC combines the insights of two previous models: it
extends the Dependency Core Calculus with features made possible by the
Flow-Limited Authorization Model. FLAC provides strong end-to-end information
security guarantees even for programs that incorporate and implement rich
dynamic authorization mechanisms. These guarantees include noninterference and
robust declassification, which prevent attackers from influencing information
disclosures in unauthorized ways. We prove these security properties formally
for all FLAC programs and explore the expressiveness of FLAC with several
examples.
Flow-Limited Authorization
CSF’15
Arden, Owen and Liu, Jed and Myers, Andrew C.
@inproceedings{flam,
author = {Arden, Owen and Liu, Jed and Myers, Andrew C.},
booktitle = {2015 IEEE 28th Computer Security Foundations Symposium},
title = {Flow-Limited Authorization},
year = {2015},
volume = {},
number = {},
pages = {569-583},
doi = {10.1109/CSF.2015.42},
month = jul,
series = {CSF'15},
month_numeric = {7}
}
Because information flow control mechanisms often rely on an
underlying authorization mechanism, their security guarantees can be subverted
by weaknesses in authorization. Conversely, the security of authorization can
be subverted by information flows that leak information or that influence how
authority is delegated between principals. We argue that interactions between
information flow and authorization create security vulnerabilities that have
not been fully identified or addressed in prior work. We explore how the
security of decentralized information flow control (DIFC) is affected by three
aspects of its underlying authorization mechanism: first, delegation of
authority between principals, second, revocation of previously delegated
authority, third, information flows created by the authorization mechanisms
themselves. It is no surprise that revocation poses challenges, but we show
that even delegation is problematic because it enables unauthorized
downgrading. Our solution is a new security model, the Flow-Limited
Authorization Model (FLAM), which offers a new, integrated approach to
authorization and information flow control. FLAM ensures robust authorization,
a novel security condition for authorization queries that ensures attackers
cannot influence authorization decisions or learn confidential trust
relationships. We discuss our prototype implementation and its algorithm for
proof search.
>