Bay Area Security Day

The Golden Gate Bridge over San Francisco Bay

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

Sponsorship

Organizers

Emma Dauterman, Stanford
Henry Corrigan-Gibbs, UC Berkeley
Raluca Ada Popa, UC Berkeley

Program

  1. Coffee and registration

  2. 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.

  3. 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.

  4. 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.

  5. 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.

  6. Lunch

  7. 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.

  8. 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.

  9. Coffee break

  10. Keynote talk: Securing Code with AI agents and Gemini Cyber

    Raluca Ada Popa, UC Berkeley and Google DeepMind

  11. 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.