Abstract
Systems and networks access control configuration are usually analyzed independently although they are logically combined to define 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 to 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. In this paper, we introduce a cross-layer modeling and verification system that can analyze 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 allows analyzing, for example, firewall polices in the context of application access control and vice versa providing 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 configuration, 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.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Al-Shaer, E., Hamed, H.: Discovery of policy anomalies in distributed firewalls. In: Proceedings of IEEE INFOCOM’04, Hong Kong (2004)
Al-Shaer, E., Hamed, H.: Taxonomy of conflicts in network security policies. IEEE Commun. Mag. 44(3), 134–141 (2006)
Al-Shaer, E., Marrero, W., El-Atawy, A., Elbadawi, K.: Network configuration in a box: towards end-to-end verification of network reachability and security. In: ICNP, Princeton, pp. 123–132 (2009)
Alimi, R., Wang, Y., Yang, Y.R.: Shadow configuration as a network management primitive. In: SIGCOMM’08: Proceedings of the ACM SIGCOMM 2008 Conference on Data Communication, Seattle, pp. 111–122. ACM, New York (2008)
Ballani, H., Francis, P.: Conman: a step towards network manageability. SIGCOMM Comput. Commun. Rev. 37(4), 205–216 (2007)
Bartal, Y., Mayer, A., Nissim, K., Wool, A.: Firmato: a novel firewall management toolkit. ACM Trans. Comput. Syst. 22(4), 381–420 (2004)
Burch, J., Clarke, E., McMillan, K., Dill, D., Hwang, J.: Symbolic model checking: 1020 states and beyond. J. Inf. Comput. 98(2), 1–33 (1992)
Bush, R., Griffin, T.: Integrity for virtual private routed networks. In: Proceedings of IEEE INFOCOM’03, San Franciso, vol. 2, pp. 1467–1476 (2003)
Feamster, N., Balakrishnan, H.: Detecting BGP configuration faults with static analysis. In: NSDI, Boston (2005)
Fu, Z., Wu, F., Huang, H., Loh, K., Gong, F., Baldine, I., Xu, C.: IPSec/VPN security policy: correctness, conflict detection and resolution. In: Policy’01 Workshop, Bristol, pp. 39–56 (2001)
Griffin, T.G., Wilfong, G.: On the correctness of IBGP configuration. In: SIGCOMM’02: Proceedings of the ACM SIGCOMM 2002 Conference on Data Communication, Pittsburgh, pp. 17–29 (2002)
Guttman, J.: Filtering posture: local enforcement for global policies. In: IEEE Symposium on Security and Privacy, Oakland, pp. 120–129 (1997)
Hamed, H., Al-Shaer, E., Marrero, W.: Modeling and verification of IPSec and VPN security policies. In: IEEE International Conference of Network Protocols (ICNP’05), Boston (2005)
Hinrichs, S.: Policy-based management: bridging the gap. In: 15th Annual Computer Security Applications Conference (ACSAC’99), Phoenix, pp. 209–218 (1999)
Ioannidis, S., Keromytis, A., Bellovin, S., Smith, J.: Implementing a distributed firewall. In: 7th ACM Conference on Computer and Comminications Security (CCS’00), Athens, pp. 190–199 (2000)
Luck, I., Schafer, C., Krumm, H.: Model-based tool assistance for packet-filter design. In: IEEE Workshop on Policies for Distributed Systems and Networks (POLICY’01), Bristol, pp. 120–136 (2001)
Mahajan, R., Wetherall, D., Anderson, T.: Understanding BGP misconfiguration. In: SIGCOMM’02: Proceedings of the ACM SIGCOMM 2002 Conference on Data Communications, Pittsburgh, pp. 3–16. ACM, New York (2002)
Mai, H., Khurshid, A., Agarwal, R., Caesar, M., Godfrey, P.B., King, S.T.: Debugging the data plane with anteater. SIGCOMM Comput. Commun. Rev. 41(4), 290–301 (2011)
Mayer, A., Wool, A., Ziskind, E.: Fang: a firewall analysis engine. In: IEEE Symposium on Security and Privacy (SSP’00), Berkeley, pp. 177–187 (2000)
Narain, S.: Network configuration management via model finding. In: LISA, San Diego, pp. 155–168 (2005)
Wool, A.: A quantitative study of firewall configuration errors. IEEE Comput. 37(6), 62–67 (2004)
Xie, G.G., Zhan, J., Maltz, D.A., Zhang, H., Greenberg, A., Hjalmtysson, G., Rexford, J.: On static reachability analysis of IP networks. In: IEEE INFOCOM, Miami, vol. 3, pp. 2170–2183 (2005)
Yang, Y., Martel, C.U., Wu, S.F.: On building the minimum number of tunnels: an ordered-split approach to manage ipsec/vpn tunnels. In: 9th IEEE/IFIP Network Operation and Management Symposium (NOMS’04), Seoul, pp. 277–290, (2004)
Yuan, L., Mai, J., Su, Z., Chen, H., Chuah, C., Mohapatra, P.: FIREMAN: a toolkit for firewall modeling and analysis. In: IEEE Symposium on Security and Privacy (SSP’06), Berkeley/Oakland (2006)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer International Publishing Switzerland
About this chapter
Cite this chapter
Alsaleh, M.N., Al-Shaer, E., El-Atawy, A. (2013). Towards a Unified Modeling and Verification of Network and System Security Configurations. In: Al-Shaer, E., Ou, X., Xie, G. (eds) Automated Security Management. Springer, Cham. https://doi.org/10.1007/978-3-319-01433-3_1
Download citation
DOI: https://doi.org/10.1007/978-3-319-01433-3_1
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-01432-6
Online ISBN: 978-3-319-01433-3
eBook Packages: Computer ScienceComputer Science (R0)