Глава 7. Динамический мониторинг

В этой главе рассматривается вопрос интегральной проверки соответствия поведения ядра Linux требованиям модели политики безопасности управления доступом (например, МРОСЛ ДП-модели). Соответствие проверяется посредством сверки результатов реальных операций по запросу доступа при помощи системных вызовов ядра ОС с правилами предоставления доступа (или отказа в доступе) модели политики безопасности. Для этого во время выполнения приложений (программ пользовательского пространства) в динамике трассируются системные вызовы, фиксируются их параметры и результаты. Далее на основе полученных данных воспроизводится обработка запросов доступа в ядре на формальной функциональной спецификации на языке Event-B (ФСП). На функциональной спецификации проверяется допустимость результатов обработки системного вызова.

Данный подход наиболее целесообразно применять в рамках выполнения требований класса доверия «Тестирование» ГОСТ Р ИСО/МЭК 15408-3, который требует проведения тестирования ОО на соответствие функциональной спецификации (см. семейство доверия ATE_COV «Покрытие»). Автоматический сбор трассы выполнения и проведение проверки её соответствия формальной функциональной спецификации на языке Event-B позволяет избавиться от необходимости вручную вычислять ожидаемый результат каждой операции, что, в свою очередь, даёт возможность значительно повысить число и разнообразие проводимых тестов. Сбор информации о покрытии различных ситуаций в формальной функциональной спецификации также позволяет автоматизировать оценку покрытия интерфейсов функций безопасности, что является еще одним требованием семейства доверия ATE_COV «Покрытие».

7.1. Управление доступом в ядре ОС Linux

Предварительно рассмотрим несколько подробнее схему работы ядра ОС в случае, когда необходимо провести анализ возможности предоставления того или иного вида доступа к некоторому ресурсу. Это позволит нам обосновать утверждение, что динамический мониторинг является необходимым этапом процесса верификации механизма управления доступом в ОССН.

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

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

Подобная ошибка может произойти по разным причинам. Первая причина — ошибка обусловлена некорректной функциональностью модуля LSM. Это означает, что модуль неправильно реализует модель политики безопасности. Стадия дедуктивной верификации исходного кода модуля LSM, описанная в главе 6, нужна для того, чтобы исключить подобные ошибки. Вторая причина ошибки — ядро в какой-то момент не вызывает интерфейс LSM [88–90], хотя это необходимо сделать. Либо LSM-интерфейс может быть не достаточно полным, в нем может не хватать некоторых функций для проверки определенных ситуаций [91, 92].

Помимо этого, стоит отметить, что дедуктивная верификация это статический анализ кода. Его точность зависит, в том числе, от самих инструментов анализа и от того, насколько модели, лежащие в основе анализа, полны и адекватны. Так, на текущий момент инструменты дедуктивной верификации (Frama-C и AstraVer) не моделируют стек (см. главу 6). В предусловиях к функциям нет требования на размер доступной памяти в стеке, необходимой для корректной работы функции. Также не моделируются еще некоторые ошибки, например не различается память, доступная только на чтение или на запись и чтение. Дедуктивная верификация анализирует тексты исходных кодов, в то время как на процессоре выполняется бинарный код, который был получен из исходного посредством компиляции. То есть мы не имеем гарантий того, что бинарный код семантически эквивалентен исходному [93]. Все перечисленные моменты являются ограничениями дедуктивной верификации и являются аргументами в пользу необходимости интегральной проверки соответствия поведения ядра ОС требованиям модели политики безопасности управления доступом в динамике, на основе анализа трасс выполнения системных вызовов.

Для динамической проверки необходим тестовый набор, который воспроизводит разнообразные ситуации, связанные с запросами на доступ. Помимо этого, должен быть реализован «тестовый оракул» для проверки соответствия результатов работы системы ее функциональной спецификации как минимум в той части, которая определяется моделью политики безопасности управления доступом. В данной работе мы не рассматриваем вопрос построения такого тестового набора и вопрос критериев его полноты. Далее описывается сам метод динамической проверки, т. е. рассматриваются два вопроса: как получить данные о поведении ОО (трассу) и как выполнить динамический анализ трассы, т. е. как должен быть построен тестовый оракул.

7.2. Схема работы анализа

Схема работы мониторинга разбивается на две последовательных стадии — сбора информации о поведении ОО и ее анализ.

На первой стадии осуществляется сбор трассы выполнения ядра Linux с модулем защиты в отдельную базу событий в человекочитаемом формате. В ОС в этот момент либо запускается специальный тестовый набор, либо система работает в стандартном режиме (работают некоторые пользовательские приложения). Важно уточнить, что ядро ОС в этот момент работает в одноядерном режиме, без поддержки мультипроцессорности и без режима вытеснения.

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

Далее в трассу собирается информация об обработке системных вызовов ядром. Для работы с тестовым набором собирается информация только о системных вызовах от тестов, в ином случае рассматриваются все процессы. В трассу попадает информация об аргументах системного вызова, о результатах его обработки ядром с кодом возврата. Дополнительно в трассу может записываться информация, которая помогает отобразить аргументы системных вызовов в вид, пригодный для использования при сравнении с ФСП.

В момент завершения анализа в трассу записывается информация о глобальном состоянии ядра аналогично тому, как это делается при старте анализа.

На второй стадии осуществляется анализ собранной трассы с целью выявления в ней ошибок предоставления доступа. Для этого обработка системных вызовов из собранной трассы перепроверяется на ФСП, т.е. обработка системных вызовов воспроизводится на ФСП. Результаты обработки системных вызовов в ядре и в спецификации сверяются. Здесь необходимо помнить, что в ФСП (см. главу 5) задаются события старта и конца обработки для каждого системного вызова, вводятся промежуточные события между событиями Event-B спецификации МРОСЛ ДП-модели и порядок их выполнения. Событие начала обработки системного вызова принимает на вход аргументы системного вызова. ФСП разрабатывается так, что при заданных аргументах системного вызова и состоянии системы из каждого события существует не более одного возможного следующего события обработки системного вызова, не являющегося событием возврата кода ошибки. Это означает, что существует не более одного пути в графовом представлении цепочки событий обработки системного вызова из начального события системного вызова в его конечное событие. В момент начала анализа трассы состояние формальной функциональной спецификации инициализируется в соответствии с записанной информацией о состоянии ядра ОС на момент старта мониторинга. В случае, если такая информация не собиралась, используется стандартная инициализация состояния спецификации.

Далее последовательно анализируются системные вызовы из собранной трассы. Воспроизведение обработки системного вызова на ФСП выглядит следующим образом:

в событие начала обработки данного системного вызова поступают аргументы с реальной системы (берутся из трассы). В соответствии со спецификацией вычисляется следующее событие, обновляется состояние ФСП;
если обработка следующего события оказалась невозможной, так как его охранные условия не выполнены, то считается, что с точки зрения ФСП доступ к ресурсу в результате обработки системного вызова не мог быть предоставлен;
если охранные условия для следующего события выполнены и оно не является уточняющим для вышележащего слоя спецификации, то его обработка происходит так же, как в пункте 1;
если охранные условия для следующего события выполнены и оно является уточняющим для вышележащего слоя спецификации, то происходит проверка охранных условий всех вышележащих уровней уточнений. В случае успешного прохождения последней состояние спецификации обновляется в соответствии с правилами перехода системы из состояния в состояние. Если же условия не выполнены, то считается, что доступ к запрашиваемому ресурсу не мог быть предоставлен в соответствии с моделью политики безопасности;
в случае, если обработка системного вызова на ФСП дошла до события завершения системного вызова и охранные условия для него были выполнены, то считается, что с точки зрения ФСП и модели политики безопасности доступ к ресурсу может быть предоставлен (системный вызов может быть успешно обработан).

Следующим шагом сверяются результаты (возвращаемые коды) обработки системного вызова из трассы и из ФСП :

когда оба результата положительны (нет ошибки, доступ запрещен), осуществляется переход к анализу следующего системного вызова из трассы;
когда результат в трассе отрицательный (доступ запрещен), а на ФСП положительный (доступ разрешен), то рассматривается код ошибки системного вызова. В коде ошибки содержится информация о причине неудачи обработки системного вызова. После рассмотрения «расхождения» на ФСП происходит возврат к модельному состоянию «до начала обработки» данного системного вызова (на момент вызова события его обработки), и начинается обработка следующего системного вызова из трассы. Если причина неудачи обработки системного вызова в ядре Linux заключается в:
- нехватке ресурсов физической машины, то не производится никаких дополнительных действий;
- в «некорректных» аргументах системного вызова, то с большой вероятностью это сигнализирует о том, что ФСП недостаточно полна. Данное расхождение записывается в журнал «аномалий»;
- нехватке разрешений (для доступа), то с большой вероятностью это сигнализирует о наличии ошибки в ядре и модуле безопасности ядра (слишком сильное ограничение). Данное расхождение записывается в журнал «аномалий»;
когда результат в трассе положительный, а на ФСП отрицательный, данная ситуация свидетельствует об ошибке в ядре и модуле безопасности ядра. При этом расхождении дальнейший анализ трассы теряет смысл. Анализ останавливается и сигнализирует о найденной ошибке предоставления доступа;
когда оба результата отрицательны (ошибка, доступ разрешен), осуществляется переход к анализу следующего системного вызова из трассы;
если анализ трассы дошел до ее конца, то производится сверка состояний спецификации и ядра. Расхождения записываются в журнал «аномалий».

Результатом работы анализа является журнал «аномалий», в котором содержатся пункты расхождения поведения реальной системы с ФСП. Данные журнала анализируются ручным образом. По результатам выявляются ошибки либо в исходном коде ядра и модуля безопасности, либо в ФСП.

В этом разделе была рассмотрена общая схема работы анализатора, состоящая из двух последовательных этапов: сбор трасс и их анализ на ФСП. Далее будут рассмотрены механизмы осуществления данных этапов.

7.3. Сбор трасс ядра

Для мониторинга ядра Linux существует большое число инструментов [94–100]. Одним из наиболее удобных является SystemTap. Он позволяет относительно легко логировать, как обработку системных вызовов, так и иные события на работающем ядре Linux.

SystemTap поддерживает специальный язык (похожий на скриптовый) для описания точек мониторинга и сбора информации о работающей системе. При этом инструментом предоставляется возможность обращения к практически любой информации в точке мониторинга: глобальные и локальные переменные, стек вызовов и др.

Описание скрипта мониторинга преобразуется инструментом в код загружаемого модуля ядра Linux на языке Си. Для мониторинга данный код компилируется и динамическим образом загружается в ядро, что не требует перезагрузки системы. Инструмент предоставляет наиболее богатые возможности описания точек мониторинга, если ядро Linux собрано с отладочной информацией, что ведет к дополнительным накладным расходам и частично объясняет разбиение анализа на два последовательных этапа.

SystemTap имеет много уже готовых описаний точек мониторинга (probe points). Например, для мониторинга большинства системных вызовов, их аргументов и результатов их обработки на одноядерной машине возможно использовать простой скрипт:

Листинг 7.1. Скрипт мониторинга системных вызовов SystemTap

probe syscall.* {
  printf("%s: %s(%s)",
    execname(), name, argstr)
}
probe syscall.*.return {
  printf("res: %s\n", retstr)
}

Пример выводимого лога приведен в табл. 7.1.

Для воспроизведения поведения ядра на ФСП в трассу необходимо собирать информацию об аргументах системных вызовов, результатах их обработки, дополнительную информацию, которая позволила бы отображать состояние структур данных ядра на состояние структур данных спецификации, глобальное состояние структур данных ядра на момент начала и конца мониторинга.

