Формальные методы - мощные математические инструменты для создания надежного и безопасного ПО. Вот ключевые моменты:
- Используют строгие математические подходы для разработки и проверки ПО
- Позволяют доказать отсутствие уязвимостей на уровне проектирования
- Применяются в критически важных системах (авиация, военная сфера и др.)
- Обеспечивают высокий уровень гарантий безопасности
Основные типы формальных методов:
| Метод | Описание | Применение |
|---|---|---|
| Проверка моделей | Автоматизированный анализ моделей систем | Поиск ошибок в параллельных системах |
| Доказательство теорем | Математическое доказательство на основе логики | Верификация криптографических протоколов |
| Статический анализ | Анализ кода без выполнения | Поиск типовых ошибок в коде |
| Абстрактная интерпретация | Анализ на основе упрощенной модели программы | Проверка свойств безопасности |
Несмотря на сложность применения, формальные методы становятся неотъемлемой частью разработки критически важных систем, обеспечивая беспрецедентный уровень кибербезопасности.
История формальных методов
Ранние дни в информатике
Формальные методы берут свое начало в математической логике и теоретической информатике. Их история уходит корнями в работы выдающихся математиков и логиков:
- Готфрид Вильгельм Лейбниц предложил идею символического языка для интеллектуального дискурса
- Джордж Буль и Огастес де Морган разработали булеву алгебру
- Готлоб Фреге создал первое аксиоматическое представление логики предикатов (Begriffsschrift)
- Бертран Рассел и Альфред Норт Уайтхед попытались описать основы математики чисто логическим способом в Principia Mathematica
Эти работы заложили фундамент для развития формальных методов в компьютерных науках.
В 1954 году Мартин Дэвис разработал первое компьютерное доказательство теоремы для разрешимого фрагмента логики первого порядка. Это стало важным шагом в развитии автоматизированных методов доказательства.
Рост в сфере безопасности
Применение формальных методов в кибербезопасности началось в 1970-х годах. Они использовались для удовлетворения государственных требований к безопасности критически важных систем.
Ключевые вехи:
- 1972: Роберт С. Бойер и Дж. Строзер Мур создали Nqthm - первый успешный машинный доказыватель теорем
- 1994: Ричард Кеммерер, Кэтрин Медоуз и Джон Миллен применили формальные методы для обнаружения неизвестных уязвимостей в криптографическом протоколе
"Формальные методы так же хорошо подходят для решения проблем безопасности, как и для решения проблем безопасности." - Конни Хайтмейер, Naval Research Labs
Сегодня формальные методы широко применяются в разработке аэрокосмического ПО NASA и верификации аппаратного обеспечения в компаниях AMD и Intel.
Эксперты отмечают, что формальные методы способны выявлять проблемы, которые могут быть пропущены при тестировании или ручном анализе. Это делает их особенно ценными для обеспечения безопасности сложных систем.
Ключевые идеи
Математические основы
Формальные методы в кибербезопасности опираются на строгие математические принципы для доказательства защищенности систем от кибератак. Вот основные математические концепции:
- Математическая логика: Используется для создания точных описаний поведения систем и формулировки требований безопасности.
- Теория множеств: Применяется для моделирования состояний системы и операций над ними.
- Теория графов: Помогает анализировать структуру программ и потоки данных.
- Теория вероятностей: Используется для оценки рисков и моделирования случайных процессов в системах безопасности.
Эти математические инструменты позволяют создавать точные модели систем и проводить строгие доказательства их свойств безопасности.
Формальные языки
Формальные языки играют ключевую роль в описании свойств систем и спецификации требований безопасности. Основные типы формальных языков:
| Тип языка | Описание | Пример применения |
|---|---|---|
| Логика первого порядка | Позволяет выражать сложные утверждения о системе | Спецификация свойств безопасности протоколов |
| Темпоральная логика | Описывает поведение системы во времени | Верификация параллельных программ |
| Языки спецификаций | Специализированные языки для описания требований | Формальная спецификация криптографических протоколов |
Использование формальных языков помогает однозначно описать требования безопасности и избежать двусмысленностей, которые могут привести к уязвимостям.
Важно отметить, что применение формальных методов требует специальных навыков и ресурсов. Однако результаты могут быть очень значимыми. Например, исследователи из Carnegie Mellon University CyLab разработали инструмент для математического доказательства корректности параллельных программ. А криптографическая библиотека EverCrypt, разработанная с использованием формальных методов, была интегрирована в ядро Linux.
"Доказательство теорем о программах было мечтой компьютерных наук последние 60 лет или более, и мы наконец можем делать это в масштабах, необходимых для важного, широко развернутого критически важного для безопасности программного обеспечения." - Сотрудник команды Microsoft
Формальные методы позволяют достичь уровня гарантий безопасности, сравнимого с математическими доказательствами. Это особенно важно для критически важных систем, где цена ошибки может быть очень высока.
Типы формальных методов
В кибербезопасности используются различные формальные методы для проверки и обеспечения безопасности систем. Рассмотрим основные из них:
Проверка моделей
Проверка моделей - это автоматизированный метод верификации систем. Он позволяет:
- Создавать математические модели систем
- Проверять выполнение заданных свойств безопасности
- Находить ошибки в параллельных и распределенных системах
Например, исследователи из Carnegie Mellon University CyLab разработали инструмент для математического доказательства корректности параллельных программ с помощью проверки моделей.
Доказательство теорем
Доказательство теорем - это метод, основанный на математической логике. Его особенности:
- Позволяет работать со сложными формализмами
- Требует участия человека-эксперта
- Обеспечивает высокий уровень гарантий безопасности
Пример успешного применения - криптографическая библиотека EverCrypt, разработанная с использованием доказательства теорем и интегрированная в ядро Linux.
Статический анализ
Статический анализ проводится без выполнения программы и позволяет:
- Находить типовые ошибки в коде
- Проверять соответствие стандартам кодирования
- Выявлять потенциальные уязвимости
Например, компания Polyspace разработала инструменты статического анализа для поиска ошибок переполнения буфера, деления на ноль и других проблем в программах на C/C++.
Абстрактная интерпретация
Абстрактная интерпретация - это метод анализа программ, который:
- Создает упрощенную модель программы
- Позволяет проверять свойства безопасности
- Эффективен для поиска ошибок доступа к памяти
Один из разработчиков создал инструмент статического анализа для программ на языке IEC61131-3, используемом в программируемых логических контроллерах. Инструмент включает простой движок абстрактной интерпретации на основе z3.
Таблица сравнения формальных методов:
| Метод | Подход | Сильные стороны | Слабые стороны |
|---|---|---|---|
| Проверка моделей | Автоматизированный анализ моделей систем | Эффективен для поиска взаимоблокировок и состояний гонки | Ограничен свойствами, которые можно смоделировать |
| Доказательство теорем | Математическое доказательство на основе логики | Высокая надежность, устраняет целые классы ошибок | Требует специальных навыков, трудоемкий процесс |
| Статический анализ | Автоматизированный анализ кода без выполнения | Быстрый, обнаруживает распространенные ошибки кодирования | Может давать ложные срабатывания, ограничен качеством кода |
| Абстрактная интерпретация | Анализ на основе упрощенной модели программы | Эффективен для проверки свойств безопасности | Может пропускать ошибки из-за упрощения модели |
Каждый из этих методов имеет свои преимущества и ограничения. Выбор конкретного метода зависит от специфики проекта, доступных ресурсов и требуемого уровня гарантий безопасности.
Где используются формальные методы
Формальные методы находят применение в различных областях кибербезопасности, помогая обеспечить надежность и безопасность систем. Рассмотрим основные сферы их использования:
Проверка протоколов
Формальные методы активно применяются для анализа и верификации криптографических протоколов. Например:
- Инструмент Tamarin Prover используется для символического моделирования и анализа протоколов безопасности.
- При разработке протокола TLS 1.3 применялись формальные методы с использованием механизированных доказателей для детального анализа.
Проверка программного обеспечения
В сфере разработки ПО формальные методы помогают находить уязвимости и доказывать корректность кода:
- Фреймворк Frama-C применяется для формальной верификации свойств безопасности в программах на C.
- ANSSI использовала комбинацию инструментов Eva и Wp для доказательства отсутствия ошибок времени выполнения в эталонной реализации парсера X.509.
Безопасность аппаратного обеспечения
Формальные методы играют важную роль в обеспечении безопасности аппаратных систем:
- Инструменты формальной верификации, такие как Verilog и SystemVerilog, используются для проверки аппаратного обеспечения с 1984 года.
- Программа HACMS агентства DARPA продемонстрировала, что применение формальных методов при разработке бортового ПО для квадрокоптера привело к созданию кода, крайне устойчивого к кибератакам.
Проверка методов шифрования
Формальные методы активно применяются для верификации криптографических алгоритмов и их реализаций:
- Команда Project Everest разработала High-Assurance Cryptographic Library (HACL*), которая используется в Mozilla Firefox и ядре Linux.
- Код из проекта Fiat Cryptography был интегрирован в BoringSSL, используемый в Google Chrome.
- Инструмент Cryptoline применяется для верификации реализаций в OpenSSL, BoringSSL и mbed TLS.
Таблица: Примеры использования формальных методов в различных областях
| Область | Пример применения | Результат |
|---|---|---|
| Протоколы | Анализ TLS 1.3 | Повышение безопасности протокола |
| ПО | Верификация парсера X.509 | Доказательство отсутствия ошибок времени выполнения |
| Аппаратное обеспечение | Программа HACMS для квадрокоптера | Создание кода, устойчивого к кибератакам |
| Криптография | Библиотека HACL* | Интеграция в Firefox и ядро Linux |
Как отметил Карфикеян Баргаван, директор по исследованиям в Inria, Париж:
"Формальные методы могут закрыть этот пробел, предоставляя всесторонние гарантии для криптографического механизма против некоторого четко определенного набора атакующих."
Использование формальных методов особенно важно в отраслях, где соблюдение строгих стандартов является обязательным, например, в авионике или медицинском оборудовании, где программная ошибка может иметь катастрофические последствия.
Преимущества формальных методов
Формальные методы предоставляют ряд существенных преимуществ в сфере кибербезопасности:
Надежные гарантии безопасности
Формальные методы обеспечивают математически обоснованные гарантии безопасности систем:
- Позволяют доказать отсутствие ошибок в программном коде
- Выявляют сложные уязвимости на ранних этапах разработки
- Предоставляют уровень уверенности, недостижимый другими методами
Как отметил д-р Ашиш Дарбари, генеральный директор Axiomise:
"Формальная верификация может доказать отсутствие ошибок, одновременно обнаруживая граничные случаи ошибок за считанные секунды."
Раннее обнаружение проблем
Интеграция формальных методов в процесс разработки позволяет:
- Выявлять ошибки на ранних этапах, когда их исправление менее затратно
- Сокращать общее количество дефектов в программном обеспечении
- Ускорять процесс разработки за счет автоматизации проверок
| Этап разработки | Преимущество формальных методов |
|---|---|
| Проектирование | Выявление логических ошибок |
| Кодирование | Автоматическое обнаружение уязвимостей |
| Тестирование | Доказательство корректности критических функций |
Соответствие стандартам безопасности
Формальные методы помогают организациям:
- Соответствовать строгим отраслевым стандартам безопасности
- Упростить процесс сертификации программного обеспечения
- Снизить риски несоответствия нормативным требованиям
Фабьен Шуто, ведущий специалист по глобальному техническому маркетингу AdaCore, подчеркивает:
"Формальные методы могут быть включены в процесс разработки для снижения распространенности нескольких категорий уязвимостей."
Применение формальных методов особенно важно в критически важных системах, таких как авионика или медицинское оборудование, где программные ошибки могут иметь катастрофические последствия.
Проблемы и ограничения
При использовании формальных методов в кибербезопасности возникает ряд сложностей:
Работа с крупными системами
Применение формальных методов к большим и сложным системам представляет серьезную проблему:
- Увеличение масштаба системы значительно усложняет процесс верификации
- Инструменты вынуждены искать компромисс между точностью и масштабом анализируемого ПО
- Полная верификация крупных систем часто невозможна из-за огромного пространства состояний
Например, при разработке автономных систем сочетание дискретных и непрерывных аспектов делает верификацию всей системы практически невыполнимой задачей.
Сложность применения
Формальные методы требуют специальных знаний и навыков:
- Необходимо глубокое понимание математики и теории доказательств
- Разработка формальных спецификаций - сложная задача, требующая опыта
- Написание доказательств занимает много времени и ресурсов
| Аспект | Сложность |
|---|---|
| Спецификации | Перевод требований в формальный вид |
| Доказательства | Более строгие, чем в традиционной математике |
| Инструменты | Требуют специальных навыков использования |
"Написание доказательств требует временных затрат, которые обычно измеряются в человеко-годах, а объем доказательств может в несколько раз превышать объем кода реализации." - Nelson et al., SOSP'19
Потребность в ресурсах
Применение формальных методов требует значительных ресурсов:
- Высокие затраты времени на разработку спецификаций и доказательств
- Необходимость в квалифицированных специалистах по формальным методам
- Дорогостоящие инструменты и программное обеспечение
Например, проект IronFleet использовал передовые SMT-решатели и современный язык верификации для написания 5000 строк проверенного кода Dafny за 3,7 человеко-лет, в среднем по 4 строки в день.
Несмотря на эти сложности, формальные методы остаются мощным инструментом для обеспечения безопасности критически важных систем. Их применение требует тщательного планирования и оценки соотношения затрат и выгод в каждом конкретном случае.
sbb-itb-b726433
Инструменты и технологии
Популярные инструменты
В области формальных методов для кибербезопасности существует ряд широко используемых инструментов:
| Инструмент | Описание | Применение |
|---|---|---|
| Frama-C | Платформа для анализа C-кода с формальными аннотациями ACSL | Верификация библиотек и приложений |
| KeY | Система формальной верификации | Проверка корректности Java-программ |
| Z3 | Эффективный SMT-решатель | Используется в различных инструментах формальных методов |
| VC Formal™ | Инструмент формальной верификации от Synopsys | Анализ и проверка RTL-дизайнов |
| TLA+ | Язык формальных спецификаций | Документирование и проверка требований к системе |
Frama-C зарекомендовал себя в промышленных проектах. Например, ANSSI использовала комбинацию модулей Eva и Wp для доказательства отсутствия ошибок времени выполнения в эталонной реализации парсера X.509.
Использование в разработке
Инструменты формальных методов интегрируются в процесс разработки следующим образом:
-
Ранний анализ: Инструменты вроде VC Formal™ позволяют анализировать RTL-дизайны на ранних этапах без сложной настройки или тестовых сценариев.
-
Верификация спецификаций: Языки вроде TLA+ помогают формально описать требования к системе и проверить их на непротиворечивость.
-
Доказательство корректности: Инструменты типа KeY применяются для строгого доказательства корректности критически важных компонентов.
-
Поиск ошибок: Формальные методы позволяют находить сложные ошибки до этапа симуляции, ускоряя разработку.
"Использование MetAcsl и Wp сыграло важную роль в сертификации виртуальной машины JavaCard компании Thales на уровне EAL7." - из отчета о применении Frama-C
Несмотря на сложность освоения, формальные методы становятся все более доступными для применения в разработке ПО за пределами критически важных встраиваемых систем.
Реальные примеры
Использование в промышленности
Формальные методы активно применяются в различных отраслях для повышения кибербезопасности:
-
Транспорт: Siemens Transportation Systems использует метод B для разработки систем автоматизации метро в Париже и Сан-Паулу. Это обеспечивает высокий уровень безопасности на всех этапах жизненного цикла.
-
Авиация: NASA применяет формальные методы для верификации систем управления воздушным движением и автопилотов самолетов. Это критически важно для безопасности полетов.
-
Военная сфера: DARPA активно разрабатывает фреймворки на основе формальных методов для усиления кибербезопасности военных систем. В 2022 году стартовала программа Constellation между DARPA и Кибернетическим командованием США для ускоренного внедрения кибертехнологий.
"Эти методы начинают демонстрировать большие перспективы в повышении безопасности и действительно повышают нашу эффективность во всех вооруженных силах." - Бенджамин У. Бишоп, заместитель директора по переходу в Управлении адаптивных возможностей DARPA.
- Криптография: Проект Everest разработал верифицированную криптографическую библиотеку HACL*, которая используется в Firefox. Fiat Cryptography применяется в Chrome, Firefox и ядре Linux для VPN WireGuard.
Прогресс в исследованиях
Академические исследования также демонстрируют значительный прогресс:
- Верифицированные криптобиблиотеки: Команда CyLab под руководством Брайана Парно создала первую в мире верифицируемо безопасную промышленную криптографическую библиотеку EverCrypt, которая была интегрирована в ядро Linux.
"В статье, представленной на симпозиуме USENIX Security, Брайан Парно и команда исследователей продемонстрировали новый инструмент программирования, который позволяет создавать высокопроизводительный криптографический код, верифицируемо корректный и безопасный." - Исследовательская команда CyLab.
-
Верификация смарт-карт: Исследователи успешно применили формальные методы для разработки и сертификации безопасности программного обеспечения смарт-карт Java Card по высшему уровню безопасности Common Criteria.
-
Автономные системы: Программа HACMS продемонстрировала эффективность формально верифицированного ПО на примере беспилотного вертолета Boeing AH-6, успешно противостоявшего кибератакам в полете в феврале 2017 года.
Эти примеры показывают, что формальные методы становятся неотъемлемой частью разработки критически важных систем, обеспечивая беспрецедентный уровень кибербезопасности.
Будущие направления
Новые подходы
Формальные методы в кибербезопасности переживают возрождение и интегрируются в основные практики разработки программного обеспечения. Новые подходы делают их более применимыми к сложным инженерным задачам, включая разработку целых операционных систем и критически важных компонентов ПО.
Ключевые направления развития:
-
Интеграция в процесс разработки: Ведущие технологические компании внедряют формальные методы для повышения безопасности и надежности ПО. Например, Amazon Web Services создала специальную команду, использующую формальные методы для обеспечения "доказуемой безопасности" для своих клиентов.
-
Масштабирование: Microsoft работает над доказательством теорем о программах в масштабах, необходимых для широко распространенного критически важного ПО.
-
Непрерывная верификация: Facebook интегрировал методы формальной верификации в свою систему INFER, которая постоянно проверяет код при каждом обновлении мобильных приложений.
-
Гибридная верификация: Сочетание тестирования и формальных методов для использования сильных сторон обоих подходов. Язык SPARK, формально анализируемое подмножество Ada 2012, иллюстрирует, как гибридная верификация может повысить надежность критически важного ПО.
Работа с ИИ
Интеграция формальных методов и искусственного интеллекта открывает новые возможности для повышения безопасности и надежности систем ИИ:
1. Верифицируемый ИИ
Цель - создание систем ИИ с сильными, в идеале доказуемыми, гарантиями корректности относительно математически заданных требований. Это включает:
- Разработку языков и алгоритмов для моделирования окружающей среды и данных
- Создание абстракций и представлений для сложных компонентов и систем машинного обучения
- Разработку новых формализмов спецификации и свойств для систем ИИ и данных
2. Повышение надежности систем машинного обучения
Формальные методы применяются для:
- Оценки точности и надежности систем МЛ в критических приложениях (автономное вождение, медицинская диагностика)
- Обнаружения и устранения недостатков и уязвимостей в системах МЛ
- Снижения риска непредвиденных последствий и повышения общей производительности
3. Объяснимый ИИ (XAI) и формальные методы
Интеграция XAI и формальных методов для обеспечения корректности внутреннего принятия решений моделями "черного ящика":
- Использование техник XAI (LIME, SHAP) для интерпретации моделей
- Применение формальных методов для валидации и объяснения внутреннего принятия решений
Пример: Исследователи разработали подход, объединяющий XAI и формальные методы для повышения надежности ИИ-диагностики в здравоохранении. Методология включает обучение моделей "черного ящика" на нейронных сетях, интерпретацию с помощью LIME и SHAP, и применение формальных методов для обеспечения корректности.
Эти направления демонстрируют, как формальные методы могут способствовать созданию более безопасных и надежных систем ИИ в будущем.
Советы по использованию формальных методов
Начало работы
Чтобы начать применять формальные методы в организации:
1. Определите подходящую область применения. Начните с небольших, критически важных компонентов системы. Например, Amazon Web Services использует инструмент SAW для проверки безопасности своих криптографических систем.
2. Выберите подходящий инструмент. Рассмотрите такие варианты:
- Alloy для моделирования и анализа
- SPARK для высоконадежного ПО
- Z для спецификации
3. Интегрируйте в существующий процесс разработки. Facebook внедрил формальную верификацию в свою систему INFER, которая проверяет каждый коммит в кодовых базах C и Java.
4. Начните с документирования. Напишите спецификации для существующей системы, чтобы получить практический опыт.
5. Продемонстрируйте ценность. Покажите, как формальные методы могут выявить скрытые ошибки. Например, Microsoft использует Static Driver Verifier для проверки правильности взаимодействия драйверов устройств с ядром Windows.
Обучение и навыки
Для эффективного использования формальных методов необходимо:
1. Изучить основы. Рекомендуемые книги:
- "Software Foundations" от Benjamin C. Pierce и др.
- "Introduction to the Theory of Computation" от Michael Sipser
- "Principles of Model Checking" от Christel Baier и Joost-Pieter Katoen
2. Пройти онлайн-курсы. Платформы Coursera и edX предлагают курсы от университетов Stanford, MIT и ETH Zurich.
3. Практиковаться с инструментами. Освойте такие инструменты, как Alloy, TLA+, SPIN или NuSMV, используя прилагаемые к ним учебные пособия и примеры.
4. Развивать математическое мышление. Формальные методы требуют навыков работы с математической логикой и доказательствами.
5. Участвовать в сообществе. Используйте ресурсы вроде Formal Methods Wiki и сабреддита Formal Methods для обмена опытом и получения поддержки.
Помните, что главным препятствием в использовании формальных методов является образование. Инвестируйте в обучение инженеров для лучшего понимания и применения этих методов.
Заключение
Ключевые выводы
Формальные методы в кибербезопасности предоставляют мощные инструменты для создания надежного и безопасного программного обеспечения. Вот основные моменты:
- Математическая основа: Формальные методы используют математические доказательства для обеспечения безопасности систем.
- Раннее обнаружение уязвимостей: В отличие от традиционного подхода, формальные методы позволяют выявлять проблемы безопасности до того, как они станут угрозой.
- Широкое применение: От криптографических библиотек до операционных систем, формальные методы находят применение в различных областях.
Взгляд в будущее
Формальные методы играют все более важную роль в кибербезопасности:
- Интеграция в разработку: Крупные технологические компании, такие как Amazon, Facebook и Microsoft, внедряют формальные методы в свои процессы разработки.
- Повышение доступности: Снижение стоимости инструментов статического анализа делает формальные методы более доступными для широкого круга разработчиков.
- Стандартизация: Организации, такие как NIST и ANSSI, рекомендуют использование формальных методов в разработке программного обеспечения.
Пример успешного применения формальных методов:
"Код из криптографической библиотеки EverCrypt, которая была разработана с использованием формальных методов, был официально включен в ядро Linux." - Брайан Парно, исследователь CyLab
Этот факт демонстрирует, что формальные методы не только теоретически обоснованы, но и практически применимы в крупномасштабных проектах.
Таблица: Преимущества формальных методов в кибербезопасности
| Преимущество | Описание |
|---|---|
| Надежность | Математическое доказательство безопасности |
| Раннее обнаружение | Выявление уязвимостей на этапе разработки |
| Соответствие стандартам | Помощь в достижении высоких уровней сертификации (например, EAL7) |
| Экономическая эффективность | Снижение затрат на устранение ошибок в долгосрочной перспективе |
В будущем ожидается дальнейшее развитие и распространение формальных методов в кибербезопасности, что приведет к созданию более защищенных и надежных систем.
Часто задаваемые вопросы
В чем разница между формальной верификацией и символьным выполнением?
Формальная верификация и символьное выполнение - это два связанных понятия в области формальных методов кибербезопасности. Вот ключевые различия:
| Аспект | Формальная верификация | Символьное выполнение |
|---|---|---|
| Определение | Доказательство или опровержение свойств системы с помощью математической модели | Техника анализа программ, используемая для формальной верификации |
| Цель | Проверка корректности всей системы | Анализ конкретных путей выполнения программы |
| Область применения | Широкая - от протоколов до аппаратного обеспечения | В основном программное обеспечение |
| Результат | Математическое доказательство корректности | Набор символьных выражений и ограничений |
Фабьен Шуто, ведущий специалист по глобальному техническому маркетингу AdaCore, объясняет:
"Формальная верификация - это акт доказательства или опровержения заданного свойства системы с использованием математической модели. Символьное выполнение - это одна из техник, используемых для формальной верификации."
Символьное выполнение предоставляет механизм для формального доказательства корректности программ. Оно позволяет создать набор правил вывода, которые полезны для выражения семантики языка и формируют основу для автоматического генератора условий верификации.
