权益分类	功能权益	普通用户	{{item.name}}会员
{{category.name}}	{{benefitItem.name}}

SHF: Small: ConfigV: Automated Verification of Configuration Files

SHF：小：ConfigV：配置文件自动验证

基本信息

批准号：
1715387
负责人：
Ruzica Piskac
金额：
$ 45万
依托单位：
Yale University
依托单位国家：
美国
项目类别：
Standard Grant
财政年份：
2017
资助国家：
美国
起止时间：
2017-09-01 至 2021-08-31
项目状态：
已结题

来源：
https://www.nsf.gov/awardsearch/showAward?AWD_ID=1715387&HistoricalAwards=false
关键词：
SHF Small ConfigV Automated Verification

项目摘要

Configuration files allow programmers to easily control many key software settings, but this variety of settings creates a large surface for potential errors, with impacts as severe as performance degradation or system-wide failure. These configuration errors have affected many software-based services, from social networking to emergency dispatch call systems. The fundamental issue this project addresses is the need to detect these errors, before they are released in production, by automatically checking configuration files against a set of rules that describe safe configurations. Since there are many different types of configuration languages, all with too many complex rules to be manually written, configuration file verification must automatically learn rules from existing examples of configuration files. This project will have broader impact in the field, expanding the verification beyond just traditional programs, and allowing for ensuring the safety of both configuration files and other complex and unstructured objects.The goal of this proposal is to develop a fully automated verification framework for general software configurations. To do this, the user must provide a set of example configuration files, from which we learn rules that describe various properties that hold on the given example set. These rules, in general, specify which properties the keywords in a configuration file need to satisfy. A key challenge in the process of inferring such a specification is that configuration files are generally an untyped, unstructured sequence of assignments - making the application of existing formal methods approaches difficult. To add structure to these files, the PI uses a probabilistic type inference algorithm to assign each keyword a type. The learning process then relies on matching the inferred types to a set of very general templates, which describe the keywords and their relations. This project further extends the areas where formal verification can be applied and develops a tool set for configuration file verification that can increase the productivity of software practitioners.

配置文件允许程序员轻松控制许多关键的软件设置，但这些设置为潜在的错误创建了一个大的表面，其影响严重到性能下降或系统范围的故障。这些配置错误影响了许多基于软件的服务，从社交网络到紧急调度呼叫系统。该项目解决的基本问题是需要在这些错误发布到生产环境之前检测它们，方法是根据一组描述安全配置的规则自动检查配置文件。由于有许多不同类型的配置语言，都有太多复杂的规则需要手动编写，因此配置文件验证必须从现有的配置文件示例中自动学习规则。该项目将在该领域产生更广泛的影响，将验证扩展到传统程序之外，并允许确保配置文件和其他复杂和非结构化对象的安全性。要做到这一点，用户必须提供一组示例配置文件，我们可以从中学习描述给定示例集上的各种属性的规则。这些规则通常指定配置文件中的关键字需要满足哪些属性。在推断这样的规范的过程中的一个关键挑战是，配置文件通常是一个无类型的，非结构化的序列分配-使现有的正式方法的应用程序的方法困难。为了给这些文件添加结构，PI使用概率类型推断算法为每个关键字分配一个类型。然后，学习过程依赖于将推断出的类型与一组非常通用的模板进行匹配，这些模板描述了关键字及其关系。该项目进一步扩展了形式验证的应用领域，并开发了一套用于配置文件验证的工具，可以提高软件从业人员的生产力。

项目成果

期刊论文数量（11）

专著数量（0）

科研奖励数量（0）

会议论文数量（0）

专利数量（0）

Automated repair by example for firewalls

防火墙自动修复示例

DOI：
10.1007/s10703-020-00346-0
发表时间：
2020
期刊：
Formal Methods in System Design
影响因子：
0.8
作者：
Hallahan, William T.;Zhai, Ennan;Piskac, Ruzica
通讯作者：
Piskac, Ruzica

Software Engineering for Infrastructure and Configuration (SEConfig) - Workshop Report

基础设施和配置软件工程 (SEConfig) - 研讨会报告

DOI：
10.1145/3385678.3385686
发表时间：
2020
期刊：
ACM SIGSOFT Software Engineering Notes
影响因子：
0
作者：
Cito, Jürgen;Santolucito, Mark
通讯作者：
Santolucito, Mark

Programming-by-example for audio: synthesizing digital signal processing programs

音频编程示例：合成数字信号处理程序

DOI：
10.1145/3242903.3242906
发表时间：
2018
期刊：
and Design
影响因子：
0
作者：
Santolucito, Mark;Rogers, Kate;Lombardo, Aedan;Piskac, Ruzica
通讯作者：
Piskac, Ruzica

Static detection of silent misconfigurations with deep interaction analysis

DOI：
10.1145/3485517
发表时间：
2021-10
期刊：
Proceedings of the ACM on Programming Languages
影响因子：
0
作者：
Jialu Zhang;R. Piskac;Ennan Zhai;Tianyin Xu
通讯作者：
Jialu Zhang;R. Piskac;Ennan Zhai;Tianyin Xu

Towards checkpoint placement for dynamic memory allocation in intermittent computing

间歇性计算中动态内存分配的检查点放置

DOI：
10.1145/3427764.3428323
发表时间：
2020
期刊：
TAPAS 2020: Proceedings of the 11th ACM SIGPLAN International Workshop on Tools for Automatic Program Analysis
影响因子：
0
作者：
Shoemaker, Nicholas;Piskac, Ruzica;Santolucito, Mark
通讯作者：
Santolucito, Mark