Рассмотрен подход к оценке защищенности информационных систем путем представления и проверки безопасности их состояний с использованием логики предикатов. Представлен пример применения логического анализа настроек безопасности. Предложенный подход является основой для разработки средств автоматического доказательства безопасности информационных систем. Он реализован с помощью механизмов вычислительного ядра системы "Декарт ", которая в автоматизированном режиме выполняет анализ безопасности настроек операционной системы семейства Windows. Ключевые слова: автоматизированный анализ, оценка безопасности, критерий, логика предикатов, настройки безопасности, информационная безопасность, уязвимость.
