От мусора от ИИ к формальной верификации: как мы меняем подход к Bug Bounty в эпоху ИИ

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

После этого аудита мы продвинемся дальше к формальной верификации. Сейчас ИИ-модели вроде Claude Fable упрощают поиск атак, и мы замечаем, что наша программа Bug Bounty в основном привлекает «мусор от ИИ» — люди пытаются прогнать наш код через ИИ-аудит безопасности.

В Nym мы начали постоянно использовать Claude Fable для анализа нашего кода, чтобы находить реальные ошибки. Подобно обновлению Ironwood у ZCash, единственный способ гарантировать защиту нашего кода от ошибок, которые может найти ИИ, — это формальная верификация каждого примитива и протокола, используемого в Nym.

Программа Bug Bounty: что меняется

В рамках подготовки к следующему аудиту безопасности и переходу к формальной верификации мы останавливаем нашу программу Bug Bounty в её текущем виде.

Это означает прекращение действующей системы выплат, в которой токены $NYM выплачивались по фиксированной шкале в зависимости от серьёзности сообщённой проблемы. Теперь Nym будет выплачивать вознаграждение только на усмотрение команды за серьёзные и важные находки. Мы по-прежнему принимаем отчёты, и исследователи могут и должны продолжать присылать нам всё, что находят. Наша политика безопасной гавани и правила ответственного раскрытия остаются в силе.

Актуальные правила всегда доступны по ссылке nym.com/vdp-bbp.

Почему мы это делаем

Код Nym — открытый и ежегодно проходит независимую проверку, а не принимается на веру.

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

Следующая остановка: формальная верификация

После этого аудита мы вместе с нашими партнёрами из Cryspen движемся к формальной верификации. Там, где Bug Bounty и обычный аудит ищут ошибки с помощью тестирования и проверки, формальная верификация создаёт математические доказательства поведения кода, показывая, что критические части системы ведут себя именно так, как задумано, и не могут выполнять определённые действия в принципе. Это наивысший стандарт гарантий в инженерии безопасности, и именно туда должна двигаться такая приватная инфраструктура, как наша.

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

Чтобы узнать больше о формальной верификации, прочитайте статью «Дорожная карта высоконадёжной криптографии», написанную нашим генеральным директором Гарри Халпином, когда он работал в Inria de Paris в 2017 году вместе с Картиком Бхаргаваном, который руководил формальной верификацией протоколов (таких как TLS 1.3 и Signal), на которых держится весь интернет. Теперь, когда Картик Бхаргаван работает в Cryspen, мы будем сотрудничать с его командой над формальной верификацией основной криптографии и протоколов Nym.

Наши аудиты на сегодняшний день

Nym и NymVPN проходят независимые аудиты и проверки ведущими фирмами и криптографами с первых дней существования сети. Отчёты публично доступны в нашем Центре доверия:

• Cure53 (июль 2024). Комплексный аудит мобильных и десктопных приложений Nym, VPN, сетевой инфраструктуры и криптографии, проведённый командой, в которую входил доктор Дэниел Блейхенбахер. Ознакомьтесь с аудитом Cure53.

• Oak Security (январь 2023). Два аудита: микснета Nym и контракта вестинга, а также кошелька Nym.

• Д-р Ж.П. Омассон (сентябрь 2021). Ранний аудит безопасности сети, проведённый одним из самых известных криптографов в этой области.

• Технические обзоры Cryspen (2023–2024). Криптографические обзоры распределённой генерации ключей Nym и формата пакетов Outfox под руководством доктора Картикеяна Бхаргавана и его коллег с использованием формальных методов.

Последний пункт важен: формальная, математическая проверка не является чем-то новым для Nym. Следующий аудит расширяет этот подход на большую часть системы.

Что это значит для вас?

Для пользователей ничего не меняется, кроме того, что наш процесс безопасности становится надёжнее. Ваш NymVPN и сеть продолжают работать в обычном режиме.

Для исследователей безопасности дверь остаётся открытой. Если вы нашли уязвимость, сообщите о ней на security@nym.com, желательно с шифрованием через наш PGP-ключ, с чёткими шагами для воспроизведения.

Вознаграждения теперь выдаются на усмотрение команды, только за серьёзные и важные находки, но каждый достоверный отчёт по-прежнему получает подтверждение, исправление и помогает защитить всех пользователей Nym. Полные инструкции — на странице раскрытия уязвимостей.