I study decentralized security with a focus on
using programming language theory and design to build decentralized
applications that are secure by construction. My research includes both
foundational and practical contributions, from developing novel, more expressive
security models and formalized programming languages, to building secure decentralized systems
and compilers.
Improving the recoverability of Byzantine fault tolerant protocols.
ICBC’23
Tran, Tuan and Nawab, Faisal and Alvaro, Peter and Arden, Owen
@inproceedings{phoenix,
author = {Tran, Tuan and Nawab, Faisal and Alvaro, Peter and Arden, Owen},
title = {Unstick Yourself: Recoverable Byzantine Fault Tolerant Services},
booktitle = {2023 IEEE International Conference on Blockchain and Cryptocurrency (ICBC)},
blurb = {Improving the recoverability of Byzantine fault tolerant protocols.},
series = {ICBC'23},
%doi = {10.1109/ICBC54727.2022.9805547},
file = {Phoenix.pdf},
year = {2023},
month = may,
address = {New York, NY, USA}
}
Byzantine fault tolerant (BFT) state machine
replication (SMR) protocols that can tolerate up to f failures in a
configuration of n = 3f + 1 replicas cannot make any liveness guarantee once
the number of faults surpasses f, even if some of these faults are benign crash
faults. We argue that this weakness makes BFT protocols impractical in
real-world deployments where faults accumulate over time. In this paper, we
present a new reconfiguration mechanism, Phoenix, that builds on the
pre-existing fault detection and reconfiguration mechanisms of BFT protocols to
remove faulty replicas proactively using a trusted (but limited) configuration
manager. We show that Phoenix can recover from f B Byzantine faults and f_C
crash faults, where f_C ≤ f_B, if the system deploys n = 3f_B + f_C + 1
replicas. If a synchronous network connection is guaranteed between replicas
and the configuration manager during reconfiguration, a synchronous variant of
Phoenix needs only n = 3f_B +1 replicas to achieve the same recoverability. To
validate our approach, we implement Phoenix as an extension of the BFT-SMaRT
library.
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},
blurb = {A formal language for building application-level consensus and replication protocols
that are secure by construction.},
awards = {Distinguished paper award},
series = {CSF'22},
year = {2022},
month = aug,
doi = {10.1109/CSF54842.2022.9919637},
file = {flaqr.pdf},
volume = {},
number = {}
}
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.
Payment Channels Under Network Congestion
Addressing congestion attacks in payment channel networks.
ICBC’22 (short paper)
Tran, Tuan and Zheng, Haofan and Alvaro, Peter and Arden, Owen
@inproceedings{icbc22,
author = {Tran, Tuan and Zheng, Haofan and Alvaro, Peter and Arden, Owen},
title = {Payment Channels Under Network Congestion},
booktitle = {2022 IEEE International Conference on Blockchain and Cryptocurrency (ICBC)},
blurb = {Addressing congestion attacks in payment channel networks.},
series = {ICBC'22 (short paper)},
doi = {10.1109/ICBC54727.2022.9805547},
file = {icbc22.pdf},
year = {2022},
month = may,
address = {New York, NY, USA}
}
Sending transactions on leading blockchains such as
Ethereum can be slow and costly. A payment channel is a wellknown scaling
solution that minimizes transactions sent on the chain, and allows users to
transact more efficiently. One of the guarantees of payment channels is that
there is no counterparty risk, so an honest party is able to withdraw the
amount of money that is reflected by the most recent transaction agreed by both
parties. In this paper, we show that this guarantee can be violated when the
network is under congestion. Regardless of whether or not the honest party is
online, the malicious party can leverage high transaction fees to gain more
money than they’re supposed to. We present a novel construction of payment
channels that helps mitigates these types of attacks.
Total Eclipse of the Enclave: Detecting Eclipse Attacks From Inside TEEs
Using difficulty monitoring to reliably detect extended eclipse attacks, even when the
adversary controls all network connectivity.
ICBC’21 (short paper)
Zheng, Haofan and Tran, Tuan and Arden, Owen
@inproceedings{haofan2021eclipse,
author = {Zheng, Haofan and Tran, Tuan and Arden, Owen},
title = {Total Eclipse of the Enclave: Detecting Eclipse Attacks From Inside TEEs},
booktitle = {2021 IEEE International Conference on Blockchain and Cryptocurrency (ICBC)},
year = {2021},
month = may,
address = {New York, NY, USA},
doi = {10.1109/ICBC51069.2021.9461081},
series = {ICBC'21 (short paper)},
file = {eclipse.pdf},
blurb = {Using difficulty monitoring to reliably detect extended eclipse attacks, even when the
adversary controls all network connectivity.}
}
Enclave applications that rely on blockchains for integrity
and availability are vulnerable to eclipse attacks. In this paper, we present
an approach for reliably detecting extended eclipse attacks, even when the
adversary controls all network connectivity. By monitoring changes to the
difficulty parameter in Proof-of-Work (PoW) protocols, our algorithm detects
suppression of new blocks, as well as difficulty-lowering attacks that attempt
to force an enclave client onto a malicious fork mined solely by an attacker.
We present analysis that attackers have negligible probability of evading our
block monitoring algorithm, and demonstrate its robustness to most historical
fluctuations in difficulty on the Ethereum blockchain, resulting in a very low
false-positive rate.
Secure Distributed Applications the Decent Way
A framework for building secure decentralized applications with trusted execution environments
and remote attestation.
ASSS’21
Zheng, Haofan and Arden, Owen
@inproceedings{decent,
author = {Zheng, Haofan and Arden, Owen},
title = {Secure Distributed Applications the Decent Way},
year = {2021},
doi = {10.1145/3457340.3458304},
booktitle = {Proceedings of the 2021 International Symposium on Advanced Security on Software and Systems},
pages = {29-42},
month = jan,
numpages = {14},
series = {ASSS'21},
file = {decent.pdf},
blurb = {A framework for building secure decentralized applications with trusted execution environments
and remote attestation.}
}
Remote attestation (RA) authenticates code running in
trusted execution environments (TEEs), allowing trusted code to be deployed
even on untrusted hosts. However, trust relationships established by one
component in a distributed application may impact the security of other
components, making it difficult to reason about the security of the application
as a whole. Furthermore, traditional RA approaches interact badly with modern
web service design, which tends to employ small interacting microservices,
short session lifetimes, and little or no state.
This paper presents the Decent Application Platform, a framework for building
secure decentralized applications. Decent applications authenticate and
authorize distributed enclave components using a protocol based on
self-attestation certificates, a reusable credential based on RA and verifiable
by a third party. Components mutually authenticate each other not only based on
their code, but also based on the other components they trust, ensuring that no
transitively-connected components receive unauthorized information. While some
other TEE frameworks support mutual authentication in some form, Decent is the
only system that supports mutual authentication without requiring an additional
trusted third party besides the trusted hardware’s manufacturer. We have
verified the secrecy and authenticity of Decent application data in ProVerif,
and implemented two applications to evaluate Decent’s expressiveness and
performance: DecentRide, a ride-sharing service, and DecentHT, a distributed
hash table. On the YCSB benchmark, we show that DecentHT achieves 7.5x higher
throughput and 3.67x lower latency compared to a non-Decent implementation.
AttkFinder: Discovering Attack Vectors in PLC Programs Using Information Flow Analysis
Using information flow analysis to discover attack vectors in industrial control systems.
RAID’21
Castellanos, John H. and Ochoa, Martin and Cardenas, Alvaro A. and Arden, Owen and Zhou, Jianying
@inproceedings{raid21,
author = {Castellanos, John H. and Ochoa, Martin and Cardenas, Alvaro A. and Arden, Owen and Zhou, Jianying},
title = {AttkFinder: Discovering Attack Vectors in PLC Programs Using Information Flow Analysis},
year = {2021},
doi = {10.1145/3471621.3471864},
booktitle = {24th International Symposium on Research in Attacks, Intrusions and Defenses},
pages = {235-250},
numpages = {16},
series = {RAID'21},
file = {attkfinder.pdf},
blurb = {Using information flow analysis to discover attack vectors in industrial control systems.}
}
To protect an Industrial Control System (ICS), defenders
need to identify potential attacks on the system and then design mechanisms to
prevent them. Unfortunately, identifying potential attack conditions is a
time-consuming and error-prone process. In this work, we propose and evaluate a
set of tools to symbolically analyse the software of Programmable Logic
Controllers (PLCs) guided by an information flow analysis that takes into
account PLC network communication (compositions). Our tools systematically
analyse malicious network packets that may force the PLC to send specific
control commands to actuators. We evaluate our approach in a real-world system
controlling the dosing of chemicals for water treatment. Our tools are able to
find 75 attack tactics (56 were novel attacks), and we confirm that 96% of
these tactics cause the intended effect in our testbed.
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},
file = {jflactr.pdf},
blurb = {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.},
awards = {Revised, corrected, and expanded version of CSF'16 paper}
}
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},
file = {flafol.pdf},
blurb = {A logic for reasoning about authorization decisions in the presence of information-flow policies.}
}
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.
AnyLog: a Grand Unification of the Internet of Things
A new vision for a completely decentralized, ownerless platform for sharing
structured data.
CIDR’20
Abadi, Daniel and Arden, Owen and Nawab, Faisal and Shadmon, Moshe
@inproceedings{anylog,
title = {{AnyLog}: a Grand Unification of the Internet of Things},
author = {Abadi, Daniel and Arden, Owen and Nawab, Faisal and Shadmon, Moshe},
booktitle = {Conference on Innovative Data Systems Research (CIDR)},
year = {2020},
series = {CIDR'20},
file = {anylog.pdf},
url = {http://cidrdb.org/cidr2020/papers/p9-abadi-cidr20.pdf},
blurb = {A new vision for a completely decentralized, ownerless platform for sharing
structured data.}
}
AnyLog is a decentralized platform for data publishing,
sharing, and querying IoT (Internet of Things) data that enables an unlimited
number of independent participants to publish and access the contents of IoT
datasets stored across the participants. AnyLog provides decentralized
publishing and querying functionality over structured data in an analogous
fashion to how the world wide web (WWW) enables decentralized publishing and
accessing of unstructured data. However, AnyLog differs from the traditional
WWW in the way that it provides incentives and financial reward for performing
tasks that are critical to the well-being of the system as a whole, including
contribution, integration, storing, and processing of data, as well as
protecting the confidentiality, integrity, and availability of that data.
Another difference is how Anylog enforces good behavior by the participants
through a collection of methods, including blockchain, secure enclaves, and
state channels.
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},
file = {dflate.pdf},
blurb = {DFLATE offers high-level security abstractions that reflect both the guarantees
and limitations of the TEE security mechanisms.}
}
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},
file = {nmifc_ccs17.pdf},
blurb = {A new 4-safety hyperproperty for secure declassification and endorsement and a
type system for enforcing it.},
awards = {Best paper finalist (11 finalists out of 151 accepted papers).}
}
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.
Fabric: Building Open Distributed Systems Securely by Construction
A secure, decentralized, and distributed programming language and system.
JCS’17
Liu, Jed and Arden, Owen and George, Michael D. and Myers, Andrew C.
@article{jfabric,
title = {{Fabric}: {B}uilding Open Distributed Systems Securely by Construction},
author = {Liu, Jed and Arden, Owen and George, Michael D. and Myers, Andrew C.},
journal = {J. Computer Security},
month = may,
year = {2017},
volume = {25},
number = {4--5},
pages = {319--321},
doi = {10.3233/JCS-0559},
series = {JCS'17},
file = {jfabric.pdf},
blurb = {A secure, decentralized, and distributed programming language and system.}
}
Distributed information systems are prevalent in modern
computing but difficult to build securely. Because systems commonly span domains
of trust, host nodes share data and code of varying degrees of trustworthiness.
Modern systems are often open and extensible, making security even harder to
reason about. Unfortunately, standard methods for software construction do not
help programmers enough with ensuring their software is secure.
Fabric is a system and language for building open, distributed, extensible
information systems that are secure by construction. Fabric is a decentralized
system that allows nodes to securely share both data and code despite mutual
distrust. All resources are labeled with confidentiality and integrity policies
that are enforced through a combination of compile-time and run-time
mechanisms.
The Fabric language offers a high-level but powerful model of computation. All
resources appear as objects in the language, and the distribution and
persistence of code and data are largely transparent to programmers. Fabric
supports both data-shipping and query/RPC styles of computation: computation
and information can both move between nodes. Optimistic, nested transactions
ensure consistency across all objects and nodes. Fabric programs can securely
share mobile code across trust domains, enabling more reuse and evolution of
code and supporting new kinds of secure applications not possible in other
distributed systems. Results from applications built using Fabric suggest that
Fabric enforces strong security while offering a clean, concise, powerful
programming model with good performance. An open-source prototype is available
for download.
Cryptographically Secure Information Flow Control on Key-Value Stores
An information flow control system that transparently
incorporates cryptography to enforce confidentiality and integrity policies on
untrusted storage.
CCS’17
Waye, Lucas and Buiras, Pablo and Arden, Owen and Russo, Alejandro and Chong, Stephen
@inproceedings{clio,
author = {Waye, Lucas and Buiras, Pablo and Arden, Owen and Russo, Alejandro and Chong, Stephen},
title = {Cryptographically Secure Information Flow Control on Key-Value Stores},
booktitle = {24\textsuperscript{th} ACM Conf.~on Computer and Communications Security (CCS)},
pages = {1893--1907},
year = {2017},
url = {http://doi.acm.org/10.1145/3133956.3134036},
doi = {10.1145/3133956.3134036},
series = {CCS'17},
file = {clio_ccs17.pdf},
blurb = {An information flow control system that transparently
incorporates cryptography to enforce confidentiality and integrity policies on
untrusted storage.}
}
We present Clio, an information flow control (IFC) system that
transparently incorporates cryptography to enforce confidentiality and
integrity policies on untrusted storage. Clio 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 Clio 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 Clio
implementation and a case study that demonstrates Clio’s practicality.
