Towards a Formal Data Flow Oriented Model for Network Security Policies Analysis

Network security policy enforcement consists in configuring heterogeneous security mechanisms (IPsec gateways, ACLs on routers, stateful firewalls, proxies, etc) that are available in a given network environment. The complexity of this task resides in the number, the nature, and the interdependence of the mechanisms to consider. Although several researchers have proposed different analysis tools, achieving this task requires experienced and proficient security administrators who can handle all these parameters today. We propose in the article a mathematical data flow oriented modelling approach in order to detect inconsistencies between security mechanisms. Our model is independent from specific security mechanisms to admit of their diversity, and also future security mechanisms not yet available. In addition, it allows fine-grained inconsistency analysis.