Bugs in Code: Understanding, Detecting, and Fixing

The course will show the ways in which the software engineering research community approaches research on program correctness. I will present a summary of collaboration with open source projects around understanding historical bugs and building tools for detecting new bugs.

In the first part, I will report the state of the union for bugs in two complex software systems : the Linux kernel (which is likely the most popular operating system on the planet) and the ROS operating system (which is not an operating system at all, but likely the most popular robotics middleware on the planet). In both cases, we will look into programming language aspects of problems observed in the very rich histories stored in the source code repositories of this projects. In the Linux kernel case, we will additionally focus on challenges introduced by the highly configurable aspect (bugs hidden well in rare configurations). For ROS, we will emphasize robotics-specific bugs and problems hidden in intensive modularity of the ROS applications architectures. Then, we will ask basic methodological questions: Why a tool builder fighting with bugs might want to search and understand real bugs? What is the cost of studying bugs? How and what kinds of benchmarks can reduce this cost? What can be learnt from real bugs? What are the challenges of studying real bugs, and what methods do we have to reproduce real bugs, in order to use them for experiments later? How can we create benchmarks that will survive a long time, without bit rotting?

In the second part, I will show the EBA tool, specifically designed to uncover resource manipuation bugs in the Linux kernel; in response to some requirements presented in the first part of this lecture. EBA (an effect-based analyzer) creates a program abstraction performing a type inference in a rich type system tracking regions (a memory abstraction), simple shapes (hierarchies of pointers nested in structures) and side-effects of computations. This abstraction is then overlayed on a control-flow graph and fed to a reachability checking algorithm that identifies suspicious sequences of effects: for instance a lock taken twice. I will describe how EBA works, and how we used it to uncover about a dozen sequential double-lock bugs in the Linux kernel.

In the third part, I will attempt to define the problem of program repair, and present several exemplary works by other authors on generating fixes for bugs in software. We will conclude with reflection on challenges in bug finding and bug fixing research.

More details at http://phdopen.mimuw.edu.pl/index.php?page=l19w2.