ИИ взломает программное обеспечение по всему миру, прежде чем защитит его

Первоисточник: публикация Арджуна Кхемани в X | Автор: Арджун Кхемани

В статье приведено личное мнение автора.

ИИ сначала вызовет краткосрочный кризис безопасности, а затем приведёт к её долгосрочному возрождению. Для Zcash это возрождение уже началось.

Сложное программное обеспечение долго оставалось относительно защищённым благодаря тому, что лишь немногие могли разобраться в нём настолько хорошо, чтобы его взломать. Уязвимости сохранялись годами: мало кто знал, где искать, а поиск обходился дорого.

Но ИИ напоминает: если свидетельств нет, это ещё не значит, что проблемы не существует. Скрытые уязвимости всё ещё могут ждать своего часа.

Zcash, возможно, станет первым наглядным примером того, как ИИ сначала ломает критически важное программное обеспечение, а затем делает его безопаснее, чем когда-либо.

Как передовая модель помогла найти в Zcash уязвимость, позволявшую подделывать монеты

29 мая специалист по безопасности Тейлор Хорнби, которого наняли специально для поиска ошибок в коде протокола Zcash, с помощью передовой модели обнаружил критическую уязвимость в Orchard, нынешнем защищённом пуле Zcash. Ошибка находилась в схеме доказательства с нулевым разглашением, подтверждающей, что конфиденциальные транзакции соблюдают денежные правила Zcash. Теоретически злоумышленник мог использовать её для создания поддельных ZEC внутри Orchard, не оставляя видимых в блокчейне признаков инфляции.

Уязвимость годами оставалась незамеченной во время разработки, аудитов и экспертных проверок. Затем, почти сразу после появления более мощной передовой модели, ИИ помог исследователю её найти.

Исследователь обнаружил ошибку, ответственно сообщил о ней тем, кто мог её устранить, и исправление развернули немедленно. Свидетельств эксплуатации уязвимости нет. Zcash готовится запустить новый защищённый пул, чтобы подтвердить, что ею действительно не воспользовались и что подобные ошибки больше никогда не повторятся (подробнее об этом ниже).

Под угрозой любая система, «проверенная в бою»

Опыт Zcash показывает: критически важным протоколам и программам нужен ИИ, чтобы укреплять безопасность.

Многие системы называют проверенными в бою лишь потому, что их ещё никто не взломал. Зачастую это означает только одно: искать уязвимости было слишком дорого. ИИ удешевляет такой поиск, в том числе для тех, кому вы предпочли бы не давать такой возможности.

Поначалу всё может выглядеть хаотично: прежде скрытые ошибки начнут обнаруживаться повсюду. Системы покажутся менее безопасными, хотя уязвимости уже были в них. Разница лишь в том, что теперь ИИ можно применять в большом масштабе, и находить ошибки стало намного проще.

Этап защиты

Та же технология, которая удешевляет атаки, удешевляет и защиту.

Сегодня программное обеспечение защищают проверкой кода, тестами, аудитами и наблюдением за работающими системами. Всё это полезно, но недостаточно. Тесты охватывают лишь те варианты поведения, которые вы предусмотрели. Аудиты лишь время от времени проверяют отдельные компоненты. А во время эксплуатации обнаруживаются только те сбои, которые действительно произошли.

ИИ может сделать контроль безопасности непрерывным. Каждое изменение можно проверять с помощью нескольких моделей, а прежние допущения пересматривать по мере появления более совершенных моделей. Аудит может перестать быть разовым ритуалом перед запуском и стать частью повседневной разработки.

Но широкое распространение формальной верификации станет ещё более значительным изменением, чем улучшение тестирования.

Формальная верификация переводит утверждение о безопасности на язык математики. Вместо слов «аудиторы не нашли уязвимости» вы точно формулируете нужное свойство и строите доказательство, которое машина шаг за шагом проверяет при заданных допущениях.

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

ИИ резко снижает эти затраты. Модели превращают неформальные рассуждения в формальные утверждения, создают леммы, автоматизируют повторяющиеся действия и перебирают 100 подходов за то время, пока человек пробует один. Современные системы проверки доказательств, такие как Lean, проверяют каждый шаг. Поэтому модели под руководством человека теперь могут сократить работу, прежде занимавшую годы, до нескольких недель, даже для сложных криптосистем.

При этом доверять модели не обязательно. ИИ способен выдавать бессмыслицу, но неверное доказательство не уговорит программу проверки пропустить его. Модель предлагает, программа проверяет. Модель может ошибаться сколько угодно, но ошибки будут обнаружены.

Остаётся риск доказать не то. Доказательство подтверждает только точно сформулированное утверждение и с одинаковой готовностью подтвердит как полезное, так и бесполезное. Можно неопровержимо доказать, что одну монету нельзя потратить дважды, но ничего не сказать о возможности создавать монеты из ничего, если это свойство забыли проверить. Такое доказательство будет правильным и бесполезным. Машина проверяет логику, но не может сообщить, что вы выбрали не ту угрозу. Решать, что именно доказывать, по-прежнему должен человек. Он же должен следить, чтобы математическая модель соответствовала реально работающей программе. ИИ не устраняет необходимость в человеческой оценке. Он лишь фиксирует её в форме, которую люди могут обсуждать и оспаривать.

От исправления ошибок к доказательству их отсутствия

История Zcash показывает весь этот путь, и исправление не сводится к словам «мы выпустили заплатку».

