SHF: Small: Formal Methods for Modern System Configuration Languages

University Of Massachusetts Amherst, Amherst MA

Investigators

Abstract

Computer systems play an essential role in all aspects of business, education, and the military. However, modern computer systems are incredibly complicated and thus prone to failure and susceptible to being hacked. System administrators, whose job it is to ensure that computer systems run smoothly, have a very difficult time managing and defending computing infrastructure. This research project is developing tools and techniques to make the job of system administrators dramatically easier. The project is focused on techniques that work well with existing, industry-standard tools and practices, which will make its research contributions easier to apply. The intellectual merits are that the project is (1) developing new tools for maintaining computer systems, (2) designing models of computer systems that are amenable to analysis and verification, and (3) advancing the state of the art in formal methods for system administration tools. The project's broader significance and importance are that (1) it directly addresses a current and urgent problem that affects the nation's computing infrastructure, (2) it is developing tools that system administrators will be able to use, and (3) it will spur further research and development in this important area by publishing and releasing its products as open source software. This project leverages recent advances in program verification and program synthesis to make system administration dramatically easier. Instead of proposing completely new abstractions that would be unfamiliar to system administrators, the project is developing techniques that are applicable to mainstream system configuration languages, such as Puppet, Chef, and Ansible. The project is developing tools to verify both universal properties of configurations and configuration-specific properties that govern how components of complex systems interact. Moreover, since real system configurations often invoke external commands, the project is also investigating a model-learning approach to accommodate them. Finally, even verified configurations need to be updated, and updates introduce new errors. To address this problem, the project is developing new abstractions to make configuration updates dramatically easier.