arXiv subjects

Andrew C. Myers

Publications and source records attributed to Andrew C. Myers.

17 recordsLinked to original sources

arXiv2026

Oblivious Probabilistic Outcome Logic: Verifying Probabilistic Programs with an Oblivious Adversary

In the context of probabilistic programs, an oblivious adversary resolves nondeterminism without seeing the outcomes of random draws. Obliviousness is a common assumption in online algorithms and distributed protocols, but the complex interaction between random draws and adversarial choices makes it challenging to reason about correctness. While there has been significant progress toward reasoning about programs that combine randomization with nondeterminism, most of the work has focused on the adaptive model, whose omniscient view of program state is too powerful to establish correctness for certain classes of programs. We introduce Oblivious Probabilistic Outcome Logic (opOL), a new logic for reasoning about probabilistic programs with nondeterminism controlled by an oblivious adversary. Building on Outcome Logic and Probabilistic Separation Logic, opOL models adversarial choice as a resource and uses probabilistic independence to ensure that random outcomes are hidden from the adversary. The opOL proof system provides expressive and compositional rules for case analysis on both random and nondeterministic outcomes, and for proving almost-sure termination. Expressivity is tested through several case studies, including a paging algorithm and a leader election protocol. The opOL metatheory and case studies are mechanized in Lean 4.

cs.PL↗

arXiv2025

An Algebraic Approach to Asymmetric Delegation and Polymorphic Label Inference (Technical Report)

Language-based information flow control (IFC) enables reasoning about and enforcing security policies in decentralized applications. While information flow properties are relatively extensional and compositional, designing expressive systems that enforce such properties remains challenging. In particular, it can be difficult to use IFC labels to model certain security assumptions, such as semi-honest agents. Motivated by these modeling limitations, we study the algebraic semantics of lattice-based IFC label models, and propose a semantic framework that allows formalizing asymmetric delegation, which is partial delegation of confidentiality or integrity. Our framework supports downgrading of information and ensures their safety through nonmalleable information flow (NMIF). To demonstrate the practicality of our framework, we design and implement a novel algorithm that statically checks NMIF and a label inference procedure that efficiently supports bounded label polymorphism, allowing users to write code generic with respect to labels.

cs.PL↗

arXiv2025

A Language for Smart Contracts with Secure Control Flow (Technical Report)

Smart contracts are frequently vulnerable to control-flow attacks based on confused deputies, reentrancy, and incorrect error handling. These attacks exploit the complexity of interactions among multiple possibly unknown contracts. Existing best practices to prevent vulnerabilities rely on code patterns and heuristics that produce both false positives and false negatives. Even with extensive audits and heuristic tools, new vulnerabilities continue to arise, routinely costing tens of millions of dollars. We introduce SCIF, a language for secure smart contracts, that addresses these classes of control-flow attacks. By extending secure information flow mechanisms in a principled way, SCIF enforces both classic end-to-end information flow security and new security restrictions on control flow, even when SCIF contracts interact with malicious non-SCIF code. SCIF is implemented as a compiler to Solidity. We show how SCIF can secure contracts with minimal overhead through case studies of applications with intricate security reasoning and a large corpus of insecure code.

cs.CR↗

arXiv2024

An Array Intermediate Language for Mixed Cryptography

We introduce AIRduct, a new array-based intermediate representation designed to support generating efficient code for interactive programs employing multiple cryptographic mechanisms. AIRduct is intended as an IR for the Viaduct compiler, which can synthesize secure, distributed programs with an extensible suite of cryptography. Therefore, AIRduct supports an extensible variety of cryptographic mechanisms, including MPC and ZKP.

cs.CR↗

arXiv2024

Secure Synthesis of Distributed Cryptographic Applications (Technical Report)

