Automatic Verification of Conformance of Firewall Configurations to Security Policies

Nihel Ben Youssef 1 Adel Bouhoula 1 Florent Jacquemard 2
1 SUP'COM [TUNIS] - Ecole supérieure des télécommunications de Tunis
2 DAHU - Verification in databases
CNRS - Centre National de la Recherche Scientifique : UMR8643, Inria Saclay - Ile de France, ENS Cachan - École normale supérieure - Cachan, LSV - Laboratoire Spécification et Vérification [Cachan]
Abstract : The configuration of firewalls is highly error prone and automated solution are needed in order to analyze its correctness. We propose a formal and automatic method for checking whether a firewall reacts correctly wrt a security policy given in an high level declarative language. When errors are detected, some feedback is returned to the user in order to correct the firewall configuration. Furthermore, the procedure verifies that no conflicts exist within the security policy. We show that our method is both correct and complete. Finally, it has been implemented in a prototype of verifier based on a satisfiability solver modulo theories (SMT). Experiment conducted on relevant case studies demonstrate the efficiency and scalability of the approach.
Keywords : Security Firewall Configuration Security Policy Formal Verification SMT solver
Document type :
Conference papers
Complete list of metadatas

Cited literature [12 references]  Display  Hide  Download
https://hal.inria.fr/inria-00578926
Contributor : Florent Jacquemard <>
Submitted on : Tuesday, March 22, 2011 - 4:40:49 PM
Last modification on : Thursday, February 7, 2019 - 5:29:23 PM
Long-term archiving on : Thursday, June 23, 2011 - 2:51:42 AM

File

paper8.pdf
Files produced by the author(s)

Identifiers

Collections

INRIA | ENS-CACHAN

Citation

Nihel Ben Youssef, Adel Bouhoula, Florent Jacquemard. Automatic Verification of Conformance of Firewall Configurations to Security Policies. IEEE Symposium on Computers and Communications (ISCC), Jul 2009, Sousse, Tunisia. pp.526-531, ⟨10.1109/ISCC.2009.5202309⟩. ⟨inria-00578926⟩

Export

BibTeX TEI DC DCterms EndNote

Share

Metrics

Record views

229

Files downloads

672

Contact


archive-ouverte@inria.fr