About

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 foundational and practical contributions, such as developing novel security models, formalized programming languages, secure decentralized systems, and compilers.

Research topics

• Computer Security
• Computer Science
• Programming language
• Mathematics
• Computer network
• Theoretical computer science
• Software engineering
• World Wide Web
• Astronomy
• Operating system
• Embedded system

Selected publications

• Enhancing Accuracy in Approximate Byzantine Agreement with Bayesian Inference

  2025-06-23

  articleSenior author

  Multi-agent sensor networks and control systems make important control decisions at the edge using inputs from networked sensor (or sensor-derived) data streams, some of which may be faulty or compromised. These inputs are used to update models that represent the physical state of cyber-physical systems, smart power grids, or robot swarms, and drive decision procedures that seek to maintain system properties (e.g., keep temperature near 70°F), enforce safety requirements (e.g., shutdown power if current exceeds 3A), or achieve a goal (e.g., reach a particular location). Noisy values proposed by replicas obscure latent information in their proposed values, but extracting this information is complicated by the presence of malicious replicas.This paper outlines Proximal Byzantine Agreement (PBA), a new stochastic agreement protocol that improves the accuracy of selected values using robust statistical inference. Our initial results indicate PBA’s potential for statistically-superior accuracy compared to existing agreement protocols.

  PublisherDOI

• Decentagram: Highly-Available Decentralized Publish/Subscribe Systems

  2024-06-24 · 1 citations

  articleSenior author

  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 on-chain. 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 third-party 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 off-chain 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.

  PublisherDOI

• Proximal Byzantine Consensus

  arXiv (Cornell University) · 2024-02-19

  preprintOpen accessSenior author

  Distributed control systems require high reliability and availability guarantees despite often being deployed at the edge of network infrastructure. Edge computing resources are less secure and less reliable than centralized resources in data centers. Replication and consensus protocols improve robustness to network faults and crashed or corrupted nodes, but these volatile environments can cause non-faulty nodes to temporarily diverge, increasing the time needed for replicas to converge on a consensus value, and give Byzantine attackers too much influence over the convergence process. This paper proposes proximal Byzantine consensus, a new approximate consensus protocol where clients use statistical models of streaming computations to decide a consensus value. In addition, it provides an interval around the decision value and the probability that the true (non-faulty, noise-free) value falls within this interval. Proximal consensus (PC) tolerates unreliable network conditions, Byzantine behavior, and other sources of noise that cause honest replica states to diverge. We evaluate our approach for scalar values, and compare PC simulations against a vector consensus (VC) protocol simulation. Our simulations demonstrate that consensus values selected by PC have lower error and are more robust against Byzantine attacks. We formally characterize the security guarantees against Byzantine attacks and demonstrate attacker influence is bound with high probability. Additionally, an informal complexity analysis suggests PC scales better to higher dimensions than convex hull-based protocols such as VC.

  PublisherOA PDFDOI

• Unstick Yourself: Recoverable Byzantine Fault Tolerant Services

  2023-05-01 · 1 citations

  articleSenior author

  Byzantine fault tolerant (BFT) state machine replication (SMR) protocols that can tolerate up to <tex>$f$</tex> failures in a configuration of <tex>$n=3f+1$</tex> 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 <tex>$f_{B}$</tex> Byzantine faults and <tex>$f_{C}$</tex> crash faults, where <tex>$f_{C}\leq f_{B}$</tex>, if the system deploys <tex>$n=3f_{B}+f_{C}+1$</tex> replicas. If a synchronous network connection is guaranteed between replicas and the configuration manager during reconfiguration, a synchronous variant of Phoenix needs only <tex>$n=3f_{B}+1$</tex> replicas to achieve the same recoverability. To validate our approach, we implement Phoenix as an extension of the BFT-SMaRT library.

  PublisherDOI

• Applying consensus and replication securely with FLAQR

  arXiv (Cornell University) · 2022-05-09

  preprintOpen accessSenior author

  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 type-level 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.

  PublisherOA PDFDOI

• Payment Channels Under Network Congestion

  2022-05-02 · 1 citations

  articleSenior author

  Sending transactions on leading blockchains such as Ethereum can be slow and costly. A payment channel is a well-known 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.

  PublisherDOI

• Applying consensus and replication securely with FLAQR

  2022-08-01 · 3 citations

  articleSenior author

  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 type-level 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.

  PublisherDOI

• Secure Distributed Applications the Decent Way

  2021-05-24 · 6 citations

  articleOpen accessSenior author

  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.

  PublisherOA PDFDOI

• A Calculus for Flow-Limited Authorization

  arXiv (Cornell University) · 2021-04-21

  preprintOpen access1st authorCorresponding

  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.

  PublisherOA PDFDOI

• AttkFinder: Discovering Attack Vectors in PLC Programs using Information Flow Analysis

  2021 · 14 citations

  • Computer Science
  • Computer Security
  • Computer Science

  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.

  PublisherDOI

Recent grants

• CAREER: Building Secure Decentralized Applications with Trusted Hardware and Blockchains

  NSF · $511k · 2018–2023

Frequent coauthors

• Andrew C. Myers

  20 shared

• Jed Liu

  7 shared

• Samuel Madden

  7 shared

• Michael George

  6 shared

• Alvin Cheung

  University of California, Berkeley

  6 shared

• Haofan Zheng

  University of California, Santa Cruz

  5 shared

• Stephen Chong

  4 shared

• Ethan Cecchetti

  4 shared

Awards & honors

• Distinguished artifact award at DSN’24
• Distinguished paper award at CSF’22
• Best paper award at ICBC’23