The Stanford Software Research Lunch is a weekly event on Thursday where students and researchers present their latest work to peers. Talks are open to anybody, but regular attendees are expected to give a presentation on their work. Members of the Computer Forum are especially welcome.
Mailing list: software-research-lunch@lists.stanford.edu (subscribe via mailman)
Calendar: ical
Format: The lunch is held every week during fall, winter and spring quarter. The first week of every quarter is an organizational lunch where people can sign up to give a talk. If you'd like to give a talk, please contact Rohan Yadav.
Past quarters: Fall 2025, Spring 2025, Winter 2025, Fall 2024, Spring 2024, Winter 2024, Fall 2023, Spring 2023, Winter 2023, Fall 2022, Winter 2021, Fall 2020, Winter 2020, Fall 2019, Spring 2019, Winter 2019, Fall 2018, Spring 2018, Winter 2018, Fall 2017, Spring 2017, Winter 2017, Fall 2016.
Ordering Food: For suggestions for those ordering food for the lunch, see here.
1/8: Hardware-Software Contracts for High Assurance with Applications to Side-Channel Security
Time: Thursday, January 8, 2026, 12 noon - 1pm
Location: CoDa E401
Speaker: Caroline Trippel
Abstract: Hardware side-channel attacks occur when a victim program’s hardware resource usage is influenced by a secret, and an attacker observes this resource usage (e.g., via its effect on execution time) to infer the secret’s value. Hardware side-channel attacks were once thought to threaten only secret-processing code and to be mitigated by constant-time programming, which avoids passing secrets as inputs to certain unsafe instructions that leak their operands via hardware side channels. However, Spectre attacks reveal that transient execution of instructions along mispredicted code paths can leak victim secrets, even if they are never leaked or even accessed architecturally. These attacks bypass gold standard software-level security policies (e.g., constant-time programming and sandboxing), establishing hardware side-channel attacks as a threat to all programs that hold secrets in architectural state.
Hardware side-channel defenses in general, and Spectre defenses in particular, require cooperation between hardware and software. Our research studies what this cooperation should look like and how to design and verify the implementations of new hardware-software contracts that enable it. This talk will introduce three such contracts. First, I will present the ASP contract, which empowers programs at compile-time to restrict their runtime control-/data-flow, enabling Serberus—a hardware-enabled software defense against Spectre for current-generation hardware. Next, I will present the ProtISA contract, which empowers programs at compile-time to specify what architectural registers and memory bytes may hold secrets at each program point, enabling Protean—a software-enabled hardware defense against Spectre for next-generation hardware. Finally, I will present leakage functions, a set of which form a contract that characterizes how a microarchitecture's hardware side-channels create observably-distinct executions for instructions as a function of unsafe instructions’ operands, enabling future probabilistic software-level and fine-grained hardware-level defenses against side-channel attacks.
Food:
1/15: System Support for Software Fiddling
Time: Thursday, January 15, 2026, 12 noon - 1pm
Location: CoDa E401
Speaker: Matthew Sotoudeh
Abstract: Most modern OS distributions have evolved a distinction between package maintainers (with knowledge and computing resources needed to modify software) and users (who interact solely with a precompiled binary). This strict dichotomy makes little sense today, as the popularity of programming education indicates people are acquiring the skills necessary to understand and control software running on their computers. I'll describe a new Debian variant designed around the assumption that casual users (with casual hardware and a second-year undergraduate programming skills) should be able to easily fiddle with (study, modify, and debug) the software on their machine. The distribution augments binary packages with additional information so they can be modified by the user via a software patching tool that allows fast, painless edit-rebuild-rerun cycles. Our tool also allows directly mixing Python code into C and C++ source files, letting users work in a language they might be more familiar with. Finally, I'll describe how the system makes large systems more understandable via tooling.
Food:
1/22: BEAVER: An Efficient Deterministic LLM Verifier
Time: Thursday, January 22, 2026, 12 noon - 1pm
Location: CoDa E401
Speaker: Tarun Suresh
Abstract: As large language models (LLMs) transition from research prototypes to production systems, verifying that their outputs satisfy correctness, safety, and security properties has become paramount for real-world deployment. Unlike traditional neural networks that produce a single output for a given input, LLMs induce probability distributions over output sequences, making distribution-level verification essential. However, LLMs' probabilistic choice, sequential unrolling, and decoding logic fall outside the expressiveness and scalability of traditional verification techniques based on abstract interpretation or SMT solvers. Consequently, existing work has resorted to ad hoc sampling-based estimates, but these cannot provide the rigorous guarantees required for reliable deployment. Therefore, new verification principles are needed to reason soundly about the probabilistic semantics of LLMs.
In this work, we formalize the LLM verification problem as computing the total probability that an LLM's output distribution satisfies a specified constraint. Contrary to popular belief, we demonstrate that deterministic verification is both possible and practical. We introduce BEAVER, the first framework for efficiently computing provably sound bounds on this likelihood for any given prompt and decidable prefix-closed constraint. BEAVER performs systematic Branch-and-Bound exploration of the generation space using novel data structures, maintains provably sound and monotonically tightening bounds at every iteration, and thus provides anytime certificates. We demonstrate BEAVER's effectiveness across a wide range of tasks, including correctness verification, privacy verification, and secure code generation on multiple state-of-the-art LLMs. Our results show that BEAVER achieves 6-8 times tighter probability bounds and identifies 3-4 times more high-risk instances than baseline methods under identical computational budgets.
Food:
1/29: TBD
Time: Thursday, January 29, 2026, 12 noon - 1pm
Location: CoDa E401
Speaker: TBD
Abstract: TBD
Food:
2/5: TBD
Time: Thursday, February 5, 2026, 12 noon - 1pm
Location: CoDa E401
Speaker: Genghan Zhang
Abstract: TBD
Food:
2/12: TBD
Time: Thursday, February 12, 2026, 12 noon - 1pm
Location: CoDa E401
Speaker: TBD
Abstract: TBD
Food:
2/19: TBD
Time: Thursday, February 19, 2026, 12 noon - 1pm
Location: CoDa E401
Speaker: TBD
Abstract: TBD
Food:
2/26: TBD
Time: Thursday, February 26, 2026, 12 noon - 1pm
Location: CoDa E401
Speaker: Scott Kovach
Abstract: TBD
Food:
3/5: TBD
Time: Thursday, March 5, 2026, 12 noon - 1pm
Location: CoDa E401
Speaker: Chris Gyurgyik
Abstract: TBD
Food:
3/12: A Programming Model for Passive Traffic Analysis
Time: Thursday, March 12, 2026, 12 noon - 1pm
Location: CoDa E401
Speaker: Thea Rossman
Abstract: TBD
Food:
3/19: TBD
Time: Thursday, March 19, 2026, 12 noon - 1pm
Location: CoDa E401
Speaker: TBD
Abstract: TBD
Food: