Система типов безопасности
Система типов безопасности (англ. security type system) — разновидность системы типов в информатике, представляющая собой синтаксическую структуру, определяющую набор правил для присвоения компонентам программы специальных свойств безопасности. Такие системы направлены на обеспечение безопасности программ посредством управления потоком информации, то есть проверяют соответствие переменных, функций и других объектов программного кода заданным уровням безопасности. Главная цель системы типов безопасности — гарантировать, что программа удовлетворяет установленным правилам и принципу невмешательства, то есть отсутствие недопустимого взаимодействия между различными уровнями секретности данных[1]. Системы типов безопасности относятся к инструментам языково-ориентированной безопасности и тесно связаны с контролем потоков информации и политиками информационной безопасности. Система типов безопасности позволяет выявить нарушения конфиденциальности или целостности в программе, то есть определить, соответствует ли поведение программы принятой политике потоков информации.
Простая политика контроля потоков информации
Рассмотрим пример с двумя пользователями — A и B. В программе выделяются следующие «классы безопасности» (КБ):
КБ = {∅, {A}, {B}, {A,B}}, где ∅ — пустое множество.
Политика потоков информации определяет допустимые направления перемещения информации, что зависит от правил чтения или записи данных. В этом примере учитываются операции чтения (конфиденциальность). Разрешённые потоки имеют вид:
→ = {({A}, {A}), ({B}, {B}), ({A,B}, {A,B}), ({A,B}, {A}), ({A,B}, {B}), ({A}, ∅), ({B}, ∅), ({A,B}, ∅)}
Иными словами, информация может переходить только на «более строгий» уровень конфиденциальности. Оператор объединения (⊕) выражает, какие классы безопасности могут читать данные других, например:
{A} ⊕ {A,B} = {A}— только класс {A} может читать и из {A}, и из {A,B};{A} ⊕ {B} = ∅— ни {A}, ни {B} не могут читать одновременно эти классы.
Аналогично это выражается через пересечение (∩) классов безопасности.
Политика контроля потоков может быть проиллюстрирована с помощью диаграммы Хассе. Корректная политика должна формировать решётку — то есть иметь наибольшую нижнюю и наименьшую верхнюю грань (для любых двух классов всегда можно определить их комбинацию). В случае контроля целостности направление потоков информации инвертируется, то есть политика разворачивается противоположным образом.
Политика потоков информации в системе типов безопасности
Имея заданную политику, разработчик может присваивать компонентам программы соответствующие классы безопасности. Применение системы типов безопасности обычно сочетается с компилятором, который автоматически проверяет корректность потоков информации в программах по заданным правилам. Для демонстрации рассмотрим простой псевдокод, который использует приведённую ранее политику:
if y{A} = 1 then x{A,B} := 0 else x{A,B} := 1
Здесь проверяется равенство переменной y, обладающей классом безопасности {A}. От значения этой переменной зависит переменная x с менее строгим классом ({A,B}). Это означает, что информация из {A} может утечь в {A,B}, что нарушает политику конфиденциальности. Такое нарушение должно быть обнаружено системой типов безопасности.
Пример
Проектирование системы типов безопасности требует определения функции (также называемой средой безопасности), сопоставляющей переменным их классы или типы безопасности — функцию Γ, такую что Γ(x) = τ, где x — переменная, а τ — её тип. Присвоение классов безопасности (или «суждение») оформляется так:
- Для операций чтения:
Γ ⊢ e : τ. - Для операций записи:
Γ ⊢ S : τ cmd. - Константам можно присвоить любой тип.
Декомпозиция анализа программы может быть записана в виде дробей: предпосылки1 ... предпосылкиnвывод. Разбивая программу на тривиальные проверяемые части, можно по известным правилам выводить допустимые типы для более сложных конструкций.
Правила
В основе системы типов лежат правила, определяющие разложение программы и процедуру проверки типов. В примере выше есть условный оператор и два присваивания. Правила для этих случаев выглядят следующим образом:
| Присваивание: |
|
, при условии τ2 ⊑ τ1
|
| Условный оператор: |
|
, при условии τ ⊑ τ1, τ2
|
Применяя правила к рассмотренной программе, получаем:
| 3 | Γ(y) = {A}
|
Γ(x) = {A,B} cmd, Γ ⊢ 0 : {A,B}
|
Γ(x) = {A,B} cmd, Γ ⊢ 1 : {A,B}
|
| 2 | Γ ⊢ y = 1 : {A}
|
Γ ⊢ x := 0 : {A,B} cmd
|
Γ ⊢ x := 1 : {A,B} cmd
|
| 1 | Γ ⊢ if y = 1 then x := 0 else x := 1 : Не типизируемо
| ||
Система типов фиксирует нарушение политики на втором уровне, где происходит чтение переменной класса {A}, после чего записываются значения с менее строгим классом {A,B}. Формально: {A} ⋢ {A,B}, {A,B} (в соответствии с правилом для условного оператора), то есть программа является «не типизируемой».
Параллельные и многопоточные вычисления
Формальные системы типов для параллельных и многопоточных вычислений используют расширенные структуры суждений типизации для обеспечения изоляции и принципа невмешательства.
Для контроля эффектов и разрешений, а также управления ветвлением и синхронизацией, применяется суждение вида Γ; a ⊢ t : τ, где Γ — окружение типов, a — эффект (например, ϵ для отсутствия эффектов или ocap для изоляции), t — терм, а τ — тип. Правило ветвления (оператор async) типизирует тело параллельной задачи в строгом окружении ocap, что гарантирует строгую изоляцию параллельных задач друг от друга. Правило синхронизации (оператор finish) обеспечивает безопасную точку слияния потоков, требуя корректности терма в текущем окружении и возвращая тип null.
Для предотвращения несанкционированного обмена данными через разделяемое изменяемое состояние применяются системы с временными метками. Ограничение на запись (subtiming) требует, чтобы временная метка записываемого значения предшествовала метке ссылки. Это запрещает дочернему потоку записывать свои локальные значения в родительский контейнер, делая их недоступными для параллельных потоков. В точке объединения потоков (оператор par) применяется операция backtiming: система типов перештамповывает результат выполнения временной меткой родительского потока, чтобы он мог безопасно унаследовать значения завершённых подзадач[2].
Структурный контроль потоков информации позволяет строго доказать невмешательство на уровне зависимостей данных. Для этого используются суждения вида Δ; Γ ⊢ e : A | φ, где Δ — переменные зависимостей в области видимости, а φ — набор зависимостей (уровней безопасности). Данное исчисление с помощью полиморфизма зависимостей формализует гарантию того, что выходные данные не зависят от защищённых входных аргументов[3].
Корректность
Корректность системы типов безопасности можно сформулировать неформально так: если программа P корректно типизирована, то P удовлетворяет свойству невмешательства. Первое формальное доказательство корректности системы типов безопасности для детерминированного императивного языка программирования, исходя из невмешательства, было дано Волпано, Смитом и Ирвайн[1].
Практическое применение
Реализации в языках программирования
В современных языках программирования системы типов безопасности применяются для статического контроля потоков информации. В частности, для языка Rust реализован ряд библиотек, обеспечивающих такой контроль без модификации стандартного компилятора:
- Cocoon — библиотека статического контроля потоков информации на основе типов. Использует систему типов и процедурные макросы для создания системы эффектов, обеспечивающей невмешательство[4].
- Carapace — преемник библиотеки Cocoon (2025 год)[5].
- Filament — статическая библиотека в стиле Деннинг (Denning-style). Использует вывод типов для контроля явных потоков и макрос
pc_block!для отслеживания неявных потоков через метку счётчика команд на этапе компиляции[5].
Машинное обучение
Для задач вывода типов применяются методы машинного обучения. В частности, система TYGR использует графовые нейронные сети (GNN) для анализа бинарных файлов. На наборах данных архитектуры x64 общая точность предсказания типов достигает 76,6 %, а точность определения структур — 45,2 %[6].
Несмотря на эффективность, текущие подходы на базе машинного обучения имеют ряд ограничений. Точность предсказания ограничена из-за проблем с редкими типами данных. Кроме того, алгоритмам сложно определять границы между соседними структурами, а сложности с вычислением целей косвенных переходов приводят к тому, что некоторые участки кода остаются неисследованными[6].
Нормативное регулирование
Согласно приказу ФСТЭК № 117, вступившему в силу 1 марта 2026 года, применение формальных систем контроля потоков в России требует обоснования на основе риск-ориентированного подхода и актуальной модели угроз[7].
Примечания
Литература
- Fred B. Schneider, Greg Morrisett, and Robert Harper. A Language-Based Approach to Security.
- Andrei Sabelfeld, Andrew C. Myers. Language-Based Information-Flow Security.
- Vilem-Benjamin Liepelt, Danielle Marshall, Dominic Orchard, Michael Vollmer, Vineet Rajani. On Graded Coeffect Types for Information-Flow Control — Lecture Notes in Computer Science, Vol 15500. Springer — 2026[1].
- Alex Coleman, Hrutvik Kanabar, Vineet Rajani. A graded modal approach to relaxed semantic declassification — IEEE Computer Security Foundations Symposium (CSF) — 2025[1].
- Marco Vassena, Alejandro Russo, Deepak Garg, Deian Stefan, Vineet Rajani. From Fine- to Coarse-Grained Dynamic Information Flow Control and Back — Foundations and Trends in Programming Languages — 2023[1].
- ↑ 1 2 3 Publications. Vineet Rajani. Дата обращения: 26 августа 2026.