В ядре Linux из модулей могут напрямую вызываться функции системных вызовов (то есть, условно говоря, системный вызов приходит не от приложения, а от самого ядра) и таким образом происходит вмешательство в пользовательское окружение со стороны ядра, которое в данном случае может рассматриваться как действие привилегированного процесса. Сама по себе такая ситуация происходит достаточно редко и по вполне определенным причинам (например, coredump, OOM Killer). В том случае, когда мы контролируем тестовый набор, подобного рода события могут не обрабатываться специальным образом, так как они заранее известны.

Таблица 7.1. Пример выводимого лога скрипта мониторинга системных вызовов

Процесс	Системный вызов	Аргументы	Код возврата
konsole	write	95, «\0», 1	1
ksmserver	ioctl	28, 21531, 0x7fffab1c9ec4	0
ksmserver	read	28, 0x5626d6785938, 40	40
konsole	lseek	94, -2147482516, SEEK_SET	-22 (EINVAL)
konsole	write	2, «HistoryFile::add.seek: Invalid argument», 40	40
konsole	lseek	93, 22447548, SEEK_SET	22447548
konsole	write	93, «l\004\0\200», 4	4

7.4. Механизм воспроизведения трасс на Event-B спецификации

Инструменты для работы с Event-B спецификациями [44] не предоставляют возможности проверки допустимости определенной последовательности событий. Для этого требуется интерпретатор спецификации. Добиться аналогичного результата возможно, если осуществить трансляцию Event-B спецификации в нотацию одного из интерпретируемых или исполняемых языков.

Существующие трансляторы Event-B в исполняемый код [101– 103] достаточно узкоспециализированы и в полной мере возможностей, необходимых для воспроизведения трасс, не предоставляют.

Для анализа трассы системных вызовов на воспроизводимость на ФСП используется разработанный авторами транслятор Event-B спецификации в язык Python. Правила трансляции операций аналогичны тем, которые используются в вышеприведенных работах. При трансляции задаются две модели управления: когда на вход подается трасса, где уже полностью записаны переходы между событиями спецификации, и вторая модель — когда осуществляется подбор следующего события из текущего (для ФСП).

Статическая часть спецификации Event-B транслируется в систему типов (отображения, множества, перечисления), константы, а динамическая часть в функции. Переменные состояния спецификации в соответствии с их инвариантами транслируются в глобальные переменные Python:

Листинг 7.2. Переменные состояния спецификации на Event-B

variables
  CurrUnion
  SubjectUser
invariants
  @CurrUnionType
    CurrUnion ⊆ Union
  @SubjectUserType
    SubjectUser ∈ Subjects → UserAccs

Листинг 7.3. Трансляция переменных состояния в Python

CurrUnion = set()
SubjectUser = dict()

Инварианты спецификации транслируются в функции проверки глобальных переменных, которые вызываются после каждого события спецификации:

Листинг 7.4. Инварианты Event-B спецификации

invariants
  @CurrUnionPartition
    partition(CurrUnion, UserAccs, Subjects, Entities, Roles)
  @UserAccsAreNotEmpty
    UserAccs ≠ ∅
  @SubjectsAreNotEmpty
    Subjects ≠ ∅
  @SubjectAccessesType
    SubjectAccesses ∈ Subjects → (Entities ↔ Accesses)

Листинг 7.5. Трансляция инвариантов в Python

@invariant
def CurrUnionPartiton() -> bool:
  return (CurrUnion == UserAccs | Subjects | Entities) and \
         not (UserAccs & Subjects) and \
         not (UserAccs & Entities) and \
         not (Subjects & Entities)
@invariant
def UserAccsAreNotEmpty() -> bool:
  return bool(UserAccs)
@invariant
def SubjectsAreNotEmpty() -> bool:
  return bool(Subjects)
@invariant
def SubjectAccessesType() -> bool:
  return all(map(lambda s: s in Subjects and all(map(lambda j: j[0] in Entities and type(j[1]) is Accesses, SubjectAccesses[s])), SubjectAccesses))

События транслируются в соответствующие функции. Охранные условия события транслируются в проверки внутри функции, а действия в событии преобразуются в операции обновления глобальных переменных. Уровни уточнений реализуются через механизм наследования в языке Python.

