CAREER: Inferring and Securing Software Configurations through Automated Reasoning

职业：通过自动推理推断和保护软件配置

• 批准号: 1941816
• 负责人: Paul Gazzillo
• 金额: $ 41.85万
• 依托单位: The University of Central Florida Board of Trustees
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2020
• 资助国家: 美国
• 起止时间: 2020-06-01 至 2025-05-31
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1941816&HistoricalAwards=false
• 关键词: CAREER; Inferring; Securing; Software; Configurations

Highly-configurable software forms the basis of much modern computing infrastructure, because configurability enables extensive reuse. However, software configurability opens the door to misconfiguration vulnerabilities, which are invalid settings that expose software weaknesses. Misconfiguration is one of the most critical and common security risks. Real-world software, however, can have an enormous number of possible configurations and often lacks explicit information about what configurations are secure, leaving users to find and validate configuration settings manually. Compounding the problem, a complete computing system may combine hundreds or thousands of software packages whose configuration settings interact unexpectedly. The goal of this project is to automate the creation of valid configurations that are reliable and secure. As the world increasingly depends on smart infrastructure and Internet-of-Things devices to enhance lives, this research will benefit society by improving the reliability and security of the configurable software used in these computing devices. The research topics, results, and materials from this award will be used in education and training as well as outreach aimed at broadening participation in computing.This project consists of four tasks that take the foundational first steps towards making software configuration reliable and secure. The first task is the development of a unified configuration language for configuration specifications that are explicit, well-defined, and amenable to formal modeling. To bootstrap support for existing software, this task will develop new algorithms to automatically extract specifications from known configuration mechanisms. The second task is an optimizing compiler for the unified configuration language that produces formal logic, so that checking secure configurations is equivalent to Boolean satisfiability. Algorithms for sampling and searching for valid configurations will also be developed to provide the basis for testing and security applications. The third task is a set of new techniques for testing highly-configurable software. This project will develop static analyses to localize defects to precise configurations and search-based algorithms to explore the space of valid configurations for software bugs. The fourth task is the development of new algorithms that automatically discover secure configurations, because a valid configuration may be bug-free but still violate a user's security policy. This project will develop algorithms to automatically find hardened configurations and minimize attack surface. These research tasks will be evaluated on critical, widely-used, highly-configurable software for the ability to infer, test, and secure configurations on a large scale efficiently.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.

高度可配置的软件构成了许多现代计算基础设施的基础，因为可配置性可以实现广泛的重用。然而，软件可配置性为错误配置漏洞打开了大门，这些漏洞是暴露软件弱点的无效设置。 配置错误是最严重和最常见的安全风险之一。 然而，现实世界的软件可能有大量可能的配置，并且通常缺乏有关哪些配置是安全的明确信息，导致用户必须手动查找和验证配置设置。使问题更加复杂的是，一个完整的计算系统可能会结合数百或数千个软件包，这些软件包的配置设置会意外地交互。 该项目的目标是自动创建可靠且安全的有效配置。 随着世界越来越依赖智能基础设施和物联网设备来改善生活，这项研究将通过提高这些计算设备中使用的可配置软件的可靠性和安全性来造福社会。 该奖项的研究主题、结果和材料将用于教育和培训以及旨在扩大计算参与的推广。该项目由四项任务组成，为实现软件配置的可靠性和安全性迈出了基础性的第一步。第一个任务是为配置规范开发统一的配置语言，该语言是明确的、定义良好的并且适合形式建模。 为了引导对现有软件的支持，该任务将开发新的算法，以自动从已知的配置机制中提取规范。 第二个任务是针对产生形式逻辑的统一配置语言的优化编译器，以便检查安全配置相当于布尔可满足性。 还将开发采样和搜索有效配置的算法，为测试和安全应用提供基础。 第三项任务是一套用于测试高度可配置软件的新技术。 该项目将开发静态分析以将缺陷定位到精确的配置和基于搜索的算法以探索软件错误的有效配置空间。 第四项任务是开发自动发现安全配置的新算法，因为有效的配置可能没有错误，但仍然违反用户的安全策略。 该项目将开发算法来自动查找强化配置并最大限度地减少攻击面。 这些研究任务将在关键的、广泛使用的、高度可配置的软件上进行评估，以便能够有效地进行大规模推断、测试和保护配置。该奖项反映了 NSF 的法定使命，并被认为值得通过使用评估来支持基金会的智力价值和更广泛的影响审查标准。

项目成果

Bringing Together Configuration Research: Towards a Common Ground

• DOI: 10.1145/3563835.3568737
• 发表时间: 2022-11
• 期刊: Proceedings of the 2022 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software
• 作者: Paul Gazzillo;Myra B. Cohen

Inferring and securing software configurations using automated reasoning

使用自动推理来推断和保护软件配置

• DOI: 10.1145/3368089.3417041
• 发表时间: 2020
• 期刊: Proceedings of the 28th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering
• 作者: Gazzillo, Paul

Finding broken Linux configuration specifications by statically analyzing the Kconfig language

通过静态分析 Kconfig 语言来查找损坏的 Linux 配置规范

• DOI: 10.1145/3468264.3468578
• 发表时间: 2021
• 期刊: ESEC/FSE 2021: Proceedings of the 29th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering
• 作者: Oh, Jeho;Yıldıran, Necip Fazıl;Braha, Julian;Gazzillo, Paul
• 通讯作者: Gazzillo, Paul

Semantic Analysis of Macro Usage for Portability

可移植性宏用法的语义分析

• DOI: 10.1145/3597503.3623323
• 发表时间: 2024
• 期刊: ACM
• 作者: Pappas, Brent;Gazzillo, Paul
• 通讯作者: Gazzillo, Paul