Sound Abstract Nonexploitability Analysis

on YouTube ↗20m

" summary

Defines a precise nonexploitability hyperproperty and gives a sound abstract-interpretation analysis that treats user input and randomness separately, proving nonexploitable iff the failure indicator is not tainted. Implements a 10k‑line OCaml analyzer for a C subset and runs it on 77 GNU Coreutils programs (up to 4,188 LOC) plus Juliet tests, filtering out 3498 of 4715 alarms as nonexploitable while adding under 16% runtime overhead.

AI-written summary · about

" chapters (9)

1. 0:00Introduction
2. 1:48False positives in abstract interpretation
3. 3:11Runtime errors and security
4. 5:45Nonexploitability as hyperproperty
5. 8:16Taint analysis for nonexploitability
6. 10:23Combining domains with taint tracking
7. 12:29Experimental evaluation
8. 14:40Conclusion and future work
9. 15:00Q&A

" related talks

• 25mExploits as Insecure CompilationJennifer Paykin · PriSC 2020
• 31mSound Symbolic Execution via Abstract Interpretation and its Application to Sec...Xavier Rival, Tamara Rezk, Ignacio Tiraboschi · VMCAI 2023
• 51mThe Anatomy of an ExploitPatricia Aas · ACCU 2019
• 38mEffective Usage Analysis: Boosting Developer Productivity Via Innovative, Noise-reduced Vulnerability AnalysisAharon Abadi, Ph.D · Global Security Vulnerability Summit @ Open Source Summit North America 2022
• 12mFully Abstract and Robust Compilation and How to Reconcile the Two, AbstractlyStelios Tsampas, Matteo Busi, Carmine Abate · APLAS 2021
• 22mWhen is a vulnerability not a vulnerability? Overcoming the...Adam Berman · BSidesSF 2023
• 19mExploiting Undefined Behavior in C/C++ Programs for Optimization: A Study on the(…)Nuno P. Lopes, Lucian Popescu · PLDI 2025
• 24mFuzzing Guided by Bayesian Program AnalysisXin Zhang, Yifan Zhang · POPL 2026