Модель обеспечения целостности Кларка-Уилсона: формализация и применение.
Clark–Wilson model
Модель целостности Кларка-Уилсона: формализация защиты данных от ошибок и злоумышленников. Политики целостности, метки безопасности, процедуры трансформации.
Сравнивайте с английским: нажмите на абзац — оригинал откроется в окне. Кнопка EN под абзацем показывает его прямо в тексте.
Содержание
Введение
Модель целостности Кларка-Уилсона предоставляет основу для определения и анализа политики целостности вычислительной системы. Модель в основном посвящена формализации понятия целостности информации. Целостность информации обеспечивается предотвращением искажения элементов данных в системе в результате ошибок или злонамеренных действий. Политика целостности описывает, каким образом элементы данных в системе должны оставаться корректными при переходе из одного состояния в другое, и определяет полномочия различных субъектов в системе. Модель использует метки безопасности для предоставления доступа к объектам посредством процедур преобразования и ограниченной модели интерфейса.
The Clark–Wilson integrity model provides a foundation for specifying and analyzing an integrity policy for a computing system. The model is primarily concerned with formalizing the notion of information integrity. Information integrity is maintained by preventing corruption of data items in a system due to either error or malicious intent. An integrity policy describes how the data items in the system should be kept valid from one state of the system to the next and specifies the capabilities of various principals in the system. The model uses security labels to grant access to objects via transformation procedures and a restricted interface model.
Происхождение
Модель была описана в статье 1987 года (Сравнение коммерческих и военных политик компьютерной безопасности) Дэвидом Кларком и Дэвидом Р. Уилсоном. В статье разрабатывается модель как способ формализации понятия целостности информации, особенно в сравнении с требованиями к многоуровневым системам безопасности (MLS), описанными в «Оранжевой книге». Кларк и Уилсон утверждают, что существующие модели целостности, такие как Biba (чтение вверх / запись вниз), лучше подходят для обеспечения целостности данных, чем для конфиденциальности информации. Модели Biba более эффективно применимы, например, в банковских системах классификации для предотвращения несанкционированного изменения информации и компрометации информации на более высоких уровнях классификации. В отличие от этого, модель Кларка — Уилсона более явно применима к бизнес-процессам и промышленным процессам, в которых целостность информационного содержания является первостепенной на любом уровне классификации (хотя авторы подчеркивают, что все три модели, очевидно, полезны как для государственных, так и для промышленных организаций).
The model was described in a 1987 paper (A Comparison of Commercial and Military Computer Security Policies) by David D. Clark and David R. Wilson. The paper develops the model as a way to formalize the notion of information integrity, especially as compared to the requirements for multilevel security (MLS) systems described in the Orange Book. Clark and Wilson argue that the existing integrity models such as Biba (read up/write down) were better suited to enforcing data integrity rather than information confidentiality. The Biba models are more clearly useful in, for example, banking classification systems to prevent the untrusted modification of information and the tainting of information at higher classification levels. In contrast, Clark–Wilson is more clearly applicable to business and industry processes in which the integrity of the information content is paramount at any level of classification (although the authors stress that all three models are obviously of use to both government and industry organizations).
Основные принципы
Согласно Шестому изданию учебного руководства по CISSP Стюарта и Чаппле, модель Кларка-Уилсона использует многогранный подход для обеспечения целостности данных. Вместо определения формального конечного автомата, модель определяет каждый элемент данных и разрешает их изменение только через ограниченный набор программ. Модель использует трехкомпонентное отношение субъект/программа/объект (где программа взаимозаменяема с транзакцией), известное как тройка или тройка контроля доступа. В рамках этого отношения субъекты не имеют прямого доступа к объектам. Доступ к объектам возможен только через программы. См. здесь, чтобы узнать, чем это отличается от других моделей контроля доступа. Правила обеспечения и сертификации модели определяют элементы данных и процессы, которые служат основой для политики целостности. В основе модели лежит понятие транзакции. Правильно сформированная транзакция – это последовательность операций, переводящая систему из одного согласованного состояния в другое согласованное состояние. В этой модели политика целостности касается целостности самих транзакций. Принцип разделения обязанностей требует, чтобы сертифицирующий транзакцию и разработчик были разными лицами. Модель содержит ряд базовых конструкций, представляющих как элементы данных, так и процессы, работающие с этими элементами данных. Ключевым типом данных в модели Кларка-Уилсона является ограниченный элемент данных (CDI). Процедура проверки целостности (IVP) гарантирует, что все CDI в системе будут действительны в определенном состоянии. Транзакции, обеспечивающие соблюдение политики целостности, представлены процедурами преобразования (TP). TP принимает на вход CDI или неограниченный элемент данных (UDI) и выдает CDI. TP должен перевести систему из одного допустимого состояния в другое допустимое состояние. UDI представляет собой входные данные системы (например, предоставленные пользователем или злоумышленником). TP должен гарантировать (путем сертификации), что он преобразует все возможные значения UDI в "безопасный" CDI.
According to Stewart and Chapple's CISSP Study Guide Sixth Edition, the Clark–Wilson model uses a multi faceted approach in order to enforce data integrity. Instead of defining a formal state machine, the model defines each data item and allows modifications through only a small set of programs. The model uses a three part relationship of subject/program/object (where program is interchangeable with transaction) known as a triple or an access control triple. Within this relationship, subjects do not have direct access to objects. Objects can only be accessed through programs. Look here to see how this differs from other access control models. The model's enforcement and certification rules define data items and processes that provide the basis for an integrity policy. The core of the model is based on the notion of a transaction. A well formed transaction is a series of operations that transition a system from one consistent state to another consistent state. In this model, the integrity policy addresses the integrity of the transactions. The principle of separation of duty requires that the certifier of a transaction and the implementer be different entities. The model contains a number of basic constructs that represent both data items and processes that operate on those data items. The key data type in the Clark–Wilson model is a Constrained Data Item (CDI). An Integrity Verification Procedure (IVP) ensures that all CDIs in the system are valid at a certain state. Transactions that enforce the integrity policy are represented by Transformation Procedures (TPs). A TP takes as input a CDI or Unconstrained Data Item (UDI) and produces a CDI. A TP must transition the system from one valid state to another valid state. UDIs represent system input (such as that provided by a user or adversary). A TP must guarantee (via certification) that it transforms all possible values of a UDI to a “safe” CDI.
CW-lite
Вариантом модели Кларка — Уилсона является CW lite, которая смягчает изначальное требование формальной верификации семантики TP. Верификация семантики переносится на отдельную модель и инструменты общего назначения для формальных доказательств.
A variant of Clark Wilson is the CW lite model, which relaxes the original requirement of formal verification of TP semantics. The semantic verification is deferred to a separate model and general formal proof tools.