CAREER: Inferring and Securing Software Configurations through Automated Reasoning

The University Of Central Florida Board Of Trustees, Orlando FL

Investigators

Abstract

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.