SHF: Small: ConfigV: Automated Verification of Configuration Files

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

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.