Automata-Based Bottom-Up Design of Conflict-Free Security Policies Specified as Policy Expressions

  • Ahmed KhoumsiEmail author
  • Mohammed Erradi
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11028)


Security policies (or more briefly: policies) are used to filter accesses to computing resources. A policy is usually specified by a table of rules, where each rule specifies conditions to accept or reject an access request. Since the acceptance of malicious requests or the rejection of legitimate requests may lead to serious consequences, the correct design of policies is very important. The present paper is inspired by two works: the first one uses an automata-based method to design policies, while the second one suggests a bottom-up design method of policies specified as policy expressions. A policy expression looks like a boolean expression, where policies are composed using three operators: \(\lnot \), \(\wedge \), \(\vee \). In this paper, we generalize the automata-based method for the bottom-up design of policies specified as policy expressions. In our context, designing a policy specified as a policy expression \( PE \) amounts to constructing an automaton \(\varGamma _{ PE }\) that models the access control specified in \( PE \). To respect the essence of bottom-up design, the automaton \(\varGamma _{ PE }\) is constructed incrementally, by first constructing the automata that model the basic policies that compose \( PE \), and then constructing incrementally the automata that model the subexpressions that compose \( PE \), until we obtain \(\varGamma _{ PE }\). Then we show how to use \(\varGamma _{ PE }\) to determine whether \( PE \) verifies several properties, namely adequacy, implication, and equivalence. Also, we study the problem of conflicting rules, i.e. policy rules that do not agree on whether some request must be accepted or rejected. We show that our bottom-up design supports any strategy of conflict resolution.


  1. 1.
    Acharya, H., Joshi, A., Gouda, M.: Firewall modules and modular firewalls. In: IEEE International Conference on Network Protocols (ICNP), pp. 174–182 (2010)Google Scholar
  2. 2.
    Acharya, H.B., Gouda, M.G.: Projection and division: linear space verification of firewalls. In: 30th IEEE International Conference on Distributed Computing Systems (ICDCS), Genova, Italy, pp. 736–743, June 2010Google Scholar
  3. 3.
    Acharya, H.B., Gouda, M.G.: Firewall verification and redundancy checking are equivalent. In: 30th IEEE International Conference on Computer Communication (INFOCOM), Shanghai, China, pp. 2123–2128, April 2011Google Scholar
  4. 4.
    Al-Shaer, E., Hamed, H.: Modeling and management of firewall policies. IEEE Trans. Netw. Serv. Manag. 1(1), 2–10 (2004)CrossRefGoogle Scholar
  5. 5.
    Al-Shaer, E., Marrero, W., El-Atawy, A., Elbadawi, K.: Network configuration in a box: towards end-to-end verification of networks reachability and security. In: 17th IEEE International Conference on Network Protocols (ICNP), Princeton, NJ, USA, pp. 736–743, October 2009Google Scholar
  6. 6.
    Cuppens, F., Cuppens-Boulahia, N., Garcia-Alfaro, J., Moataz, T., Rimasson, X.: Handling stateful firewall anomalies. In: Gritzalis, D., Furnell, S., Theoharidou, M. (eds.) SEC 2012. IAICT, vol. 376, pp. 174–186. Springer, Heidelberg (2012). Scholar
  7. 7.
    Elmallah, E.S., Gouda, M.G.: Hardness of firewall analysis. In: Noubir, G., Raynal, M. (eds.) NETYS 2014. LNCS, vol. 8593, pp. 153–168. Springer, Cham (2014). Scholar
  8. 8.
    Garcia-Alfaro, J., Cuppens, F., Cuppens-Boulahia, N.: Complete analysis of configuration rules to guarantee reliable network security policies. Int. J. Inf. Secur. 7(2), 103–122 (2008)CrossRefGoogle Scholar
  9. 9.
    Garcia-Alfaro, J., Cuppens, F., Cuppens-Boulahia, N., Perez, S.M., Cabot, J.: Management of stateful firewall misconfiguration. Comput. Secur. 39, 64–85 (2013)CrossRefGoogle Scholar
  10. 10.
    Hoffman, D., Yoo, K.: Blowtorch: a framework for firewall test automation. In: Proceedings of the 20th IEEE/ACM International Conference on Automated Software Engineering (ASE), Long Beach, California, USA, pp. 96–103, November 2005Google Scholar
  11. 11.
    El Kalam, A.A., et al.: Organization based access control. In: IEEE 4th International Workshop on Policies for Distributed Systems and Networks (POLICY), Lake Come, Italy, June 2003Google Scholar
  12. 12.
    Kamara, S., Fahmy, S., Schultz, E., Kerschbaum, F., Frantzen, M.: Analysis of vulnerabilities in internet firewalls. Comput. Secur. 22(3), 214–232 (2003)CrossRefGoogle Scholar
  13. 13.
    Karoui, K., Ftima, F.B., Ghezala, H.B.: Formal specification, verification and correction of security policies based on the decision tree approach. Int. J. Data Netw. Secur. 3(3), 92–111 (2013)Google Scholar
  14. 14.
    Khoumsi, A., Erradi, M., Krombi, W.: A formal basis for the design and analysis of firewall security policies. J. King Saud Univ.-Comput. Inf. Sci. 30(1), 51–66 (2018)Google Scholar
  15. 15.
    Khoumsi, A., Krombi, W., Erradi, M.: A formal approach to verify completeness and detect anomalies in firewall security policies. In: Cuppens, F., Garcia-Alfaro, J., Zincir Heywood, N., Fong, P. (eds.) FPS 2014. LNCS, vol. 8930, pp. 221–236. Springer, Cham (2015). Scholar
  16. 16.
    Krombi, W., Erradi, M., Khoumsi, A.: Automata-based approach to design and analyze security policies. In: International Conference on Privacy, Security and Trust (PST), Toronto, Canada, July 2014Google Scholar
  17. 17.
    Lee, D., Yannakakis, M.: Principles and methods of testing finite state machines - a survey. Proc. IEEE 84, 1090–1126 (1996)CrossRefGoogle Scholar
  18. 18.
    Liu, A., Gouda, M.: Diverse firewall design. IEEE Trans. Parallel Distrib. Syst. 19(9), 1237–1251 (2008)CrossRefGoogle Scholar
  19. 19.
    Liu, A., Gouda, M.: Complete redundancy removal for packet classifiers in TCAMs. IEEE Trans. Parallel Distrib. Syst. 21(4), 424–437 (2010)CrossRefGoogle Scholar
  20. 20.
    Liu, A.X., Gouda, M.G.: Structured firewall design. Comput. Netw.: Int. J. Comput. Telecommun. Netw. 51(4), 1106–1120 (2007)CrossRefGoogle Scholar
  21. 21.
    Madhuri, M., Rajesh, K.: Systematic detection and resolution of firewall policy anomalies. Int. J. Res. Comput. Commun. Technol. (IJRCCT) 2(12), 1387–1392 (2013)Google Scholar
  22. 22.
    Mallouli, W., Orset, J., Cavalli, A., Cuppens, N., Cuppens, F.: A formal approach for testing security rules. In: 12th ACM Symposium on Access Control Models and Technologies (SACMAT), Sophia Antipolis, France, June 2007Google Scholar
  23. 23.
    Mansmann, F., Göbel, T., Cheswick, W.: Visual analysis of complex firewall configurations. In: 9th International Symposium on Visualization for Cyber Security (VizSec), pp. 1–8, Seattle, WA, USA, October 2012Google Scholar
  24. 24.
    Mayer, A., Wool, A., Ziskind, E.: Fang: a firewall analysis engine. In: Proceedings of the IEEE Symposium on Security and Privacy, pp. 177–187, Berkeley, California, USA, May 2000Google Scholar
  25. 25.
    Pozo, S., Gasca, R., Reina-Quintero, A., Varela-Vaca, A.: CONFIDDENT: a model-driven consistent and non-redundant layer-3 firewall ACL design, development and maintenance framework. J. Syst. Softw. 85(2), 425–457 (2012)CrossRefGoogle Scholar
  26. 26.
    Reaz, R., Acharya, H.B., Elmallah, E.S., Cobb, J.A., Gouda, M.G.: Policy expressions and the bottom-up design of computing policies. In: El Abbadi, A., Garbinato, B. (eds.) NETYS 2017. LNCS, vol. 10299, pp. 151–165. Springer, Cham (2017). Scholar
  27. 27.
    Reaz, R., Ali, M., Gouda, M.G., Heule, M.J.H., Elmallah, E.S.: The implication problem of computing policies. In: Pelc, A., Schwarzmann, A.A. (eds.) SSS 2015. LNCS, vol. 9212, pp. 109–123. Springer, Cham (2015). Scholar
  28. 28.
    Wool, A.: A quantitative study of firewall configuration errors. Computer 37(6), 62–67 (2004)CrossRefGoogle Scholar
  29. 29.
    Yuan, L., Mai, J., Su, Z., Chen, H., Chuah, C.-N., Mohapatra, P.: FIREMAN: a toolkit for firewall modeling and analysis. In: IEEE Symposium on Security and Privacy (S&P), Berkeley/Oakland, CA, USA, May 2006Google Scholar

Copyright information

© Springer Nature Switzerland AG 2019

Authors and Affiliations

  1. 1.Department of Electrical and Computer EngineeringUniversity of SherbrookeSherbrookeCanada
  2. 2.ENSIAS, University Mohammed V in RabatRabatMorocco

Personalised recommendations