Система охранного типа - Security type system

В Информатика, а система типов можно описать как синтаксическую структуру, которая содержит набор правил, которые используются для присвоения свойства типа (int, boolean, char и т. д.) различным компонентам компьютерной программы, таким как переменные или функции. А система охранного типа работает аналогичным образом, только с упором на безопасность компьютерной программы, через поток информации контроль. Таким образом, различным компонентам программы присваиваются типы защиты или метки. Цель такой системы состоит в том, чтобы в конечном итоге иметь возможность проверить, что данная программа соответствует правилам системы типов и удовлетворяет невмешательство. Системы охранного типа - это один из многих методов безопасности, используемых в области языковая безопасность, и тесно связан с информационными потоками и политиками информационных потоков.

Проще говоря, система типов безопасности может использоваться для обнаружения каких-либо нарушений конфиденциальность или же честность в программе, то есть программист хочет определить, соответствует ли программа политике информационного потока или нет.

Простая политика потока информации

А Диаграмма Хассе, описывающая простую политику конфиденциальности информации.

Предположим, что есть два пользователя, A и B. В программе следующие классы безопасности (SC) вводятся:

SC = {∅, {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, B} является {A}.
{A} ⊕ {B} = ∅ - ни один {A} ни {B} разрешено читать с обоих {A} и {B}.

Это также можно описать как пересечение (∩) между классами безопасности.

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

Политика информационных потоков в системах охранного типа

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

если да_{A} = 1, тогда x_{{A, B}} : = 0 иначе x_{{A, B}} := 1

Здесь проверка равенства выполняется для переменной y, которой присвоен класс безопасности {A}. Переменная x с более низким классом защиты ({A, B}) находится под влиянием этой проверки. Это означает, что информация утекает из класса {A} к классу {A, B}, что является нарушением политики конфиденциальности. Эта утечка должна быть обнаружена системой охранного типа.

Пример

Для проектирования системы типов безопасности требуется функция (также известная как среда безопасности), которая создает отображение переменных в типы или классы безопасности. Эту функцию можно назвать Γ такой, что Γ (x) = τ, куда Икс переменная и τ - это класс или тип безопасности. Классы безопасности назначаются (также называемые «суждениями») программным компонентам с использованием следующих обозначений:

Типы присваиваются операциям чтения: Γ ⊢ e: τ.
Типы назначаются для операций записи: Γ ⊢ S: τ смд.
Константам можно присвоить любой тип.

Для декомпозиции программы можно использовать следующие нотации снизу вверх: предположение₁ ... предположение_п/вывод. После того, как программа разложена на тривиальные решения, с помощью которых можно легко определить тип, можно получить типы для менее тривиальных частей программы. Каждый «числитель» рассматривается изолированно, глядя на тип каждого оператора, чтобы увидеть, может ли разрешенный тип быть получен для «знаменателя» на основе определенных «правил» системы типов.

Правила

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

Назначение:

Γ (x) = τ₁, Γ ⊢ a: τ₂

Γ ⊢ x: = a: τ₁ cmd

, где должно выполняться условие: τ₂ ⊑ τ₁

Условный тест:

Γ ⊢ t: τ, Γ ⊢ S₁ : τ₁ cmd, Γ ⊢ S₂ : τ₂ cmd

Γ ⊢, если t, то S₁ иначе S₂: τ₁ ⊓ τ₂ cmd

, где должно выполняться условие: τ ⊑ τ₁, τ₂

Применяя это к простой программе, представленной выше, получаем:

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	`Γ ⊢ если y = 1, то x: = 0, иначе x: = 1: Не печатается`

Система типов обнаруживает нарушение политики в строке 2, где выполняется операция чтения класса безопасности {A} выполняется, после чего следуют две операции записи менее строгого класса безопасности {A, B}. Если говорить более формализованно, {A} ⋢ {A, B}, {A, B} (из правила условного теста). Таким образом, программа классифицируется как «нетипируемая».

Разумность

Надежность системы охранного типа можно неформально определить как: если программа п хорошо напечатан, п удовлетворяет невмешательство.

дальнейшее чтение

Фред Б. Шнайдер, Грег Моррисетт и Роберт Харпер, Языковой подход к безопасности.
Андрей Сабельфельд, Эндрю К. Майерс, Безопасность потока информации на основе языка.