SHF: Small: Formal Methods for Modern System Configuration Languages

SHF：小：现代系统配置语言的形式化方法

• 批准号: 1717636
• 负责人: Brian Levine
• 金额: $ 44.89万
• 依托单位: University of Massachusetts Amherst
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2017
• 资助国家: 美国
• 起止时间: 2017-08-01 至 2021-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1717636&HistoricalAwards=false
• 关键词: SHF; Small; Formal; Methods; Modern

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.

计算机系统在商业，教育和军事的各个方面都起着至关重要的作用。但是，现代计算机系统非常复杂，因此容易失败，并且容易被黑客入侵。系统管理员的工作是确保计算机系统运行顺利，并且在管理和捍卫计算基础架构方面非常困难。 该研究项目正在开发工具和技术，以使系统管理员的工作变得更加容易。该项目的重点是与现有的行业标准工具和实践良好配合的技术，这将使其研究贡献更容易应用。智力优点是该项目是（1）开发用于维护计算机系统的新工具，（2）设计适合分析和验证的计算机系统模型，以及（3）以正式的系统管理工具的形式方法推进最新技术。该项目的更广泛的意义和重要性是，（1）它直接解决了影响国家计算基础架构的当前和紧急问题，（2）它正在开发系统管理员将能够使用的工具，（3）它将通过发布和将其产品作为开放量的项目进行促进程序验证，从而使该产品范围更轻松地促进了该产品的范围，从而使该产品范围更加轻松地促进了该项目的范围。该项目没有提出全新的抽象，而是系统管理员不熟悉的，而是开发适用于主流系统配置语言的技术，例如木偶，厨师和Ansible。该项目正在开发工具，以验证配置的通用属性和针对复杂系统组件相互作用的特定于配置的特定属性。此外，由于实际系统配置通常调用外部命令，因此该项目还调查了一种模型学习方法以适应它们。 最后，甚至还需要更新经过验证的配置，并且更新引入了新的错误。为了解决此问题，该项目正在开发新的抽象，以使配置更新非常容易。

项目成果

Making High-Performance Robots Safe and Easy to Use for an Introduction to Computing

使高性能机器人安全且易于使用，介绍计算

• 发表时间: 2020
• 期刊: Educational Advances in Artificial Intelligence (EAAI
• 作者: Spitzer, Joseph;Biswas, Joydeep;Guha, Arjun
• 通讯作者: Guha, Arjun

Model-Based Warp Overlapped Tiling for Image Processing Programs on GPUs

GPU 上图像处理程序的基于模型的扭曲重叠平铺

• DOI: 10.1145/3410463.3414649
• 发表时间: 2020
• 期刊: International Conference on Parallel Architectures and Compilation Techniques
• 作者: Jangda, Abhinav;Guha, Arjun
• 通讯作者: Guha, Arjun