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