# Байрон Кук из AWS: «ИИ и формальные методы — это шоколад и арахисовое масло для безопасности»

Источник: https://www.youtube.com/watch?v=Dm3DHPUFNwU
Канал: Cognitive Revolution "How AI Changes Everything"
Опубликовано: 24.12.2025

---

В эпоху, когда возможности искусственного интеллекта растут экспоненциально, кибербезопасность оказывается на перепутье. С одной стороны, ИИ дает хакерам беспрецедентные инструменты для поиска уязвимостей, с другой — предлагает путь к созданию «неуязвимого» программного обеспечения. В новом выпуске подкаста The Cognitive Revolution эксперты Кэтлин Фишер (RAND) и Байрон Кук (AWS) обсуждают, как формальные методы и автоматизированное доказательство теорем в связке с нейросетями могут раз и навсегда решить проблему критических ошибок в коде.

## 🛡️ ИИ в киберпространстве: Ускорение гонки вооружений
[[JUMP:05:11]]

Обсуждение будущего кибербезопасности Натан Лабенц начал с вопроса о балансе сил между нападением и защитой. По мнению Кэтлин Фишер, ИИ сегодня помогает злоумышленникам на всех этапах так называемой «цепочки поражения» (cyber kill chain) [07:10]. Она утверждает, что технологии одинаково эффективно усиливают как новичков («скрипт-кидди»), так и профессиональные хакерские группировки, поддерживаемые государствами.

Основные угрозы, которые выделяют эксперты:

*   **Масштабируемость атак:** ИИ позволяет хакерам работать параллельно над огромным количеством целей, что раньше было невозможно из-за ограниченности человеческих ресурсов [06:56].
*   **Реверс-инжиниринг:** Эксперты по безопасности, по словам Кэтлин Фишер, шокированы тем, насколько эффективно ИИ-инструменты справляются с обратной разработкой кода [07:48].
*   **Эксплуатация уязвимостей:** Байрон Кук отмечает, что современное ПО буквально «испещрено» дырами, и ИИ делает их поиск тривиальной задачей [09:19].

Однако Байрон Кук предлагает более оптимистичный взгляд: ИИ также помогает защитникам. Он считает, что мы переходим от социотехнических механизмов защиты (основанных на доверии к людям) к формализации безопасности, где каждый инцидент позволяет мгновенно улучшить систему для всех будущих случаев [08:53].

## 🧩 Формальные методы: Математика против хакеров
[[JUMP:10:23]]

Формальные методы — это не просто тестирование, а алгоритмический поиск математических доказательств того, что программа работает именно так, как задумано, и никак иначе. Байрон Кук описывает это как возможность «рассуждать о бесконечном за конечное время и в конечном пространстве» [10:48].

Кэтлин Фишер выделяет спектр сложности и надежности этих методов:

1.  **Слабые гарантии (Type Systems):** Например, система типов в Java или TypeScript. Она автоматически доказывает, что вы не пытаетесь сложить целое число с функцией [12:17].
2.  **Памятобезопасность (Memory Safety):** Языки вроде JavaScript обеспечивают ее автоматически, тогда как в языке C программист должен следить за памятью сам, что является источником большинства уязвимостей [16:10].
3.  **Полная функциональная корректность:** Вершина методов, требующая огромных вычислительных мощностей и участия ученых. Примером служит CompCert — верифицированный компилятор C, который гарантирует, что машинный код в точности соответствует исходному [13:22].

По словам Байрона Кука, формальные методы долгое время оставались «в монастырях» (академической среде), но развитие облачных вычислений и SAT-солверов (инструментов для решения задач логической исполнимости) позволило вывести их в индустрию [1:02:47].

## 🚁 Проект HACMS: Вертолет, который невозможно взломать
[[JUMP:31:13]]

Одним из самых ярких примеров эффективности формальных методов стал проект HACMS (High Assurance Cyber Military Systems), который Кэтлин Фишер возглавляла в DARPA. Целью было создание беспилотного вертолета Boeing Little Bird, защищенного от кибератак [31:13].

Результаты исследования показали:

*   **Базовый уровень:** До вмешательства группы «красная команда» (этичные хакеры) взломала вертолет всего за шесть недель [37:12].
*   **Архитектурная изоляция:** Разработчики использовали микроядро seL4 (математически верифицированное ядро сепарации). Систему разбили на разделы, изолировав критические функции управления полетом от второстепенных, например, от камеры [32:13].
*   **Испытания в воздухе:** На финальном этапе «красной команде» разрешили атаковать вертолет прямо во время полета с двумя пилотами на борту [35:40]. Хакеры смогли «уронить» только раздел камеры, но не смогли повлиять на управление или связь. Пилоты даже не заметили атаки [36:06].

