[TPSA'25] Scalable Bug Detection for Internally Unsafe Libraries: A Logical Approach to Type(…)

Описание: Scalable Bug Detection for Internally Unsafe Libraries: A Logical Approach to Type Refutation (Video, Theory and Practice of Static Analysis)
Pedro Carrott, Sacha-élie Ayoun, and Azalea Raad
(Imperial College London; Imperial College London; Imperial College London)

Abstract: Recent work has shown promising advances in techniques for scalable bug detection by leveraging \emph{under-approximate} (UX) reasoning. This work presents a UX approach to \emph{automatically} detect type unsoundness in libraries that rely on internal use of \emph{unsafe features}. To reason about such libraries, we build on prior work by encoding type assignments as \emph{separation logic} assertions. Our key insight is that undefined behaviour obtained from incorrect uses of unsafe features may be reasoned about by refuting such type assignments via \emph{incorrectness logic}. We demonstrate how our approach may be used to detect memory safety bugs in a simple language with an ownership type system.


Presentation at the Theory and Practice of Static Analysis workshop, January 21, 2025, https://popl25.sigplan.org/home/tpsa-...
Sponsored by ACM SIGPLAN