Ensuring the Survivability of a Complex Technical System Under Special Conditions

Full Text

Введение В настоящее время трудно представить выполнение сложной технической системой (СТС) функциональных задач без использования информационных технологий. Отказы технических и коммуникационных средств, а также ошибки в проектном решении по системе и программном обеспечении (ПО) могут привести к нарушению качества функционирования системы в специальных условиях. Под специальными условиями понимается высокая вероятность воздействия на СТС деструктив-ных внешних факторов в процессе ее функцио-нирования, приводящих к нарушению функционирования СТС в целом и, как следствие, снижению живучести. На данный момент существует множество научных работ, посвященных восстановлению элементов системы и их связей после сбоев и отказов, вызванных внутренними факторами. Результаты, представленные в этих публикациях, не входят в рамки нашего исследования. Большой интерес с точки зрения обеспечения живучести СТС представляют исследования, нацеленные на обнаружение ошибок в проект-ном решении и ПО, возобновление работы системы в соответствии с предъявляемыми тре-бованиями после воздействия деструктивных внешних факторов. Современным направлением исследований является обеспечение живучести СТС, значительную роль в функционировании которых играют информационно-управляющие подсистемы (ИУП) [1]. ИУП управляет объектом с помощью программно реализованных алгоритмов, из чего следует, что функционирование ИУП СТС зависит от качества ПО и корректности алгоритмов. Цена ошибок, допущенных на этапах проектирования СТС (до непосредственной реализации), особенно высока [2]. На основе анализа систематизированных в [3] причин некорректной работы ПО целесообразно выделить в отдельную группу логические ошибки. Под логическими ошибками в данном исследовании будем понимать ошибки в постановке или формализации требований, а также в их реализации, после возникновения которых в результате функционирования системы параметры информационных потоков изменяются не так, как определено конструкторской, программной и эксплуатационной документациями. Следует отметить, что логическая ошибка может быть вызвана деструктивным внешним воздействием на СТС как со стороны злоумышленника, так и действиями легитимного пользователя системы. При проведении исследования учтено, что информационный процесс представляет собой иерархически упорядоченную структуру информационных процессов и ошибка на низшем уровне иерархии может распространиться на высшие уровни. Ошибки могут привести к функциональному отказу системы самостоятельно или стать причиной получения некорректной или непредусмотренной для пользователя информации, после чего уже пользователь может совершить ошибку и вызвать функциональный отказ системы [1]. Обнаружение подавляющего большинства логических ошибок в ПО на практике выполняется с применением технологий статического и динамического анализа [4; 5]. Это объясняется относительно высокой точностью и незначительными требованиями к ресурсам, необходимым для их использования. В [6] показано, что применение статических и динамических анализаторов для выявления логических ошибок, приводящих к нарушению параметров информационных потоков, не является эффективным. Автор предлагает механизм формальной верификации для контроля параметров информационных потоков, в основе которого лежит математический аппарат темпоральной логики. Существенным огра-ничением предложенного в работе механизма видится ориентированность на работу с хранимыми процедурами баз данных и позднее (после разработки ПО) выявление ошибок. Противоположный, с точки зрения стадии проектирования, подход представлен в [7]. Описывается поиск логических ошибок в проектном решении с помощью построения DFD (Data Flow Diagram) диаграммы с использованием расширенной нотации Демарко [8] и запросов к логической базе знаний. Недостатком данного подхода является сложность интерпретации результата и неприменимость подхода на этапе проверок соответствия реализации техническому заданию[8]. Проведенный анализ доказывает актуальность разработки алгоритма обеспечения живучести СТС в специальных условиях на основе математического аппарата темпоральной логики, к достоинствам которого можно отнести формализацию зависящих от времени свойств, применимость для моделирования поведения системы, наличие инструментов автоматической проверки модели и визуализации последовательности принимаемых состояний модели системы. 1. Материалы и методы В [7] представлена методика применения метода дедуктивной верификации для поиска ошибок на этапе проектирования системы. Особенность этой методики заключается в построении DFD-диаграммы с использованием расширенной нотации Демарко [8], которая затем транслируется в программу на языке логического программирования Prolog [9]. Верификация выполняется посредством запросов к логической базе знаний. В процессе верификации строится сеть распространения особых меток, присвоенных данным, и проводится анализ соответствия меток в сети требованиям к системе. Результатом является список всех обнаруженных нарушений. В [10] представлен подход для анализа наличия логических ошибок, применяемый на этапе проектирования СТС, в основе которого лежит статический анализ DFD-диаграмм. В статье предложено использовать SecDFD (Security Data Flow Diagram), расширение DFD для построения модели системы. Аналогично [7] данным присваиваются метки, основываясь на требованиях к системе. По диаграмме SecDFD строится граф, в узлах которого хранятся метки данных. Контроль параметров информационных потоков выполняется за счет статической проверки соответствия графовой модели требованиям к системе. Соответствие может быть установлено после распространения меток с помощью обхода в ширину графа согласно семантике узлов. А.М. Каннер продемонстрировал преимущества применения математического аппарата темпоральной логики и инструментальных средств автоматической верификации моделей (в публикации это модели безопасности), сформулированных на формальном языке, пригодном для верификации, для поиска ошибок в модели [11]. При верификации модели в качестве формального языка в [11] использован язык спецификаций TLA+ (Temporal Logic of Actions) [12] и метод model checking [13]. Темпоральная логика - это логика, в которой истинное значение логических формул зависит от момента времени, в котором вычисляются значения этих формул. Основная идея темпоральной логики состоит в том, чтобы фиксировать только относительный порядок собы-тий - фактически текущее, будущее и прошедшее время [13]. В [6] представлен алгоритм контроля параметров информационных потоков, проверяющий модель вычислений в системе, выполняемых с помощью Oracle/PLSQL блоков. Верификация модели происходит автоматически с использованием инструмента типа model checker - TLC (Temporal Logic Checker) [12]. Предложенный А.А. Тимаковым алгоритм выявляет запрещенные политиками безопасности информационные потоки. Анализ траекторий функционирования системы, полученных в результате работы TLC, позволяет сформулировать рекомендации по корректировке кода и изменению политики безопасности для устранения нарушений. Данный алгоритм способен обнаружить логические ошибки как на стадии ввода в действие, так и при сопровождении СТС [8]. Разделение анализа наличия логических ошибок на анализ на этапе проектирования и анализ на этапе реализации позволяет достичь композиционности [10]. Однако разделение анализа порождает проблему согласованности реализации и проектного решения. В [14] представлен подход, основанный на двухэтапном анализе наличия логических ошибок, включающий в себя механизм обеспечения согласованности реализации и проектного решения. Моделирование системы и проверка модели происходит аналогично [10]. Затем строится программная модель с помощью фреймворка GRaViTY [16] и выполняется автоматизированное сопоставление элементов программы с элементами SecDFD, с последующим статическим анализом соответствия реализации системы ее модели. Описанный в [15] фреймворк GRaViTY способен выполнять проверку артефактов разработки системы, а также обеспечивать синхронизацию изменений между ними. Под артефактами разработки в публикации понимаются модели системы различной степени абстракции и программная реализация. Следует отметить простоту интеграции GRaViTY в суще-ствующие системы, в которых отсутствуют актуальные модели, с помощью автоматизированного получения моделей из программной реализации. Для анализа наличия логических ошибок в артефактах разработки системы в фреймворке используются статические и динамические проверки. Проведенный анализ современного состояния исследований в области контроля параметров информационных потоков для обеспечения живучести СТС в специальных условиях обосновывает предположение о целесообразности применения алгоритма в составе ИУП, обладающего следующими особенностями: - в основе алгоритма лежит математический аппарат темпоральной логики; - реализация алгоритма должна применяться на этапах проектирования, ввода в действие и сопровождения СТС; - алгоритм способен контролировать параметры информационных потоков СТС; - алгоритм выявляет несогласованность реализации ПО СТС и проектного решения. 2. Результаты В качестве подхода для обеспечения живучести СТС в специальных условиях рассмотрим алгоритм поиска логических ошибок в проектном решении и программном обеспечении СТС (рис. 1), базирующийся на темпоральной логике. Для обнаружения логических ошибок в проектном решении и несоответствия программной реализации проектному решению СТС необходимо выполнить моделирование в виде DFD-диаграммы функций СТС, работающих с наиболее чувствительной информацией непосредственно или через использование других функций. Под чувствительной информацией будем понимать информацию, доступ к которой ограничен и раскрытие которой может привести систему к снижению эффективности функционирования системы [16]. Поиск функций и объектов, содержащих чувствительную информацию, осуществляется аналитиками системы исходя из понимания особенностей ее функционирования. По полученной на прошлом шаге DFD-диаграмме необходимо написать TLA+-спецификацию. Процесс написания TLA+-спецификаций является трудоемкой и весьма нетривиальной задачей. Это объясняется тем, что TLA+ ориентирован на описание поведения систем, но не на описание информационных потоков. Для решения этой проблемы в алгоритм был добавлен шаг составления спецификации на языке TIFL (TIFL-спецификации), описывающей информационные потоки в системе. Язык TIFL (Trivial Information Flow Language) обладает простым для описания информационных потоков синтаксисом и является доменно-специфичным языком (DSL - Domain Specific Language). Доменно-специфичные языки - это языки, ориентированные на решения проблем в конкретных областях в отличие от языков общего назначения [17]. Обоснованием разработки языка TIFL служит проведенный анализ исследования, опубликованного в [18]. Среди представленных автором доменно-специфичных языков в категории контроля параметров информационных потоков (IFC - Information Flow Control) не было выявлено существующего языка, который можно было бы применить для эффективного описания информационных потоков и последующей трансляции в TLA+-спецификацию. TIFL-спецификация является формальным представлением DFD-диаграммы, необходимым для проведения верификации параметров информационных потоков (обнаружения потоков информации, не соответствующих заданным критериям) в автоматическом режиме. В контексте верификации параметров информационных потоков нас интересуют источники и получатели информации, а также условия возникновения информационных потоков. Проверка TIFL-спецификации выполняется посредством трансляции спецификации на языке TIFL в спецификацию на языке TLA+ с помощью утилиты tifl2tla[9] и последующего запуска утилиты TLC. При проигрывании модели с помощью TLC проверяется, что наблюдаемые результаты выполняемых СТС функций не противоречат правилам разграничения доступа к информационным ресурсам, предъявляемым к системе. Далее проверяемое условие будем называть инвариантом. Если в конце проверки модели обнаруживается, что объект системы начинает содержать более чувствительную информацию, то следует повторить проигрывание модели, считая, что данный объект в начальном состоянии содержит информацию, чей уровень чувствительности соответствует уровню текущего конечного состояния. Повторять проигрывание моделей целесообразно до тех пор, пока при очередном проигрывании моделей не выявится нарушение инварианта или не перестанет меняться уровень чувствительности информации в объектах системы. Рис. 1. Схема алгоритма поиска логических ошибок в проектном решении и программном обеспечении СТС И с т о ч н и к: выполнено В.В. Алексеевым, Д.А. Ивановым, И.Г. Рыжовым Figure 1. Flowchart of the algorithm for identifying logical errors in the design solution and software of a complex technical system S o u r c e: by V.V. Alekseev, D.A. Ivanov, I.G. Ryzhov В случае нарушения инварианта по траектории перемещения информации, полученной в результате работы TLC, можно отследить логические ошибки в проектном решении СТС. В качестве решений по исправлению нарушений, исходя из предположения о корректности работы утилиты трансляции tifl2tla и соответствия DFD-диаграммы TIFL-спецификации, может быть внесение правок в проектное решение или в спецификацию (в случае ложно-положительного нарушения инварианта) и соответствующую ей DFD-диаграмму. Если изменениям подверглось проектное решение, то необходимо произвести актуализацию DFD-диаграммы с последующей генерацией спецификаций. После модификации спецификаций вне зависимости от принятого решения необходимо выполнить повторный запуск TLC. Если же нарушений инварианта не выявлено, то проектное решение системы не содержит логических ошибок, приводящих к нарушению параметров информационных потоков. В таком случае для систем, в которых отсутствует ПО, соответствующее проектному решению, разрешается приступить к его разработке. Разработанное (для анализа вновь создаваемых систем) или существующее (для анализа эксплуатируемых систем) ПО необходимо транслировать в TIFL-спецификацию. Особенностью этапа перевода на язык TIFL является то, что он происходит с учетом абстрагирования от реальных вычислений в системе. При описании информационных потоков на языке TIFL рекомендуется использовать как можно меньшее число локальных переменных. Так, например, вместо занесения суммы переменных a и b в локальную переменную c и последующей передачи этой переменной получателю информационного потока r можно сразу описать передачу информационному потоку r последовательности переменных a и b. Тем не менее необходимо с осторожностью подходить к объединению информационных потоков и учитывать допустимость отсутствия атомарности процесса, который будет иметь объединенный выходной информационный поток, в реализованной системе. Возможное влияние подобных способов описания спецификаций на точность анализа наличия логических ошибок в программном обеспечении СТС и разрешенные преобразования над спецификациями для приведения их к некоторому нормальному виду (процедура нормализации) требуют отдельных исследований и в данной статье не рассматриваются. Представленный для демонстрации выразительности языка TIFL фрагмент программы (рис. 2) получен из фрагмента программы на языке Oracle/PLSQL (рис. 3): - исключением синтаксических конструкций, которые не порождают информационные потоки и не добавляют условия для их возникновения; - заменой описаний вычислений над строковыми и числовыми типами данных описаниями информационных потоков, представленных с помощью меток, соответствующих переменным и литералам, участвующим в вычислениях. Рис. 2. Фрагмент программы на языке TIFL, соответствующий коду на рис. 3 И с т о ч н и к: выполнено В.В. Алексеевым, Д.А. Ивановым, И.Г. Рыжовым Figure 2. Program excerpt in the TIFL language corresponding to the code in Figure 3 S o u r c e: by V.V. Alekseev, D.A. Ivanov, I.G. Ryzhov Рис. 3. Фрагмент программы на языке Oracle/PLSQL И с т о ч н и к: составлено по Oracle/PLSQL Figure 3. Program excerpt in Oracle/PLSQL language S o u r c e: compiled by Oracle/PL SQL ORACLE PL/SQL. Базы данных. IF-THEN-ELSE ОПЕРАТОР. URL: https://oracleplsql.ru/if-then-else.html (accessed: 27.11.2024). Теперь, когда получены проверенная TIFL-спецификация проектного решения СТС и непроверенная TIFL-спецификация фактической реализации ПО, необходимо убедиться, что программная реализация соответствует проектному решению СТС. Для этого выполняется сопоставление TIFL-спецификаций, включающее процесс нормализации спецификаций. Если спецификации на языке TIFL сопоставимы, то считается, что реализация соответствует проектному решению СТС и не содержит логических ошибок, приводящих к нарушению параметров информационных потоков. В противном случае необходимо привести реализацию в соответствие проектному решению. На этапе приведения реализации в соответствие проектному решению могут как изменяться программная реализация, так и корректироваться проектное решение СТС. Если правки вносились только в ПО, то нужно заново транслировать ПО в TIFL-спецификацию и повторить шаг сопоставления TIFL-спецификаций. Однако если в ходе приведения реализации в соответствие проектному решению подверглось изменениям проектное решение, то необ-ходимо перейти к шагу актуализации DFD-диаграммы. Работа алгоритма завершается, когда TIFL-спецификации проектного решения и ПО будут считаться сопоставимыми. 3.Обсуждение Разработанный алгоритм поиска логических ошибок в проектном решении и программном обеспечении СТС рекомендуется применять для обеспечения живучести совместно с другими существующими подходами, обеспечивающими живучесть, позволяющими обнаруживать логические ошибки в ПО (например, статический и динамический анализы [4; 5]), и подходами, сфокусированными на поиск ошибок в проектных решениях (например, дедуктивной верификацией потоков, представленных в DFD [7]). Для автоматизации написания TLA+-спецификаций в [6] использована утилита [19], ориентированная на работу с программными блоками баз данных, написанными на языке Oracle/PLSQL, что дополнительно ограничи-вает совершенствование подхода развитием вендорской технологии. Использование доменно-специфичного языка TIFL и утилиты трансляции tifl2tla в алгоритме, представленном в данной статье, позволяет не только упростить процесс получения TLA+-спецификаций, но и абстрагироваться от использованных в реализации СТС технологий. Такое абстрагирование дает возможность независимо развиваться утилитам трансляции, доменно-специфичному языку TIFL и самому подходу к обеспечению живучести СТС. Алгоритм поиска логических ошибок в проектном решении и программном обеспечении СТС, как и подходы, представленные в [14; 15], обнаруживает ошибки в проектном решении и программном обеспечении СТС, а также обеспечивает согласованность проектного решения и варианта реализации системы, но отличается использованием метода верификации моделей model checking, лежащего в основе алгоритма, который исчерпывающе проверяет пространство состояний модели системы [13]. Определение эффективности предложенного в данной статье алгоритма требует оценки живучести СТС. С точки зрения проведения оценки живучести интерес представляют подходы, описанные в [20-23]. Снижения сложности внедрения алгоритма в процесс создания систем и повышения удобства использования алгоритма можно достичь за счет автоматизации шагов алгоритма. Авторы видят наиболее приоритетными для автоматизации шаги создания актуальной DFD-диаграммы и TIFL-спецификаций, соответствующих DFD-диаграмме и ПО. Для автоматизации создания DFD-диа-грамм, соответствующих словесно сформулированным требованиям, перспективным выглядит использование больших языковых моделей с помощью метода RAG [24]. Автоматизация создания TIFL-специфика-ции, соответствующей DFD-диаграмме, может быть выполнена посредством специально разрабатываемого редактора, сохраняющего по-строенные диаграммы в виде TIFL-специфи-каций и позволяющего отобразить визуально TIFL-спецификации. TIFL-спецификацию, соответствующую ПО, следует получать автоматизированно, применяя утилиты трансляции, подобные [19], для исходных кодов, написанных на различных языках программирования. Заключение Определен подход и создан алгоритм, позволяющий обеспечивать живучесть СТС в специальных условиях. В ходе исследования установлено, что проблемами с точки зрения обеспечения живучести для СТС являются логические ошибки в требованиях и их реализации. В результате на основе анализа существующих подходов к обнаружению логических ошибок разработан алгоритм, базирующийся на темпоральной логике, который позволяет своевременно обнаруживать такие ошибки и способствует их дальнейшему устранению, тем самым обеспечивая живучесть системы. Данный алгоритм целесообразно применять на этапах проектирования, ввода в действие и сопровождения систем. Дальнейшие исследования авторы видят в следующей очередности: 1) определение необходимой степени абстракции проверяемых моделей и влияние композиции моделей на точность анализа; 2) выбор подходящей DFD-нотации для построения моделей и разработка алгоритма сопоставления TIFL-спецификаций; 3) разработка алгоритма поддержки принятия решений по исправлению нарушений инварианта и устранению несоответствия реализации проектному решению; 4) определение эффективности предлагаемого в статье алгоритма посредством сравнения оценок живучести до и после его применения; 5) повышение уровня автоматизации шагов алгоритма, простоты внедре-ния алгоритма и удобства его использования

About the authors

Vladimir V. Alekseev

RUDN University

Email: vvalex1961@mail.ru
ORCID iD: 0000-0002-0398-4426
SPIN-code: 9320-9713

Doctor of Sciences (Techn.), Professor of the Department of the Department of Mechanics and Control Processes, Academy of Engineering

6 Miklukho-Maklaya St, Moscow, 117198, Russian Federation

Dmitry A. Ivanov

RUDN University

Email: 1142230113@pfur.ru
ORCID iD: 0009-0004-0182-5095
SPIN-code: 4761-2024

Postgraduate student of the Department of Mechanics and Control Processes, Academy of Engineering

6 Miklukho-Maklaya St, Moscow, 117198, Russian Federation

Ilya G. Ryzhov

RUDN University

Author for correspondence.
Email: ryzhov.ilgen@gmail.com
ORCID iD: 0000-0001-6014-6982
SPIN-code: 1818-9990

Postgraduate student of the Department of Mechanics and Control Processes, Academy of Engineering

6 Miklukho-Maklaya St, Moscow, 117198, Russian Federation

References

Supplementary files