Этот успех продемонстрировал, что математические доказательства могут обеспечить уровень безопасности, недоступный традиционным методам тестирования.

## ☁️ Опыт AWS: Безопасность на уровне миллиарда операций в секунду
[[JUMP:44:32]]

Байрон Кук рассказал, как формальные методы применяются в AWS (Amazon Web Services). Одной из ключевых задач было доказательство корректности интерпретатора политик доступа IAM.

Масштаб задачи впечатляет:

*   Интерпретатор политик вызывается более **1 миллиарда раз в секунду** [47:33].
*   Любая ошибка в логике «разрешить/запретить» может привести к утечке данных миллионов клиентов.
*   AWS внедрила инструменты автоматизированного рассуждения, такие как IAM Access Analyzer и VPC Reachability Analyzer, которые позволяют клиентам доказывать отсутствие нежелательных путей доступа в их сетях [46:41].

Кук подчеркивает, что формальные методы в AWS стали частью процесса непрерывной интеграции (CI/CD). Даже если инженер просто меняет имя переменной, система автоматически проверяет, не нарушило ли это доказательство корректности [1:04:07].

## 🤖 Нейросимволический ИИ: Шоколад и арахисовое масло
[[JUMP:1:13:00]]

Самым перспективным направлением спикеры считают слияние статистического ИИ (LLM) и символической логики (формальных методов). Фишер и Кук сравнивают это сочетание с «шоколадом и арахисовым маслом», которые вместе создают идеальный вкус [1:39:04].

Как ИИ помогает в доказательстве теорем:

*   **Поиск инвариантов:** Самая сложная часть доказательства — найти «индуктивный инвариант» (логическое утверждение, которое остается верным всегда). Раньше это делали доктора наук, теперь с этим успешно справляются LLM [1:13:22].
*   **Автоформализация:** ИИ способен переводить требования с естественного языка на язык логики, что значительно упрощает написание спецификаций [1:18:36].
*   **Генерация кода с гарантиями:** Вместо того чтобы просто писать код, ИИ будущего сможет генерировать код вместе с математическим доказательством его безопасности [1:08:10].

По мнению Байрона Кука, модели вроде GPT-6 или Gemini 4, вероятно, станут «сверхчеловеческими» в написании безопасного кода, если обучать их на массивах формальных доказательств [1:19:02].

## ⚖️ Automated Reasoning Checks: Этические стражи для ИИ-агентов
[[JUMP:1:31:30]]

Одной из новых разработок AWS стал продукт Automated Reasoning Checks (ARC). Он предназначен для того, чтобы ИИ-агенты соблюдали корпоративные политики, не галлюцинируя и не нарушая правила [1:32:10].

Принцип работы ARC:

1.  **Трансляция политики:** Например, справочник HR по отпускам переводится в набор логических правил.
2.  **Верификация ответа:** Когда пользователь спрашивает агента об отпуске, ARC проверяет предложенный ИИ ответ на соответствие формальной логике политики [1:34:43].
3.  **Точность:** Система обеспечивает до **99% точности** верификации, что значительно выше, чем у обычных чат-ботов [1:52:24].

Натан Лабенц выразил опасение, что такая жесткая логика может лишить системы «гибкости», присущей людям, которые иногда делают исключения из правил [1:35:50]. Байрон Кук возразил, что гибкость можно встроить в саму систему правил как отдельную опцию («если все условия нарушены, позови Стива»), сохраняя при этом полную прозрачность принятия решений [1:36:40].

## 🚀 Прогноз: Великая перезапись ПО
[[JUMP:1:21:50]]

Кэтлин Фишер считает, что мы стоим на пороге «великой перезаписи». Использование ИИ для автоматического перевода старого, небезопасного кода (например, на C) в современный памятобезопасный код (на Rust) может радикально снизить киберриски во всем мире [1:22:03].

Ключевые выводы экспертов:

*   Технологии для создания безопасного мира уже существуют, вопрос лишь в мотивации общества и бизнеса [1:23:42].
*   Будущее за нейросимволическим подходом, где гибкость нейросетей уравновешивается строгостью математики [1:39:55].
*   Программное обеспечение может перестать быть источником уязвимостей, оставив хакерам только атаки на «человеческий фактор» и «железо» [1:28:53].