Nickolai Zeldovich

Proceedings of the 16th USENIX Symposium on Operating Systems Design and Implementation, 2022

2021

GoJournal: a verified, concurrent, crash-safe journaling system.

[BibT_eX]

[DOI]

Proceedings of the 15th USENIX Symposium on Operating Systems Design and Implementation, 2021

2020

Notary: A Device for Secure Transaction Approval.

[BibT_eX]

[DOI]

GetMobile Mob. Comput. Commun., 2020

Compact Certificates of Collective Knowledge.

[BibT_eX]

[DOI]

IACR Cryptol. ePrint Arch., 2020

Aardvark: A Concurrent Authenticated Dictionary with Short Proofs.

[BibT_eX]

[DOI]

IACR Cryptol. ePrint Arch., 2020

Efficiently Mitigating Transient Execution Attacks using the Unmapped Speculation Contract.

[BibT_eX]

[DOI]

Proceedings of the 14th USENIX Symposium on Operating Systems Design and Implementation, 2020

2019

Yodel: strong metadata security for voice calls.

[BibT_eX]

[DOI]

David Lazar

Yossi Gilad

Proceedings of the 27th ACM Symposium on Operating Systems Principles, 2019

Verifying concurrent, crash-safe systems with Perennial.

[BibT_eX]

[DOI]

Proceedings of the 27th ACM Symposium on Operating Systems Principles, 2019

Argosy: verifying layered storage systems with recovery refinement.

[BibT_eX]

[DOI]

Proceedings of the 40th ACM SIGPLAN Conference on Programming Language Design and Implementation, 2019

Extracting and Optimizing Formally Verified Code for Systems Programming.

[BibT_eX]

[DOI]

Eleftherios Ioannidis

Proceedings of the NASA Formal Methods - 11th International Symposium, 2019

Vault: Fast Bootstrapping for the Algorand Cryptocurrency.

[BibT_eX]

[DOI]

Proceedings of the 26th Annual Network and Distributed System Security Symposium, 2019

2018

Vault: Fast Bootstrapping for Cryptocurrencies.

[BibT_eX]

[DOI]

IACR Cryptol. ePrint Arch., 2018

A Revised and Verified Proof of the Scalable Commutativity Rule.

[BibT_eX]

[DOI]

CoRR, 2018

Karaoke: Distributed Private Messaging Immune to Passive Traffic Analysis.

[BibT_eX]

[DOI]

David Lazar

Yossi Gilad

Proceedings of the 13th USENIX Symposium on Operating Systems Design and Implementation, 2018

Proving confidentiality in a file system using DiskSec.

[BibT_eX]

[DOI]

Proceedings of the 13th USENIX Symposium on Operating Systems Design and Implementation, 2018

Verifying concurrent software using movers in CSPEC.

[BibT_eX]

[DOI]

Proceedings of the 13th USENIX Symposium on Operating Systems Design and Implementation, 2018

Veil: Private Browsing Semantics Without Browser-side Assistance.

[BibT_eX]

[DOI]

Frank Wang

James Mickens

Proceedings of the 25th Annual Network and Distributed System Security Symposium, 2018

2017

Algorand: Scaling Byzantine Agreements for Cryptocurrencies.

[BibT_eX]

[DOI]

IACR Cryptol. ePrint Arch., 2017

Certifying a file system using crash hoare logic: correctness in the presence of crashes.

[BibT_eX]

[DOI]

Commun. ACM, 2017

Stadium: A Distributed Metadata-Private Messaging System.

[BibT_eX]

[DOI]

Proceedings of the 26th Symposium on Operating Systems Principles, 2017

Verifying a high-performance crash-safe file system using a tree specification.

[BibT_eX]

[DOI]

Proceedings of the 26th Symposium on Operating Systems Principles, 2017

Scaling a file system to many cores using an operation log.

[BibT_eX]

[DOI]

Proceedings of the 26th Symposium on Operating Systems Principles, 2017

2016

Stadium: A Distributed Metadata-Private Messaging System.

[BibT_eX]

[DOI]

