FaVe: Modeling IPv6 firewalls for fast formal verification
- 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.
| Author details: | Claas LorenzORCiD, Sebastian Kiekheben, Bettina SchnorORCiDGND |
|---|---|
| DOI: | https://doi.org/10.1109/NetSys.2017.7903956 |
| Title of parent work (English): | International Conference on Networked Systems (NetSys) 2017 |
| Publisher: | IEEE |
| Place of publishing: | New York |
| Publication type: | Other |
| Language: | English |
| Date of first publication: | 2017/04/24 |
| Publication year: | 2017 |
| Release date: | 2022/11/18 |
| Article number: | 16836488 |
| Number of pages: | 8 |
| Organizational units: | An-Institute / Hasso-Plattner-Institut für Digital Engineering gGmbH |
| DDC classification: | 0 Informatik, Informationswissenschaft, allgemeine Werke / 00 Informatik, Wissen, Systeme |
| Peer review: | Referiert |
