Towards A Unified Modeling and Verification of Network and System Security Configuration
Abstract
Systems and networks access control configuration are usually analyzed independently although they are logically combined to define the the end-to-end security property. While systems and applications security policies define access control based on user identity or group, request type and the requested resource, network security policies uses flow information such as host and service addresses for source and destination to define access control. Therefore, both network and systems access control have to be configured consistently in order enforce end-to-end security policies. Many previous research attempt to verify either side separately, but it does not provide a unified approach to automatically validate the logical consistency between both of them. Thus, using existing techniques requires error-prone manual and ad-hoc analysis to validate this link.In this paper, we introduce a cross-layer modeling and verification system that can analyzes the configurations and policies across both application and network components as a single unit. It combines policies from different devices as firewalls, NAT, routers and IPSec gateways as well as basic RBAC-based policies of higher service layers. This will allow analyzing, for example, firewall polices in the context of application access control and vice versa. Thus, by incorporating policies across the network and over multiple layers, we provide a true end-to-end configuration verification tool. Our model represents the system as a state machine where packet header, service request and location determine the state and transitions that conform with the configurations, device operations, and packet values are established. We encode the model as Boolean functions using binary decision diagrams (BDDs). We used an extended version of computational tree logic (CTL) to provide more useful operators and then use it with symbolic model checking to prove or find counter examples to needed properties. The tool is implemented and we gave special consideration to efficiency and scalability. Our extensive evaluation study shows acceptable computation and space requirements with large number of nodes and configuration sizes.
Research Areas
