Методы и модели анализа безопасности программного обеспечения

Выделяют формальные методы доказательства правильности программ (их верификация), а также методы анализа и оценки безопасности ПО.

Если первые методы обладают строгой доказуемостью (поэтому требование формальной верификации и предъявляется к сертификации по высоким классам защищенности), то вторые, как правило – оценочные, вероятностные.

Формальные методы доказательства

правильности программ и их спецификаций

Начало данному направлению было положено работами П. Наура и Р. Флойда, в которых сформулирована идея приписывания точке программы так называемого индуктивного, или промежуточного утверждения и указана возможность доказательства частичной правильности программы, построенного на установлении согласованности индуктивных утверждений.

Формальное доказательство в виде вывода в некоторой логической системе вполне надежно, но сами доказательства оказываются очень длинными и часто необозримыми.

Методы доказательства правильности программ могут быть применены для анализа безопасности ПО при существенных ограничениях на размеры и сложность создаваемых программ. Поэтому в частных случаях они могут оказаться более эффективными, чем другие известные методы анализа программ.

Анализ и оценка безопасности программного обеспечения

Выделяют две категории методов анализа и оценки безопасности ПО – контрольно-испытательные и логико-аналитические (см. рис. 62).

Контрольно-испытательные методы анализа рассматривают АД через призму фиксации факта нарушения безопасного состояния системы, а логико-аналитические – через призму доказательства наличия отношения эквивалентности между моделью исследуемой программы и моделью АД.

Комплексная система исследования безопасности ПО должна включать как контрольно-испытательные, так и логико-аналитические методы анализа, используя преимущества каждого их них. С методической точки зрения логико-аналитические методы выглядят более предпочтительными, т.к. позволяют оценить надежность полученных результатов и проследить последовательность (путем обратных рассуждений) их получения. Однако эти методы пока еще мало развиты и, несомненно, более трудоемки, чем контрольно-испытательные.

Заменить РПС на АД

Рис. 62. Методы, модели и средства анализа безопасности программ