SHF: Small: Formal Methods for Modern System Configuration Languages

计算机系统在商业、教育和军事的各个方面都发挥着至关重要的作用。然而，现代计算机系统非常复杂，因此容易出现故障，很容易被黑客攻击。系统管理员的工作是确保计算机系统平稳运行，他们在管理和保护计算基础设施方面遇到了非常困难的问题。该研究项目正在开发工具和技术，使系统管理员的工作大大简化。该项目专注于与现有的行业标准工具和实践很好地配合使用的技术，这将使其研究贡献更容易应用。该项目的智力优点是(1)开发用于维护计算机系统的新工具，(2)设计易于分析和验证的计算机系统模型，以及(3)在系统管理工具的形式化方法方面推进最先进的技术。该项目更广泛的意义和重要性在于：(1)它直接解决了影响国家计算基础设施的当前和紧迫的问题；(2)它正在开发系统管理员能够使用的工具；(3)它将通过以开源软件的形式发布和发布其产品，促进这一重要领域的进一步研究和开发。该项目利用程序验证和程序合成方面的最新进展，使系统管理大大简化。该项目不是提出系统管理员不熟悉的全新抽象，而是开发适用于主流系统配置语言的技术，如Pupket、Chef和Ansible。该项目正在开发工具，以验证配置的通用属性和特定于配置的属性，这些属性管理复杂系统的组件如何交互。此外，由于实际系统配置经常调用外部命令，该项目还在研究一种适应这些命令的模型学习方法。最后，即使是经过验证的配置也需要更新，而更新会带来新的错误。为了解决这个问题，该项目正在开发新的抽象，使配置更新变得非常容易。

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.