призводить запуск програми. Ці методи найбільш поширені, так як вони не вимагають формального аналізу, дозволяють використовувати наявні технічні та програмні засоби і швидко ведуть до створення готових методик. Як приклад - можна навести методику пробного запуску в спеціальному середовищі з фіксацією спроб порушення систем захисту та розмежування доступу. Розглянемо формальну постановку задачі аналізу безпеки ПЗ для вирішення її за допомогою контрольно-випробувальних методів. p align="justify"> Нехай задано безліч обмежень на функціонування програми, що визначають її відповідність вимогам з безпеки в системі передбачуваної експлуатації. Ці обмеження задаються у вигляді безлічі предикатів С = {ci (a1, a2, ... am) | i = 1, ..., N} залежних від безлічі аргументів A = {ai | i = 1, ..., M }.
Це безліч складається з двох підмножин:
підмножини обмежень на використання ресурсів апаратури та операційної системи, наприклад оперативної пам'яті, процесорного часу, ресурсів ОС, можливостей інтерфейсу та інших ресурсів;
підмножини обмежень, що регламентують доступ до об'єктів, що містить дані (інформацію), тобто областям пам'яті, файлів і т.д.
Для доказу того, що досліджувана програма задовольняє вимогам з безпеки, що пред'являються на передбачуваному об'єкті експлуатації, необхідно довести, що програма не порушує жодної з умов, що входять до С. Для цього необхідно визначити безліч параметрів P = {pi | i = 1, ..., K}, контрольованих при тестових запусках програми. Параметри, які входять у це безліч визначаються використовуваними системами тестування. Безліч контрольованих параметрів повинно бути вибрано таким чином, що по безлічі виміряних значень параметрів Р можна було отримати безліч значень аргументів А.
Після проведення Т випробувань за вектором отриманих значень параметрів Pi, i = 1, ..., T можна побудувати вектор значень аргументів Ai, i = 1, ..., T.
Тоді завдання аналізу безпеки формалізується наступним чином.
Програма не містить РПС, якщо для будь-якого її випробування i = 1, ..., T безліч предикатів C = {cj (a1i, a2i ... aMi) | j = 1, ... , N} істинно.
Очевидно, що результат виконання програми залежить від вхідних даних, оточення і т.д., тому при обмеженні ресурсів, необхідних для проведення випробувань, контрольно-випробувальні методи не обмежуються тестовими запусками і застосовують механізми екстраполяції результатів випробувань , включають в себе методи символічного тестування і інші методи, запозичені з досить проробленою теорії верифікації (тестування правильності) програми.
Контрольно-випробувальні методи аналізу безпеки починаються з визначення набору контрольованих параметрів середовища або програми. Необхідно відзначити, що цей набір параметрів буде залежати від використовуваного апаратно...
