Automation of Verification of Incorrectness for Firewall Configurations

This article is devoted to the automation of the search of firewall configuration errors on the basis of logical analysis. As a rule, process models have been used for a description the behavior of firewalls, and the language of modal logic has been applied in order to formulate requirements (properties) of incorrectness. We focus on the presentation of a detailed methodology of the transition from process models of a description the behaviors of firewalls and conditions of their incorrectness (which were formulated in the language of modal logic) to the specific logical programs that allows to implement verification of incorrectness of firewall configurations.

References

[1] Devyatkov V.V., Tun M. Tan. Logical analysis of the correctness of the of firewall configurations. Jelektr. nauchno-tehn. Izd. "Inzhenernyy zhurnal: nauka i innovacii" MGTU im. N.E. Baumana: Informatsionnye tekhnologii [El. Sc.-Tech. Publ. "Eng. J.: Science and Innovation" of Bauman MSTU: Information technology], 2013, iss. 11 (23), 17 p. (in Russ.). Available at: http://www.engjournal.ru/catalog/it/security/988.html (accessed 24.11.2014).

[2] Yuan L., Mai J., Su Zh., Chuah Ch.-N., Chen H., Su Zh. FIREMAN: A toolkit for firewall modeling and analysis. Proc. of the IEEE Symposium on Security and Privacy 2006, pp. 199-213. Available at: http://www.cse.psu.edu/ mcdaniel/cse544/slides/cse544-fireman-lin.pdf (accessed 24.09.2014).

[3] Devyatkov V.V. Sistemy iskusstvennogo intellekta [Artificial intelligence systems]. Moscow, MGTU im. N.E. Baumana Publ., 2001. 352 p.

[4] Firewall wizards security mailing list. Available at: http://honor.icsalabs.com/mailman/listinfo/firewall-wizards (accessed 24.09.2014).

[5] Devyatkov V.V. Building, optimization and modification of processes. Vestn. Mosk. Gos. Tekh. Univ. im. N.E. Baumana, Priborostr. [Herald of the Bauman Moscow State Tech. Univ., Instrum. Eng.], 2012, no. 2, pp. 60-79 (in Russ.).

[6] Wool A. A quantitative study of firewall configuration errors. IEEE Computer, 2004, vol. 37, no. 6, pp. 62-67. DOI:10.1109/MC.2004.2

[7] Manna Z., Pnueli A. Temporal verification of reactive systems: progress. N.Y., Springer-Verlag, 1996. Draft manuscript.

[8] Lemmon E. Algebraicheskaya semantika dlya modal’nykh logik I. II. V kn.: Semantika modal’nykh i intensional’nykh logik. Pod red. Smirnova V.A. [Algebraic semantics for modal logics I. II. In book: The semantics of modal and intensional logics. Ed. by Smirnov V.A.]. Moscow, Progress Publ., 1981. 424 p.

[9] Osnovy programmirovaniya na yazyke Prolog: Informatsiya [Fundamentals of Programming in Prolog: Information]. Available at: http://www.intuit.ru/studies/courses/44/44/info (accessed 24.09.2014).

[10] Osnovy programmirovaniya na yazyke Visual Prolog [Fundamentals of Programming in Visual Prolog]. Available at: http://www.intuit.ru/studies/courses/12333/1180/info (accessed 24.09.2014).