SHF: Small: ConfigV: Automated Verification of Configuration Files

点击翻译按钮获取中文摘要

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.