SPATA: Effective OS Bug Detection with Summary-Based, Alias-Aware, and Path-Sensitive Typestate Analysis

The operating system (OS) is the cornerstone for computer systems. It manages hardware and provides fundamental service for user-level applications. Thus, detecting bugs in OSes is important to improve the reliability of computer systems. Static typestate analysis is a common technique for detecting various types of bugs, but it is often inaccurate or unscalable for large-size OS code, due to imprecision of identifying alias relationships as well as high costs of typestate tracking, path-feasibility validation, and inter-procedural analysis. In this article, 1 we present SPATA, a novel summary-based, alias-aware, and path-sensitive typestate analysis framework to detect OS bugs. To identify precise alias relationships in the OS code, SPATA performs a path-based alias analysis based on control-flow paths and access paths. With these alias relationships, SPATA reduces the costs of typestate tracking and path-feasibility validation, to accelerate path-sensitive typestate analysis for accurate bug detection. Moreover, SPATA uses an alias-summary-based analysis to accelerate inter-procedural bug detection, without time-consuming alias analysis across functions. We have evaluated SPATA on the Linux kernel and three popular IoT OSes, and it finds 651 real bugs with a false-positive rate of 18%. Besides, our alias-summary-based analysis achieves a 6.7x speedup in bug detection compared to non-summary-based analysis.