Система типов безопасности
Система типов безопасности (англ. 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} (в соответствии с правилом для условного оператора), то есть программа является «не типизируемой».
Корректность системы типов безопасности можно сформулировать неформально так: если программа P корректно типизирована, то P удовлетворяет свойству невмешательства. Первое формальное доказательство корректности системы типов безопасности для детерминированного императивного языка программирования, исходя из невмешательства, было дано Волпано, Смитом и Ирвайн[1].
Примечания
Литература
- Fred B. Schneider, Greg Morrisett, and Robert Harper. A Language-Based Approach to Security.
- Andrei Sabelfeld, Andrew C. Myers. Language-Based Information-Flow Security.