Соучредитель Ethereum Виталик Бутерин не верит, что совершенствование искусственного интеллекта в конечном итоге сделает кибербезопасность принципиально безнадёжной.
Бутерин уверен, что в конечном итоге может произойти обратное: ИИ может дать защитникам инструменты, необходимые для создания программного обеспечения, которое изначально значительно труднее эксплуатировать.
«Всё чаще встречается мнение, что ИИ-хакерство означает, что кибербезопасность обречена. Я не согласен», — написал Бутерин в среду в пространном и характерно содержательном посте в социальной сети X.
По мнению соучредителя Ethereum, кибербезопасность должна естественным образом благоприятствовать защитникам, как только разработчики начнут в полной мере использовать формальную верификацию.
Бутерин также напрямую связал это убеждение со своей собственной подверженностью криптовалюте, раскрыв, что примерно 90% его чистого состояния по-прежнему находится в криптовалюте.
Тот, кто продолжает держать значительные суммы криптовалюты, утверждал он, неявно делает ставку на то, что достаточно безопасные цифровые системы могут быть построены, несмотря на всё более изощрённых атакующих.
«Если ИИ может доказать Навье — Стокса и ВТФ, то ИИ может доказать утверждение "эта программа безопасна" как математическую теорему», — написал Бутерин, имея в виду проблему Навье — Стокса и Великую теорему Ферма.
Его аргумент основан на формальной верификации — методе математического доказательства того, что программное обеспечение удовлетворяет определённым свойствам.
Бутерин подробно исследовал ту же идею в своём майском эссе, в котором он описал формальную верификацию с помощью ИИ как чрезвычайно преобразующий инструмент для программного обеспечения, критически важного для безопасности. Однако доказать, что такое программное обеспечение безопасно, может оказаться сложной задачей.
Проблема определения
Бутерин использовал приложение для зашифрованных сообщений Signal в качестве примера, чтобы показать, почему это может быть сложно.
Атакующий может попытаться подделать сообщения, помешать их доставке, воспроизвести старые сообщения, скомпрометировать сервер, манипулировать процессом, используемым для обнаружения открытого ключа другого пользователя, или воспользоваться уязвимостью в операционной системе.
Другие проблемы могут возникнуть из-за повреждённых баз данных, вредоносных библиотек, компиляторов или даже утечек информации на уровне оборудования.
Даже если содержимое разговора остаётся зашифрованным, атакующий всё равно может узнать, кто общается. В результате математическое определение того, что на самом деле означает «безопасный», само по себе может стать чрезвычайно сложным.
«Так что... даже определения могут занимать более тысячи строк кода, и для их выяснения требуются глубокие тщательные размышления», — написал Бутерин.
Атакующий и защитник
Несомненно, более способные системы ИИ могут облегчить поиск уязвимостей.
Однако то же самое улучшение машинного рассуждения может также резко снизить стоимость формального доказательства того, что программное обеспечение ведёт себя в соответствии с тщательно построенными спецификациями безопасности.
У обеих сторон будет ИИ.