Листинг 7.6. Пример транслируемых Event-B событий

event delete_user
  any user
  where
    @grd1 user ∈ UserAccs
    @grd2 ∀ s · s ∈ Subjects ⇒ SubjectUser(s) ≠ user
  then
    @act1 CurrUnion := CurrUnion \ {user}
    @act2 UserAccs := UserAccs \ {user}
end
event create_object
  any subject object parent name dLabel mountPoint depth
  where
    @grd1 object ∈ Union \ CurrUnion
    @grd2 subject ∈ Subjects
    @grd3 parent ∈ Containers
    @grd4 parent ↦ WriteA ∈ SubjectAccesses(subject)
    @grd5 name ∈ Names
    @grd6 ∀ e · e ∈ dom(EntityNames) ⇒ parent ↦ name ∉
      EntityNames(e)
    @grd7 mountPoint ∈ Containers
    @grd8 dLabel ∈ BOOL
    @grd9 ∀ e · e ∈ dom(EntityNames) ∧ parent ∈ dom(EntityNames(e))
      ⇒ Direct(e) = dLabel
    @grd10 dLabel = TRUE ⇒ Direct(parent) = TRUE
    @grd11 dLabel = TRUE ⇒ mountPoint = Root
    @grd12 dLabel = FALSE ∧ Direct(parent) = FALSE
      ⇒ mountPoint = EntityMP(parent)
    @grd13 dLabel = FALSE ∧ Direct(parent) = TRUE ⇒ mountPoint =
      parent
  then
    @act1 CurrUnion := CurrUnion ∪ {object}
    @act2 Entities := Entities ∪ {object}
    @act3 Objects := Objects ∪ {object}
    @act4 EntityNames(object) := {parent ↦ name}
    @act5 Direct(object) := dLabel
    @act6 EntityMP(object) := mountPoint
end

Листинг 7.7. Пример результата трансляции Event-B событий в Python

@event
def delete_user(user):
  global CurrUnion
  global UserAccs
  assert user in UserAccs, "grd1"
  assert all(map(lambda s: SubjectUser[s] != user, Subjects)), "grd2"
  CurrUnion.discard(user)
  UserAccs.discard(user)
@event
def create_object(subject, object: Union, parent, name: Names, dLabel: bool, mountPoint):
  global CurrUnion
  global Entities
  global Objects
  global EntityNames
  global Direct
  global EntityMP
  assert object not in CurrUnion, "grd1"
  assert subject in Subjects, "grd2"
  assert parent in Containers, "grd3"
  assert (parent, WriteA) in SubjectAccesses[subject], "grd4"
  assert all(map(lambda e: (parent, name) not in EntityNames[e], dom(EntityNames))), "grd6"
  assert mountPoint in Containers, "grd7"
  assert all(map(lambda e: not (parent in dom(EntityNames[e])) or Direct[e] == dLabel, dom(EntityNames))), "grd9"
  assert not(dLabel == True) or Direct[parent] == True, "grd10"
  assert not(dLabel == True) or mountPoint == Root, "grd11"
  assert not(dLabel == False and Direct[parent] == False) or (mountPoint == EntityMP[parent]), "grd12"
  assert not(dLabel == False and Direct[parent] == True) or (mountPoint == parent), "grd13"
  CurrUnion.add(object)
  Entities.add(object)
  Objects.add(object)
  EntityNames[object] = {(parent, name)}
  Direct[object] = dLabel
  EntityMP[object] = mountPoint

7.5. Интеграция дедуктивной верификации и динамического мониторинга при верификации модуля безопасности

За рамками данной главы остается вопрос трансляции ACSL спецификаций в проверки времени выполнения кода (assertions).

Дедуктивная верификация основывается на следующих предположениях.

