Demonstrating topoS: Theorem-Prover-Based Synthesis of Secure Network Configurations
This addresses security breaches in network management by automating configuration synthesis, though it appears incremental as it builds on existing theorem-proving methods.
The authors tackled the problem of human error in network security by developing topoS, a tool that automatically synthesizes low-level network configurations from high-level security goals, with formal verification in Isabelle/HOL to prevent implementation errors.
In network management, when it comes to security breaches, human error constitutes a dominant factor. We present our tool topoS which automatically synthesizes low-level network configurations from high-level security goals. The automation and a feedback loop help to prevent human errors. Except for a last serialization step, topoS is formally verified with Isabelle/HOL, which prevents implementation errors. In a case study, we demonstrate topoS by example. For the first time, the complete transition from high-level security goals to both firewall and SDN configurations is presented.