Верификация правил фильтрации с временными характеристиками методом “проверки на модели”
Ключевые слова:
сетевая безопасность, верификация, проверка на модели, аномалии правил фильтрацииАннотация
В статье описывается подход к верификации правил фильтрации межсетевого экрана, в том числе представляются модели, алгоритмы и разработанный программный прототип, предназначенные для обнаружения аномалий фильтрации в спецификации политики безопасности компьютерной сети. Предлагаемый подход основан на применении метода ―проверки на модели‖ (Model Checking) и позволяет использовать темпоральную логику для спецификации и анализа информационных процессов, протекающих в модели компьютерной сети c функционирующей системой безопасности, которые изменяются во времени и могут нарушить такие свойства безопасности, как конфиденциальность и доступность.Литература
Baier C., Katoen J.-P. Principles of Model Checking // The MIT Press, 2008. 984 p.
Holzmann G. The Spin Model Checker Primer and Reference Manual // Addison-Wesley, 2003. 608 p.
Manna Z., Pnueli A. Temporal Verification of Reactive Systems: Safety // Springer-Verlag, New York, 1995. 530 p.
Карпов Ю.Г. 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
Тишков А.В., Котенко И.В., Черватюк О.В., Лакомов Д.П., Резник С.А., Сидельникова Е.В. Обнаружение и разрешение конфликтов в политиках безопасности компьютерных сетей // Труды СПИИРАН, Выпуск 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
Braghin C., Sharygina N., Barone-Adesi K. A Model Checking-based Approach for Security Policy Verification of Mobile Systems // Formal Aspects of Computing Journal, Springer, 2010. Vol. 23, No. 5, P.627-648
Pham H.T., Truong N.-T., Nguyen V.-H. Analyzing RBAC Security Policy of Implementation Using AST // Proceedings of the 2009 International Conference on Knowledge and Systems Engineering (KSE ‗09), 2009. P. 215-219
Jajodia S., Samarati P., Sapino M.L., Subrahmanian V.S. Flexible support for multiple access control policies // ACM Transaction Database Systems. Vol.26, No.2, 2001. P.214-260
Zhang N., Ryan M. D. Guelev D. Evaluating Access Control Policies Through Model Checking // The 8th Information Security Conference (ISC‘05). Lecture Notes in Computer Science. Springer-Verlag. Vol. 3650, 2005. P.446–460
Bandara A.K., Kakas A.S., Lupu E.C., Russo A. Using Argumentation Logic for Firewall Policy Specification and Analysis // 17th IFIP/IEEE International Workshop on Distributed Systems: Operations and Management. DSOM 2006, 2006. P.185-196
Al-Shaer E., Hamed H., Boutaba R., Hasan M. Conflict classification and analysis of distributed firewall policies // IEEE Journal on Selected Areas in Communications, Vol.23, No.10, 2005. P.2069-2084
Sirjani M. Formal specification and verification of concurrent and reactive systems // Ph.D. Thesis. Sharif University of Technology, 2004. 175 p.
Rothmaier G., Kneiphoff T., Krumm H. Using SPIN and Eclipse for Optimized High-Level Modeling and Analysis of Computer Network Attack Models // Lecture Notes in Computer Science, Springer-Verlag, 2005. Vol. 3639. P.236–250
Conrad S., Campbell L.A., Cheng B.H.C., Deng M. A requirements patterns-driven approach to specify systems and check properties // 18th International SPIN Workshop, Snowbird, UT, USA. Lecture Notes in Computer Science, Vol. 2648. Springer-Verlag, 2003. P.18-33
Benthem J.М., Meulen A.T. (Eds.) Handbook of Logic and Language // North-Holland, 1997
Westerinen A., Strassner J., Scherling M., Quinn B., Herzog S., Huynh A., Carlson M., Perry J., Waldbusser S. Terminology for Policy-Based Management (RFC 3198). http://www.rfc-archive.org/getrfc.php?rfc=3198
Hamed H., Al-Shaer E. Taxonomy of Conflicts in Network Security Policies // IEEE Communications Magazine, March 2006, Vol. 44, No. 3. P.134-141
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
Common Information Model (CIM) Standards. http://www.dmtf.org/standards/cim
McMillan K. The SMV System. http://www.cs.cmu.edu/_modelcheck/smv.html
Alur R., Anand H., Grosu R., Ivancic F., etc Mocha User Manual. Jmocha Version 2.0. http://embedded.eecs.berkeley.edu/research/mocha/doc/j-doc/
Кларк Э.М., Грамберг О., Пелед Д. Верификация моделей программ. Model Checking. М.: МЦНМО. 2002
Holzmann G. The Spin Model Checker Primer and Reference Manual // Addison-Wesley, 2003. 608 p.
Manna Z., Pnueli A. Temporal Verification of Reactive Systems: Safety // Springer-Verlag, New York, 1995. 530 p.
Карпов Ю.Г. 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
Тишков А.В., Котенко И.В., Черватюк О.В., Лакомов Д.П., Резник С.А., Сидельникова Е.В. Обнаружение и разрешение конфликтов в политиках безопасности компьютерных сетей // Труды СПИИРАН, Выпуск 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
Braghin C., Sharygina N., Barone-Adesi K. A Model Checking-based Approach for Security Policy Verification of Mobile Systems // Formal Aspects of Computing Journal, Springer, 2010. Vol. 23, No. 5, P.627-648
Pham H.T., Truong N.-T., Nguyen V.-H. Analyzing RBAC Security Policy of Implementation Using AST // Proceedings of the 2009 International Conference on Knowledge and Systems Engineering (KSE ‗09), 2009. P. 215-219
Jajodia S., Samarati P., Sapino M.L., Subrahmanian V.S. Flexible support for multiple access control policies // ACM Transaction Database Systems. Vol.26, No.2, 2001. P.214-260
Zhang N., Ryan M. D. Guelev D. Evaluating Access Control Policies Through Model Checking // The 8th Information Security Conference (ISC‘05). Lecture Notes in Computer Science. Springer-Verlag. Vol. 3650, 2005. P.446–460
Bandara A.K., Kakas A.S., Lupu E.C., Russo A. Using Argumentation Logic for Firewall Policy Specification and Analysis // 17th IFIP/IEEE International Workshop on Distributed Systems: Operations and Management. DSOM 2006, 2006. P.185-196
Al-Shaer E., Hamed H., Boutaba R., Hasan M. Conflict classification and analysis of distributed firewall policies // IEEE Journal on Selected Areas in Communications, Vol.23, No.10, 2005. P.2069-2084
Sirjani M. Formal specification and verification of concurrent and reactive systems // Ph.D. Thesis. Sharif University of Technology, 2004. 175 p.
Rothmaier G., Kneiphoff T., Krumm H. Using SPIN and Eclipse for Optimized High-Level Modeling and Analysis of Computer Network Attack Models // Lecture Notes in Computer Science, Springer-Verlag, 2005. Vol. 3639. P.236–250
Conrad S., Campbell L.A., Cheng B.H.C., Deng M. A requirements patterns-driven approach to specify systems and check properties // 18th International SPIN Workshop, Snowbird, UT, USA. Lecture Notes in Computer Science, Vol. 2648. Springer-Verlag, 2003. P.18-33
Benthem J.М., Meulen A.T. (Eds.) Handbook of Logic and Language // North-Holland, 1997
Westerinen A., Strassner J., Scherling M., Quinn B., Herzog S., Huynh A., Carlson M., Perry J., Waldbusser S. Terminology for Policy-Based Management (RFC 3198). http://www.rfc-archive.org/getrfc.php?rfc=3198
Hamed H., Al-Shaer E. Taxonomy of Conflicts in Network Security Policies // IEEE Communications Magazine, March 2006, Vol. 44, No. 3. P.134-141
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
Common Information Model (CIM) Standards. http://www.dmtf.org/standards/cim
McMillan K. The SMV System. http://www.cs.cmu.edu/_modelcheck/smv.html
Alur R., Anand H., Grosu R., Ivancic F., etc Mocha User Manual. Jmocha Version 2.0. http://embedded.eecs.berkeley.edu/research/mocha/doc/j-doc/
Кларк Э.М., Грамберг О., Пелед Д. Верификация моделей программ. Model Checking. М.: МЦНМО. 2002
Verification of security policy filtering rules with temporal parameters by Model Checking
Abstract
The paper outlines an approach to verification of filtering rules of firewalls. The approach is intended for detection and resolution of filtering anomalies in the specification of the security policy of computer networks. It is based on Model Checking technique. The paper proposes the models of computer networks, the models of firewalls and filtering anomalies, as well as the algorithm of detection of such anomalies. The main peculiarities of the approach consist in using Model Checking exactly to detect the anomalies of filtering rules and in ability to specify temporal parameters in filtering rules.Опубликован
2012-09-01
Как цитировать
Полубелова, О. В., & Котенко, И. В. (2012). Верификация правил фильтрации с временными характеристиками методом “проверки на модели”. Труды СПИИРАН, 3(22), 113-138. https://doi.org/10.15622/sp.22.7
Раздел
Статьи
Авторы, которые публикуются в данном журнале, соглашаются со следующими условиями:
Авторы сохраняют за собой авторские права на работу и передают журналу право первой публикации вместе с работой, одновременно лицензируя ее на условиях Creative Commons Attribution License, которая позволяет другим распространять данную работу с обязательным указанием авторства данной работы и ссылкой на оригинальную публикацию в этом журнале.
Авторы сохраняют право заключать отдельные, дополнительные контрактные соглашения на неэксклюзивное распространение версии работы, опубликованной этим журналом (например, разместить ее в университетском хранилище или опубликовать ее в книге), со ссылкой на оригинальную публикацию в этом журнале.
Авторам разрешается размещать их работу в сети Интернет (например, в университетском хранилище или на их персональном веб-сайте) до и во время процесса рассмотрения ее данным журналом, так как это может привести к продуктивному обсуждению, а также к большему количеству ссылок на данную опубликованную работу (Смотри The Effect of Open Access).