Developing secure distributed systems is difficult, and even harder when advanced cryptography must be used to achieve security goals. Following prior work, we advocate using secure program partitioning to synthesize cryptographic applications: instead of implementing a system of communicating processes, the programmer implements a centralized, sequential program, which is automatically compiled into a secure distributed version that uses cryptography. While this approach is promising, formal results for the security of such compilers are limited in scope. In particular, no security proof yet simultaneously addresses subtleties essential for robust, efficient applications: multiple cryptographic mechanisms, malicious corruption, and asynchronous communication. In this work, we develop a compiler security proof that handles these subtleties. Our proof relies on a novel unification of simulation-based security, information-flow control, choreographic programming, and sequentialization techniques for concurrent programs. While our proof targets hybrid protocols, which abstract cryptographic mechanisms as idealized functionalities, our approach offers a clear path toward leveraging Universal Composability to obtain end-to-end, modular security results with fully instantiated cryptographic mechanisms. Finally, following prior observations about simulation-based security, we prove that our result guarantees robust hyperproperty preservation, an important criterion for compiler correctness that preserves all source-level security properties in target programs.

cs.CR↗

arXiv2023

A Compiler from Array Programs to Vectorized Homomorphic Encryption

Homomorphic encryption (HE) is a practical approach to secure computation over encrypted data. However, writing programs with efficient HE implementations remains the purview of experts. A difficult barrier for programmability is that efficiency requires operations to be vectorized in inobvious ways, forcing efficient HE programs to manipulate ciphertexts with complex data layouts and to interleave computations with data movement primitives. We present Viaduct-HE, a compiler generates efficient vectorized HE programs. Viaduct-HE can generate both the operations and complex data layouts required for efficient HE programs. The source language of Viaduct-HE is array-oriented, enabling the compiler to have a simple representation of possible vectorization schedules. With such a representation, the compiler searches the space of possible vectorization schedules and finds those with efficient data layouts. After finding a vectorization schedule, Viaduct-HE further optimizes HE programs through term rewriting. The compiler has extension points to customize the exploration of vectorization schedules, to customize the cost model for HE programs, and to add back ends for new HE libraries. Our evaluation of the prototype Viaduct-HE compiler shows that it produces efficient vectorized HE programs with sophisticated data layouts and optimizations comparable to those designed by experts.

cs.PL↗

arXiv2021

A Calculus for Flow-Limited Authorization

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.

cs.CR↗

arXiv2021

Compositional Security for Reentrant Applications

The disastrous vulnerabilities in smart contracts sharply remind us of our ignorance: we do not know how to write code that is secure in composition with malicious code. Information flow control has long been proposed as a way to achieve compositional security, offering strong guarantees even when combining software from different trust domains. Unfortunately, this appealing story breaks down in the presence of reentrancy attacks. We formalize a general definition of reentrancy and introduce a security condition that allows software modules like smart contracts to protect their key invariants while retaining the expressive power of safe forms of reentrancy. We present a security type system that provably enforces secure information flow; in conjunction with run-time mechanisms, it enforces secure reentrancy even in the presence of unknown code; and it helps locate and correct recent high-profile vulnerabilities.

cs.CR↗

arXiv2020

Heterogeneous Paxos: Technical Report

In distributed systems, a group of $\textit{learners}$ achieve $\textit{consensus}$ when, by observing the output of some $\textit{acceptors}$, they all arrive at the same value. Consensus is crucial for ordering transactions in failure-tolerant systems. Traditional consensus algorithms are homogeneous in three ways: - all learners are treated equally, - all acceptors are treated equally, and - all failures are treated equally. These assumptions, however, are unsuitable for cross-domain applications, including blockchains, where not all acceptors are equally trustworthy, and not all learners have the same assumptions and priorities. We present the first consensus algorithm to be heterogeneous in all three respects. Learners set their own mixed failure tolerances over differently trusted sets of acceptors. We express these assumptions in a novel $\textit{Learner Graph}$, and demonstrate sufficient conditions for consensus. We present $\textit{Heterogeneous Paxos}$: an extension of Byzantine Paxos. Heterogeneous Paxos achieves consensus for any viable Learner Graph in best-case three message sends, which is optimal. We present a proof-of-concept implementation, and demonstrate how tailoring for heterogeneous scenarios can save resources and latency.

