Demonstrating topoS: Theorem-Prover-Based Synthesis of Secure Network Configurations

TL;DR

This paper introduces topoS, a formally verified tool that automatically synthesizes secure network configurations from high-level security goals, reducing human errors in network management.

Contribution

The paper presents topoS, a novel tool that automates the synthesis of network configurations from security goals with formal verification, covering both firewall and SDN setups.

Findings

Successfully demonstrated complete transition from high-level goals to configurations

Formal verification with Isabelle/HOL ensures implementation correctness

First case study showing end-to-end synthesis from goals to configurations

Abstract

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.