Incorrectness Logic for Scalable Bug Detection

ABSTRACT

Incorrectness Logic (IL) has recently been advanced as a logical under-approximate theory for proving the presence of bugs—dual to Hoare Logic, which is an over-approximate theory for proving the absence of bugs. To facilitate scalable bug detection, later we developed incorrectness separation logic (ISL) by marrying the under-approximate reasoning of IL with the local reasoning of separation logic and its frame rule. This locality leads to techniques that are compositional both in code (concentrating on a program component) and in the resources accessed (spatial locality), without tracking the entire global state or the global program within which a component sits. This enables reasoning to scale to large teams and codebases: reasoning can be done even when a global program is not present. We then developed Pulse-X, an automatic program analysis for catching memory safety errors, underpinned by ISL. Using PulseX, deployed at Meta, we found a number of real bugs in codebases such as OpenSSL, which were subsequently confirmed and fixed. We have compared the performance of Pulse-X against the state-of-the-art tool Infer on a number of large programs; our comparison shows that Pulse-X is comparable with Infer in terms of performance, and in certain cases its fix-rate surpasses that of Infer.

Authors

Dr Azalea Raad is a senior lecturer (associate professor) at the Department of Computing of Imperial College London. Her research interests include persistent programming, concurrent verification, hardware validation and bug detection tools and techniques for concurrent programs. In 2021 she was awarded a UKRI Future Leaders Fellowship to pursue advanced research into the foundations of non-volatile memory and persistent programming. She also received the President's Award for Outstanding Early Career Research from Imperial College London. As part of her research she closely collaborates with industry partners such as Intel, ARM, Meta (previously Facebook) and Bloomberg. Between 2020 and 2022 she worked as a consulting research scientist at Meta on projects such as Infer and the Incorrectness Logic Lab. She is also a verification consultant at Bloomberg, working on scalable techniques for detecting security exploits.