Automatic identification of semantic security vulnerabilities in system software such as kernels

An operating system kernel is the most security-critical piece of system software running on a computer. Linux for example supports a plethora of hardware and different features for its many different use cases. To support its modularity and configurability, this code contains many indirections and interactions between different components. This leads to Linux being a security-critical code base, but at the same time being a code base which is hard to analyse. The correct execution of this expansive code base furthermore relies on developers adhering to many rules, both explicit and implicit. Analysis tools exist that try to reconstruct these rules, and then use this information to find violations in the codebase. However, their false positive rates and their lack of proof-of-concept inputs limit their usefulness to developers. Moreover, the security rules and guidelines are not enforced during the writing of the code, instead analysis is treated as an afterthought. In short, existing tools for securing the Linux kernel suffer from a lack of timely feedback, low overhead analysis and implied rules. My overall goal is to research if I can provide developers of system software with faster and more actionable feedback of their code, increasing the security of their products in the long term. My vision is to have real-time feedback during development of system-level code, rather than post-hoc analyses result that arrive only when the developer has moved on to other aspects.