CAREER: Towards Reliable Operating Systems through Scalable Control- and Data-Flow Analysis

Purdue University, West Lafayette IN

Investigators

Abstract

Operating systems kernels are an essential software component of servers, desktops, mobile devices, and embedded devices. However, kernels are large and particularly complex, making them exceptionally difficult to implement correctly and prone to software bugs. This project develops testing techniques that are especially suited to find software bugs in modern kernels, which are highly concurrent. This project is expected to develop effective techniques to help ensure developers find kernel defects before deployment to users. The project develops methods that uncover and analyze schedule-dependent non-determinism to find challenging classes of kernel concurrency bugs. This work is composed of three main components. First, it develops scalable techniques that analyze potential inter-thread communication to pair sequential tests intelligently and select schedules that expose kernel concurrency bugs. Second, it develops data-flow-aware techniques that advance sequential test generation by producing representative sequential tests that expose operating system non-determinism when combined. Third, it explores methods that analyze kernel output across schedules to detect subtle semantic bugs with a high impact on reliability and security. This work increases the reliability and security of virtually all classes of computer systems, including Internet-of-Things devices, consumer desktops, data center servers, and critical infrastructures. In addition, this work reduces the development, testing, and operational costs and reduces the occurrence of bugs that slip into deployed systems. Thus, this project reduces the incidence of downtime, loss of data, and other incorrect behavior across a wide range of systems used by billions of users. All project data is stored in public sites and university storage systems to ensure safe long-term storage for at least seven years from the award conclusion or public release, whichever comes later. The data produced includes system implementations and source code, documentation, kernel analysis datasets, and mentoring material, which will be located at https://www.cs.purdue.edu/homes/pfonseca/projects/reliable-concurrent-os.html. This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.