Предположение о корректной работе компилятора. Процесс дедуктивной верификации доказывает соответствие исходного кода требованиям. В дальнейшем исходный код преобразуется транслятором/компилятором в бинарный. Дедуктивная верификация опирается на то предположение, что трансляция кода в бинарный осуществляется корректным образом. Отталкиваясь от этого предположения, можно сказать, что требования по безопасности соблюдаются и на бинарном коде, т. е. том коде, что непосредственно выполняется на процессоре.
Предположение о корректной работе инструментов дедуктивной верификации. Ошибки в инструментах дедуктивной верификации не являются чем-то исключительным и могут приводить к разнообразным последствиям. Большинство из них удается выявить на этапе работы с инструментами, так как они имеют видимые проявления. Например, инструменты не запускаются на коде, порождаемые логические формулы не доказываются. К сожалению, нельзя исключать возможности ошибок в инструментах, которые приводили бы к тому, что порождаемые условия верификации доказываются, хотя на самом этого происходить не должно (по причине ошибки в коде/требованиях).
Предположение о полноте спецификаций внешних интерфейсов модуля (интерфейсов ядра). Как правило, размер модуля безопасности ядра ограничивается несколькими тысячами строк кода. Размеры сердцевины ядра, как и остальных модулей ядра, используемых при работе, в сумме могут давать несколько миллионов строк кода [104]. Модуль безопасности ядра взаимодействует с сердцевиной посредством интерфейса LSM (сердцевина \rightarrow модуль) и через экспортируемые функции ядра (модуль \rightarrow сердцевина). Доказательство корректности экспортируемых ядром функций не представляется возможным, так как для этого, по меньшей мере, потребовалось бы доказательство корректности сердцевины ядра. Соответственно, для задействованных модулем функций ядра составляются спецификации без их доказательства, для функций интерфейса LSM составляются спецификации, описывающие контекст их вызова, которые также остаются без доказательства. В данных спецификациях могут быть ошибки, отсутствие полноты описания возможных особенностей контекста вызова. В случае подобной ошибки. например, в предусловиях к интерфейсу LSM в коде модуля также могут обнаружится ситуации, обработка которых не предусматривалась. В таком случае дедуктивная верификация покажет, отталкиваясь от неполных/ошибочных предположений, полную корректность кода.

Учитывая отсутствие гарантий выполнения перечисленных выше предположений и принимая во внимание ограничения подхода, можно в дополнение к дедуктивной верификации осуществлять проверки в момент выполнения кода. Так, например, если оттранслировать предусловия к интерфейсу LSM в проверки времени выполнения (assertions), то это позволит в динамике проверить спецификации, при отсутствии возможности их доказать. Таким образом повышается общий уровень доверия к тем исходным предположениям, на основе которых осуществлялась дедуктивная верификация.

Для реализации этой идеи можно воспользоваться расширением E-ACSL [105] для платформы Frama-C, где на основе исходных кодов и спецификаций к ним на языке ACSL порождает новый исходный код с проверками времени выполнения. Расширение E-ACSL работает лишь с подмножеством языка ACSL [106]. Так, например, невозможно отобразить леммы и аксиомы в исполняемый код по очевидным причинам. Для моделирования работы со спецификационными типами чисел (неограниченными) используется библиотека libgmp, а также собственная библиотека для отслеживания состояний памяти [107].

К сожалению, существующие инструменты для подобного рода трансформации спецификаций недостаточно зрелы для использования на коде ядра Linux и поддерживают в полной мере лишь некоторое подмножество E-ACSL. В инструментах реализована пока далеко не полная функциональность из заявленной в E-ACSL.

Данный вид анализа важен и должен быть интегрирован в систему тестирования модуля безопасности по мере развития средств верификации. Одним из открытых вопросов его интеграции остается трансляция логических утверждений, описывающих состояние памяти. Для ядра Linux это требует гораздо больших усилий, чем при работе с приложением пользовательского уровня. Одним из решений могло бы быть использование уже существующих динамических средств проверок доступа к памяти kasan, kmsan. Однако их использование не позволяет в полной мере транслировать все допустимые языком E-ACSL логические утверждения на память в проверки времени выполнения и не позволяет обращаться к состояниям памяти по временным меткам.