Bay Area Security Day

Program

1. 9:30–10am

   Coffee and registration

2. 10–10:30am

   Antiproof: Synthesizing Vulnerability Detectors and Proofs of Exploitability

   Alon Shakevsky, UC Berkeley

   Abstract

   Discovering vulnerabilities before attackers exploit them requires high recall and reliable automatic validation, but existing approaches struggle to achieve both without prohibitive cost. We present Antiproof, an end-to-end vulnerability discovery system that combines neuro-symbolic detector synthesis for high-recall discovery with proof-of-exploitability oracles for automatic validation. Antiproof learns and iteratively refines static detectors from vulnerability datasets, then validates candidates by verifying whether executable proofs demonstrate concrete attacker capabilities. Evaluated on BountyBench and our curated KEVBench dataset, Antiproof detects 64 of 66 vulnerabilities, improving recall by more than 60 percentage points over static-analysis and neuro-symbolic baselines. In a scan of 50 widely deployed systems, Antiproof uncovered several hundred previously unknown vulnerabilities. We are responsibly disclosing all confirmed zero-days and have received 12 CVE assignments to date, including remote code execution vulnerabilities in Ray, SGLang, vLLM, and LiteLLM that could allow attackers to take over LLM training and inference systems.

   Bio

   Alon Shakevsky is a PhD researcher at UC Berkeley, working with Raluca Ada Popa and Ion Stoica on effective vulnerability discovery. His previous research includes trusted execution environments, applied cryptography, and cloud and AI infrastructure security. He received his M.Sc. with distinction from Tel Aviv University in 2022 under the supervision of Eyal Ronen and Avishai Wool.

3. 10:30–11am

   Innovations in Agent Security

   Darya Kaviani, Anthropic

4. 11–11:30am

   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. 11:30am–noon

   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. noon–1:30pm

   Lunch

7. 1:30–2pm

   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. 2–2:30pm

   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. 2:30–3pm

   Coffee break

10. 3–4pm

    Keynote talk: Securing Code with AI agents and Gemini Cyber

    Raluca Ada Popa, UC Berkeley and Google DeepMind

11. 4–4:30pm

    Crustify: Generating and Auditing Safe Rust Bindings using LLM Agents and Executable Verifiers

    Marius Momeu, UC Berkeley

    Abstract

    A crucial step towards migrating legacy systems code to a safe Rust ecosystem is generating safe interfaces (aka bindings) over unsafe C/C++ APIs, allowing them to be integrated in native Rust without trading off memory safety. Implementing safe bindings however requires writing unsafe Rust, where the compiler trusts the programmer to ensure that the code holds its invariants, i.e. is sound—any programming mistake in unsafe Rust introduces undefined behavior.

    In this talk I will present Crustify, an automated transpiler that leverages LLM agents to synthesize safe Rust interfaces over unsafe APIs and sanitizer-backed verifiers that achieve high coverage to ensure soundness and functional equivalence. Crustify employs a two-agent architecture that consists of an orchestrator and a translator, and a pipeline that supports workload decomposition, concurrent execution, and adversarial review using independent models. Additionally, we equip Crustify agents with wavefront, a static analysis tool for precise scheduling and decomposition, and ffibox, a crate of audited primitives for synthesizing safe Rust bindings that are sound.

    On generating safe bindings for two production codebases with over 100K LoC, libgit2 and ffmpeg, Crustify exceeded the API coverage of existing baselines, as well as their testing coverage for soundness and functional equivalence. Moreover, on auditing over ten human-written Rust crates that implement safe bindings, Crustify found over 100 reproducible cases of undefined behavior that can be triggered from purely safe Rust.

    Bio

    Marius Momeu is currently postdoc in the Sky lab at UC Berkeley, advised by Koushik Sen, where he works on developing Crustify for automating the migration to safe Rust with correctness guarantees. Our team is part of the TRACTOR program funded by DARPA. 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 which were published at top-tier security conferences.