Главный научный сотрудник Certora Мули Сагив: безопасность блокчейна - это больше, чем просто код
Какие самые большие угрозы безопасности будут стоять перед криптовалютами в 2026 году?
- Опубликовано:
- Отредактировано:
Если 2025 год и научил нас чему-то, так это тому, что Solana набрала скорость прорыва и утвердилась в качестве “розничной сети". Каждый день тысячи пользователей перемещают средства и заключают сделки, взаимодействуя с непостижимо сложными смарт-контрактами, не заботясь о потенциальных рисках.
Конечно, риски все еще существуют под сервисом. Но хотя взломы и эксплойты криптовалют все еще происходят гораздо чаще, чем хотелось бы, люди обычно полагают, что самые большие риски погребены глубоко в непонятной логике и технических кодовых базах.
Мули Сагив так не считает. По словам главного научного сотрудника Certora, компании, занимающейся безопасностью блокчейна и обеспечивающей защиту более $190B в DeFi TVL, большинство потерь вызвано не ошибками в логике кода или программировании, а гораздо более простыми виновниками: ключами, хранением и человеческим фактором. Количество потерь, которые могут быть вызваны ошибками в логике кода или ошибками программирования.
“Следите за своим ключом… и следите за своим телефоном. Это’простое предупреждение, но оно отражает критически важный и часто упускаемый из виду подход к криптобезопасности. Сбои в системе безопасности редко бывают “просто ошибкой”, а распространение мобильных криптоприложений только увеличивает количество переменных и потенциальных уязвимостей. Сагив обладает уникальными возможностями, чтобы доказать это. Главный научный сотрудник Certora Шмуэль (Мули) Сагив, известный среди своих коллег по академическому сообществу как Шмуэль (Мули) Сагив, на протяжении почти 28 лет также занимал должность заведующего кафедрой программных систем Тель-Авивского университета. Имея за плечами десятилетия исследований в области анализа и верификации программ, Сагив играет ведущую роль в стремлении Certora ’вывести формальную верификацию за рамки нишевой дисциплины и сделать ее доступной для разработчиков на постоянной основе.
Выступая с SolanaFloor на Breakpoint 2025, Мули Сагив пролил свет на темный лес безопасности блокчейна. Главный научный сотрудник Certora, ответственный за аудит некоторых из крупнейших имен в сфере DeFi, рассказал о некоторых из самых больших заблуждений пользователей криптовалют относительно безопасности, о важности формальной верификации и о том, являются ли риски ИИ и квантовых вычислений преувеличенными. Когда речь заходит о заблуждениях относительно безопасности блокчейна, Сагив утверждает, что криптокультура слишком расхлябанна. Самое опасное заблуждение - это вера в то, что уязвимости находятся исключительно в коде и что если код подвергается аудиту, то пользователи могут отменить здравый смысл. “Все считают, что все ошибки находятся в коде. Но это не всегда так, и, возможно, ваш код совершенно хорош, но есть что-то, что не соответствует тому, как он развернут…”.
Криптовалютчики придерживаются основных философских постулатов, таких как ‘код - это закон’. Но хотя это и верно, все же существуют десятки переменных, которые необходимо учитывать. Протокол может быть “правильным” и все равно небезопасным, потому что ключи плохо контролируются, интеграция небезопасна или операционная среда скомпрометирована. Приложение безопасно лишь настолько, насколько безопасны системы и поведение людей, управляющих им.
Второе заблуждение Сагива - это то, во что хотят верить большинство пользователей: что “аудит” подразумевает безопасность. “Он” никогда не бывает полностью безопасным. Мы можем сделать его более безопасным…, но он’ никогда не бывает полностью безопасным. “Аудированный” подразумевает безопасность.
Аудиты, несомненно, являются неотъемлемой частью криптобезопасности, но они ’ни в коем случае не являются гарантией. У людей возникает ложное чувство безопасности, когда они видят, что приложение прошло аудит, но пользователям DeFi, безусловно, не стоит забывать о базовых практиках безопасности. Сагив не отвергает аудиты. На самом деле он прямо выступает против идеи, что формальная проверка заменяет человеческий аудит. Напротив, формальная проверка и человеческий аудит в идеале должны использоваться в тандеме, чтобы обеспечить максимально возможный охват. В беседе с SolanaFloor Сагив рассказал о том, как аудит обычно защищает от известных шаблонов атак, в то время как формальная верификация может уменьшить подверженность “неизвестным” “Когда вы” проводите аудит, вы проверяете свой код [с] лучшим человеком на предмет известной атаки. Когда вы можете провести формальную верификацию…, у вас есть некое [предотвращение] неизвестных атак.” ”.
Эта разница имеет значение, потому что криптовалюты - это гонка вооружений. Методы атак развиваются, а хакеры и киберпреступники постоянно находят новые способы и методы взлома приложений, которые стоят миллиарды долларов и которыми мы пользуемся каждый день. Это важно, потому что криптовалюты - это гонка вооружений.
Целые новые классы багов обнаруживаются потому, что кто-то, где-то, нашел умный способ нарушить предположения, о которых индустрия даже не подозревала. Формальная верификация призвана обеспечить еще одну линию защиты от этих “неизвестных”. Сагив описывает модель, которую Certora наблюдала неоднократно. Команды могут делать все “правильно”, выделяя огромные внутренние ресурсы на безопасность, нанимая элитных аудиторов, а затем формальная проверка все равно выявляет дополнительные проблемы высокой степени серьезности. “Вы позволяете лучшему [исследователю] безопасности … найти 10 критических. Вы ’очень довольны. А потом вы запускаете формальную верификацию. Она находит еще две. Этот тезис был подкреплен руководителем группы формальной верификации Certora’ Паминой Георгиев, которая выступила на сцене Solana Breakpoint, чтобы проиллюстрировать важность и влияние FV.
Несмотря на все обещания и защиту, которые дает формальная верификация, она ’все еще далека от совершенства. Формальная верификация вряд ли является непроницаемым силовым полем, которое останавливает хакеров на своем пути, несмотря на то, что некоторые круги криптовалютного Твиттера могут заставить вас поверить в это. Сагив прямо говорит о том, почему такое представление опасно. “Самая большая проблема [в] формальной верификации - это понимание того, какое свойство нужно [указать] “.
Формальная верификация не доказывает, что код безопасен в каком-то абсолютном смысле. Она доказывает, что код удовлетворяет набору свойств; свойств, которые вы попросили ее доказать. Если вы выберете неправильные свойства, то в итоге получите нечто, что выглядит чрезвычайно правдоподобно, но далеко не водонепроницаемо. Один из самых четких тезисов, высказанных Сагивом на Breakpoint, заключается в том, что безопасность - это не одноразовая акция. Не потому, что приложение прошло один аудит несколько лет назад, оно будет безопасным и сегодня. Это особенно актуально для криптовалют, где протоколы и методы атак постоянно повторяются, а изменения в одной строке кода могут иметь последствия в других частях стека.
“Он полностью меняется, одно изменение одной строки может сломать весь код. Поэтому Certora продвигает верификацию в рабочий процесс разработчика. По словам Сагива, Certora интегрируется в конвейеры CI, поэтому каждый новый коммит автоматически запускает проверку, создавая непрерывное ограждение, а не разовую веху.
“Каждый раз, когда они вносят изменения, делают коммит в коде, мы запускаем формальную верификацию. В этом, собственно, и заключается вся прелесть нашего инструмента. Наш инструмент автоматический, человек не участвует в этом процессе” “.
Компания Certora ведет специальную документацию по формальной верификации программ Solana, в том числе “Certora Solana Prover”, предназначенный для проверки смарт-контрактов Solana, написанных на языке Rust. В отличие от многих историй происхождения криптовалют, которые часто уходят корнями в киберпанк, антиистеблишмент, Сагив привносит в индустрию столь необходимый академический класс. Он описывает свой переход из академической среды как столкновение интеллектуального вызова и реальных ставок. “Криптовалюты - единственная область, где небольшой код несет в себе большую ценность” В традиционном программном обеспечении, критичном для безопасности, код может быть огромным, но он&rsquo ; часто старый, стабильный и является полной противоположностью криптовалют&rsquo ; с их быстрой итерацией. Возможно, это послужило основой для одного из любимых слоганов Certora: “Двигайся быстро и ничего не ломай” Сагив считает, что криптовалюты идеально подходят для формальных методов, поскольку очень многое в них является математическим по своей сути: балансы, инварианты, ограничения на сохранение, правила управления доступом и переходы состояний, которые можно точно выразить. Сагив считает, что криптовалюты - это не только формальные методы, но и формальные методы.
“Я по-прежнему читаю академические лекции. Некоторым людям не нравится криптовалюта. Я пытаюсь мотивировать их с технической стороны. Я возвращаюсь к техническим аспектам и рассказываю им о том, что является сложным” “.
Даже если его академические коллеги скептически относятся к криптовалютам, Сагив подчеркивает, что криптовалюты - одна из наиболее стимулирующих и мотивирующих областей информатики для начинающих разработчиков. Certora ни в коем случае не является эксклюзивной фирмой по безопасности Solana, но это не означает, что компания не вплетена глубоко в DeFi-сцену сети. Работая с некоторыми из самых крупных и влиятельных приложений Solana&rsquo ;, Sagiv обеспечивает экосистеме тот уровень оперативного уважения, который возникает только при общении с топ-командами.
Сертора’впервые начала работать в Solana со Squads, которую Сагив называет “потрясающей”. После этого Сертора работала с Solana Foundation и проверяла свойства SPL-программ, описывая сотрудничество как необычайно восприимчивое. Сертора’работает с Solana Foundation и проверяет свойства SPL-программ.
Самым интересным является его сравнение с другими средами. Рассказывая о своем опыте работы с Solidity Developers, Сагич отметил, что команды могут быть невосприимчивы к изменениям. “Когда мы говорим с людьми, иногда в Solidity, просим их изменить код, они очень неохотно соглашаются. Они говорят, что у нас ограниченное количество времени… Здесь [в Solana] у людей больше ‘can do’ отношения. Вы просите их изменить код, и они очень прямолинейны. В ответ на вопрос о самых больших угрозах, о которых люди должны знать в 2026 году, Сагив еще раз подчеркнул, что люди не должны ’зацикливаться&rsquo ; на уязвимостях кода. Хорошая операционная безопасность - это многогранный зверь, и среднестатистический держатель криптовалюты с гораздо большей вероятностью может стать жертвой социальной инженерии или ошибки хранителя, чем потерять средства в результате DeFi эксплойта. “Мы видим, как происходят самые разные вещи, это ’не только код” Он&rsquo ; не ошибается. Согласно отчету Chainalysis’ 2025 Crypto Crime Report, за 2025 год мошенники украли $14B, что стало еще одним рекордным показателем. Сагив также считает, что угроза ИИ, возможно, раздувается из мухи слона. Как и следовало ожидать от профессионала в области безопасности, главный ученый Certora’считает ИИ не вредоносной угрозой, а инструментом. Конечно, искусственный интеллект может послужить для злоумышленников, но он также может быть использован защитниками и компаниями, занимающимися вопросами безопасности. “Плохие парни могут использовать ИИ. Хорошие парни могут использовать ИИ,” “Плохие парни могут использовать ИИ.
Если ИИ помогает найти уязвимости, он также может помочь доказать свойства, сгенерировать более сильные спецификации и решить проблемы верификации. Искусственный интеллект может помочь найти уязвимости, но он также может помочь доказать свойства, создать более сильные спецификации и решить проблемы верификации.
Криптовалюты никогда не будут “полностью безопасными”, и Solana не будет ’неуязвима” для любой следующей волны злоумышленников. Но путь вперед остается верным курсу Crypto Security 101: ужесточите управление ключами, используйте здравый смысл и относитесь к безопасности как к чему-то, что вы постоянно доказываете, а не как к чему-то, что вы заявляете один раз и забываете.
Единственная определенность - это неопределенность.
Гибридный подход к безопасности от компании Certora’
CI, автоматизация и “отсутствие человека в петле”
Шифропанки и наука
Солана’“Can-Do Attitude”
Угрозы безопасности в 2026 году
Читать подробнее о SolanaFloor
SolanaFloor сидит с Certora’s Mooly Sagiv
