Preview

Труды Института системного программирования РАН

Расширенный поиск

К формальной верификации стандартов кибербезопасности

https://doi.org/10.15514/ISPRAS-2018-30(4)-5

Аннотация

Стандарты кибербезопасности часто используются для обеспечения защищенности промышленных систем управления. В последнее время такие системы становятся все более децентрализованными, что делает их все более уязвимыми для разного рода кибератак. Одна из проблем реализации стандартов кибербезопасности в промышленных системах управления состоит в том, что невозможно своевременно проверить, соответствуют ли разрабатываемые системы этим стандартам или нет. Помимо прочего, соответствие стандарту кибербезопасности только валидируется, а не верифицируется формально, что, как правило, не дает убедительных доказательств правильного использования стандарта. В статье предлагается подход, в котором проверка защищенности промышленных систем управления осуществляется путем формального анализа. Подход состоит в следующем: определяются строительные блоки, необходимые для формального описания системы; составляется формальная модель системы; модель анализируется с помощью инструмента Alloy Analyzer. Предлагаемый подход может использоваться на ранних стадиях проектирования, где проблемы не так дороги для исправления. Чтобы показать применимость подхода, были смоделированы две кибератаки, а также стратегии противодействия им. Подход был также оценен на предмет гибкости - возможности совмещения разных аспектов стандартов кибербезопасности. В статье также обсуждаются будущие направления исследования

Об авторах

Томаш Кулик
Орхусский университет
Дания


Питер Горм Ларсен
Орхусский университет
Дания


Список литературы

1. International Society of Automation. The 62443 Series of Standards. http://isa99.isa.org/Public/Information/The-62443-Series-Overview.pdf, accessed on 13/3/18

2. D. Jackson, Software Abstractions: Logic, Language, and Analysis. Heyward Street, Cambridge, MIT Press, April 2006, iSBN-10: 0-262-10114-9.

3. Tomas Kulik, Peter W. V. Tran-Jørgensen, Jalil Boudjadar, and Carl Schultz. A framework for threat-driven cyber security verification of iot systems. In Proc. of the First International Workshop on Verification and Validation of Internet of Things, Västerås, Sweden, april 2018, in print.

4. C. Bekara. Security issues and challenges for the iot-based smart grid. Procedia Computer Science, vol. 34, 2014, pp. 532-537. [Online]. Available: http://www.sciencedirect.com/science/article/pii/S1877050914009193

5. The Alloy Analyzer Modelling website, http://alloy.mit.edu/alloy/, 2018

6. Tomas Kulik and Peter Gorm Larsen. Extensions to formal security modeling framework. https://github.com/kuliktomas/FCSVIoT/commit/189c7962f7f0870fa5315c31a71a6b35e896e47d, 2018.

7. N. Jazdi. Cyber physical systems in the context of industry 4.0. In Proc. of the 2014 IEEE International Conference on Automation, Quality and Testing, Robotics, May 2014, pp. 1-4.

8. M. Ge and D. S. Kim. A framework for modeling and assessing security of the internet of things. In Proc. of the 2015 IEEE 21st International Conference on Parallel and Distributed Systems (ICPADS), 2015, pp. 776-781.

9. C. Heitmeyer, M. Archer, E. Leonard, and J. McLean. Applying Formal Methods to a Certifiably Secure Software System. Software Engineering, IEEE Transactions on Software Engineering, vol. 34, no. 1, 2008, pp. 82 -98.

10. A. N. Haidar and A. E. Abdallah. Formal modelling of pki based authentication. Electronic Notes in Theoretical Computer Science, vol. 235, 2009, pp. 55 - 70. [Online]. Available: http://www.sciencedirect.com/science/article/pii/S157106610900084X

11. D. C. Wardell, R. F. Mills, G. L. Peterson, and M. E. Oxley. A method for revealing and addressing security vulnerabilities in cyber-physical systems by modeling malicious agent interactions with formal verification. Procedia Computer Science, vol. 95, no. Supplement C, 2016, pp. 24 - 31, Available: http://www.sciencedirect.com/science/article/pii/S1877050916324619

12. F. A. Teixeira, F. M. Pereira, H.-C. Wong, J. M. Nogueira, and L. B. Oliveira. Siot: Securing internet of things through distributed systems analysis. Future Generation Computer Systems, 2017. [Online]. Available: http://www.sciencedirect.com/science/article/pii/S0167739X17304235

13. J. Woodcock, S. Stepney, D. Cooper, J. A. Clark, and J. Jacob. The Certification of the Mondex Electronic Purse to ITSEC Level E6. Formal Aspects of Computing, vol. 20, no. 1, 2008, pp. 5-19.

14. D. K. Holstein and K. Stouffer. Trust but verify critical infrastructure cyber security solutions. In Proc. of the 43rd Hawaii International Conference on System Sciences, 2010, pp. 1-8.

15. S. Morimoto, S. Shigematsu, Y. Goto, and J. Cheng. Formal verification of security specifications with common criteria. In Proceedings of the 2007 ACM Symposium on Applied Computing, ser. SAC ’07, 2007, pp. 1506-1512. [Online]. Available: http://doi.acm.org/10.1145/1244002.1244325

16. L. Lamport, Specifying systems: the TLA+ language and tools for hardware and software engineers. Addison-Wesley Longman Publishing Co., Inc., 2002, Boston, MA, USA, 384 pages.


Рецензия

Для цитирования:


Кулик Т., Ларсен П.Г. К формальной верификации стандартов кибербезопасности. Труды Института системного программирования РАН. 2018;30(4):79-94. https://doi.org/10.15514/ISPRAS-2018-30(4)-5

For citation:


Kulik T., Larsen P.G. Towards formal verification of cyber security standards. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2018;30(4):79-94. https://doi.org/10.15514/ISPRAS-2018-30(4)-5



Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 2079-8156 (Print)
ISSN 2220-6426 (Online)