Тенденции развития технологий синтеза системы защиты информации с помощью smt-решателей

DOI:

Проблема синтеза системы защиты информации для автоматизированной системы в общем случае сводится к оптимальному выбору таких мер защиты, которые бы обеспечивали функционирование системы при минимальных приемлемых рисках в условиях существования определенных угроз. В зависимости от требований к автоматизированной системе (АС) и специфики ее работы задача синтеза может углубляться. Например, понятие оптимальности системы защиты информации (СЗИ) может как означать макси- мальную эффективность СЗИ при минимальных затратах на ее внедрение и поддержание, так и дополнительно учитывать степень ее влияния на работу АС. Последний вариант трактовки особенно актуален для средств антивирусной защиты, устанавливаемых на автоматизированное рабочее место пользователей АС. Другой причиной усложнения рассматриваемой проблемы является возможность варьирования самих компонентов защищаемой АС. Наконец, главная сложность заключается в формализации списка угроз и зна- чений рисков, которые могут представлять собой зависимые от различных факторов и друг от друга величины.

Наиболее известным подходом к решению задачи синтеза СЗИ является использование модели с полным перекрытием. Однако, ввиду описанных выше сложностей, неизбежно возникающих при работе с реальными АС, непосредственное применение данной модели затруднено, как на этапе формализации, так и на этапе поиска решения. Для преодоления этих трудностей предлагается подход, заключающийся в следующем:

• 1.    Исходная задача кодируется в терминах теории UFLRA (линейная арифметика с неинтерпретируемыми типами и функциями).

• 2.    Полученная задача решается с помощью одного из существующих программных SMT-решателей.

• 3.    Производится интерпретация результата.

В языке UFLRA разрешается составлять выражения, состоящие из действительных чисел и арифметических действий над ними, использовать кванторы ∃ и ∀ , объединять переменные в упорядоченные множества произвольной длины (пары, тройки, и т. д.), а также вводить собственные неинтерпретируе-мые типы данных.

Первый этап кодирования задачи синтеза СЗИ на языке SMT-решателя заключается в определении домена дискурса D . В большинстве случаев D представляет собой упорядоченное множество, имеющее в качестве своих элементов значения, каждое из которых описывает определенное свойство или характеристику защищаемой АС. Благодаря возможности использования неинтерпретируемых типов характеристики АС не обязательно должны иметь численные значения. Таким образом, отдельно взятое значение d ∈ D описывает текущее состояние защищаемой АС.

Угрозы АС также могут быть описаны значением из домена дискурса, так как для каждой угрозы можно определить, подвержена ли ей защищаемая АС в текущем состоянии d или нет. Для выражения зависимостей между отдельными угрозами на элементы d можно накладывать дополнительные ограничения, учитывающие значения нескольких свойств одновременно.

Наконец, механизмы защиты кодируются в виде функций с сигнатурой M:D → D, так как это отвечает мысли о том, что применение каждого механизма изменяет состояние системы. Благодаря тому, что механизм защиты в предлагаемой модели является функцией, а не значением, возможности определения свойств механизмов защиты значительно расширяются. Так, например, использование каких-либо двух механизмов может давать кумулятивный эффект или, наоборот, снижать эффективность третьего механизма.

Задав принципы кодирования составляющих задачи синтеза, определим и что является ее решением. Результатом синтеза системы защиты информации является множество функций М , такое, что при применении всех функций из этого множества к начальному состоянию АС d ₀ будет достигнуто состояние оптимальной защиты. Это определение исходит из посылки, что композиция любых двух функций из M коммутативна. В большинстве случаев это условие соблюдается, однако при наличии в модели особенно сложных средств защиты может начать играть роль порядок их применения для достижения искомого состояния. В этом случае решением задачи синтеза будет являться не множество средств защиты, а однонаправленный граф, узлам которого соответствуют средства защиты из множества M , а ребра определяют порядок применения средств защиты к защищаемой АС. Легко заметить, что последний случай является обобщением первого – элементы множества можно связать в граф таким образом, что каждый узел будет иметь не более чем два ребра, а свойство направленности ребер графа здесь не играет роли.

Формально задача синтеза системы защиты АС с помощью SMT-решателя требует следующие входные данные:

• 1.    Функция защиты φ _защ, устанавливающая соотношение между исходным состоянием защищаемой АС и состоянием, которое необходимо достичь.

• 2.    Множество функций φ _i ( d_i , d_i+ 1), описывающих применяемые механизмы защиты. Как и в случае с φ _защ, эффект от механизма защиты выражается в виде соотношения между предыдущим и следующим состояниями АС.

Обозначим ф с_з = ф 1 л ... лф n . Тогда конечное выражение, подающееся на вход SMT-решателя, будет иметь вид

∃ φ_соед ( d ₁ , ..., d_n ) ∀ d _вх , d _вых , d ₁ , ..., d_n : ( φ_сз ( d ₁ ∧ φ_соед ( d ₁ , ..., d_n ) ) → φ_защ ( d _вх , d _вых ) ,

., d_n ) ∧ (1)

где φ _соед – вспомогательная функция-ограничение, играющая роль композиции для функций φ _i .

Язык теории UFLRA, однако, не позволяет использовать функции в подкванторных выражениях. Чтобы решить эту проблему, вводятся дополнительные целочисленные переменные l_i в количестве, равном мощности множества M средств защиты. Эти переменные кодируют позиции узлов в графе и их связи с другими узлами. Эта мысль выражается ограничением 0 ≤ l_d ≤ N . Таким образом, квантифицированное выражение ∃φ _соед: ... может быть заменено на ∃ l_d , ..., l_d : ..., что удовлетворяет требованиям SMT-решателя.

К выражению (1) необходимо также добавить еще одно ограничение – требование отсутствия циклов в графе. Это ограничение имеет вид l _d <  l _d <  ... <  l _d и добавляется к выражению (1) с помощью конъюнкции.

Выражение синтеза передается на вход SMT-решателя, который подбирает значения переменных l_i , удовлетворяющие всем заданным ограничениям. Эти значения представляют собой решение задачи синтеза СЗИ в АС – последовательность действий, которые необходимо осуществить, чтобы достичь желаемого состояния системы, причем это решение будет использовать минимально необходимое число средств защиты. Если добавить полученное решение в выражение (1) в виде дополнительных ограничений, можно получить новое решение, отличающееся от предыдущего. Повторение этого процесса позволит найти все возможные решения задачи синтеза для данной АС.

Расширив домен дискурса D свойством, характеризующим оптимальность СЗИ с нужной нам точки зрения (например, соотношения цена/качество или производительность/ качество), и задав отношение порядка между элементами D, можно трансформировать задачу синтеза в задачу поиска локального минимума или максимума. Современные SMT-решатели обладают функционалом для авто- матического решения задач такого типа, то есть от пользователя даже не требуется дополнительного кодирования ограничений, выражающих искомые экстремумы.

В заключение необходимо отметить, что несмотря на свою эффективность описанный подход обладает и недостатками:

• 1.    Формальное описание механизмов защиты является нетривиальной задачей и требует от пользователя определенных навыков.

• 2.    Данный метод нельзя применять для автоматического синтеза СЗИ, так как задача удовлетворения ограничений, к которой сводится задача синтеза, является неразрешимой в общем случае. На практике имеет место тонкая подстройка параметров SMT-решателя, что требует участия человека.

• 3.    Для получения окончательного решения необходима дополнительная обработка результатов, полученных от решателя.

• 4.    Метод имеет экспоненциальную сложность по времени в зависимости от мощности в худшем случае.