МОДЕЛЬ БЕЛЛА-ЛАПАДУЛА

Класичною мандатної моделлю безпеки є модель Белла-ЛаПадула. У ній для опису системи використовуються:

S - безліч суб'єктів (наприклад, безліч користувачів і програм);

Про - безліч об'єктів (наприклад, безліч файлів);

L - лінійно впорядкована множина рівнів безпеки (наприклад, «загальний доступ», «для службового користування», «секретно», «совершенно секретно»);

F: S і Про -> L - функція, що визначає рівень безпеки суб'єкта або об'єкта в даному стані;

V - безліч станів - безліч впорядкованих пар (F, М), де М - матриця доступу суб'єктів до об'єктів (матриця, рядки якої відповідають суб'єктам системи, стовпці - об'єктам, елемент матриці M so , далі позначається як M [s, о], описує права на доступ суб'єкта s до об'єкта о).

Система описується початковим станом v 0 eV, безліччю запитів R і функцією переходів Т: ( 'V х R) -> V, яка описує перехід системи зі стану в стан під дією запиту.

У моделі Белла-ЛаПадула вводиться визначення двох властивостей безпеки системи: безпека з читання та безпеку за записом.

Стан (F, М) безпечно з читання тоді і тільки тоді, коли для V s е S, V про е Про виконується вимога: читання е M [s, о] => F (s)> F (o),

т. е. суб'єкт s може прочитати інформацію з об'єкта о, тільки якщо рівень секретності про менше або дорівнює рівню доступу s. Дана властивість безпеки також називається правилом заборони читання з верхнього рівня.

Стан (F, М) безпечно по запису тоді і тільки тоді, коли для V s е S, V про е Про виконується вимога: запис е Mfs, ol => F (o)> F (s),

т. е. суб'єкт s може записати інформацію в об'єкт о, тільки якщо рівень секретності про вище або дорівнює рівню доступу s. Дана властивість безпеки також називається правилом заборони запису на нижній рівень.

Стан системи veV безпечно тоді і тільки тоді, коли воно безпечне і з читання, і за записом.

Система (v 0 . R, Т) безпечна тоді і тільки тоді, коли її початковий стан v 0 безпечно і будь-який стан, досяжне з v 0 після виконання кінцевої послідовності запитів з R, також безпечно.

Великою перевагою моделі Бслла-ЛаПадула є те, що для неї доведена основна теорема безпеки. У загальному випадку, дана теорема формулюється так: якщо початковий стан системи безпечно, і всі переходи зі стану в стан не порушують обмежень, сформульованих політикою безпеки, то будь-який стан системи, досяжне за кінцеве число переходів буде безпечним. У разі моделі Белла-ЛаПадула обмеження не дозволяють порушити безпеку з читання та запису.

Основна теорема безпеки для моделі Белла-ЛаПадула

Система (v 0 , R. Т) (т. Е. Система з початковим станом v 0 , безліччю запитів R, функцією переходів Т) безпечна тоді і тільки тоді, коли сосгояніе v 0 безпечно, і функція переходів Т така, що для V veV, досгіжімого зі стану v 0 після виконання кінцевої послідовності запитів з R (таких що T (v, г) = v *, де v = (F, М) - початковий стан, v * = (F *, М *) - стан після переходу), для V s е S, V про е про виконуються наступні умови:

  • - якщо чтеніееМ | s, o] і 4TeHHegM | s, o], то F '(s)> F * (o);
  • - якщо 4TenHeeM | s, o] і F * (s)то читанням M * [s, о];
  • - якщо запис е M * [s, о] і запис g M [s, о], то F * (o)> F (s);
  • - якщо запис е M | s, о] і F * (o) M * [s, о).

Коротко розглянемо доказ теореми.

Необхідність. Якщо система безпечна, то початковий стан v 0 безпечно за визначенням. Нехай існує деякий стан v *, досяжне з v 0 шляхом виконання кінцевого числа запитів з R і отримане в результаті переходу з безпечного стану v: T (v, г) = v *. Тоді, якщо при такому переході порушено хоча б одне з перших двох обмежень, що накладаються теоремою на функцію Т, то стан v "не буде безпечним з читання. Якщо функція Т порушує одне з двох останніх умов теореми, то стан v не будуть безпечними за записом. Таким чином, при порушенні умов теореми система стає небезпечною. Необхідність доведена.

Достатність. Використовуємо метод докази від протилежного. Нехай система небезпечна. У цьому випадку або початковий стан v 0 небезпечно, що суперечить умовам теореми, або має існувати небезпечний стан v ', досяжне з безпечного початкового стану v 0 шляхом виконання кінцевого числа запитів з R. У цьому випадку обов'язково матиме місце перехід T (v, г) = v *, при якому стан v - безпечно, av * - немає. Однак чотири умови теореми роблять такий перехід неможливим.

Незважаючи на достоїнства моделі Белла-ЛаПадула, при її суворої реалізації в реальних АС виникає ряд проблем.

  • 1. Завищення рівня секретності , пов'язане з однорівневої природою об'єктів і правилом безпеки по запису. Якщо суб'єкт з високим рівнем доступу хоче записати щось в об'єкт з низьким рівнем секретності, то спочатку доводиться підвищити рівень секретності об'єкта, а потім здійснювати запис. Таким чином, навіть один параграф, доданий у великій документ суб'єктом з високим рівнем доступу, підвищує рівень секретності всього цього документа. Якщо по ходу роботи зміни в документ вносять суб'єкти зі все більш високим рівнем доступу, рівень секретності документа також постійно зростає.
  • 2. Запис наосліп. Ця проблема виникає, коли суб'єкт виробляє операцію запису в об'єкт з більш високим рівнем безпеки, ніж його власний. У цьому випадку після завершення операції запису суб'єкт не зможе перевірити правильність виконання записи за допомогою контрольного читання, так як йому це заборонено відповідно до правила безпеки з читання.
  • 3. Проблема віддаленого читання-запису. У розподілених системах при віддаленому читанні файлу створюються два потоки: від суб'єкта до об'єкта (запити на читання, підтвердження, інша службова інформація) і від об'єкта до суб'єкта (самі запитувані дані). При цьому, наприклад, якщо F (s)> F (o), то перший потік буде суперечити властивості безпеки по запису. На практиці для вирішення цієї проблеми треба розділяти службові потоки (запити, підтвердження) та власне передачу інформації.

А. Довірені суб'єкти. Модель Белла-ЛаПадула не враховує, що в реальній системі, як правило, існують суб'єкти, що діють в інтересах адміністратора, а також системні процеси, наприклад, драйвери. Жорстке дотримання правил заборони читання з верхнього рівня і заборони запису на нижній рівень в ряді випадків унеможливлює роботу подібних процесів. Відповідно, їх також доводиться виділяти.

 
Переглянути оригінал
< Попер   ЗМІСТ   ОРИГІНАЛ   Наст >