Demonstrating topoS: Theorem-Prover-Based Synthesis of Secure Network Configurations
Networking and Internet Architecture
2016-04-04 v1 Cryptography and Security
Software Engineering
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.
Cite
@article{arxiv.1604.00273,
title = {Demonstrating topoS: Theorem-Prover-Based Synthesis of Secure Network Configurations},
author = {Cornelius Diekmann and Andreas Korsten and Georg Carle},
journal= {arXiv preprint arXiv:1604.00273},
year = {2016}
}
Comments
In 2nd International Workshop on Management of SDN and NFV Systems, manSDN/NFV, Barcelona, Spain, November 2015