CRII: SHF: Analyzing the Linux's KBuild Makefile

Linux系统支持广泛的计算机设备，从微型物联网传感器和手机到台式机和超级计算机。这种灵活性归功于Linux高度可配置的设计，允许用户定制和构建具有广泛选项的Linux。这种可重构性有很多好处，但由于可能的配置数量太多，它也使测试和调试等任务变得非常复杂。该项目旨在开发算法和工具来分析复杂的Linux构建过程，以了解配置选项如何影响单个源文件的构建。这项研究将允许开发人员找到在构建过程中从未使用过的孤立文件，检查和测试影响单个源文件的配置，并确定补丁或代码更改如何影响给定的配置。这项研究还有助于用户，例如，允许嵌入式系统制造商优化Linux以适应他们的设备。此外，该研究允许发现许多关于Linux构建系统的有趣和有用的信息，例如，构建条件的复杂性、极具影响力的配置选项等。该项目旨在开发静态和动态分析来分析Linux构建系统，特别是控制单个源文件的构建和链接的“生成文件”。研究分为三个主要活动。前者开发了一种符号执行技术，模拟了Make文件的运行，以获得映射到构建文件的配置选项的路径条件。这些路径条件提供了配置选项如何影响单个内核文件构建的形式化描述。第二种开发了一种动态分析，它从实际Make运行的内核文件中学习路径条件，并对配置样本进行运行。这一分析将基于该团队最近开发的一项工作，该工作在学习和检查阶段之间交替进行，以提高学习条件的整体质量。最后，通过将获得的路径条件表示为逻辑公式，现代约束求解器可以应用于解决诸如寻找孤立文件以及配置选项对建筑物中包含的文件的影响等问题。该奖项反映了NSF的法定使命，并通过使用基金会的智力优势和更广泛的影响审查标准进行评估，被认为值得支持。

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.