Уязвимости, позволяющие подделывать монеты, встречаются не только в конфиденциальных деньгах. В начале истории Bitcoin была такая ошибка: кто-то создал из ничего миллиарды монет, а исправление выпустили за несколько часов. Bitcoin спасла прозрачность. В публичном реестре видно всё, поэтому историю можно воспроизвести и проверить, использовал ли кто-нибудь ошибку. Конфиденциальность Zcash лишает систему такой страховки. Уязвимость в зашифрованном пуле могла бы позволить незаметно подделывать монеты, и никто никогда об этом не узнал бы.

Поэтому настоящим противником становится необнаружимая подделка монет.

Решить задачу позволяет одно важное наблюдение. Любая уязвимость, допускающая подделку монет, находится в одном из двух мест: в спецификации, то есть в математических правилах протокола, либо в реализации, то есть в программе, которая следует этим правилам. При этом ошибка реализации может привести лишь к подделке, которую впоследствии удастся обнаружить. Блокчейн навсегда сохраняет каждую транзакцию и каждое доказательство. Поэтому любой может воспроизвести историю с помощью исправленной программы, а всё, что неисправный узел ошибочно принял, навсегда останется публичным свидетельством. Бесконечно скрываться ошибка может только в самой спецификации.

Это меняет предмет доказательства. Формально проверять миллионы строк программного кода не нужно, да и сделать это почти невозможно. Достаточно формально проверить математику, что всего лишь очень трудно. Если доказать корректность спецификации, необнаружимой подделке монет негде будет скрыться: ошибки спецификации исключит доказательство, ошибки программы проявятся в истории блокчейна, а останутся лишь явно сформулированные криптографические допущения, которые каждый сможет увидеть и оценить.

Именно это происходит с новым пулом Zcash под названием Ironwood. Старый пул Orchard закрывают: средства могут выходить только через «турникет». Этот механизм публичного учёта не позволяет вывести больше ZEC, чем было законно внесено. Платежи внутри старого пула отключены, чтобы ограничить объём монет в обращении. По мере того как кошельки переводят средства пользователей через «турникет», сам процесс укрепляет уверенность в том, что прежнюю уязвимость не использовали. Тем временем инженеры с помощью ИИ формально проверяют самое важное свойство: систему нельзя незаметно обмануть и заставить создавать поддельные монеты.

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

В результате защищённость конфиденциальных денег от скрытой подделки становится по существу сопоставимой с Bitcoin. В обеих системах подделка монет возможна, только если ошибка проявится в публичной истории или окажется неверным одно из заявленных криптографических допущений. Разница в том, что Zcash достигает этого с помощью доказательства и сохраняет конфиденциальность.

В итоге ИИ укрепил безопасность Zcash. И, полагаю, Zcash станет не последней критически важной системой, безопасность которой ИИ укрепит таким образом.

Трудный переход

Сначала побеждают атакующие.

Злоумышленнику достаточно одного незамеченного пути. Защитникам нужно перекрыть всё. Похоже, сначала ИИ даёт преимущество атакующей стороне. В ближайшие несколько лет громких сбоев может стать больше. Атаки, для которых прежде требовались ресурсы государства, будут проводить небольшие группы или отдельные люди. Критически важная инфраструктура особенно уязвима, поскольку работает на старом коде, написанном во времена, когда тщательные проверки были редкостью.

Люди будут винить ИИ, но он не создаёт эти уязвимости. Он лишь заставляет программную отрасль расплачиваться за привычку полагаться на дороговизну поиска ошибок.

Но когда непрерывный аудит станет нормой, а формальная верификация получит широкое распространение, уцелевшие системы окажутся надёжнее всего, что создавалось прежде.

Показательный случай, а не исключение

Zcash важен потому, что здесь вся история развернулась от начала до конца. Трудноуловимая ошибка годами скрывалась в сложной криптографии, пока ИИ не расширил возможности исследователя, который её нашёл. Он сообщил об уязвимости, разработчики выпустили исправление, а новый пул спроектировали так, чтобы локализовать всю неопределённость, оставшуюся после старого. Теперь ИИ помогает математически доказать и проверить на машине, что подобный сбой не сможет вернуться.

В Zcash нет ничего, что ограничивало бы эту историю одной системой. Через то же пройдут другие блокчейны, банки, браузеры, системы идентификации, медицинские устройства и программы, управляющие физической инфраструктурой. Это касается всего, где цена сбоя достаточно высока, чтобы оправдать серьёзный поиск уязвимостей. Некоторые организации будут надеяться, что пристальная проверка обойдёт их стороной. Сильнее из неё выйдут те, кто поступит как Zcash и будет рассматривать каждый сбой как ошибку, которую нужно исправить: сначала создать тест, чтобы она не могла незаметно вернуться; затем описать в спецификации, какое свойство должно было выполняться; и наконец, если оно достаточно важно, построить доказательство.

Безопасность программного обеспечения негласно держалась на том, что время и интеллектуальные возможности злоумышленников ограничены. ИИ снимает оба ограничения, и первые годы будут по-настоящему пугающими: системы, казавшиеся надёжными, начнут отказывать, а ошибки, скрывавшиеся десятилетие, будут находить за несколько часов. Но те же возможности можно использовать для защиты. Их можно применять до запуска, а не после, и делать это постоянно, а не однократно. Когда это станет нормой, безопасность критически важных систем будет меньше зависеть от обещаний организаций и больше от аргументов, которые способен проверить любой человек или любая машина.

Сегодня ИИ действует как хакер, а завтра станет защитником. Для Zcash завтра наступило раньше.

Пожалуйста, оставьте это поле пустым.

Подпишитесь на рассылку!

Никакого спама!
Только новости и видео PRO.ZCASH

Проверьте ваш почтовый ящик или спам, чтобы подтвердить свою подписку.