В эпоху, когда возможности искусственного интеллекта растут экспоненциально, кибербезопасность оказывается на перепутье. С одной стороны, ИИ дает хакерам беспрецедентные инструменты для поиска уязвимостей, с другой — предлагает путь к созданию «неуязвимого» программного обеспечения. В новом выпуске подкаста The Cognitive Revolution эксперты Кэтлин Фишер (RAND) и Байрон Кук (AWS) обсуждают, как формальные методы и автоматизированное доказательство теорем в связке с нейросетями могут раз и навсегда решить проблему критических ошибок в коде.
🛡️ ИИ в киберпространстве: Ускорение гонки вооружений 5:11
Обсуждение будущего кибербезопасности Натан Лабенц начал с вопроса о балансе сил между нападением и защитой. По мнению Кэтлин Фишер, ИИ сегодня помогает злоумышленникам на всех этапах так называемой «цепочки поражения» (cyber kill chain) . Она утверждает, что технологии одинаково эффективно усиливают как новичков («скрипт-кидди»), так и профессиональные хакерские группировки, поддерживаемые государствами.
Основные угрозы, которые выделяют эксперты:
- Масштабируемость атак: ИИ позволяет хакерам работать параллельно над огромным количеством целей, что раньше было невозможно из-за ограниченности человеческих ресурсов .
- Реверс-инжиниринг: Эксперты по безопасности, по словам Кэтлин Фишер, шокированы тем, насколько эффективно ИИ-инструменты справляются с обратной разработкой кода .
- Эксплуатация уязвимостей: Байрон Кук отмечает, что современное ПО буквально «испещрено» дырами, и ИИ делает их поиск тривиальной задачей .
Однако Байрон Кук предлагает более оптимистичный взгляд: ИИ также помогает защитникам. Он считает, что мы переходим от социотехнических механизмов защиты (основанных на доверии к людям) к формализации безопасности, где каждый инцидент позволяет мгновенно улучшить систему для всех будущих случаев .
🧩 Формальные методы: Математика против хакеров 10:23
Формальные методы — это не просто тестирование, а алгоритмический поиск математических доказательств того, что программа работает именно так, как задумано, и никак иначе. Байрон Кук описывает это как возможность «рассуждать о бесконечном за конечное время и в конечном пространстве» .
Кэтлин Фишер выделяет спектр сложности и надежности этих методов:
- Слабые гарантии (Type Systems): Например, система типов в Java или TypeScript. Она автоматически доказывает, что вы не пытаетесь сложить целое число с функцией .
- Памятобезопасность (Memory Safety): Языки вроде JavaScript обеспечивают ее автоматически, тогда как в языке C программист должен следить за памятью сам, что является источником большинства уязвимостей .
- Полная функциональная корректность: Вершина методов, требующая огромных вычислительных мощностей и участия ученых. Примером служит CompCert — верифицированный компилятор C, который гарантирует, что машинный код в точности соответствует исходному .
По словам Байрона Кука, формальные методы долгое время оставались «в монастырях» (академической среде), но развитие облачных вычислений и SAT-солверов (инструментов для решения задач логической исполнимости) позволило вывести их в индустрию .
🚁 Проект HACMS: Вертолет, который невозможно взломать 31:13
Одним из самых ярких примеров эффективности формальных методов стал проект HACMS (High Assurance Cyber Military Systems), который Кэтлин Фишер возглавляла в DARPA. Целью было создание беспилотного вертолета Boeing Little Bird, защищенного от кибератак .
Результаты исследования показали:
- Базовый уровень: До вмешательства группы «красная команда» (этичные хакеры) взломала вертолет всего за шесть недель .
- Архитектурная изоляция: Разработчики использовали микроядро seL4 (математически верифицированное ядро сепарации). Систему разбили на разделы, изолировав критические функции управления полетом от второстепенных, например, от камеры .
- Испытания в воздухе: На финальном этапе «красной команде» разрешили атаковать вертолет прямо во время полета с двумя пилотами на борту . Хакеры смогли «уронить» только раздел камеры, но не смогли повлиять на управление или связь. Пилоты даже не заметили атаки .
Этот успех продемонстрировал, что математические доказательства могут обеспечить уровень безопасности, недоступный традиционным методам тестирования.
☁️ Опыт AWS: Безопасность на уровне миллиарда операций в секунду 44:32
Байрон Кук рассказал, как формальные методы применяются в AWS (Amazon Web Services). Одной из ключевых задач было доказательство корректности интерпретатора политик доступа IAM.
Масштаб задачи впечатляет:
- Интерпретатор политик вызывается более 1 миллиарда раз в секунду .
- Любая ошибка в логике «разрешить/запретить» может привести к утечке данных миллионов клиентов.
- AWS внедрила инструменты автоматизированного рассуждения, такие как IAM Access Analyzer и VPC Reachability Analyzer, которые позволяют клиентам доказывать отсутствие нежелательных путей доступа в их сетях .
Кук подчеркивает, что формальные методы в AWS стали частью процесса непрерывной интеграции (CI/CD). Даже если инженер просто меняет имя переменной, система автоматически проверяет, не нарушило ли это доказательство корректности .
🤖 Нейросимволический ИИ: Шоколад и арахисовое масло 1:13:00
Самым перспективным направлением спикеры считают слияние статистического ИИ (LLM) и символической логики (формальных методов). Фишер и Кук сравнивают это сочетание с «шоколадом и арахисовым маслом», которые вместе создают идеальный вкус .
Как ИИ помогает в доказательстве теорем:
- Поиск инвариантов: Самая сложная часть доказательства — найти «индуктивный инвариант» (логическое утверждение, которое остается верным всегда). Раньше это делали доктора наук, теперь с этим успешно справляются LLM .
- Автоформализация: ИИ способен переводить требования с естественного языка на язык логики, что значительно упрощает написание спецификаций .
- Генерация кода с гарантиями: Вместо того чтобы просто писать код, ИИ будущего сможет генерировать код вместе с математическим доказательством его безопасности .
По мнению Байрона Кука, модели вроде GPT-6 или Gemini 4, вероятно, станут «сверхчеловеческими» в написании безопасного кода, если обучать их на массивах формальных доказательств .
⚖️ Automated Reasoning Checks: Этические стражи для ИИ-агентов 1:31:30
Одной из новых разработок AWS стал продукт Automated Reasoning Checks (ARC). Он предназначен для того, чтобы ИИ-агенты соблюдали корпоративные политики, не галлюцинируя и не нарушая правила .
Принцип работы ARC:
- Трансляция политики: Например, справочник HR по отпускам переводится в набор логических правил.
- Верификация ответа: Когда пользователь спрашивает агента об отпуске, ARC проверяет предложенный ИИ ответ на соответствие формальной логике политики .
- Точность: Система обеспечивает до 99% точности верификации, что значительно выше, чем у обычных чат-ботов .
Натан Лабенц выразил опасение, что такая жесткая логика может лишить системы «гибкости», присущей людям, которые иногда делают исключения из правил . Байрон Кук возразил, что гибкость можно встроить в саму систему правил как отдельную опцию («если все условия нарушены, позови Стива»), сохраняя при этом полную прозрачность принятия решений .
🚀 Прогноз: Великая перезапись ПО 1:21:50
Кэтлин Фишер считает, что мы стоим на пороге «великой перезаписи». Использование ИИ для автоматического перевода старого, небезопасного кода (например, на C) в современный памятобезопасный код (на Rust) может радикально снизить киберриски во всем мире .
Ключевые выводы экспертов:
- Технологии для создания безопасного мира уже существуют, вопрос лишь в мотивации общества и бизнеса .
- Будущее за нейросимволическим подходом, где гибкость нейросетей уравновешивается строгостью математики .
- Программное обеспечение может перестать быть источником уязвимостей, оставив хакерам только атаки на «человеческий фактор» и «железо» .
