Проблемы математического, алгоритмического и программного обеспечения компьютерной безопасности


         

Доказательная база надежности реализации политики безопасности - часть 2


Верификация в автоматизированном режиме на основе формальных методов доказательства -- эффективный подход к обоснованию гарантированной защищенности компьютерных систем на всех этапах их жизненного цикла. Одним из важных является направление, связанное с созданием таких систем для обеспечения безопасности сложных программных комплексов. Актуальность данного направления повышается в связи с повсеместным использованием в составе таких комплексов программных средств, которые свободно распространяются через Интернет. Хорошие перспективы имеет использование систем автоматической верификации состояния защищенности в процессе функционирования практически значимых распределенных систем. Однако, несмотря на определенные теоретические заделы и отдельные прикладные разработки, эффективных решений для подобных систем пока нет. Такое положение, в первую очередь, связано с объективной трудностью их формального описания, учета многофакторных процессов, которые следует принимать во внимание. Необходим поиск подходов к созданию подсистем, автоматизирующих процессы верификации безопасности отдельных функционально замкнутых компонентов, описанию и практической реализации моделей их взаимодействия в составе больших распределенных систем. Теоретические основы для решения подобных задач, подходы к формализации программ и потенциальных средств разрушающего воздействия, методы анализа и инструментальные средства на этом направлении только создаются.

Если модель ПБ удается достаточно подробно и четко формализовать математически, то высока вероятность получить аналитически (привлекая математический аппарат) или путем строгих логических рассуждений доказательство гарантии выполнения объектом защиты ПБ. Для относительно простых систем и перечисленных выше моделей ПБ в условиях достаточно "жестких" дополнительных ограничений получить такие оценки можно. Их удается получить, например, в рамках модели "Take-Grant" [12], описывающей с помощью теории графов способы распространения прав доступа в системах с дискреционной ПБ, или теоретико-множественных моделей "Белла -- Лападула" [21,22], "Low-Water-Mark" [23,24], автоматной модели невлияния "Гогена -- Месгауэра" [25,26] для многоуровневых систем (мандатный контроль доступа), а также ряда других.




Содержание  Назад  Вперед