Details

Целью работы является выявление ошибок и несоответствий в механизмах контроля доступа и в процессах обработки и хранения данных в распределённых системах больших данных с применением временной логики и формальной верификации. Объектом исследования является распределённая система обработки и хранения больших данных. Задачи, решаемые в ходе исследования: 1. Проанализировать задачи обеспечения безопасности распределенных систем обработки больших данных. 2. Проанализировать способы и инструменты применения временных логик в задачах информационной безопасности. 3. Разработать способ применения временной логики для верификации контроля доступа в системах больших данных. 4. Разработать способ применения временной логики для верификации процессов обработки и хранения больших данных. 5. Разработать и протестировать программный прототип, обеспечивающий автоматическую верификацию политик безопасности на основе временной логики. В результате выполнения ВКР был выполнен анализ архитектур и подходов к обеспечению безопасности в распределённых системах, обоснован выбор логики линейного времени и инструмента TLA+, предложена формализация модели контроля доступа и жизненного цикла обработки больших данных. Разработан тестовый стенд, выполняющий автоматическую генерацию спецификаций на языке TLA+ для политик доступа и обработки данных, а также их верификацию. Стенд предназначен для учебных целей: демонстрации применения формальных методов, анализа логики обработки и обучения верификации политик безопасности.

The purpose of the study is identify errors and inconsistencies in access control mechanisms and in data processing and storage workflows within distributed big data systems using temporal logic and formal verification. The object of the study is a distributed big data processing and storage system. The research set the following goals: 1. Analyze the security challenges of distributed big data processing systems. 2. Explore methods and tools for applying temporal logic to information security tasks. 3. Develop an approach for using temporal logic to verify access control in big data systems. 4. Develop an approach for using temporal logic to verify data processing and storage workflows. 5. Design and test a software prototype that enables automatic verification of security policies based on temporal logic. As a result of the thesis, an analysis of architectures and approaches to ensuring security in distributed systems was carried out. The choice of linear temporal logic and the TLA+ tool was justified, and a formal model of access control and data lifecycle was proposed. A test stand was developed to automatically generate TLA+ specifications for access and processing policies and to perform their verification. The stand is intended for educational use, including demonstration of formal methods, analysis of processing logic, and training in the verification of security policies.