CRII: SHF: Analyzing the Linux's KBuild Makefile

CRII：SHF：分析 Linux 的 KBuild Makefile

• 批准号: 1948536
• 负责人: ThanhVu Nguyen
• 金额: $ 17.5万
• 依托单位: University of Nebraska-Lincoln
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2020
• 资助国家: 美国
• 起止时间: 2020-04-01 至 2022-12-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1948536&HistoricalAwards=false
• 关键词: CRII; SHF; Analyzing; Linux; KBuild

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.

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