IACR Cryptol. ePrint Arch., 2016

Report on the NSF Workshop on Formal Methods for Security.

[BibT_eX]

[DOI]

CoRR, 2016

Alpenhorn: Bootstrapping Secure Communication without Leaking Metadata.

[BibT_eX]

[DOI]

David Lazar

Proceedings of the 12th USENIX Symposium on Operating Systems Design and Implementation, 2016

Sieve: Cryptographically Enforced Access Control for User Data in Untrusted Clouds.

[BibT_eX]

[DOI]

Proceedings of the 13th USENIX Symposium on Networked Systems Design and Implementation, 2016

2015

Nail: A Practical Tool for Parsing and Generating Data Formats.

[BibT_eX]

[DOI]

Julian Bangert

A Differential Approach to Undefined Behavior Detection.

[BibT_eX]

[DOI]

ACM Trans. Comput. Syst., 2015

The Scalable Commutativity Rule: Designing Scalable Software for Multicore Processors.

[BibT_eX]

[DOI]

ACM Trans. Comput. Syst., 2015

Guidelines for Using the CryptDB System Securely.

[BibT_eX]

[DOI]

Raluca Ada Popa

Hari Balakrishnan

IACR Cryptol. ePrint Arch., 2015

Vuvuzela: scalable private messaging resistant to traffic analysis.

[BibT_eX]

[DOI]

Proceedings of the 25th Symposium on Operating Systems Principles, 2015

Using Crash Hoare logic for certifying the FSCQ file system.

[BibT_eX]

[DOI]

Proceedings of the 25th Symposium on Operating Systems Principles, 2015

Specifying Crash Safety for Storage Systems.

[BibT_eX]

[DOI]

Proceedings of the 15th Workshop on Hot Topics in Operating Systems, 2015

Amber: Decoupling User Data from Web Applications.

[BibT_eX]

[DOI]

Proceedings of the 15th Workshop on Hot Topics in Operating Systems, 2015

Hare: a file system for non-cache-coherent multicores.

[BibT_eX]

[DOI]

Charles Gruenwald III

Filippo Sironi

Proceedings of the Tenth European Conference on Computer Systems, 2015

2014

Building Web Applications on Top of Encrypted Data Using Mylar.

[BibT_eX]

[DOI]

Nail: A Practical Interface Generator for Data Formats.

[BibT_eX]

[DOI]

Julian Bangert

Proceedings of the 35. IEEE Security and Privacy Workshops, 2014

Jitk: A Trustworthy In-Kernel Interpreter Infrastructure.

[BibT_eX]

[DOI]

Proceedings of the 11th USENIX Symposium on Operating Systems Design and Implementation, 2014

Identifying Information Disclosure in Web Applications with Retroactive Auditing.

[BibT_eX]

[DOI]

Proceedings of the 11th USENIX Symposium on Operating Systems Design and Implementation, 2014

Building Web Applications on Top of Encrypted Data Using Mylar.

[BibT_eX]

[DOI]

Proceedings of the 11th USENIX Symposium on Networked Systems Design and Implementation, 2014

VerSum: Verifiable Computations over Large Public Logs.

[BibT_eX]

[DOI]

Jelle van den Hooff

Proceedings of the 2014 ACM SIGSAC Conference on Computer and Communications Security, 2014

Why does cryptographic software fail?: a case study and open problems.

[BibT_eX]

[DOI]

Proceedings of the Asia-Pacific Workshop on Systems, 2014

2013

Processing Analytical Queries over Encrypted Data.

[BibT_eX]

[DOI]

Proc. VLDB Endow., 2013

Multi-Key Searchable Encryption.

[BibT_eX]

[DOI]

IACR Cryptol. ePrint Arch., 2013

An Ideal-Security Protocol for Order-Preserving Encoding.

[BibT_eX]

[DOI]

Frank H. Li

IACR Cryptol. ePrint Arch., 2013

Overcoming the Worst-Case Curse for Cryptographic Constructions.

[BibT_eX]

[DOI]

IACR Cryptol. ePrint Arch., 2013

