Scalable Bug Detection for Internally Unsafe Libraries: A Logical Approach to Type Refutation

Abstract

Recent work has shown promising advances in techniques for scalable bug detection by leveraging under-approximate (UX) reasoning. This work presents a UX approach to automatically detect type unsoundness in libraries that rely on internal use of unsafe features. To reason about such libraries, we build on prior work by encoding type assignments as 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 incorrectness logic. We demonstrate how our approach may be used to detect memory safety bugs in a simple language with an ownership type system.