CRII: SHF: Analyzing the Linux's KBuild Makefile

Linux系统支持广泛的计算机设备，从微型物联网传感器和移动电话到台式和超级计算机。这种灵活性是由于Linux的高度可配置设计，允许用户使用广泛的选项集定制和构建Linux。这种可重构性有很多好处，但是由于有大量可能的配置，它也使测试和调试等任务变得非常复杂。该项目旨在开发算法和工具来分析复杂的Linux构建过程，以了解配置选项如何影响单个源文件的构建。这项研究将允许开发人员找到在构建过程中从未使用过的文件，检查和测试影响单个源文件的配置，并确定补丁或代码更改如何影响给定的配置。这项研究也帮助用户，例如，允许嵌入式系统制造商优化Linux以适应他们的设备。此外，该研究允许发现许多关于Linux构建系统的有趣和有用的信息，例如，构建条件的复杂性，高度影响的配置选项等。该项目旨在开发静态和动态分析来分析Linux构建系统，特别是控制单个源文件的构建和链接的“makefiles”。这项研究分为三个主要活动。第一部分开发了一种符号执行技术，该技术模拟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.