Коротко: три уровня валидации безопасности дополняют друг друга — модели угроз для управления риском и приоритезации, статический анализ для автоматического поиска классических уязвимостей в коде, формальная верификация для математически обоснованных гарантий критичных компонентов.
$1$ Модели угроз
- Что: систематический анализ кто, как и зачем может атаковать систему (методики: STRIDE, PASTA, attack trees, DREAD).
- Задачи: выявить активы, атакующие поверхности, сценарии атак, вероятности/влияния; задать требования безопасности и приоритеты.
- Когда оправдано: всегда на стадии проектирования и архитектуры; особенно важно при новом дизайне, интеграциях, при требовании соответствия регуляциям или когда ресурсы на исправления ограничены.
- Плюсы/минусы: дешёвая проактивная мера, ориентирует инженерные усилия; не даёт доказательств корректности кода, зависит от полноты и квалификации аналитиков.
$2$ Статический анализ
- Что: автоматический анализ кода без запуска (линейные линтеры, SAST, taint-анализ, абстрактная интерпретация, символьное исполнение, bounded model checking). Инструменты: clang-tidy, Frama‑C, Infer, Coverity, CBMC и др.
- Задачи: находить буферные переполнения, null‑deref, утечки, инъекции, небезопасные API-использования; проверять соответствие политик.
- Когда оправдано: всегда в разработке/CI для большого объёма кода; особенно полезно для сервисного кода, библиотек, приложений с частыми релизами.
- Плюсы/минусы: масштабируемо, автоматично, интегрируется в пайплайн; даёт много быстрых находок. Ограничения — ложные срабатывания, возможные пропуски (неполнота), символьное исполнение/брут‑форс ограничены путевой экспоненциальностью и границами проверок.
$3$ Формальная верификация
- Что: математическое доказательство свойств системы на модели или исходном коде (методы: model checking, SMT/SAT, исчисление высказаний, интерактивные доказатели). Инструменты: SPIN, TLA+, Alloy, Coq, Isabelle/HOL, Dafny, VCC, VeriFast и др.
- Задачи: доказать отсутствие классов ошибок (deadlock, нарушение инвариантов), корректность протоколов, соответствие спецификации.
- Когда оправдано: для критичных компонентов с высокими требованиями надёжности/безопасности — криптопримитивы, ядра/микроядра, контроллеры авионики/медицины, блоки консенсуса; когда требуется сертификация (DO‑178C, Common Criteria) или потенциальный ущерб от ошибки очень велик. Также оправдано при небольшом объёме кода (малый TCB) или при возможности формализовать спецификацию.
- Плюсы/минусы: даёт сильные гарантии в пределах модели/спецификации; очень дорогая по времени и экспертизе, подвержена ошибкам моделирования, плохо масштабируется без абстракций.
Рекомендация по применению (кратко):
- Используйте модели угроз на ранних стадиях всегда.
- Внедряйте статический анализ в CI как стандартную практику для большинства кода.
- Применяйте формальную верификацию селективно — к небольшим, критичным модулям или там, где экономически/регуляторно оправдано.
- Комбинация: модель угроз → автоматический статический анализ + fuzzing для широкого покрытия → формальная верификация для критичных частей или обнаруженных сложных сценариев.
Если нужно, могу привести пример критериев «когда верифицировать» в виде чек‑листа или подобрать инструменты под ваш стек.