Firewalls are a fundamental tool for managing and protecting computer networks. They behave according to a configuration that specifies the desired policy, i.e., which packets are allowed to enter a network, possibly with modified addresses. Several tools allow the user to specify policies in various high level languages, and to compile them into different target configuration languages, as well as to automatically migrate a configuration from a system to another. Often, these tools implicitly assume that the target system can enforce any desired policy. Unexpectedly, we find that this is not always the case. In particular, we show that the most common UNIX firewall systems, i.e., iptables, ipfw, pf, are not equally expressive, in that some policies can be implemented in one system but not in another. Here, we formally investigate the expressive power of these firewall systems using techniques from programming language semantics, and set up a formal model to precisely characterize their relationships. Based on this formal model we then present F2F, a prototypical tool that predicts when a policy cannot be expressed in a given system. Our prototype gives detailed information about the unexpressible parts of a policy and provides administrators with hints for fixing the detected problems.

Can my Firewall System Enforce this Policy?

Pierpaolo Degano;Letterio Galletta
2022

Abstract

Firewalls are a fundamental tool for managing and protecting computer networks. They behave according to a configuration that specifies the desired policy, i.e., which packets are allowed to enter a network, possibly with modified addresses. Several tools allow the user to specify policies in various high level languages, and to compile them into different target configuration languages, as well as to automatically migrate a configuration from a system to another. Often, these tools implicitly assume that the target system can enforce any desired policy. Unexpectedly, we find that this is not always the case. In particular, we show that the most common UNIX firewall systems, i.e., iptables, ipfw, pf, are not equally expressive, in that some policies can be implemented in one system but not in another. Here, we formally investigate the expressive power of these firewall systems using techniques from programming language semantics, and set up a formal model to precisely characterize their relationships. Based on this formal model we then present F2F, a prototypical tool that predicts when a policy cannot be expressed in a given system. Our prototype gives detailed information about the unexpressible parts of a policy and provides administrators with hints for fixing the detected problems.
Formal security models, Language-based security, Configuration languages, Semantics of firewalls, Automatic analysis of firewalls
File in questo prodotto:
File Dimensione Formato  
download.pdf

accesso aperto

Tipologia: Documento in Pre-print
Licenza: Creative commons
Dimensione 324.44 kB
Formato Adobe PDF
324.44 kB Adobe PDF Visualizza/Apri
1-s2.0-S0167404822000815-main.pdf

non disponibili

Tipologia: Versione Editoriale (PDF)
Licenza: Nessuna licenza
Dimensione 3.03 MB
Formato Adobe PDF
3.03 MB Adobe PDF   Visualizza/Apri   Richiedi una copia

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: http://hdl.handle.net/20.500.11771/21038
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 0
social impact