Provably Secure Networks: Methodology and Toolset for Configuration Management

TL;DR

This paper presents a methodology and toolset using formal verification with Isabelle to improve security configuration management in networks, aiding both design and analysis of access controls.

Contribution

It introduces two automated, formally verified tools for network configuration, one for designing networks and another for analyzing iptables rules, enhancing security reliability.

Findings

Tools successfully identify configuration bugs

Formal verification improves network security assurance

Automated guidance streamlines network design and analysis

Abstract

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.