39 citations · 123 across the 14 of their papers we have counts for
14 papers
Oblivious Probabilistic Outcome Logic: Verifying Probabilistic Programs with an Oblivious Adversary
Hanxi Chen, Noam Zilberstein, Andrew C. Myers +1
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…
A Calculus for Flow-Limited Authorization
Owen Arden, Anitha Gollamudi, Ethan Cecchetti +2
Real-world applications routinely make authorization decisions based on dynamic computation. Reasoning about dynamically computed authority is challenging. Integrity of the system…
Compositional Security for Reentrant Applications
Ethan Cecchetti, Siqiu Yao, Haobin Ni +1
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. Informatio…
Heterogeneous Paxos: Technical Report
Isaac Sheff, Xinwen Wang, Robbert van Renesse +1
In distributed systems, a group of achieve when, by observing the output of some , they all arrive at the same value. C…
Handling Bidirectional Control Flow: Technical Report
Yizhou Zhang, Guido Salvaneschi, Andrew C. Myers
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. M…
The Cost of Software-Based Memory Management Without Virtual Memory
Drew Zagieboylo, G. Edward Suh, Andrew C. Myers
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 isola…
Charlotte: Composable Authenticated Distributed Data Structures, Technical Report
Isaac Sheff, Xinwen Wang, Haobin Ni +2
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 Cha…
A Web of Blocks
Isaac Sheff, Xinwen Wang, Andrew C. Myers +1
Blockchains offer a useful abstraction: a trustworthy, decentralized log of totally ordered transactions. Traditional blockchains have problems with scalability and efficiency, pre…
Nonmalleable Information Flow: Technical Report
Ethan Cecchetti, Andrew C. Myers, Owen Arden
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 secur…
Safe Serializable Secure Scheduling: Transactions and the Trade-off Between Security and Consistency
Isaac Sheff, Tom Magrino, Jed Liu +2
Modern applications often operate on data in multiple administrative domains. In this federated setting, participants may not fully trust each other. These distributed applications…
Report on the NSF Workshop on Formal Methods for Security
Stephen Chong, Joshua Guttman, Anupam Datta +5
Report on the NSF Workshop on Formal Methods for Security, held 19-20 November 2015.
Distributed Protocols and Heterogeneous Trust: Technical Report
Isaac C. Sheff, Robbert van Renesse, Andrew C. Myers
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…
Automatic Partitioning of Database Applications
Alvin Cheung, Owen Arden, Samuel Madden +1
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 la…
Attacker Control and Impact for Confidentiality and Integrity
Aslan Askarov, Andrew Myers
Language-based information flow methods offer a principled way to enforce strong security properties, but enforcing noninterference is too inflexible for realistic applications. Se…