Practical and Effective Sandboxing for Non-root Users.

[BibT_eX]

[DOI]

Proceedings of the 2013 USENIX Annual Technical Conference, 2013

Reusable garbled circuits and succinct functional encryption.

[BibT_eX]

[DOI]

Proceedings of the Symposium on Theory of Computing Conference, 2013

Towards optimization-safe systems: analyzing the impact of undefined behavior.

[BibT_eX]

[DOI]

Proceedings of the ACM SIGOPS 24th Symposium on Operating Systems Principles, 2013

Asynchronous intrusion recovery for interconnected web services.

[BibT_eX]

[DOI]

Proceedings of the ACM SIGOPS 24th Symposium on Operating Systems Principles, 2013

Systematic Analysis of Defenses against Return-Oriented Programming.

[BibT_eX]

[DOI]

Proceedings of the Research in Attacks, Intrusions, and Defenses, 2013

RadixVM: scalable address spaces for multithreaded applications.

[BibT_eX]

[DOI]

Austin T. Clements

Proceedings of the Eighth Eurosys Conference 2013, 2013

How to Run Turing Machines on Encrypted Data.

[BibT_eX]

[DOI]

Proceedings of the Advances in Cryptology - CRYPTO 2013, 2013

Authenticated storage using small trusted hardware.

[BibT_eX]

[DOI]

Proceedings of the CCSW'13, 2013

Optimizing unit test execution in large software programs using dependency analysis.

[BibT_eX]

[DOI]

Proceedings of the Asia-Pacific Workshop on Systems, 2013

Security bugs in embedded interpreters.

[BibT_eX]

[DOI]

Proceedings of the Asia-Pacific Workshop on Systems, 2013

2012

Succinct Functional Encryption and Applications: Reusable Garbled Circuits and Beyond.

[BibT_eX]

[DOI]

IACR Cryptol. ePrint Arch., 2012

CryptDB: processing queries on an encrypted database.

[BibT_eX]

[DOI]

Catherine M. S. Redfield

Hari Balakrishnan

Commun. ACM, 2012

CPHASH: a cache-partitioned hash table.

[BibT_eX]

[DOI]

Zviad Metreveli

Proceedings of the 17th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, 2012

Improving Integer Security for Systems with KINT.

[BibT_eX]

[DOI]

Proceedings of the 10th USENIX Symposium on Operating Systems Design and Implementation, 2012

Efficient Patch-based Auditing for Web Application Vulnerabilities.

[BibT_eX]

[DOI]

Proceedings of the 10th USENIX Symposium on Operating Systems Design and Implementation, 2012

Improving network connection locality on multicore systems.

[BibT_eX]

[DOI]

Proceedings of the European Conference on Computer Systems, 2012

Scalable address spaces using RCU balanced trees.

[BibT_eX]

[DOI]

Austin T. Clements

Proceedings of the 17th International Conference on Architectural Support for Programming Languages and Operating Systems, 2012

Undefined behavior: what happened to my code?

[BibT_eX]

[DOI]

Proceedings of the Asia-Pacific Workshop on Systems, 2012

Recovering from intrusions in distributed systems with DARE.

[BibT_eX]

[DOI]

Proceedings of the Asia-Pacific Workshop on Systems, 2012

2011

Making information flow explicit in HiStar.

[BibT_eX]

[DOI]

Commun. ACM, 2011

Experiences in Cyber Security Education: The MIT Lincoln Laboratory Capture-the-Flag Exercise.

[BibT_eX]

[DOI]

Proceedings of the 4th Workshop on Cyber Security Experimentation and Test, 2011

Secure In-Band Wireless Pairing.

[BibT_eX]

[DOI]

Proceedings of the 20th USENIX Security Symposium, 2011

CryptDB: protecting confidentiality with encrypted query processing.

[BibT_eX]

[DOI]

Catherine M. S. Redfield

Hari Balakrishnan

Proceedings of the 23rd ACM Symposium on Operating Systems Principles 2011, 2011

Software fault isolation with API integrity and multi-principal modules.

