Abstract
We present a formal model of network protocols and their application
to modeling firewall policies. The formalization is based on the
Unified Policy Framework (UPF). The formalization was originally
developed with for generating test cases for testing the security
configuration actual firewall and router (middle-boxes) using
HOL-TestGen. Our work focuses on modeling application level protocols
on top of tcp/ip.
License
Topics
Session UPF_Firewall
- NetworkCore
- DatatypeAddress
- DatatypePort
- IntegerAddress
- IntegerPort
- IntegerPort_TCPUDP
- IPv4
- IPv4_TCPUDP
- NetworkModels
- PolicyCore
- PolicyCombinators
- PortCombinators
- ProtocolPortCombinators
- Ports
- PacketFilter
- NAT
- FWNormalisationCore
- NormalisationGenericProofs
- NormalisationIntegerPortProof
- NormalisationIPPProofs
- ElementaryRules
- FWNormalisation
- LTL_alike
- StatefulCore
- FTP
- FTP_WithPolicy
- VOIP
- FTPVOIP
- StatefulFW
- UPF-Firewall
- DMZDatatype
- DMZInteger
- DMZ
- Voice_over_IP
- Transformation01
- Transformation02
- Transformation
- NAT-FW
- PersonalFirewallInt
- PersonalFirewallIpv4
- PersonalFirewallDatatype
- PersonalFirewall
- Examples