CAREER: Inferring and Securing Software Configurations through Automated Reasoning

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

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.