Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top
Published in:
Towards Customizable CPS: Composability, Efficiency and Predictability Read chapter Read first chapter

2017 | OriginalPaper | Chapter

Inconsistency Analysis of Time-Based Security Policy and Firewall Policy

Authors : Yi Yin, Yuichiro Tateiwa, Yun Wang, Yoshiaki Katayama, Naohisa Takahashi

Published in: Formal Methods and Software Engineering

Publisher: Springer International Publishing

Log in

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

Packet filtering in firewall either accepts or denies packets based upon a set of predefined rules called firewall policy. In recent years, time-based firewall policies are widely used in many firewalls such as CISCO ACLs. Firewall policy is always designed under the instruction of security policy, which is a generic document that outlines the needs for network access permissions. It is difficult to maintain the consistency of normal firewall policy and security policy, not to mention time-based firewall policy and security policy. Even though there are many analysis methods for security policy and firewall policy, they cannot deal with time constraint. To resolve this problem, we firstly represent time-based security policy and firewall policy as logical formulas, and then use satisfiability modulo theories (SMT) solver Z3 to verify them and analyze inconsistency. We have implemented a prototype system to verify our proposed method, experimental results showed the effectiveness.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

inform now
previous chapter Learning Types for Binaries
next chapter An Algebraic Approach to Automatic Reasoning for NetKAT Based on Its Operational Semantics
Literature
1.
2.
3.
Yin, Y., Xu, X., Katayama, Y., Takahashi, N.: Inconsistency detection system for security policy and rewall policy. In: 2010 First International Conference on Networking and Computing, pp. 294–297. IEEE (2011)
4.
Yin, Y., Xu, J., Takahashi, N.: Verifying consistency between security policy and firewall policy by using a constraint satisfaction problem server. In: Zhang, Y. (ed.) Future Wireless Networks and Information Systems. LNEE, vol. 144, pp. 135–145. Springer, Heidelberg (2012). doi:10.​1007/​978-3-642-27326-1_​18
5.
6.
Thanasegaran, S., Tateiwa, Y., Katayama, Y., Takahashi, N.: Design and implementation of conflict detection system for time-based firewall policies. J. Next Gener. Inf. Technol. 2(4), 24–39 (2011)CrossRef
7.
8.
Moura, L.D., Bjørner, N.: Z3: an efficient SMT solver. In: Proceedings of the Theory and practice of software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pp. 337–340 (2008)
9.
10.
Wool, A.: Trends in firewall configuration errors: measuring the holes in swiss cheese. IEEE Internet Comput. 14(4), 58–65 (2010)CrossRef
11.
Al-Shaer, E.: Automated Firewall Analytics Design, Configuration and Optimization. Springer, Heidelberg (2014)
12.
Hu, H., Ahn, G., Kulkarni, K.: Detecting and resolving firewall policy anomalies. IEEE Trans. Secure Comput. 9(3), 318–331 (2012)CrossRef
13.
Jeffrey, A., Samak, T.: Model checking firewall policy configurations. In: IEEE International Symposium on Policies for Distributed Systems and Networks, pp. 60–67 (2009)
14.
Bouhoula, A., Yazidi, A.: A security policy query engine for fully automated resolution of anomalies in firewall configurations. In: IEEE 15th International Symposium on Network Computing and Applications, pp. 76–80 (2016)
15.
Matsumoto, S., Bouhoula, A.: Automatic verification of firewall configuration with respect to security policy requirements. In: Proceedings of the International Workshop on Computational Intelligence in Security for Information Systems, pp. 123–130 (2008)
16.
Youssef, N.B., Bouhoula, A., Jacquemard, F.: Automatic verification of conformance of firewall configurations to security policies. In: IEEE Symposium on Computers and Communications, pp. 526–531 (2009)
17.
18.
Ranathunga, D., Roughan, M., Kernick, P., Falkner, N.: Malachite: firewall policy comparison. In: IEEE Symposium on Computers and Communication, pp. 310–317 (2016)
19.
Cupens, F., Cuppens-Boulahia, N., Sans, T., Miege, A.: A formal approach to specify and deploy a network security policy. In: Second Workshop on Formal Aspects in Security and Trust, pp. 203–218 (2004)
20.
Bartal, Y., Mayer, A.J., Nissim, K., Wool, A.: Firmato: a novel firewall management toolkit. ACM Trans. Comput. Syst. 22(4), 381–420 (2004)CrossRef
Metadata
Title
Inconsistency Analysis of Time-Based Security Policy and Firewall Policy
Authors
Yi Yin
Yuichiro Tateiwa
Yun Wang
Yoshiaki Katayama
Naohisa Takahashi
Copyright Year
2017
Book
Formal Methods and Software Engineering

Print ISBN: 978-3-319-68689-9

Electronic ISBN: 978-3-319-68690-5

Copyright Year: 2017

DOI
https://doi.org/10.1007/978-3-319-68690-5_27

Premium Partner

    Image Credits