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