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.
Recent publications
Decentagram: Highly-Available Decentralized Publish/Subscribe Systems
A secure, decentralized pub/sub system for on-chain and off-chain subscribers using smart contracts and trusted execution environments.
DSN’24
Distinguished artifact award
Zheng, Haofan and Tran, Tuan and Shadmon, Roy and Arden, Owen
@inproceedings{decentagram,
author = {Zheng, Haofan and Tran, Tuan and Shadmon, Roy and Arden, Owen},
title = {Decentagram: Highly-Available Decentralized Publish/Subscribe Systems},
booktitle = {2024 54th Annual IEEE/IFIP International Conference on Dependable Systems and Networks (DSN)},
series = {DSN'24},
year = {2024},
month = {}
}
This paper presents Decentagram, a decentralized framework for data
dissemination using the publish/subscribe messaging model. Decentagram uses
blockchain smart contracts to authenticate events that will be published
using digital signatures or self-attestation certificates from code running
in trusted execution environments (TEEs), both of which are verified
onchain. This approach permits any host with valid credentials to publish
verified updates, increasing decentralization and availability of the system
as a whole by simplifying compensation and incentivization, even for
untrusted hosts running TEEs. Decentagram also supports on-chain
subscribers where thirdparty contracts receive events immediately: within
the same transaction as the published event. The same event will also be
delivered to off-chain subscribing applications through an offchain event
broker. We provide an open-source implementation of Decentagram, and
evaluate the gas cost of its on-chain components and the end-to-end latency
of its off-chain component.
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)},
series = {ICBC'23},
doi = {10.1109/ICBC56567.2023.10174886},
year = {2023},
month = may,
month_numeric = {5}
}
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},
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.
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)},
series = {ICBC'22 (short paper)},
doi = {10.1109/ICBC54727.2022.9805547},
year = {2022},
month = may,
month_numeric = {5}
}
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,
doi = {10.1109/ICBC51069.2021.9461081},
series = {ICBC'21 (short paper)},
month_numeric = {5}
}
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},
month_numeric = {1}
}
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}
}
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}
}
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.
