Precise and Scalable Detection of Double-Fetch Bugs in OS Kernels

Explore a comprehensive analysis of double-fetch bugs in operating system kernels through this IEEE conference talk. Delve into the challenges of detecting these critical vulnerabilities and learn about Deadline, a static analysis system designed to automatically identify double-fetch bugs. Discover the formal definition of these bugs, understand the limitations of previous detection methods, and gain insights into the systematic approach used to find multi-reads in kernel code. Examine the specialized symbolic checking techniques employed to verify potential double-fetch bugs and review the findings from applying Deadline to Linux and FreeBSD kernels. Investigate four generic strategies proposed for patching and preventing these vulnerabilities, based on extensive research and discussions with kernel maintainers. Gain valuable knowledge about address-based separation protection, dependency analysis, and mitigation techniques to enhance operating system security.

Introduction
Why do we do this
Addressbased separation protection
Why do we doublefetch
What could go wrong
Why is it difficult to detect
Dependency Lowcut
What can go wrong
Proof attacks
Overlap
Control Dependence
Data Dependence
Recap
Goal
Topdown approach
Some details
Symbolic Checking
Code Walkthrough
More Complex Example
Findings
Mitigation
Single fetch
Limitations
Conclusion
Chan