Volume 8 - Issue 1
A formal approach for network security policy validation
- Fulvio Valenza
Politecnico di Torino, Dip. di Automatica e Informatica, Torino, Italy, CNR-IEIIT, c.so Duca degli Abruzzi 24, Torino I-10129, Italy, CNR-IEIIT, c.so Duca degli Abruzzi 24, Torino I-10129, Italy
fulvio.valenza@polito.it
- Tao Su
Politecnico di Torino, Dip. di Automatica e Informatica, Torino, Italy, CNR-IEIIT, c.so Duca degli Abruzzi 24, Torino I-10129, Italy
tao.su@polito.it
- Serena Spinoso
Politecnico di Torino, Dip. di Automatica e Informatica, Torino, Italy, CNR-IEIIT, c.so Duca degli Abruzzi 24, Torino I-10129, Italy
serena.spinoso@polito.it
- Antonio Lioy
Politecnico di Torino, Dip. di Automatica e Informatica, Torino, Italy, CNR-IEIIT, c.so Duca degli Abruzzi 24, Torino I-10129, Italy
antonio.lioy@polito.it
- Riccardo Sisto
Politecnico di Torino, Dip. di Automatica e Informatica, Torino, Italy, CNR-IEIIT, c.so Duca degli Abruzzi 24, Torino I-10129, Italy
riccardo.sisto@polito.it
- Marco Vallini
Politecnico di Torino, Dip. di Automatica e Informatica, Torino, Italy, CNR-IEIIT, c.so Duca degli Abruzzi 24, Torino I-10129, Italy
marco.vallini@polito.it
Keywords: network security policy, policy conflict analysis, policy validation, remote attestation.
Abstract
Network security is a crucial aspect for administrators due to increasing network size and number
of functions and controls (e.g. firewall, DPI, parental control). Errors in configuring security controls
may result in serious security breaches and vulnerabilities (e.g. blocking legitimate traffic or
permitting unwanted traffic) that must be absolutely detected and addressed. This work proposes a
novel approach for validating network policy enforcement, by checking the network status and configuration,
and detection of the possible causes in case of misconfiguration or software attacks. Our
contribution exploits formal methods to model and validate the packet processing and forwarding
behaviour of security controls, and to validate the trustworthiness of the controls by using remote
attestation. A prototype implementation of this approach is proposed to validate different scenarios.