Тип системы безопасности
 | Эта статья включает список литературы , связанную литературу или внешние ссылки , но ее источники остаются неясными, поскольку в ней отсутствуют встроенные цитаты . ( Июль 2020 г. ) |
В информатике можно систему типов описать как синтаксическую структуру, содержащую набор правил, которые используются для присвоения свойства типа (int, boolean, char и т. д.) различным компонентам компьютерной программы, таким как переменные или функции. . Система типа безопасности работает аналогичным образом, только с основным упором на безопасность компьютерной программы посредством информационными потоками управления . Таким образом, различным компонентам программы присваиваются типы безопасности или метки. Целью такой системы является в конечном итоге возможность проверить, что данная программа соответствует правилам системы типов и удовлетворяет требованиям невмешательства . Системы типов безопасности — это один из многих методов безопасности, используемых в области языковой безопасности , и он тесно связан с информационными потоками и политиками информационных потоков.
Проще говоря, систему типов безопасности можно использовать для обнаружения наличия какого-либо нарушения конфиденциальности или целостности в программе, т.е. программист хочет определить, соответствует ли программа политике потока информации или нет.
Простая политика потока информации
[ редактировать ]
Предположим, есть два пользователя А и Б. В программе следующие классы безопасности введены (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}.
Это также можно описать как пересечение (∩) между классами безопасности.
Политику информационных потоков можно проиллюстрировать в виде диаграммы Хассе . Политика также должна представлять собой решетку , то есть иметь наибольшую нижнюю границу и наименьшую верхнюю границу (всегда существует комбинация между классами безопасности). В случае целостности информация будет течь в противоположном направлении, поэтому политика будет инвертирована.
Политика информационных потоков в системах типа безопасности
[ редактировать ]После внедрения политики разработчик программного обеспечения может применить классы безопасности к компонентам программы. Использование системы типов безопасности обычно сочетается с компилятором, который может выполнять проверку информационного потока в соответствии с правилами системы типов. Для простоты в качестве демонстрации можно использовать очень простую компьютерную программу вместе с политикой потока информации, описанной в предыдущем разделе. Простая программа представлена в следующем псевдокоде:
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 : Not typeable
| ||
Система типов обнаруживает нарушение политики в строке 2, где выполняется операция чтения класса безопасности. {A} выполняется, после чего следуют две операции записи менее строгого класса безопасности {A,B}. Говоря более формализованно, {A} ⋢ {A,B}, {A,B} (из правила условного теста). Таким образом, программа классифицируется как «нетипизированная».
разумность
[ редактировать ]Надежность системы типа безопасности можно неформально определить как: если программа P хорошо напечатан, P удовлетворяет принципу невмешательства. Вольпано, Смит и Ирвин были первыми, кто доказал правильность системы типов безопасности для детерминированного императивного языка программирования со стандартной (неинструментальной) семантикой, используя понятие невмешательства. [1]
Ссылки
[ редактировать ]- ^ Вольпано, Деннис; Смит, Джеффри; Ирвин, Синтия (1996). «Надежная система для безопасного анализа потока». Журнал компьютерной безопасности . 4 (2).
Дальнейшее чтение
[ редактировать ]- Фред Б. Шнайдер, Грег Моррисетт и Роберт Харпер, Языковой подход к безопасности .
- Андрей Сабельфельд, Эндрю Майерс, Языковая безопасность информационных потоков .