CRII: SHF: Analyzing the Linux's KBuild Makefile

University Of Nebraska-Lincoln, Lincoln NE

Investigators

Abstract

The Linux system empowers a wide range of computer devices, ranging from tiny IoT sensors and mobile phones to desktop and supercomputers. This flexibility is due to the highly-configurable design of Linux, allowing the users to customize and build Linux with an extensive set of options. This reconfigurability has many benefits, but it also greatly complicates tasks such as testing and debugging due to the large number of possible configurations. This project aims to develop algorithms and tools to analyze the complex Linux build process to understand how configuration options affect the building of individual source files. This research will allow developers to find orphan files that are never used in the build process, examine and test configurations that affect individual source files, and determine how patches or code changes affect a given configuration. The research also helps users, e.g., allowing embedded system manufacturers to optimize Linux to fit their devices. In addition, the research allows for the discovery of many interesting and useful information about the Linux build system, e.g., the complexity of build conditions, highly-influential configuration options, etc. This project aims to develop static and dynamic analyses to analyze the Linux build system, in particular the "makefiles" that control the building and linking of individual source files. The research is divided into three main activities. The first develops a symbolic execution technique that simulates the runs of the makefiles to obtain path conditions over configuration options mapping to built files. These path conditions provide a formal description of how configuration options affect the building of individual kernel files. The second develops a dynamic analysis that learns path conditions from kernel files built from actual make runs over a sample of configurations. This analysis will be based on a recent work developed by the team that alternates between a learning and checking phase to improve the overall quality of the learned conditions. Finally, by representing the obtained path conditions as logical formulae, modern constraint solvers can be applied to solve problems such as finding orphan files and the impact of configuration options to files included in a build. 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.