Модель Бела — ЛаПадули — модель контролю та керування доступом, яка заснована на мандатній моделі керування доступом. У моделі аналізуються умови, при яких неможливе утворення інформаційних потоків від суб'єктів з вищим рівнем доступу до суб'єктів з нижчим рівнем доступу.
Історія
Класична модель Бела — ЛаПадули описана у 1975 р. співробітниками Девідом Белом та Леонардом ЛаПадулою. До створення моделі їх підштовхнула система безпеки при роботі з таємними документами уряду США. Сутність системи полягає у тому, що кожному суб'єкту (особі, яка працює з документами) і об'єкту (документу) надавалась мітка конфіденційності, починаючи з найвищої («Top Secret») до найнижчої («Unclassified»). Причому суб'єкт, якому дозволено доступ до об'єктів з нижчою міткою конфіденційності, не може отримати доступ до об'єкта з вищою міткою конфіденційності. Також суб'єкту забороняється запис у об'єкти з нижчою міткою конфіденційності.
Особливості
Модель Бела — ЛаПадули є моделлю розмежування доступу до інформації, що захищається. Вона описується скінченним автоматом з допустимим набором станів, у яких може знаходитись інформаційна система. Усі елементи у складі інформаційної системи поділені на суб'єкти і об'єкти. Кожному суб'єкту приписується рівень доступу, який відповідає рівню конфіденційності. Аналогічно об'єкту надається рівень таємності. Поняття захищеної визначається наступним чином: кожен стан системи повинен відповідати політиці безпеки, встановленої для даної інформаційної системи. Перехід між станами описується функціями переходу. Система знаходиться у безпечному стані тільки у тому випадку, коли у кожного суб'єкта наявний доступ тільки до тих об'єктів, до яких від дозволений на основі поточної політики безпеки. Для визначення права доступу суб'єкта до об'єкта рівень доступу суб'єкта порівнюється з рівнем таємності об'єкта, і на підставі цього приймається рішення щодо надання запитаного рівня доступу. Набори рівень доступу/рівень таємності описуються матрицею доступу. Основними правилами, що забезпечують розмежування доступу, є:
Проста властивість безпеки (The Simple Security)
Суб'єкт з рівнем доступу може читати інформацію з об'єкта з рівнем таємності тоді і тільки тоді, коли перевищує . Це правило також відоме під назвою «Немає читання зверху» (No read up, NRU). Наприклад, суб'єкт, який має доступ лише до нетаємних даних, спробує прочитати об'єкт з рівнем «цілком таємно», то йому буде відмовлено.
Властивість ★ (The ★-property)
Сутність властивості ★ (читається як «властивість зірочка») полягає у тому, що суб'єкт з рівнем доступу s може писати інформацію у об'єкт з рівнем таємності xо тільки якщо xо перевищує . Це правило також відоме під назвою «Немає запису вниз» (No write down, NWD). Наприклад, якщо суб'єкт, який має рівень доступу «цілком таємно» спробує записати у об'єкт з рівнем таємності «таємно», то йому буде відмовлено у цьому.
Сильна властивість ★ (Strong ★ Property)
Сильна властивість ★ є альтернативною властивості ★, у якій суб'єкти можуть писати у об'єкти тільки з тим рівнем таємності, що відповідає рівню доступу суб'єкта. Таким чином, операція запису вгору, присутня при властивості ★, відсутня, а лише наявна операція запису у об'єкти з тим же рівнем доступу. Сильна властивість ★ зазвичай згадується у контексті багаторівневих систем керування базами даних і обумовлена вимогами цілісності. Сильна властивість ★ передбачається моделлю Біби, де було показано, що стійка цілісність у поєднанні з моделлю Бела — ЛаПадули забезпечується читанням і записом у межах єдиного рівня таємності.
Принцип стійкості
Принцип стійкості моделі Бела — ЛаПадули стверджує, що рівень таємності/доступу суб'єкта або об'єкта не змінюється під час звернення. Є дві форми принципу стійкості. Принцип сильної стійкості стверджує, що рівень безпеки не зміниться під час нормальної роботи системи. Принцип слабкої стійкості стверджує, що рівень безпеки неможливо змінити таким чином, що порушилась політика безпеки. Принцип слабкої стійкості дозволяє дотримуватися принципу мінімуму повноважень у системі. Тобто процеси починаються з низьким рівнем ознайомленості, незалежно від рівня ознайомленості їх власників, і у процесах поступово накопичуються більш високі рівні обізнаності, по мірі потреби у діях, які вимагають підвищення рівня обізнаності.
Формальний опис моделі
Позначення
- — множина суб'єктів;
- — множина об'єктів, ;
- — множина прав доступу, — доступ на читання, — доступ на запис;
- — множина рівнів таємності, — відкрита, — для службового користування, — таємна, — цілком таємна;
- — решітка рівнів секретності, де:
- — оператор, що визначає часткове несуворе відношення порядку рівнів таємності;
- — оператор найменшої верхньої межі;
- — оператор найбільшої нижньої межі.
- — множина станів системи, що представляється у вигляді впорядкованих пар , де:
- — функція рівнів таємності, яка ставить у відповідність кожному об'єкту і суб'єкту в системі певний рівень таємності;
- — матриця поточних прав доступу.
Оператор відношення має наступні властивості:
- Рефлексивність: , полягає тому, що між суб'єктами та об'єктами одного рівня таємності передача інформації дозволена.
- Антисиметричність: , полягає у тому, що якщо інформація може передаватися від суб'єктів та об'єктів рівня A до суб'єктів та об'єктів рівня B, і ід суб'єктів та об'єктів рівня B до суб'єктів та об'єктів рівня A, то ці рівні еквівалентні.
- Транзитивність: , полягає у тому, що якщо інформація може передаватися від суб'єктів і об'єктів рівня A до суб'єктів і об'єктів рівня B, і від суб'єктів і об'єктів рівня B до суб'єктів і об'єктів рівня C, то вона може передаватися від суб'єктів і об'єктів рівня A до суб'єктів і об'єктів рівня C.
Оператор найменшої верхньої межі визначається відношенням:
Оператор найбільшої нижньої межі визначається відношенням: З визначення цих двох операторів можна показати, що для кожної пари існує єдиний елемент найменшої верхньої межі та єдиний елемент найбільшої нижньої межі.
Система у моделі Бела — ЛаПадули складається з наступних елементів:
- — початковий стан системи;
- — множина прав доступу;
- — функція переходу, яка у ході виконання запитів переводить систему із одного стану у інший.
Визначення безпечного стану
Стан називається досяжним у системі , якщо існує послідовність Початковий стан є досяжним за визначенням.
Стан системи називається безпечним по читанню (або просто безпечним (від простої властивості)), якщо для кожного суб'єкта, який здійснює у цьому стані доступ на читання до об'єкта, рівень доступу суб'єкта переважає рівень таємності об'єкта:
Стан системи називається безпечним по запису (або ★ — безпечним (від властивості ★)), якщо для кожного суб'єкта, який здійснює у цьому стані доступ на запис до об'єкта, рівень таємності об'єкта переважає рівень доступу суб'єкта:
Стан називається безпечним, якщо він є безпечним і по читанню, і по запису.
Система називається безпечною, якщо її початковий стан є безпечним, і усі стани, які можуть бути досягнуті з шляхом застосування скінченної послідовності запитів з , безпечні.
Основна теорема безпеки Бела — ЛаПадули
Система безпечна тоді, і тільки тоді, коли виконані наступні умови:
- Початковий стан є безпечним.
- Для будь-якого стану , яке досяжне з шляхом застосування скінченної послідовності запитів з , таких, що и , для виконані умови:
- Якщо и , то
- Якщо и , то
- Якщо и , то
- Якщо и , то
Доказ.
Необхідність твердження.
Нехай система безпечна. У цьому випадку початковий стан безпечний за визначенням. Припустимо, що існує безпечний стан , досяжний із стану , і для даного переходу порушено одну з умов 1-4. Легко помітити, що якщо порушені властивості 1 або 2, то стан не буде безпечним по читанню, а якщо порушені властивості 3 або 4, то стан не буде безпечним по запису. У обох випадках стан не є безпечним.
Достатність твердження.
Система може бути небезпечною у двох випадках:
- У випадку, якщо початковий стан небезпечний. Однак це твердження суперечить умовам теореми.
- Якщо існує небезпечний стан , досяжний з безпечного стану шляхом застосування скінченного числа запитів . Це означає, що на певному проміжному етапі відбувся перехід , де – безпечний стан, а — небезпечний. Однак умови 1-4 роблять такий перехід неможливим.
Недоліки
Пониження рівня таємності
Ця вразливість полягає у тому, що класична модель не попереджує пониження рівня таємності об'єкта (зміну рівня таємності аж до «відкрита» за бажанням суб'єкта з допуском до «цілком таємно»). Наприклад, нехай суб'єкт з високим рівнем доступу A читає інформацію з об'єкта з тим же рівнем таємності. Далі він понижує свій рівень до низького B, і записує зчитану раніше інформацію у об'єкт з низьким рівнем таємності. Таким чином, хоч модель формально не порушена, було порушено політику безпеки. Для вирішення цієї проблеми вводяться правила:
- Правило сильного спокою — рівні безпеки суб'єктів і об'єктів ніколи не змінюються під час роботи системи.
- Правило слабкого спокою — рівні безпеки суб'єктів і об'єктів ніколи не змінюються під час роботи системи таким чином, щоб порушити задану політику безпеки.
Віддалене читання
Ця вразливість проявляється у розподілених комп'ютерних системах. Припустимо, суб'єкт A з високим рівнем доступу намагається прочитати інформацію об'єкта B з низьким рівнем таємності. Під час операції між віддаленими об'єктами відбувається утворення потоку інформації від об'єкта, що читається, до суб'єкта, який запитав читання. Цей потік є безпечним, тому що інформація недоступна неавторизованим суб'єктам. Однак у розподіленій системі читання ініціюється запитом від одного об'єкта до іншого. Такий запит створює потік інформації, який направлений від об'єкта з високим рівнем таємності до об'єкта з низьким рівнем таємності, що заборонено класичною моделлю Бела — ЛаПадули.
Див. також
Примітки
- Bell, David Elliott and LaPadula, Leonard J. Secure Computer Systems: Mathematical Foundations (PDF). — MITRE Corporation, 1973. з джерела 18 червня 2006. Процитовано 15 січня 2016.
- Bell, David Elliott and LaPadula, Leonard J. Secure Computer System: Unified Exposition and Multics Interpretation (PDF). — MITRE Corporation, 1976. з джерела 29 серпня 2008. Процитовано 15 січня 2016.
- Bell, David Elliott (December 2005). (PDF). Proceedings of the 21st Annual Computer Security Applications Conference. Tucson, Arizona, USA. с. 337—351. doi:10.1109/CSAC.2005.37. Архів оригіналу (PDF) за 21 лютого 2020. Процитовано 15 січня 2016. Slides — Looking Back at the Bell-LaPadula Model [ 8 червня 2008 у Wayback Machine.]
- Sandhu, Ravi S. (1994). (PDF). Handbook of Information Security Management (1994-95 Yearbook). Auerbach Publishers. с. 145—160. Архів оригіналу (PDF) за 1 вересня 2006. Процитовано 12 серпня 2006.
Література
- Цирлов В. Л. Основы информационной безопасности автоматизированных систем. — Р.: Феникс, 2008. С. 40-44
- Девянин П. Н. Модели безопасности компьютерных систем: Учебное пособие для студентов высших учебных заведений. — М.: Издательский центр «Академия», 2005. С. 55-66
- Грушо А. А., Тимонина Е. Е. Теоретические основы защиты информации. — М.: Издательство Агентства «Яхтсмен», 1996. С 52-55
- А. П. Баранов, Н. П. Борисенко, П. Д. Зегжда, А. Г. Ростовцев, Корт С. С. — Математические основы информационной безопасности. — М.: Издательство Агентства «Яхтсмен», 1997. C 22-36
Вікіпедія, Українська, Україна, книга, книги, бібліотека, стаття, читати, завантажити, безкоштовно, безкоштовно завантажити, mp3, відео, mp4, 3gp, jpg, jpeg, gif, png, малюнок, музика, пісня, фільм, книга, гра, ігри, мобільний, телефон, android, ios, apple, мобільний телефон, samsung, iphone, xiomi, xiaomi, redmi, honor, oppo, nokia, sonya, mi, ПК, web, Інтернет
Model Bela LaPaduli model kontrolyu ta keruvannya dostupom yaka zasnovana na mandatnij modeli keruvannya dostupom U modeli analizuyutsya umovi pri yakih nemozhlive utvorennya informacijnih potokiv vid sub yektiv z vishim rivnem dostupu do sub yektiv z nizhchim rivnem dostupu IstoriyaKlasichna model Bela LaPaduli opisana u 1975 r spivrobitnikami Devidom Belom ta Leonardom LaPaduloyu Do stvorennya modeli yih pidshtovhnula sistema bezpeki pri roboti z tayemnimi dokumentami uryadu SShA Sutnist sistemi polyagaye u tomu sho kozhnomu sub yektu osobi yaka pracyuye z dokumentami i ob yektu dokumentu nadavalas mitka konfidencijnosti pochinayuchi z najvishoyi Top Secret do najnizhchoyi Unclassified Prichomu sub yekt yakomu dozvoleno dostup do ob yektiv z nizhchoyu mitkoyu konfidencijnosti ne mozhe otrimati dostup do ob yekta z vishoyu mitkoyu konfidencijnosti Takozh sub yektu zaboronyayetsya zapis u ob yekti z nizhchoyu mitkoyu konfidencijnosti OsoblivostiModel Bela LaPaduli ye modellyu rozmezhuvannya dostupu do informaciyi sho zahishayetsya Vona opisuyetsya skinchennim avtomatom z dopustimim naborom staniv u yakih mozhe znahoditis informacijna sistema Usi elementi u skladi informacijnoyi sistemi podileni na sub yekti i ob yekti Kozhnomu sub yektu pripisuyetsya riven dostupu yakij vidpovidaye rivnyu konfidencijnosti Analogichno ob yektu nadayetsya riven tayemnosti Ponyattya zahishenoyi viznachayetsya nastupnim chinom kozhen stan sistemi povinen vidpovidati politici bezpeki vstanovlenoyi dlya danoyi informacijnoyi sistemi Perehid mizh stanami opisuyetsya funkciyami perehodu Sistema znahoditsya u bezpechnomu stani tilki u tomu vipadku koli u kozhnogo sub yekta nayavnij dostup tilki do tih ob yektiv do yakih vid dozvolenij na osnovi potochnoyi politiki bezpeki Dlya viznachennya prava dostupu sub yekta do ob yekta riven dostupu sub yekta porivnyuyetsya z rivnem tayemnosti ob yekta i na pidstavi cogo prijmayetsya rishennya shodo nadannya zapitanogo rivnya dostupu Nabori riven dostupu riven tayemnosti opisuyutsya matriceyu dostupu Osnovnimi pravilami sho zabezpechuyut rozmezhuvannya dostupu ye Prosta vlastivist bezpeki The Simple Security Sub yekt z rivnem dostupu xs displaystyle x s mozhe chitati informaciyu z ob yekta z rivnem tayemnosti xo displaystyle x o todi i tilki todi koli xs displaystyle x s perevishuye xo displaystyle x o Ce pravilo takozh vidome pid nazvoyu Nemaye chitannya zverhu No read up NRU Napriklad sub yekt yakij maye dostup lishe do netayemnih danih sprobuye prochitati ob yekt z rivnem cilkom tayemno to jomu bude vidmovleno Vlastivist The property Sutnist vlastivosti chitayetsya yak vlastivist zirochka polyagaye u tomu sho sub yekt z rivnem dostupu s mozhe pisati informaciyu u ob yekt z rivnem tayemnosti xo tilki yaksho xo perevishuye xs displaystyle x s Ce pravilo takozh vidome pid nazvoyu Nemaye zapisu vniz No write down NWD Napriklad yaksho sub yekt yakij maye riven dostupu cilkom tayemno sprobuye zapisati u ob yekt z rivnem tayemnosti tayemno to jomu bude vidmovleno u comu Silna vlastivist Strong Property Silna vlastivist ye alternativnoyu vlastivosti u yakij sub yekti mozhut pisati u ob yekti tilki z tim rivnem tayemnosti sho vidpovidaye rivnyu dostupu sub yekta Takim chinom operaciya zapisu vgoru prisutnya pri vlastivosti vidsutnya a lishe nayavna operaciya zapisu u ob yekti z tim zhe rivnem dostupu Silna vlastivist zazvichaj zgaduyetsya u konteksti bagatorivnevih sistem keruvannya bazami danih i obumovlena vimogami cilisnosti Silna vlastivist peredbachayetsya modellyu Bibi de bulo pokazano sho stijka cilisnist u poyednanni z modellyu Bela LaPaduli zabezpechuyetsya chitannyam i zapisom u mezhah yedinogo rivnya tayemnosti Princip stijkosti Princip stijkosti modeli Bela LaPaduli stverdzhuye sho riven tayemnosti dostupu sub yekta abo ob yekta ne zminyuyetsya pid chas zvernennya Ye dvi formi principu stijkosti Princip silnoyi stijkosti stverdzhuye sho riven bezpeki ne zminitsya pid chas normalnoyi roboti sistemi Princip slabkoyi stijkosti stverdzhuye sho riven bezpeki nemozhlivo zminiti takim chinom sho porushilas politika bezpeki Princip slabkoyi stijkosti dozvolyaye dotrimuvatisya principu minimumu povnovazhen u sistemi Tobto procesi pochinayutsya z nizkim rivnem oznajomlenosti nezalezhno vid rivnya oznajomlenosti yih vlasnikiv i u procesah postupovo nakopichuyutsya bilsh visoki rivni obiznanosti po miri potrebi u diyah yaki vimagayut pidvishennya rivnya obiznanosti Formalnij opis modeliPoznachennya S displaystyle S mnozhina sub yektiv O displaystyle O mnozhina ob yektiv S O displaystyle S subset O R r w displaystyle R r w mnozhina prav dostupu r displaystyle r dostup na chitannya w displaystyle w dostup na zapis L U SU S TS displaystyle L U SU S TS mnozhina rivniv tayemnosti U displaystyle U vidkrita SU displaystyle SU dlya sluzhbovogo koristuvannya S displaystyle S tayemna TS displaystyle TS cilkom tayemna L L displaystyle Lambda L leq bullet otimes reshitka rivniv sekretnosti de displaystyle leq operator sho viznachaye chastkove nesuvore vidnoshennya poryadku rivniv tayemnosti displaystyle bullet operator najmenshoyi verhnoyi mezhi displaystyle otimes operator najbilshoyi nizhnoyi mezhi V displaystyle V mnozhina staniv sistemi sho predstavlyayetsya u viglyadi vporyadkovanih par F M displaystyle F M de F S O L displaystyle F S cup O rightarrow L funkciya rivniv tayemnosti yaka stavit u vidpovidnist kozhnomu ob yektu i sub yektu v sistemi pevnij riven tayemnosti M displaystyle M matricya potochnih prav dostupu Operator vidnoshennya displaystyle leq maye nastupni vlastivosti Refleksivnist 8 a L a a displaystyle mathcal 8 a in L a leq a polyagaye tomu sho mizh sub yektami ta ob yektami odnogo rivnya tayemnosti peredacha informaciyi dozvolena Antisimetrichnist a1 a2 L a1 a2 amp a2 a1 a2 a1 displaystyle forall a 1 a 2 in L a 1 leq a 2 And a 2 leq a 1 rightarrow a 2 a 1 polyagaye u tomu sho yaksho informaciya mozhe peredavatisya vid sub yektiv ta ob yektiv rivnya A do sub yektiv ta ob yektiv rivnya B i id sub yektiv ta ob yektiv rivnya B do sub yektiv ta ob yektiv rivnya A to ci rivni ekvivalentni Tranzitivnist a1 a2 a3 L a1 a2 amp a2 a3 a1 a3 displaystyle forall a 1 a 2 a 3 in L a 1 leq a 2 And a 2 leq a 3 rightarrow a 1 leq a 3 polyagaye u tomu sho yaksho informaciya mozhe peredavatisya vid sub yektiv i ob yektiv rivnya A do sub yektiv i ob yektiv rivnya B i vid sub yektiv i ob yektiv rivnya B do sub yektiv i ob yektiv rivnya C to vona mozhe peredavatisya vid sub yektiv i ob yektiv rivnya A do sub yektiv i ob yektiv rivnya C Operator najmenshoyi verhnoyi mezhi displaystyle bullet viznachayetsya vidnoshennyam a a1 a2 a1 a2 a amp a 2L a a a a1 a a2 displaystyle a a 1 bullet a 2 Leftrightarrow a 1 a 2 leq a And forall a mathcal 2 L a leq a rightarrow a leq a 1 vee a leq a 2 Operator najbilshoyi nizhnoyi mezhi displaystyle otimes viznachayetsya vidnoshennyam a a1 a2 a a1 a2 amp a 2L a a1 amp a a2 a a displaystyle a a 1 otimes a 2 Leftrightarrow a leq a 1 a 2 And forall a mathcal 2 L a leq a 1 And a leq a 2 rightarrow a leq a Z viznachennya cih dvoh operatoriv mozhna pokazati sho dlya kozhnoyi pari a1 a2 2 L displaystyle a 1 a 2 mathcal 2 L isnuye yedinij element najmenshoyi verhnoyi mezhi ta yedinij element najbilshoyi nizhnoyi mezhi Sistema S n0 R T displaystyle Sigma nu 0 R T u modeli Bela LaPaduli skladayetsya z nastupnih elementiv n0 displaystyle nu 0 pochatkovij stan sistemi R displaystyle mathbb R mnozhina prav dostupu T V R V displaystyle T V times R rightarrow V funkciya perehodu yaka u hodi vikonannya zapitiv perevodit sistemu iz odnogo stanu u inshij Viznachennya bezpechnogo stanu Stan n displaystyle nu nazivayetsya dosyazhnim u sistemi S n0 R T displaystyle Sigma nu 0 R T yaksho isnuye poslidovnist r0 n0 rn 1 nn 1 rn nn T ri ni ni 1 i 0 n 1 displaystyle r 0 nu 0 r n 1 nu n 1 r n nu n T r i nu i nu i 1 forall i 0 n 1 Pochatkovij stan n0 displaystyle nu 0 ye dosyazhnim za viznachennyam Stan sistemi F M displaystyle F M nazivayetsya bezpechnim po chitannyu abo prosto bezpechnim vid prostoyi vlastivosti yaksho dlya kozhnogo sub yekta yakij zdijsnyuye u comu stani dostup na chitannya do ob yekta riven dostupu sub yekta perevazhaye riven tayemnosti ob yekta s S o O r M s o F o F s displaystyle forall s in S forall o in O r in M s o rightarrow F o leq F s Stan sistemi F M displaystyle F M nazivayetsya bezpechnim po zapisu abo amp x2605 bezpechnim vid vlastivosti amp x2605 yaksho dlya kozhnogo sub yekta yakij zdijsnyuye u comu stani dostup na zapis do ob yekta riven tayemnosti ob yekta perevazhaye riven dostupu sub yekta s S o O w M s o F s F o displaystyle forall s in S forall o in O w in M s o rightarrow F s leq F o Stan F M displaystyle F M nazivayetsya bezpechnim yaksho vin ye bezpechnim i po chitannyu i po zapisu Sistema S n0 R T displaystyle Sigma nu 0 R T nazivayetsya bezpechnoyu yaksho yiyi pochatkovij stan n0 displaystyle nu 0 ye bezpechnim i usi stani yaki mozhut buti dosyagnuti z n0 displaystyle nu 0 shlyahom zastosuvannya skinchennoyi poslidovnosti zapitiv z R displaystyle R bezpechni Osnovna teorema bezpeki Bela LaPaduli Sistema S n0 R T displaystyle Sigma nu 0 R T bezpechna todi i tilki todi koli vikonani nastupni umovi Pochatkovij stan n0 displaystyle nu 0 ye bezpechnim Dlya bud yakogo stanu n displaystyle nu yake dosyazhne z n0 displaystyle nu 0 shlyahom zastosuvannya skinchennoyi poslidovnosti zapitiv z R displaystyle R takih sho T n r n n F M displaystyle T nu r nu nu F M i n F M displaystyle nu F M dlya 8s2S 8o2O displaystyle mathcal 8 s mathcal 2 S mathcal 8 o mathcal 2 O vikonani umovi Yaksho r2M s o displaystyle r mathcal 2 M s o i r M s o displaystyle r notin M s o to F o F s displaystyle F o leq F s Yaksho r2M s o displaystyle r mathcal 2 M s o i F s lt F o displaystyle F s lt F o to r M s o displaystyle r notin M s o Yaksho w2M s o displaystyle w mathcal 2 M s o i w M s o displaystyle w notin M s o to F s F o displaystyle F s leq F o Yaksho w2M s o displaystyle w mathcal 2 M s o i F o lt F s displaystyle F o lt F s to w M s o displaystyle w notin M s o Dokaz Neobhidnist tverdzhennya Nehaj sistema S n0 R T displaystyle Sigma nu 0 R T bezpechna U comu vipadku pochatkovij stan n0 displaystyle nu 0 bezpechnij za viznachennyam Pripustimo sho isnuye bezpechnij stan n displaystyle nu dosyazhnij iz stanu n T n r n displaystyle nu T nu r nu i dlya danogo perehodu porusheno odnu z umov 1 4 Legko pomititi sho yaksho porusheni vlastivosti 1 abo 2 to stan n displaystyle nu ne bude bezpechnim po chitannyu a yaksho porusheni vlastivosti 3 abo 4 to stan n displaystyle nu ne bude bezpechnim po zapisu U oboh vipadkah stan n displaystyle nu ne ye bezpechnim Dostatnist tverdzhennya Sistema S n0 R T displaystyle Sigma nu 0 R T mozhe buti nebezpechnoyu u dvoh vipadkah U vipadku yaksho pochatkovij stan n0 displaystyle nu 0 nebezpechnij Odnak ce tverdzhennya superechit umovam teoremi Yaksho isnuye nebezpechnij stan n displaystyle nu dosyazhnij z bezpechnogo stanu n0 displaystyle nu 0 shlyahom zastosuvannya skinchennogo chisla zapitiv R displaystyle R Ce oznachaye sho na pevnomu promizhnomu etapi vidbuvsya perehid T n r n displaystyle T nu r nu de n displaystyle nu bezpechnij stan a n displaystyle nu nebezpechnij Odnak umovi 1 4 roblyat takij perehid nemozhlivim NedolikiPonizhennya rivnya tayemnosti Cya vrazlivist polyagaye u tomu sho klasichna model ne poperedzhuye ponizhennya rivnya tayemnosti ob yekta zminu rivnya tayemnosti azh do vidkrita za bazhannyam sub yekta z dopuskom do cilkom tayemno Napriklad nehaj sub yekt z visokim rivnem dostupu A chitaye informaciyu z ob yekta z tim zhe rivnem tayemnosti Dali vin ponizhuye svij riven do nizkogo B i zapisuye zchitanu ranishe informaciyu u ob yekt z nizkim rivnem tayemnosti Takim chinom hoch model formalno ne porushena bulo porusheno politiku bezpeki Dlya virishennya ciyeyi problemi vvodyatsya pravila Pravilo silnogo spokoyu rivni bezpeki sub yektiv i ob yektiv nikoli ne zminyuyutsya pid chas roboti sistemi Pravilo slabkogo spokoyu rivni bezpeki sub yektiv i ob yektiv nikoli ne zminyuyutsya pid chas roboti sistemi takim chinom shob porushiti zadanu politiku bezpeki Viddalene chitannya Cya vrazlivist proyavlyayetsya u rozpodilenih komp yuternih sistemah Pripustimo sub yekt A z visokim rivnem dostupu namagayetsya prochitati informaciyu ob yekta B z nizkim rivnem tayemnosti Pid chas operaciyi mizh viddalenimi ob yektami vidbuvayetsya utvorennya potoku informaciyi vid ob yekta sho chitayetsya do sub yekta yakij zapitav chitannya Cej potik ye bezpechnim tomu sho informaciya nedostupna neavtorizovanim sub yektam Odnak u rozpodilenij sistemi chitannya iniciyuyetsya zapitom vid odnogo ob yekta do inshogo Takij zapit stvoryuye potik informaciyi yakij napravlenij vid ob yekta z visokim rivnem tayemnosti do ob yekta z nizkim rivnem tayemnosti sho zaboroneno klasichnoyu modellyu Bela LaPaduli Div takozhDerzhavna tayemnicya Informacijna bezpeka Keruvannya dostupomPrimitkiBell David Elliott and LaPadula Leonard J Secure Computer Systems Mathematical Foundations PDF MITRE Corporation 1973 z dzherela 18 chervnya 2006 Procitovano 15 sichnya 2016 Bell David Elliott and LaPadula Leonard J Secure Computer System Unified Exposition and Multics Interpretation PDF MITRE Corporation 1976 z dzherela 29 serpnya 2008 Procitovano 15 sichnya 2016 Bell David Elliott December 2005 PDF Proceedings of the 21st Annual Computer Security Applications Conference Tucson Arizona USA s 337 351 doi 10 1109 CSAC 2005 37 Arhiv originalu PDF za 21 lyutogo 2020 Procitovano 15 sichnya 2016 Slides Looking Back at the Bell LaPadula Model 8 chervnya 2008 u Wayback Machine Sandhu Ravi S 1994 PDF Handbook of Information Security Management 1994 95 Yearbook Auerbach Publishers s 145 160 Arhiv originalu PDF za 1 veresnya 2006 Procitovano 12 serpnya 2006 LiteraturaCirlov V L Osnovy informacionnoj bezopasnosti avtomatizirovannyh sistem R Feniks 2008 S 40 44 ISBN 978 5 222 13164 0 Devyanin P N Modeli bezopasnosti kompyuternyh sistem Uchebnoe posobie dlya studentov vysshih uchebnyh zavedenij M Izdatelskij centr Akademiya 2005 S 55 66 ISBN 5 7695 2053 1 Grusho A A Timonina E E Teoreticheskie osnovy zashity informacii M Izdatelstvo Agentstva Yahtsmen 1996 S 52 55 A P Baranov N P Borisenko P D Zegzhda A G Rostovcev Kort S S Matematicheskie osnovy informacionnoj bezopasnosti M Izdatelstvo Agentstva Yahtsmen 1997 C 22 36