Архитектура и программная реализация системы верификации правил фильтрации
Ключевые слова:
архитектура системы верификации, сетевая безопасность, верификация, проверка на модели, аномалии правил фильтрацииАннотация
В статье описывается общая архитектура системы верификации правил фильтрации межсетевого экрана, а также рассматриваются аспекты программной реали- зации этой системы. Реализация выполнена на основе применения метода «проверки на модели» (Model Checking). В качестве верификатора используется программная система SPIN. Также был разработан пользовательский интерфейс, который позволяет загружать данные о верифицируемой системе, правила политики фильтрации, управлять процессом верификации, а также в удобном виде представлять ее результаты. Кроме того, в предлагаемой системе реализована возможность применения различных стратегий разрешения аномалий.Литература
Котенко И.В., Юсупов Р.М. Перспективные направления исследований в области компьютерной безопасности // Защита информации. Инсайд, № 2, 2006. С.46–57
Полубелова О.В., Котенко И.В. Верификация правил фильтрации с временными характеристиками методом “проверки на модели” // Труды СПИИРАН. Вып.3 (22). СПб.: Наука, 2012. С.113-138
Kotenko I., Polubelova O. Verification of Security Policy Filtering Rules by Model Checking // Proceedings of IEEE Fourth International Workshop on “Intelligent Data Acquisition and Advanced Computing Systems: Technology and Applications” (IDAACS’2011). Prague, Czech Republic, 15-17 September 2011. P. 706-710
Тишков А.В., Котенко И.В., Черватюк О.В., Лакомов Д.П., Резник С.А., Сидельникова Е.В. Обнаружение и разрешение конфликтов в политиках безопасности компьютерных сетей // Труды СПИИРАН, Выпуск 3, Том 2. СПб.: Наука, 2006. С.102- 114
Котенко И.В., Тишков А.В., Черватюк О.В., Лакомов Д.П. Поиск конфликтов в политиках безопасности // Изв. Вузов. Приборостроение, Т.49, № 11, 2006, С.45-49
Котенко И.В., Тишков А.В., Черватюк О.В., Резник С.А., Сидельникова Е.В. Система верификации политики безопасности компьютерной сети // Вестник компь- ютерных и информационных технологий, № 11, 2007. C.48-56
Котенко И.В., Тишков А.В., Сидельникова Е.В., Черватюк О.В. Проверка правил политики безопасности для корпоративных компьютерных сетей // Защита инфор- мации. Инсайд, № 5, 2007. С.46-49; № 6, 2007. С.52-59
Черватюк О.В., Котенко И.В. Верификация правил фильтрации политики безопасности методом “проверки на модели” // Изв. Вузов. Приборостроение, Т.51, № 12, 2008, С.44-49. ISSN 0021-3454
Holzmann G. The Spin Model Checker Primer and Reference Manual // Addison- Wesley, 2003. P. 608
Manna Z., Pnueli A. Temporal Verification of Reactive Systems: Safety // Springer-Verlag, New York, 1995. P. 530
Карпов Ю.Г. Model checking. Верификация параллельных и распределенных программных систем // СПб.: БХВ, 2009. 560 с.
Миронов А.М. Математическая теория программных систем. http://intsys.msu.ru/staff/mironov
On-The-Fly, LTL Model Checking with SPIN. http://netlib.belllabs. com/netlib/spin/whatispin.html
Ehab Al-Shaer, Adel El-Atawy, Taghrid Samak Automated pseudo-live testing of firewall configuration enforcement. IEEE Journal on Selected Areas in Communications V. 27(3). 2009. P. 302-314
Ting Yu; Dhivya Sivasubramanian; Tao Xie Security policy testing via automated program code generation // ACM International Conference Proceeding Series. 2009
Ehab Al-Shaer; Will Marrero; Adel El-Atawy; Khalid ElBadawi Network configuration in a box: Towards end-to-end verification of network reachability and security // Proceedings - International Conference on Network Protocols, ICNP. 2009. P. 123-132
Fei Chen; Alex X. Liu; Jeehyun Hwang; Tao Xie First step towards automatic correction of firewall policy faults // ACM Transactions on Autonomous and Adaptive Systems. V. 7(2). 2012
Linghao Zhang; Xiaoxing Ma; Jian Lu; Tao Xie; Nikolai Tillmann; Peli De Halleux Environmental modeling for automated cloud application testing // IEEE Software. V. 29(2). 2012. P. 30-35
JeeHyun Hwang; Tao Xie; Fei Chen; Alex X. Liu Systematic structural testing of firewall policies // IEEE Transactions on Network and Service Management.V. 9(1). 2012. P. 1-11
Alain J. Mayer, Avishai Wool, Elisha Ziskind Offline firewall analysis. Int. J. Inf. Sec. 5(3). 2006. P. 125-144
Khalid Al-Tawil, Ibrahim A. Al-Kaltham Evaluation and testing of internet firewalls. Int. Journal of Network Management 9(3): 1999. P. 135-149
Jan Jürjens , Guido Wimmel Specification-Based Testing of Firewalls (2001) // In proceeding of the 4th International Conference of perspectives of System Informatics (PSI’02). 2002. P. 308-316
Baier C., Katoen J.-P. Principles of Model Checking // The MIT Press, 2008. P. 984
Полубелова О.В., Котенко И.В. Верификация правил фильтрации с временными характеристиками методом “проверки на модели” // Труды СПИИРАН. Вып.3 (22). СПб.: Наука, 2012. С.113-138
Kotenko I., Polubelova O. Verification of Security Policy Filtering Rules by Model Checking // Proceedings of IEEE Fourth International Workshop on “Intelligent Data Acquisition and Advanced Computing Systems: Technology and Applications” (IDAACS’2011). Prague, Czech Republic, 15-17 September 2011. P. 706-710
Тишков А.В., Котенко И.В., Черватюк О.В., Лакомов Д.П., Резник С.А., Сидельникова Е.В. Обнаружение и разрешение конфликтов в политиках безопасности компьютерных сетей // Труды СПИИРАН, Выпуск 3, Том 2. СПб.: Наука, 2006. С.102- 114
Котенко И.В., Тишков А.В., Черватюк О.В., Лакомов Д.П. Поиск конфликтов в политиках безопасности // Изв. Вузов. Приборостроение, Т.49, № 11, 2006, С.45-49
Котенко И.В., Тишков А.В., Черватюк О.В., Резник С.А., Сидельникова Е.В. Система верификации политики безопасности компьютерной сети // Вестник компь- ютерных и информационных технологий, № 11, 2007. C.48-56
Котенко И.В., Тишков А.В., Сидельникова Е.В., Черватюк О.В. Проверка правил политики безопасности для корпоративных компьютерных сетей // Защита инфор- мации. Инсайд, № 5, 2007. С.46-49; № 6, 2007. С.52-59
Черватюк О.В., Котенко И.В. Верификация правил фильтрации политики безопасности методом “проверки на модели” // Изв. Вузов. Приборостроение, Т.51, № 12, 2008, С.44-49. ISSN 0021-3454
Holzmann G. The Spin Model Checker Primer and Reference Manual // Addison- Wesley, 2003. P. 608
Manna Z., Pnueli A. Temporal Verification of Reactive Systems: Safety // Springer-Verlag, New York, 1995. P. 530
Карпов Ю.Г. Model checking. Верификация параллельных и распределенных программных систем // СПб.: БХВ, 2009. 560 с.
Миронов А.М. Математическая теория программных систем. http://intsys.msu.ru/staff/mironov
On-The-Fly, LTL Model Checking with SPIN. http://netlib.belllabs. com/netlib/spin/whatispin.html
Ehab Al-Shaer, Adel El-Atawy, Taghrid Samak Automated pseudo-live testing of firewall configuration enforcement. IEEE Journal on Selected Areas in Communications V. 27(3). 2009. P. 302-314
Ting Yu; Dhivya Sivasubramanian; Tao Xie Security policy testing via automated program code generation // ACM International Conference Proceeding Series. 2009
Ehab Al-Shaer; Will Marrero; Adel El-Atawy; Khalid ElBadawi Network configuration in a box: Towards end-to-end verification of network reachability and security // Proceedings - International Conference on Network Protocols, ICNP. 2009. P. 123-132
Fei Chen; Alex X. Liu; Jeehyun Hwang; Tao Xie First step towards automatic correction of firewall policy faults // ACM Transactions on Autonomous and Adaptive Systems. V. 7(2). 2012
Linghao Zhang; Xiaoxing Ma; Jian Lu; Tao Xie; Nikolai Tillmann; Peli De Halleux Environmental modeling for automated cloud application testing // IEEE Software. V. 29(2). 2012. P. 30-35
JeeHyun Hwang; Tao Xie; Fei Chen; Alex X. Liu Systematic structural testing of firewall policies // IEEE Transactions on Network and Service Management.V. 9(1). 2012. P. 1-11
Alain J. Mayer, Avishai Wool, Elisha Ziskind Offline firewall analysis. Int. J. Inf. Sec. 5(3). 2006. P. 125-144
Khalid Al-Tawil, Ibrahim A. Al-Kaltham Evaluation and testing of internet firewalls. Int. Journal of Network Management 9(3): 1999. P. 135-149
Jan Jürjens , Guido Wimmel Specification-Based Testing of Firewalls (2001) // In proceeding of the 4th International Conference of perspectives of System Informatics (PSI’02). 2002. P. 308-316
Baier C., Katoen J.-P. Principles of Model Checking // The MIT Press, 2008. P. 984
Architecture and software implementation of the system of verification of filtering rules
Abstract
The paper describes the general architecture of the system of verification of filter rules firewall and discusses aspects of the software implementation. The implementation is based on the method of "model checking". SPIN software system is used as a verifier. Also designed user interface is described in the paper. It allows to download data on verifiable system and filtering policy rules. The user interface includes elements for management verification process and presentation of its results. In addition, the proposed system allows using different strategies to resolve the anomalies.Опубликован
2013-06-01
Как цитировать
Полубелова, О. В. (2013). Архитектура и программная реализация системы верификации правил фильтрации. Труды СПИИРАН, 3(26), 79-90. https://doi.org/10.15622/sp.26.6
Раздел
Статьи
Авторы, которые публикуются в данном журнале, соглашаются со следующими условиями:
Авторы сохраняют за собой авторские права на работу и передают журналу право первой публикации вместе с работой, одновременно лицензируя ее на условиях Creative Commons Attribution License, которая позволяет другим распространять данную работу с обязательным указанием авторства данной работы и ссылкой на оригинальную публикацию в этом журнале.
Авторы сохраняют право заключать отдельные, дополнительные контрактные соглашения на неэксклюзивное распространение версии работы, опубликованной этим журналом (например, разместить ее в университетском хранилище или опубликовать ее в книге), со ссылкой на оригинальную публикацию в этом журнале.
Авторам разрешается размещать их работу в сети Интернет (например, в университетском хранилище или на их персональном веб-сайте) до и во время процесса рассмотрения ее данным журналом, так как это может привести к продуктивному обсуждению, а также к большему количеству ссылок на данную опубликованную работу (Смотри The Effect of Open Access).
