Formal integrated network security analysis tool: formal query‐based network security configuration analysis. Issue 2 (1st March 2015)

• Record Type: Journal Article
• Authors: Maity, Soumya; Bera, P.; Ghosh, Soumya K.; Al‐Shaer, Ehab
• Is Part Of: IET networks. Volume 4:Issue 2(2015)
• Page Start: 137
• Page End: 147
• Publication Date: 2015-03-01
• Subjects: computer network security -- query processing -- computational complexity -- telecommunication network topology -- protocols -- authorisation -- computability -- data mining -- graph theory; graph mining procedures -- static access queries -- complex service access queries -- fault‐based queries -- SAT‐based decision procedures -- Boolean satisflability -- query‐based formal security analysis tool -- hidden access paths -- ACL conflgurations -- access control lists -- network devices -- protocol -- trafflc source -- security policy -- organisational security policies -- security measures -- enterprise networks -- heterogeneous network services -- large topology -- network conflgurations complexity -- formal query‐based network security configuration analysis -- formal integrated network security analysis tool; Computer network architectures -- Periodicals; Computer network protocols -- Periodicals; Information networks -- Periodicals; Telecommunication systems -- Periodicals; 004.605
• DOI: 10.1049/iet-net.2013.0090
• Languages: English
• ISSNs: 2047-4954

Abstract

Abstract : Owing to increasing complexity of network configurations with large topology and use of heterogeneous network services, enterprise networks deploy various security measures based on the organisational security policies. Typically, security policy represents the high level requirements for controlling the resource accesses by traffic source, destination, protocol, access time and so on. Security policies are implemented in the network devices (routers, firewalls and so on) in a distributed fashion through various access control lists (ACLs). The ACL configurations may contain different level of inconsistencies which may make the network vulnerable. In addition, there may exist inconsistent 'hidden access paths' in the implementation because of transitive access relationships between the network services. Further, the failure of network link(s) may form alternative routing paths that violate ACL. Manual analysis of this problem can be overwhelming and potentially inaccurate. In this study, a query‐based formal security analysis tool has been presented that automates the process using Boolean satisfiability (SAT). The tool allows network administrators to systematically evaluate the distributed ACL configurations through various standard and complex service access queries. The tool evaluates the static access queries through SAT‐based decision procedures, and the fault‐based queries (under network link failures) through graph mining procedures.