10/06/2020 – Dry Run: “Finding Resource Manipulation Bugs With Monitor Automata On The Example Of The Linux Kernel” By Anders Fischer-Nielsen

Anders Fischer-Nielsen will give a dry run of his master thesis presentation. Details below.


Anders Fischer-Nielsen, MSc student.


Finding Resource Manipulation Bugs with Monitor Automata on the Example of the Linux Kernel


I present the concept and the implementation of monitor templates, a way of expressing bug checkers operating on code — here on the Linux kernel. Monitor templates define properties of source code leading to resource manipulation bugs on memory cells, allowing detecting and reporting these bugs. I define monitor templates and their implementation on the example of the Linux kernel by extending the shape-and-effect analysis by Iago Abal et. al. Monitor templates are deterministic finite automata specified on so-called effects inferred from executing program points in the control flow of a program. I present an implemented reference implementation of such monitor templates as an extension to the work by Abal et. al. and an evaluation of the resulting bug checker on the Linux kernel showing greater expressiveness of bug checkers and a higher accuracy for detection of bugs compared to a previous approach based on the existing theory by Abal. et. al., albeit with a greater number of false positives being present as well.