Bay Area Security Day
A one-day workshop for academic researchers studying computer security, co-hosted by Stanford and UC Berkeley.
We plan to make this a once-a-semester tradition!
Please register here so that we order enough food.
Logistics
When
October 30, 2026
10am–5pm
Where
Stanford University
CoDa W450
Lunch
Free!
Updates
Join the Google Group here to hear about future events
Thanks to Google for sponsoring the Security Day for 2026–2027!
Organizers
Emma Dauterman, Stanford
Henry Corrigan-Gibbs, UC Berkeley
Raluca Ada Popa, UC Berkeley
Program
-
Coffee and registration
-
Effective Vulnerability Discovery at AI Speed
Alon Shakevsky, UC Berkeley
Abstract
Exploitable vulnerabilities are the most common initial-access vector in organizational data breaches and the leading root cause of ransomware incidents. Large language models are changing the economics of cybersecurity as they significantly lower the cost of discovering and exploiting such vulnerabilities for attackers. As attackers only need one successful exploit, defenders must secure systems against every vulnerability that attackers can exploit. However, existing vulnerability discovery methods struggle to achieve high recall and precision without prohibitive cost. To reverse this asymmetry in favor of defenders, we need effective methods to find and fix vulnerabilities before attackers exploit them. In this talk, I will present key challenges, insights, and neuro-symbolic methods for effective vulnerability discovery.
Bio
Alon Shakevsky is a PhD researcher at UC Berkeley, working with Raluca Ada Popa and Ion Stoica on effective vulnerability discovery. He received his M.Sc. with distinction from Tel Aviv University in 2022 under the supervision of Eyal Ronen and Avishai Wool.
-
Measuring and Mitigating Agent Sandbox Escape with Siren
Darya Kaviani and Oscar O’Rahilly, Anthropic
Abstract
AI agents are usually run inside sandboxes, but sandboxes can have weaknesses, and an agent that finds one may use it to finish its task. We measure this behavior with Siren, an evaluation that sets routine dev-ops tasks in deliberately weakened sandboxes with a useful credential or file just outside. This talk covers what makes agents reach outside, what stops them, and how we mitigate against them.
-
LFI-XL: Scaling Software Fault Isolation Beyond 4GiB
Zachary Yedidia, Stanford
Abstract
Software-based fault isolation (SFI) confines memory-safety bugs in native code, but modern SFI schemes limit sandboxes to 4GiB in size to exploit 32-bit addressing tricks for low overhead. This cap makes it difficult to use SFI systems in both applications like browser JITs that require large address spaces, and on platforms with small virtual address spaces like Android. This talk will present LFI-XL, an extension to the Lightweight Fault Isolation (LFI) SFI system that supports sandboxes sized to any power of 2. We will also discuss how modern hardware features such as Intel MPK and CET can be used to accelerate LFI-XL, and how LFI-XL can be used to sandbox the SpiderMonkey JavaScript engine.
Bio
Zachary Yedidia is a 6th year PhD student advised by David Mazières working on security, operating systems, and compilers.
-
Trident: Improving Malware Detection with LLMs and Behavioral Features
Rebecca Saul, UC Berkeley
Abstract
Traditionally, machine learning methods for PE malware detection have relied on static features like byte histograms, string information, and PE header contents. One barrier to incorporating dynamic analysis features has been the semi-structured nature of sandbox behavior reports. We show that, using the latest generation of large language models with reasoning, it is possible to efficiently process these behavior reports and utilize them as part of a malware detection pipeline. Specifically, we leverage LLMs to generate behavior-based malware detection rules based on a small training set of labeled malware. We find that these detection rules, derived from behavioral features, are much more robust to concept drift than standard static-feature methods, while maintaining practical false positive rates. Finally, we introduce Trident, a system which combines a classic decision tree model over static features, our behavior-based detection rules, and direct LLM analysis of sandbox reports through majority voting. Trident outperforms standard methods using static features, outperforms behavior-based rules alone, and is as resilient to concept drift as active learning methods without requiring retraining.
Bio
Rebecca Saul is a Ph.D. student at the University of California, Berkeley, applying AI to solve problems in malware detection, binary analysis, and reverse engineering. She is advised by David Wagner and supported by the National Defense Science and Engineering Graduate Fellowship. Rebecca earned her B.A. in Mathematics from Harvard in 2022.
-
Lunch
-
Helium: Quantifying Microarchitectural Side-Channel Leakage with Probabilistic Guarantees
Samantha Archer, Stanford
Abstract
Constant-time programming ensures zero leakage of program secrets via hardware side channels by preventing secrets from being passed to unsafe instructions. However, as microarchitectures employ more data-dependent optimizations to boost performance, more instructions become unsafe, and constant-time code incurs high performance cost. A promising alternative is bounding leakage according to application-specific requirements, but principled methods for doing so remain elusive. We present Helium, a three-part framework for quantifying hardware side-channel leakage of program secrets on specific microarchitectures. First, it leverages a new metric for expressing probabilistic side-channel leakage guarantees. Second, it employs a novel formalism for encoding how arbitrary hardware side channels give rise to attacker observations. Third, it provides two analysis techniques—symbolic (precise) and simulation (conservatively approximate)—to determine whether high-leakage observations occur with sufficiently low probability for a given victim program, secret input, microarchitecture, and attacker model. Through case studies spanning cryptographic and image processing applications, Helium demonstrates the necessity of considering both program and microarchitecture when assessing security-performance trade-offs. In one case, improved performance does not imply worse security; in another, accepting small leakage risk enables significant performance overhead reduction compared to a recent zero-leakage software side-channel defense.
Bio
Samantha Archer is a 4th year Ph.D. student at Stanford University advised by Prof. Caroline Trippel. Her research focuses on the formal verification of hardware, with an emphasis on microarchitectural side channel verification. Her work aims to help programmers and hardware designers more precisely reason about the risk of security-critical systems leaking information through hardware side channels.
-
Verifying Distributed Schedulers by Collecting Coupons
Akshay Srivatsan, Stanford
Abstract
Distributed execution engines, such as Kubernetes, Ray, and Legion, have to negotiate a fine balance between being general enough to support arbitrary workloads and being specific enough to provide efficient scheduling. The “ideal” scheduler, in many cases, would be one provided by the application developer. However, trusting an arbitrary user-provided scheduler can compromise the integrity of the system and is therefore nonviable in many multi-tenant use cases. Most execution systems therefore provide less-efficient alternatives such as scheduler “hints” that nudge a general-purpose scheduler into finding a more optimal schedule.
In this talk, I will present the current state of our group’s work to bridge the gap between untrusted user-provided schedulers and trusted general-purpose schedulers through a low-barrier-of-entry formal verification scheme that we call a “coupon collector”. We model distributed scheduling as a type of program optimization, where a simple set of rules can be used to classify specific optimizations as valid or invalid. We are in the process of extending our group’s existing distributed execution engine, Fix, with a “coupon collector”—a lightweight stateless theorem prover that communicates with an untrusted user schedule optimizer. We have formally verified a concrete implementation of a coupon collector and prove that it can constrain an arbitrary untrusted user-provided optimizer into only producing valid schedules.
Bio
Akshay Srivatsan is a fifth-year Ph.D. student at Stanford University advised by Professors Keith Winstein and Dawson Engler. His research focuses on the intersection of programming languages and distributed operating systems. His work uses techniques from functional programming and formal verification to improve the correctness, performance, and usability of distributed systems.
-
Coffee break
-
Keynote talk: Securing Code with AI agents and Gemini Cyber
Raluca Ada Popa, UC Berkeley and Google DeepMind
-
Crustify: Repository-Level Generation of Safe Rust Bindings with LLM Agents and Coverage-Guided Testing
Marius Momeu, UC Berkeley
Abstract
A crucial step towards migrating legacy systems code to safe Rust is generating safe interfaces (aka bindings) over unsafe C/C++ APIs, which lets native Rust use them without trading off memory safety. Implementing safe bindings, however, requires writing unsafe Rust, where any mistake introduces undefined behavior.
In this talk, I will present Crustify, an agentic co-translator that generates safe Rust bindings for C libraries, with or without its user in the loop. A user-facing assistant drives the campaign: a planner schedules the library's types and functions into dependency-ordered waves, scaling to repository-level targets, binder agents wrap each wave concurrently, and reviewer agents audit it, all following a common specification. The agents build on ffibox, a crate of audited primitives that wrap C types and pointers without forming Rust references to memory C may alias; Wavefront, a neuro-symbolic static analyzer that schedules their work; and ffimap, a rustc-based analysis that maps the unsafe surface the bindings expose. Coverage-guided tests under sanitizers and Miri check the bindings for soundness and functional equivalence.
On libgit2 and FFmpeg, Crustify bound 42% of each public API in under two days, leaving only 3.6% and 1.3% of the bindings' public functions unsafe. Auditing over ten human-written binding crates, Crustify also found over 100 reproducible cases of undefined behavior triggerable from safe Rust.
Bio
Marius Momeu is currently a postdoc in the Sky Lab at UC Berkeley, advised by Koushik Sen, where he develops Crustify to automate the migration to safe Rust with soundness and equivalence checks. His team is part of DARPA's TRACTOR program. He completed his PhD summa cum laude at TU Munich, advised by Claudia Eckert and Vasileios P. Kemerlis, developing automated techniques for software hardening and vulnerability discovery that were published at top-tier security conferences.