Provably Secure Networks: Methodology and Toolset for Configuration Management
This addresses network security configuration management for administrators, but appears incremental as it builds on existing formal verification methods.
The researchers tackled the problem of network security configuration management by developing two automated, formally verified tools using the Isabelle proof assistant: one for designing networks from scratch and another for analyzing existing iptables configurations, resulting in a combined toolset for uncovering and preventing bugs.
Network administration is an inherently complex task, in particular with regard to security. Using the Isabelle interactive proof assistant, we develop two automated, formally verified tools which help uncovering and preventing bugs in network-level access control configurations. Our first tool guides the process of designing networks from scratch. Our second tool facilitates the analysis of existing iptables configurations. Combined, the two form a powerful toolset.