Відповідно до запропонованої раніше об'єктно-концептуальної моделі
РПЗ, множина А
рs
складається з трьо х підмножин: А
ps
=U
ps
∪R
ps
∪W
ps
∪E
ps
, де
U
ps
={u
p
(x)|х∈R
ss
} – обмеження на доступ до ресурсів. Елементи цієї множини
виражають заборону на використання даною програмою ресурсів апаратури й
операційної системи, наприклад, оперативної пам’яті, процесорного часу,
ресурсів ОС, можливостей інтерфейсу й ін. R
ps
={r
p
(x)|х∈D
ss
}, W
ps
={w
p
(x)|х∈D
ss
}
– обмеження на доступ до об’єктів, що містять дані (інформацію). Ці множини
забороняють доступ програм і до певних областей пам’яті, файлів, баз даних і
т.д. E
ps
={e
p
(x)|х∈P
ss
} – обмеження на запуск програм. Ці обмеження в
основному мають сенс для багатозадачних, многопоточных, а також
розподілених систем і приймають форму заборон на породження процесів,
установлення сеансів зв’язку і т.д.
Оскільки множина заборонених відносин А
рs
містить у собі множину
нелегітимних відносин L
p
, для доказу тог о , щ о д о сл ідж у в а на п р о гр ам а
задовольняє вимогам по безпеці, запропонов аним на передбачуваному об’єкті
експлуатації, досить довести, що програма при роботів цій системі не
встановлює жодну з відносин, що входять до множини А
рs
.
Тоді задача аналізу безпеки формалізується в такий спосіб: для того щоб
довести, що програма р є безпечною для застосування у обчислювальній
системі Σ досить довести, що робочий простір п рограми р у обчислювальній
системі
Σ
не містить заборонених відносин, тобто А
р
∩А
рs
=∅.
Очевидно, що набір відносин, який установлюється програмою з об’єктами
обчислювальної системи, залежить від вхідних даної програми, вихідного стану
обчислювальної системи і інтерактивної взаємодії програми з к ористувачем.
Для розв’язку цієї проблеми залучаються методи функціонального тестування,
які традиційно використовуються при верифікації (аналізі правильності)
програм [54]. За їх доп ом ог ою м ож на с тво рит и пр едс та вни цьк ий н абір т ест ів,
що дозволяє одержати робочий простір програми за допомогою обмеженого
числа тестів. Однак, з урахуванням обмеженого обсягу іспитів, контрольно-
іспитові методи, крім тестових запусків, включають механізми екстраполяції