cs.DC↗

arXiv2020

Handling Bidirectional Control Flow: Technical Report

Pressed by the difficulty of writing asynchronous, event-driven code, mainstream languages have recently been building in support for a variety of advanced control-flow features. Meanwhile, experimental language designs have suggested effect handlers as a unifying solution to programmer-defined control effects, subsuming exceptions, generators, and async--await. Despite these trends, complex control flow---in particular, control flow exhibiting a bidirectional pattern---remains challenging to manage. We introduce bidirectional algebraic effects, a new programming abstraction that supports bidirectional control transfer in a more natural way. Handlers of bidirectional effects can raise further effects to transfer control back to the site where the initiating effect was raised, and can use themselves to handle their own effects. We present applications of this expressive power, which falls out naturally as we push toward the unification of effectful programming with object-oriented programming. We pin down the mechanism and the unification formally using a core language that generalizes to effect operations and effect handlers. The usual propagation semantics of control effects such as exceptions conflicts with modular reasoning in the presence of effect polymorphism---it breaks parametricity. Bidirectionality exacerbates the problem. Hence, we set out to show the core language, which builds on the existing tunneling semantics for algebraic effects, is not only type-safe (no effects go unhandled), but also abstraction-safe (no effects are accidentally handled). We devise a step-indexed logical-relations model, and construct its parametricity and soundness proofs. These core results are fully mechanized in Coq. Preliminary experiments show that as a first-class language feature, bidirectional handlers can be implemented efficiently.

cs.PL↗

arXiv2020

The Cost of Software-Based Memory Management Without Virtual Memory

Virtual memory has been a standard hardware feature for more than three decades. At the price of increased hardware complexity, it has simplified software and promised strong isolation among colocated processes. In modern computing systems, however, the costs of virtual memory have increased significantly. With large memory workloads, virtualized environments, data center computing, and chips with multiple DMA devices, virtual memory can degrade performance and increase power usage. We therefore explore the implications of building applications and operating systems without relying on hardware support for address translation. Primarily, we investigate the implications of removing the abstraction of large contiguous memory segments. Our experiments show that the overhead to remove this reliance is surprisingly small for real programs. We expect this small overhead to be worth the benefit of reducing the complexity and energy usage of address translation. In fact, in some cases, performance can even improve when address translation is avoided.

cs.AR↗

arXiv2019

Charlotte: Composable Authenticated Distributed Data Structures, Technical Report

We present Charlotte, a framework for composable, authenticated distributed data structures. Charlotte data is stored in blocks that reference each other by hash. Together, all Charlotte blocks form a directed acyclic graph, the blockweb; all observers and applications use subgraphs of the blockweb for their own data structures. Unlike prior systems, Charlotte data structures are composable: applications and data structures can operate fully independently when possible, and share blocks when desired. To support this composability, we define a language-independent format for Charlotte blocks and a network API for Charlotte servers. An authenticated distributed data structure guarantees that data is immutable and self-authenticating: data referenced will be unchanged when it is retrieved. Charlotte extends these guarantees by allowing applications to plug in their own mechanisms for ensuring availability and integrity of data structures. Unlike most traditional distributed systems, including distributed databases, blockchains, and distributed hash tables, Charlotte supports heterogeneous trust: different observers may have their own beliefs about who might fail, and how. Despite heterogeneity of trust, Charlotte presents each observer with a consistent, available view of data. We demonstrate the flexibility of Charlotte by implementing a variety of integrity mechanisms, including consensus and proof of work. We study the power of disentangling availability and integrity mechanisms by building a variety of applications. The results from these examples suggest that developers can use Charlotte to build flexible, fast, composable applications with strong guarantees.

cs.DC↗

arXiv2018

A Web of Blocks