[BibT_eX]

[DOI]

Proceedings of the 23rd ACM Symposium on Operating Systems Principles 2011, 2011

Intrusion recovery for database-backed web applications.

[BibT_eX]

[DOI]

Proceedings of the 23rd ACM Symposium on Operating Systems Principles 2011, 2011

A Trigger-Based Middleware Cache for ORMs.

[BibT_eX]

[DOI]

Priya Gupta

Samuel Madden

Proceedings of the Middleware 2011, 2011

Energy management in mobile devices with the cinder operating system.

[BibT_eX]

[DOI]

Arjun Roy

Stephen M. Rumble

Ryan Stutsman

Philip Alexander Levis

David Mazières

Proceedings of the European Conference on Computer Systems, 2011

Relational Cloud: a Database Service for the cloud.

[BibT_eX]

[DOI]

Proceedings of the Fifth Biennial Conference on Innovative Data Systems Research, 2011

Retroactive auditing.

[BibT_eX]

[DOI]

Xi Wang

Proceedings of the APSys '11 Asia Pacific Workshop on Systems, 2011

Linux kernel vulnerabilities: state-of-the-art defenses and open problems.

[BibT_eX]

[DOI]

Proceedings of the APSys '11 Asia Pacific Workshop on Systems, 2011

2010

Apprehending joule thieves with cinder.

[BibT_eX]

[DOI]

Stephen M. Rumble

Ryan Stutsman

Philip Alexander Levis

David Mazières

Comput. Commun. Rev., 2010

Separating Web Applications from User Data Storage with BSTORE.

[BibT_eX]

[DOI]

Priya Gupta

Proceedings of the USENIX Conference on Web Application Development, 2010

Making Linux Protection Mechanisms Egalitarian with UserFS.

[BibT_eX]

[DOI]

Proceedings of the 19th USENIX Security Symposium, 2010

Tolerating Malicious Device Drivers in Linux.

[BibT_eX]

[DOI]

Silas Boyd-Wickizer

Proceedings of the 2010 USENIX Annual Technical Conference, 2010

Intrusion Recovery Using Selective Re-execution.

[BibT_eX]

[DOI]

Proceedings of the 9th USENIX Symposium on Operating Systems Design and Implementation, 2010

An Analysis of Linux Scalability to Many Cores.

[BibT_eX]

[DOI]

Proceedings of the 9th USENIX Symposium on Operating Systems Design and Implementation, 2010

Locating cache performance bottlenecks using data profiling.

[BibT_eX]

[DOI]

Aleksey Pesterev

Robert Tappan Morris

Proceedings of the European Conference on Computer Systems, 2010

2009

Nemesis: Preventing Authentication & Access Control Vulnerabilities in Web Applications.

[BibT_eX]

[DOI]

Michael Dalton

Christos Kozyrakis

Proceedings of the 18th USENIX Security Symposium, 2009

Improving application security with data flow assertions.

[BibT_eX]

[DOI]

Proceedings of the 22nd ACM Symposium on Operating Systems Principles 2009, 2009

Delegating network security with more information.

[BibT_eX]

[DOI]

Proceedings of the 1st ACM SIGCOMM 2009 Workshop on Research on Enterprise Networking, 2009

2008

Securing untrustworthy software using information flow control.

[BibT_eX]

[DOI]

PhD thesis, 2008

Hardware Enforcement of Application Security Policies Using Tagged Memory.

[BibT_eX]

[DOI]

Proceedings of the 8th USENIX Symposium on Operating Systems Design and Implementation, 2008

Securing Distributed Systems with Information Flow Control.

[BibT_eX]

[DOI]

Silas Boyd-Wickizer

David Mazières

Proceedings of the 5th USENIX Symposium on Networked Systems Design & Implementation, 2008

2005

Interactive Performance Measurement with VNCPlay.

[BibT_eX]

[DOI]

Proceedings of the FREENIX Track: 2005 USENIX Annual Technical Conference, 2005

The Collective: A Cache-Based System Management Architecture.

[BibT_eX]

[DOI]