CRII: SHF: Analyzing the Linux's KBuild Makefile

点击翻译按钮获取中文摘要

The Linux system empowers a wide range of computer devices, rangingfrom 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 setof options. This reconfigurability has many benefits, but it alsogreatly complicates tasks such as testing and debugging due to thelarge number of possible configurations. This project aims to developalgorithms and tools to analyze the complex Linux build process tounderstand how configuration options affect the building of individualsource files. This research will allow developers to findorphan files that are never used in the build process, examine andtest configurations that affect individual source files, and determinehow patches or code changes affect a given configuration. The researchalso helps users, e.g., allowing embedded system manufacturers tooptimize Linux to fit their devices. In addition, the research allowsfor the discovery of many interesting and useful information about theLinux build system, e.g., the complexity of buildconditions, highly-influential configuration options, etc.This project aims to develop static and dynamic analyses to analyzethe Linux build system, in particular the "makefiles" that control thebuilding and linking of individual source files. The research isdivided into three main activities. The first develops a symbolicexecution technique that simulates the runs of the makefiles to obtainpath conditions over configuration options mapping to built files.These path conditions provide a formal description of howconfiguration options affect the building of individual kernel files.The second develops a dynamic analysis that learns path conditionsfrom kernel files built from actual make runs over a sample ofconfigurations. This analysis will be based on a recent work developedby the team that alternates between a learning and checking phase toimprove the overall quality of the learned conditions. Finally, byrepresenting the obtained path conditions as logical formulae, modernconstraint solvers can be applied to solve problems such as findingorphan files and the impact of configuration options to files includedin 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.