Архитектура и программная реализация системы верификации правил фильтрации
Ключевые слова:
архитектура системы верификации, сетевая безопасность, верификация, проверка на модели, аномалии правил фильтрацииАннотация
В статье описывается общая архитектура системы верификации правил фильтрации межсетевого экрана, а также рассматриваются аспекты программной реали- зации этой системы. Реализация выполнена на основе применения метода «проверки на модели» (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
Опубликован
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).
