61 citations · 170 across the 18 of their papers we have counts for
19 papers
Auditing Rust Crates Effectively
Lydia Zoghbi, David Thien, Ranjit Jhala +2
We introduce Cargo Scan, the first interactive program analysis tool designed to help developers audit third-party Rust code. Real systems written in Rust rely on thousands of tran…
Robust Constant-Time Cryptography
Matthew Kolosick, Basavesh Ammanaghatta Shivakumar, Sunjay Cauligi +4
The constant-time property is considered the security standard for cryptographic code. Code following the constant-time discipline is free from secret-dependent branches and memory…
From Fine- to Coarse-Grained Dynamic Information Flow Control and Back, a Tutorial on Dynamic Information Flow
Marco Vassena, Alejandro Russo, Deepak Garg +2
This tutorial provides a complete and homogeneous account of the latest advances in fine- and coarse-grained dynamic information-flow control (IFC) security. Since the 70s, the pro…
A Turning Point for Verified Spectre Sandboxing
Sunjay Cauligi, Marco Guarnieri, Daniel Moghimi +2
Spectre attacks enable an attacker to access restricted data in an application's memory. Both the academic community and industry veterans have developed several mitigations to blo…
MSWasm: Soundly Enforcing Memory-Safe Execution of Unsafe Code
Alexandra E. Michael, Anitha Gollamudi, Jay Bosamiya +7
Most programs compiled to WebAssembly (Wasm) today are written in unsafe languages like C and C++. Unfortunately, memory-unsafe C code remains unsafe when compiled to Wasm -- and a…
Blocked or Broken? Automatically Detecting When Privacy Interventions Break Websites
Michael Smith, Peter Snyder, Moritz Haller +3
A core problem in the development and maintenance of crowd-sourced filter lists is that their maintainers cannot confidently predict whether (and where) a new filter list rule will…
SoK: Practical Foundations for Software Spectre Defenses
Sunjay Cauligi, Craig Disselkoen, Daniel Moghimi +2
Spectre vulnerabilities violate our fundamental assumptions about architectural abstractions, allowing attackers to steal sensitive data despite previously state-of-the-art counter…
Isolation Without Taxation: Near Zero Cost Transitions for SFI
Matthew Kolosick, Shravan Narayan, Evan Johnson +5
Software sandboxing or software-based fault isolation (SFI) is a lightweight approach to building secure systems out of untrusted components. Mozilla, for example, uses SFI to hard…
Solver-Aided Constant-Time Circuit Verification
Rami Gokhan Kici, Klaus v. Gleissenthall, Deian Stefan +1
We present Xenon, a solver-aided method for formally verifying that Verilog hardware executes in constant-time. Xenon scales to realistic hardware designs by drastically reducing t…
Swivel: Hardening WebAssembly against Spectre
Shravan Narayan, Craig Disselkoen, Daniel Moghimi +8
We describe Swivel, a new compiler framework for hardening WebAssembly (Wasm) against Spectre attacks. Outside the browser, Wasm has become a popular lightweight, in-process sandbo…
Automatically Eliminating Speculative Leaks from Cryptographic Code with Blade
Marco Vassena, Craig Disselkoen, Klaus V. Gleissenthall +5
We introduce BLADE, a new approach to automatically and efficiently eliminate speculative leaks from cryptographic code. BLADE is built on the insight that to stop leaks via specul…
Retrofitting Fine Grain Isolation in the Firefox Renderer (Extended Version)
Shravan Narayan, Craig Disselkoen, Tal Garfinkel +5
Firefox and other major browsers rely on dozens of third-party libraries to render audio, video, images, and other content. These libraries are a frequent source of vulnerabilities…
Gobi: WebAssembly as a Practical Path to Library Sandboxing
Shravan Narayan, Tal Garfinkel, Sorin Lerner +2
Software based fault isolation (SFI) is a powerful approach to reduce the impact of security vulnerabilities in large C/C++ applications like Firefox and Apache. Unfortunately, pra…
Iodine: Verifying Constant-Time Execution of Hardware
Klaus v. Gleissenthall, Rami Gökhan Kıcı, Deian Stefan +1
To be secure, cryptographic algorithms crucially rely on the underlying hardware to avoid inadvertent leakage of secrets through timing side channels. Unfortunately, such timing ch…
Constant-Time Foundations for the New Spectre Era
Sunjay Cauligi, Craig Disselkoen, Klaus v. Gleissenthall +4
The constant-time discipline is a software-based countermeasure used for protecting high assurance cryptographic implementations against timing side-channel attacks. Constant-time…
CT-Wasm: Type-Driven Secure Cryptography for the Web Ecosystem
Conrad Watt, John Renner, Natalie Popescu +2
A significant amount of both client and server-side cryptography is implemented in JavaScript. Despite widespread concerns about its security, no other language has been able to ma…
On Dynamic Flow-Sensitive Floating-Label Systems
Pablo Buiras, Deian Stefan, Alejandro Russo
Flow-sensitive analysis for information-flow control (IFC) allows data structures to have mutable security labels, i.e., labels that can change over the course of the computation.…
IFC Inside: Retrofitting Languages with Dynamic Information Flow Control (Extended Version)
Stefan Heule, Deian Stefan, Edward Z. Yang +2
Many important security problems in JavaScript, such as browser extension security, untrusted JavaScript libraries and safe integration of mutually distrustful websites (mash-ups),…
Flexible Dynamic Information Flow Control in the Presence of Exceptions
Deian Stefan, Alejandro Russo, John C. Mitchell +1
We describe a new, dynamic, floating-label approach to language-based information flow control. A labeled IO monad, LIO, keeps track of a current label and permits restricted acces…