| Title | Automated Verification of Security Chains in Software-Defined Networks with Synaptic |
| Publication Type | Conference Paper |
| Year of Publication | 2017 |
| Authors | Schnepf, N., Badonnel, R., Lahmadi, A., Merz, S. |
| Conference Name | 2017 IEEE Conference on Network Softwarization (NetSoft) |
| Keywords | automated verification, cloud computing, composability, Computer languages, computer network security, control systems, CVC4, data leakage prevention, dynamic networks, firewalls, formal models, formal specification, formal verification, Frenetic family, infrastructure protection, Intrusion Detection Systems, Metrics, Middleboxes, model checking, nuXmv checkers, pubcrawl, resilience, Resiliency, SDN programming languages, security, security chain verification, security chains, security functions, security management, smart devices, SMT, software defined networking, software-defined networking, Software-Defined Networks, specification translation, Synaptic, veriT |
| Abstract | Software-defined networks provide new facilities for deploying security mechanisms dynamically. In particular, it is possible to build and adjust security chains to protect the infrastructures, by combining different security functions, such as firewalls, intrusion detection systems and services for preventing data leakage. It is important to ensure that these security chains, in view of their complexity and dynamics, are consistent and do not include security violations. We propose in this paper an automated strategy for supporting the verification of security chains in software-defined networks. It relies on an architecture integrating formal verification methods for checking both the control and data planes of these chains, before their deployment. We describe algorithms for translating specifications of security chains into formal models that can then be verified by SMT1 solving or model checking. Our solution is prototyped as a package, named Synaptic, built as an extension of the Frenetic family of SDN programming languages. The performances of our approach are evaluated through extensive experimentations based on the CVC4, veriT, and nuXmv checkers. |
| DOI | 10.1109/NETSOFT.2017.8004195 |
| Citation Key | schnepf_automated_2017 |
Automated Verification of Security Chains in Software-Defined Networks with Synaptic