Методика верификации сетевых информационных потоков в информационно-телекоммуникационных системах со встроенными устройствами
Ключевые слова:
информационная безопасность, информационные потоки, встроенные устройстваАннотация
В работе представлена методика верификации сетевых информационных потоков информационно-телекоммуникационных систем со встроенными устройствами. Цель методики – оценка защищенности разрабатываемой системы и проверка соответствия информационных потоков в реальной системе заданным политикам. Проводимая верификация базируется на методе «проверки на модели» с использованием программного средства SPIN. Верификация информационных потоков проводится на начальных этапах проектирования и обеспечивает более раннее обнаружение противоречий в используемой политике безопасности и несоответствий топологии сети требованиям информационно-телекоммуникационной системы.Литература
Десницкий В.А., Котенко И.В. Проектирование защищенных встроенных устройств на основе конфигурирования // Проблемы информационной безопасности. Компьютерные системы, № 1, 2013, C 44–54.
Десницкий В.А., Чечулин А.А. Модели процесса построения безопасных встроенных систем // Системы высокой доступности, № 2, 2011. С. 97-101
Котенко И.В., Десницкий В.А., Чечулин А.А. Исследование технологии проектирования безопасных встроенных систем в проекте Европейского сообщества SecFutur // Защита информации. Инсайд, № 3, 2011. С.68-75
Полубелова О.В., Котенко И.В. Методика верификации правил фильтрации методом “проверки на модели” // Проблемы информационной безопасности. Компьютерные системы, № 1, 2013, C. 151–168
Чечулин А.А., Котенко И.В., Десницкий В.А. Анализ информационных потоков для построения защищенных систем со встроенными устройствами // Системы высокой доступности, 2012, № 2, С. 116–122
Agaskar A., He T., Tong L. Distributed Detection of Multi-hop Information Flows with Fusion Capacity Constraints // Signal Processing, IEEE Transactions on, vol. 58, no. 6: IEEE, 2010, P. 3373–3383
Baier C., Katoen J.-P. Principles of Model Checking // The MIT Press, 2008, P. 984
Braghin C., Sharygina N., Barone-Adesi K. A model checking-based approach for security policy verification of mobile systems // Formal Aspects of Computing Journal, 2011. P. 627–648
Chechulin A., Kotenko I., Desnitsky V. A Combined Approach for Network Information Flow Analysis for Systems of Embedded Components // Lecture Notes in Computer Science, Springer-Verlag, Vol. 7531. The Sixth International Conference "Mathematical Methods, Models and Architectures for Computer Networks Security" (MMM-ACNS-2012). October 17-19, 2012, St. Petersburg, Russia. P.146-155
Desnitsky V., Kotenko I., Chechulin A. Configuration-based approach to embedded device security // Lecture Notes in Computer Science, Springer-Verlag, Vol. 7531. P. 270-285
Hedin D., Sabelfeld A. A Perspective on Information-Flow Control // Proceedings of summer school Control Tools for Analysis and Verification of Software Safety and Security, Marktoberdorf, Germany. IOS Press, 2011
Pistoia M., Chandra S., Fink S., Yahav E. A Survey Of Static Analysis Methods For Identifying Security Vulnerabilities In Software Systems // IBM Systems Journal, 2007. P. 265-288
Rae A., Fidge C. Identifying Critical Components during Information Security Evaluations // Journal of Research and Practice in Information Technology, 2005. P. 391–402
Ruiz J. F., Desnitsky V., Harjani R., Manna A., Kotenko I., Chechulin A. A Methodology for the Analysis and Modeling of Security Threats and Attacks for Systems of Embedded Components // 20th Euromicro International Conference on Parallel, Distributed, and Network-Based Processing (PDP 2012). Garching/Munich. February 2012, P. 261–268
Sprintson A., El Rouayheb S., Georghiades C. A New Construction Method for Networks from Matroids // In Proceedings of the 2009 IEEE international conference on Symposium on Information Theory (ISIT'09), 2009
Десницкий В.А., Чечулин А.А. Модели процесса построения безопасных встроенных систем // Системы высокой доступности, № 2, 2011. С. 97-101
Котенко И.В., Десницкий В.А., Чечулин А.А. Исследование технологии проектирования безопасных встроенных систем в проекте Европейского сообщества SecFutur // Защита информации. Инсайд, № 3, 2011. С.68-75
Полубелова О.В., Котенко И.В. Методика верификации правил фильтрации методом “проверки на модели” // Проблемы информационной безопасности. Компьютерные системы, № 1, 2013, C. 151–168
Чечулин А.А., Котенко И.В., Десницкий В.А. Анализ информационных потоков для построения защищенных систем со встроенными устройствами // Системы высокой доступности, 2012, № 2, С. 116–122
Agaskar A., He T., Tong L. Distributed Detection of Multi-hop Information Flows with Fusion Capacity Constraints // Signal Processing, IEEE Transactions on, vol. 58, no. 6: IEEE, 2010, P. 3373–3383
Baier C., Katoen J.-P. Principles of Model Checking // The MIT Press, 2008, P. 984
Braghin C., Sharygina N., Barone-Adesi K. A model checking-based approach for security policy verification of mobile systems // Formal Aspects of Computing Journal, 2011. P. 627–648
Chechulin A., Kotenko I., Desnitsky V. A Combined Approach for Network Information Flow Analysis for Systems of Embedded Components // Lecture Notes in Computer Science, Springer-Verlag, Vol. 7531. The Sixth International Conference "Mathematical Methods, Models and Architectures for Computer Networks Security" (MMM-ACNS-2012). October 17-19, 2012, St. Petersburg, Russia. P.146-155
Desnitsky V., Kotenko I., Chechulin A. Configuration-based approach to embedded device security // Lecture Notes in Computer Science, Springer-Verlag, Vol. 7531. P. 270-285
Hedin D., Sabelfeld A. A Perspective on Information-Flow Control // Proceedings of summer school Control Tools for Analysis and Verification of Software Safety and Security, Marktoberdorf, Germany. IOS Press, 2011
Pistoia M., Chandra S., Fink S., Yahav E. A Survey Of Static Analysis Methods For Identifying Security Vulnerabilities In Software Systems // IBM Systems Journal, 2007. P. 265-288
Rae A., Fidge C. Identifying Critical Components during Information Security Evaluations // Journal of Research and Practice in Information Technology, 2005. P. 391–402
Ruiz J. F., Desnitsky V., Harjani R., Manna A., Kotenko I., Chechulin A. A Methodology for the Analysis and Modeling of Security Threats and Attacks for Systems of Embedded Components // 20th Euromicro International Conference on Parallel, Distributed, and Network-Based Processing (PDP 2012). Garching/Munich. February 2012, P. 261–268
Sprintson A., El Rouayheb S., Georghiades C. A New Construction Method for Networks from Matroids // In Proceedings of the 2009 IEEE international conference on Symposium on Information Theory (ISIT'09), 2009
A technique for verification of network information flows in information and telecommunication systems with embedded devices
Abstract
The paper comprises a technique of information flow verification for information and telecommunication systems with embedded devices. The goal of the technique is to evaluate the security level of the constructed system and check the compliance between real information flows and the set policies. The conducted verification is based on model checking with the use of SPIN tool. Implementation of such verification is fulfilled at initial design stages and provides earlier detection of contradictions in the used security policy and inconsistencies between the network topology and requirements of the information system.Опубликован
2013-12-01
Как цитировать
Десницкий, В. А. (2013). Методика верификации сетевых информационных потоков в информационно-телекоммуникационных системах со встроенными устройствами. Труды СПИИРАН, 7(30), 246-257. https://doi.org/10.15622/sp.30.15
Раздел
Статьи
Авторы, которые публикуются в данном журнале, соглашаются со следующими условиями:
Авторы сохраняют за собой авторские права на работу и передают журналу право первой публикации вместе с работой, одновременно лицензируя ее на условиях Creative Commons Attribution License, которая позволяет другим распространять данную работу с обязательным указанием авторства данной работы и ссылкой на оригинальную публикацию в этом журнале.
Авторы сохраняют право заключать отдельные, дополнительные контрактные соглашения на неэксклюзивное распространение версии работы, опубликованной этим журналом (например, разместить ее в университетском хранилище или опубликовать ее в книге), со ссылкой на оригинальную публикацию в этом журнале.
Авторам разрешается размещать их работу в сети Интернет (например, в университетском хранилище или на их персональном веб-сайте) до и во время процесса рассмотрения ее данным журналом, так как это может привести к продуктивному обсуждению, а также к большему количеству ссылок на данную опубликованную работу (Смотри The Effect of Open Access).
