TY  - GEN
A1  - Lorenz, Claas
A1  - Kiekheben, Sebastian
A1  - Schnor, Bettina
T1  - FaVe: Modeling IPv6 firewalls for fast formal verification
T2  - International Conference on Networked Systems (NetSys) 2017
N2  - As virtualization drives the automation of networking, the validation of security properties becomes more and more challenging eventually ruling out manual inspections. While formal verification in Software Defined Networks is provided by comprehensive tools with high speed reverification capabilities like NetPlumber for instance, the presence of middlebox functionality like firewalls is not considered. Also, they lack the ability to handle dynamic protocol elements like IPv6 extension header chains. In this work, we provide suitable modeling abstractions to enable both - the inclusion of firewalls and dynamic protocol elements. We exemplarily model the Linux ip6tables/netfilter packet filter and also provide abstractions for an application layer gateway. Finally, we present a prototype of our formal verification system FaVe.
Y1  - 2017
U6  - https://doi.org/10.1109/NetSys.2017.7903956
PB  - IEEE
CY  - New York
ER  -