Blockchains offer a useful abstraction: a trustworthy, decentralized log of totally ordered transactions. Traditional blockchains have problems with scalability and efficiency, preventing their use for many applications. These limitations arise from the requirement that all participants agree on the total ordering of transactions. To address this fundamental shortcoming, we introduce Charlotte, a system for maintaining decentralized, authenticated data structures, including transaction logs. Each data structurestructure -- indeed, each block -- specifies its own availability and integrity properties, allowing Charlotte applications to retain the full benefits of permissioned or permissionless blockchains. In Charlotte, a block can be atomically appended to multiple logs, allowing applications to be interoperable when they want to, without inefficiently forcing all applications to share one big log. We call this open graph of interconnected blocks a blockweb. We allow new kinds of blockweb applications that operate beyond traditional chains. We demonstrate the viability of Charlotte applications with proof-of-concept servers running interoperable blockchains. Using performance data from our prototype, we estimate that when compared with traditional blockchains, Charlotte offers multiple orders of magnitude improvement in speed and energy efficiency.

cs.DC↗

arXiv2017

Nonmalleable Information Flow: Technical Report

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.

cs.CR↗

arXiv2016

Safe Serializable Secure Scheduling: Transactions and the Trade-off Between Security and Consistency

Modern applications often operate on data in multiple administrative domains. In this federated setting, participants may not fully trust each other. These distributed applications use transactions as a core mechanism for ensuring reliability and consistency with persistent data. However, the coordination mechanisms needed for transactions can both leak confidential information and allow unauthorized influence. By implementing a simple attack, we show these side channels can be exploited. However, our focus is on preventing such attacks. We explore secure scheduling of atomic, serializable transactions in a federated setting. While we prove that no protocol can guarantee security and liveness in all settings, we establish conditions for sets of transactions that can safely complete under secure scheduling. Based on these conditions, we introduce staged commit, a secure scheduling protocol for federated transactions. This protocol avoids insecure information channels by dividing transactions into distinct stages. We implement a compiler that statically checks code to ensure it meets our conditions, and a system that schedules these transactions using the staged commit protocol. Experiments on this implementation demonstrate that realistic federated transactions can be scheduled securely, atomically, and efficiently.

cs.DC↗

arXiv2014

Distributed Protocols and Heterogeneous Trust: Technical Report

The robustness of distributed systems is usually phrased in terms of the number of failures of certain types that they can withstand. However, these failure models are too crude to describe the different kinds of trust and expectations of participants in the modern world of complex, integrated systems extending across different owners, networks, and administrative domains. Modern systems often exist in an environment of heterogeneous trust, in which different participants may have different opinions about the trustworthiness of other nodes, and a single participant may consider other nodes to differ in their trustworthiness. We explore how to construct distributed protocols that meet the requirements of all participants, even in heterogeneous trust environments. The key to our approach is using lattice-based information flow to analyse and prove protocol properties. To demonstrate this approach, we show how two earlier distributed algorithms can be generalized to work in the presence of heterogeneous trust: first, Heterogeneous Fast Consensus, an adaptation of the earlier Bosco Fast Consensus protocol; and second, Nysiad, an algorithm for converting crash-tolerant protocols to be Byzantine-tolerant. Through simulations, we show that customizing a protocol to a heterogeneous trust configuration yields performance improvements over the conventional protocol designed for homogeneous trust.

cs.DC↗

arXiv2012

Automatic Partitioning of Database Applications

Database-backed applications are nearly ubiquitous in our daily lives. Applications that make many small accesses to the database create two challenges for developers: increased latency and wasted resources from numerous network round trips. A well-known technique to improve transactional database application performance is to convert part of the application into stored procedures that are executed on the database server. Unfortunately, this conversion is often difficult. In this paper we describe Pyxis, a system that takes database-backed applications and automatically partitions their code into two pieces, one of which is executed on the application server and the other on the database server. Pyxis profiles the application and server loads, statically analyzes the code's dependencies, and produces a partitioning that minimizes the number of control transfers as well as the amount of data sent during each transfer. Our experiments using TPC-C and TPC-W show that Pyxis is able to generate partitions with up to 3x reduction in latency and 1.7x improvement in throughput when compared to a traditional non-partitioned implementation and has comparable performance to that of a custom stored procedure implementation.

cs.DB↗