FMitF: Track II: Cybolic: a symbolic execution technique and tool for analyzing CMake build scripts

FMITF：轨道 II：Cybolic：用于分析 CMake 构建脚本的符号执行技术和工具

• 批准号: 2319131
• 负责人: ThanhVu Nguyen
• 金额: $ 9.72万
• 依托单位: George Mason University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2023
• 资助国家: 美国
• 起止时间: 2023-08-01 至 2025-01-31
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2319131&HistoricalAwards=false
• 关键词: FMitF; Track; II; Cybolic; symbolic; FMitF; Track; II; Cybolic; symbolic

CMake is a well-known, platform-independent software build automation tool. When build issues arise, developers often have to manually analyze CMake scripts to determine how files or libraries are built. This manual process is both error-prone and time-consuming. This project will develop Cybolic, a formal method and tool to analyze CMake. The novelties of the project are the automated and scalable algorithms enabling Cybolic to be practical and useful for developers. The project's impacts are that the open-source Cybolic tool will improve the debugging and build process of software relying on CMake and will benefit users who currently have to manually analyze CMake scripts.The project will build the Cybolic as a symbolic execution technique that transforms CMake code into logical formulae representing build conditions, which are mappings of conditions over build options for files and compilation flags. These build conditions can help developers in many tasks, such as finding orphan code sections, files, or compilation options that are never used and determining what patches or code changes affect a compilation configuration. This project will focus on (i) making Cybolic scale to large and complex CMake-based projects, (ii) applying Cybolic to detect real-world build issues, (iii) and integrating Cybolic with popular Integrated Development Environments (IDEs) such as Visual Studio (VS) Code to improve its usability and adoption. The findings from this project will be used in the investigator’s courses and mentoring and outreach activities.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.

Cmake是一种众所周知的，独立于平台的软件构建自动化工具。当出现构建问题时，开发人员通常必须手动分析CMAKE脚本以确定文件或库的构建方式。此手动过程既容易发生又耗时。该项目将开发Cybolic，这是一种正式的方法和分析CMAKE的工具。该项目的新颖性是使Cybolics可以实用且对开发人员有用的自动化算法。该项目的影响是，开源候选工具将改善依靠CMAKE的软件的调试和构建过程，并有益于目前必须手动分析CMAKE脚本的用户。该项目将构建该项目作为符号执行技术，该技术将CMAKE代码转换为逻辑公式为代表构建的构建条件的构建和构建文件的构图，并构建了构建构建和构建文件的条件，并构建了构建范围的范围，并构建了构建量的范围。这些构建条件可以帮助开发人员在许多任务中，例如从未使用过的孤儿代码部分，文件或编译选项，并确定哪些补丁程序或代码更改会影响编译配置。该项目将重点介绍（i）将囊比例制作到大型且复杂的基于CMAKE的项目，（ii）应用Cybolic来检测现实世界中的构建问题，（iii），并将Cybolic与流行的集成开发环境（IDE）（例如Visual Studio（VS）代码（VS）代码（VS）代码（VS）代码集成在一起，以提高其可用性和采用。该项目的发现将用于研究人员的课程以及心理和外展活动。该奖项反映了NSF的法定任务，并使用基金会的知识分子优点和更广泛的影响评估标准，认为通过评估被认为是宝贵的支持。