Метамаск выкатил в ранний доступ kipuka, инструмент для защиты от вредоносных npm пакетов. В целом, всем разработчикам давно рекомендовано запускать проекты в контейнерах/VM, но не все это делают и не всегда (надо написать об этом подробный пост). Кипука оборачивает ваши запросы к npm пакетам в контейнеры автоматически, так что если вы забываете или ленитесь поднимать каждый раз безопасное окружение, то эта штука для вас

https://t.me/web3securityresearch

Уязвимость: Inflation Attack/Donation attack

Этот пост написан на основе треда security researcher Kankodu

Итак, мы знаем, что такое инфляционная атака и как можно защититься и даже применяем это на практике.
Этот отчет о уязвимости мне понравился потому, что демонстрирует важность консистентности работы с выпускаемыми токенами. Всё должно подчиняться единым правилам, иначе - дрейн

Речь пойдет об уязвимости в лендинг протоколе Vesuxyz, которая возникала в момент добавления нового asset’a к пулам коллатералов.
Сама уязвимость уже исправлена и внесенные изменения можно посмотреть здесь

Протокол VESU поддерживает деплой нескольких пулов, каждый из которых является лендинг маркетом с разными парами коллатерал - займ. Для каждой пары свой LTV (Loan-to-Value - сколько можно занять под свой залог). Такая структура позволяет использовать очень разные вариации займов. Существует Genesis pool, который содержит значительный TVL и который по сути является обычным лендинг маркетом с поддержкой регипотеки (rehypothecation - практика, при которой финансовая организация (например, банк или брокер) повторно использует залоговые активы своего клиента (такие как ценные бумаги или криптовалюта) в качестве обеспечения по своим собственным кредитам или сделкам, создавая таким образом многократное использование одного и того же актива для получения дополнительной выгоды )

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

Разработчики протокола учли первый шаг, про который я писал ранее, поэтому, если total shares = 0, то при попытке сминтить долю, сначала минтятся 1000 dead shares

Но! Когда вкладчики получали свой процент дохода, протокол забирал часть в качестве комиссии и при этом минтил эквивалентное количество shares, увеличивая общее количество shares без минта 1000 deadshares. Я думаю вы уже начали понимать, в чем загвоздка

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

Затем атакующий берет эти средства в долг на небольшое время, возвращает долг, протокол минтит немного shares, стоимостью меньше 500 wei

Теперь пул содержит больше 0 shares, а значит начальная проверка на необходимость минта 1000 dead shares обходится

Теперь атакующий может сминтить свою долю, которая тоже меньше 500 Wei, а так же он донатит большую сумму в пул

На данный момент у него есть очень небольшое количество shares, которые сопоставляются большой сумме в пуле. Под эти shares он вполне легально берет долг в других пулах

Осталось понять, как вытащить задоначенные средства и не возвращать долг

У протокола есть механизм, который скидывает остаток shares в 0, если при выводе их остается меньше 1000, это изначально было сделано для того, чтобы не оставалось «пыли». Атакующий с другого адреса вносит и выносит 1 Wei, это приводит к тому, что в пуле лежат средства, но shares равно 0

Затем так же с другого адреса вносится какое-то количество средств, атакующего больше не волнует, что сгенерилось 1000 dead shares, ведь всё равно все средства в пуле соответствуют его вновь сминченной доле. После этого он может выносить все ранее внесенное, а на другом его аккаунте висит займ, который теперь нечем закрыть. Это возможно потому, что протокол не проверяет автоматически все позиции на ликвидацию (это тоже обычная история), а когда вынос случится - ликвидировать первую позицию уже смысла нет - у нее нет обеспечения

https://t.me/web3securityresearch

подал заявку на участие в Octant DeFi Hackathon 2025

сроки проведения: 31 октября - 11 ноября

в чем суть: создать проект, использующий octant vault'ы, которые являются альтернативой erc-4626

призовой пул 21_500$, делится на разные категории, например самый чистый код (2,500) или лучшее использование aave vaults v3(2500) и так далее

я думаю, что стоит собрать команду из 2-3-4 человек, чтобы вместе поучаствовать ради опыта + проекта в гитхаб

подавайте заявки, пишите в личку, если вашу заявку одобрили

Откуда брать информацию о взломах

Один из вопросов, который вам вероятно зададут при поиске работы звучит так:

Откуда вы берете информацию о взломах? Какие ресурсы вы читаете, чтобы быть в курсе происходящего?

Да и без этого вопрос насущный, потому что чтобы обеспечить безопасность надо знать о последних новостях в сфере

Это было для меня поначалу непривычно, но email рассылка решает, вот на что я подписан

Blockchain Threat Intelligence
Моя любимая еженедельная рассылка, с недавнего времени ввели премиум, но и на бесплатном тарифе оч круто
https://newsletter.blockthreat.io/subscribe - подписка на email рассылку

Web3sec
Очень много информации разного уровня сложности
https://web3secnews.substack.com/ - подписка на email рассылку
https://www.web3sec.news/ - сайт
https://x.com/web3sec_news - твиттер

Cyfrin
про этих легенд писал здесь
https://www.cyfrin.io/newsletter - подписка на email рассылку
https://x.com/CyfrinAudits - твиттер

BlocSec
Не сколько про взломы, сколько статьи про индустрию, вот например последняя про
Drainer-as-a-Service
https://blocksec.com/blog - блог

Cantina
По сути каждая статья это короткий гайд/саммари по определенной теме, удобно для точки входа
https://cantina.xyz/blog - блог

добавлено 22.12.2025

Rekt news
https://rekt.news/ru

Halborn
https://www.halborn.com/blog

Certik
https://www.certik.com/resources

Бонус
https://x.com/blockthreat_2da - твиттер аккаунт, рассказывающий о взломах, что произошли в этот день в прошлом

https://t.me/web3securityresearch

Обновление!

Вообще хакатон начинается завтра, но первый этап - DeFi Summit уже сегодня

Расписание здесь, сегодня будут рассказывать про тренды DeFi и вообще погружать в контекст децентрализованных финансов, а завтра пройдут воркшопы по использованию Uniswap v4, Yearn, Octant v2, Superfluid, Regen и Scaffold! В общем это ультимативно быстрый способ погрузиться в DeFi разработку по разным направлениям

Насколько я понял, участие вообще доступно для всех кто подается, одобрения заявок не существует, это скорее трудности перевода, так что участвуем, не стесняемся, пишем в лс канала

Целью служит создание DeFi стратегии на основе Octant Vaults, которые используют ERC-4626, почитать можно и нужно здесь, это база

https://t.me/web3securityresearch

Начинаются воркшопы, трансляция

Upd. Презентация намного менее техническая, чем я ожидал

Upd2. Ладно, зависит от выступающих

OpenAI пришел за security researcher'ами!

Или нет (скорее нет)

Несколько дней назад, вышла статья-презентация агента AARDVARK на основе GPT-5

Он, конечно, не Web3 специфичен, его экспертиза направлена на всё многообразие ПО, существующего в мире

Схема его работы представлена на картинке, приложенной к посту.
- мониторинг коммитов и изменений в кодовых базах
- идентификация уязвимостей
- предложение исправлений

Звучит не очень подробно, но разумно

Заявляется, что никакого фаззинга и прочего традиционного инструментария агент не использует, а полагается только на понимание кода и узнавание уязвимостей. Агент должен работать с кодом как человек: читать, анализировать, писать тесты, использовать инструменты

На данный момент открыта приватная бета стадия, так что ждем, следим, имплементируем как будет возможность

Про web3 специфичное использование AI агентов в security research писал в нескольких частях начиная отсюда

https://t.me/web3securityresearch

Итак, пожалуй можно подвести итоги моего участия в хакатоне

Спойлер: подавать проект я не буду, но это было увлекательно

Это был первый мой опыт участия в такого рода мероприятии

Технически второй, но на первом, год назад, было кратно меньше кода/сложности, так что его можно не учитывать

Что пошло не так/что я сделал не так:
1) Недооценил объем. Из этого выливается вторая проблема
2) Поздно начал. И даже после того как начал, не сразу понял, что не успеваю, так что не торопился
3) Не набрал команду/не вступил в команду. Отчасти это продиктовано четвертой причиной
4) Вписался в хакатон в момент, когда на самом деле на хакатон сил не было. Поэтому не искал команду, потому что выстраивание коммуникации - это энергозатратно. По этой же причине отчасти откладывал начало - хотелось набрать энергии. В итоге чуть ли не каждый день хотелось бросить это всё и заняться чем то другим, особенно когда стало понятно, что кажется я не успеваю
5) Как итог, текущий результат к дедлайну не отвечает требованиям по покрытию тестами/не все тесты проходят + не сделана презентация. На тестах (как и должно быть) возникли вопросы, и я не готов сейчас продолжать разбираться в корне проблем (дедлайн через 6 часов)

Плюсы будут? Да
1) Octant Vaults - это эволюция ERC-4626 стандарта, который широко используется. Я познакомился с концептом, скачал себе их core репозиторий, он хорошо структурирован. В целом, надо было сразу лезть в него, быстрее бы въехал. Если коротко, то предлагается цепочка наследования, где каждый слой отвечает за свой функционал. Понравилось, что безопасность наследуется, интересный подход
2) Мне кажется, что у этих vaults есть будущее, а значит я с ними еще встречусь, так что этот опыт не пропадет. Хотя по сути они наследуют болячки от ERC-4626, такие как инфляционная атака
3) Разнообразие деятельности. Немного отвлекся от security research, от курсов, разнообразие рутины тоже полезно

Выводы
Можно было конечно снизить страдания и просто почитать документацию/посмотреть код, но тогда уровень погружения был бы ниже, хотя с большой вероятностью все равно был бы достаточен на текущий момент

Даже без подачи проекта на оценку я доволен, опыт бывает разным

По возможности старайтесь верно оценивать трудозатраты и будьте полны энергии

https://t.me/web3securityresearch

Тесты? Тесты. Часть 1

Вернемся к теории, точнее к общим положениям

Одна из задач в приватном аудите (что это такое писал здесь) - оценка зрелости кодовой базы

Важная часть этого параметра - покрытие тестами и использование специальных инструментов командой разработчиков

Тестирование мне нравится воспринимать как послойную защиту, чем больше слоев, тем меньше шансов пропустить критическую уязвимость

1 слой. Unit тесты
Что делают: здесь всё как в "обычном" программировании. У нас есть функция, мы передаем ей фиксированные параметры, чтобы проверить работает ли она ожидаемым образом с нормальными данными, с краевыми случаями, с неправильными данными. Это база, это обязательно должно быть с хорошим процентом покрытия кода
Как внедрять:
- Hardhat использует этого Mocha/Chai, на JS, с 2025 есть поддержка тестов на Solidity
- Foundry имеет встроенные инструменты с использованием cheatcodes (оч крутая штука, достойна поста), на Solidity

2 слой. Stateless Fuzz тесты
Что делают: по сути это unit тесты на стероидах. Специальный фаззер автоматически генерирует входные данные на экземпляр функции. Тысячи генераций, каждый раз новый экземпляр, поэтому и stateless, то есть без сохранения состояния. Тоже можно считать базой, пишутся достаточно просто, можно сделать из unit
Как внедрять:
- Hardhat можно использовать специализированный fuzzer Echidna, но с 2025 года имеет встроенный fuzzer
- Foundry имеет встроенный fuzzer

3 слой. Мок тесты
Что делают: Мок-тесты позволяют имитировать поведение внешних зависимостей, таких как другие контракты, оракулы или внешние вызовы, без их реального развертывания. По сути, это расширение unit-тестов для симуляции реального мира
Как внедрять:
- Hardhat: библиотека Smock для создания моков контрактов, или пишите на solidity (круто они обновились в 2025, да)
- Foundry: Встроенные cheatcodes, такие как mockCall, expectCall или prank для имитации вызовов и отправителей

4 слой. Интеграционные тесты
Что делают: проверяют, как несколько контрактов взаимодействуют друг с другом в полной системе, симулируя реальные сценарии. В отличие от unit или mok, здесь учитываются реальные зависимости, газовые затраты, события и состояние сети
Как внедрять:
- Hardhat: hardhat-network для forking mainnet (npx hardhat node --fork), развертывайте контракты и пишите тесты на JS/TS с Mocha/Chai или на Solidity
- Foundry: использовать читкод vm.createFork для симуляции реальной сети, cheatcodes для манипуляции состоянием и развертывание нескольких контрактов

5 слой. Статические анализаторы
Что делают: в отличие от предыдущих "слоев", статические анализаторы не запускают код, они исследуют его на присутствие паттернов, соответствующих потенциальным уязвимостям, нарушению лучших практик и стандартов. Легко запускаются, но выдачу надо внимательно анализировать
Как внедрять:
- Статических анализаторов несколько, например Slither, Aderyn, Mythril. Я использовал первые два, запускаются в терминале, генерируют отчеты, находят немного разное

https://t.me/web3securityresearch

Тесты? Тесты. Часть 2

6 слой. Stateful Fuzz тесты/Тесты инварианта
Инвариант - это состояние/поведение вашего контракта, которое не должно нарушаться ни при каких обстоятельствах. Из-за того, что само слово invariant несколько перегружено смыслами, то получается, что так называют и это нерушимое правило и способ тестирования.
Отличие от stateless в том, что в этом случае генерируемые фаззером значения отправляются на один и тот же экземпляр/экземпляры контракта/функций. Из-за этого его сложнее написать, это тоже достойно отдельного поста.
Суть там следующая, если не зарываться в техническое: мы создаем экземпляр контракта, выбираем какие функции из него собираемся тестировать в связке, а потом в случайном порядке подаем им случайные значения на вход. Если какая то последовательность вызовов функции нарушает наш инвариант, то мы увидим в логах всю цепочку вызовов, приведшую к ошибке.
Огромное отличие от теста без сохранения состояния в том, что мы к тому же можем ограничивать подаваемые на вход значения, чтобы уменьшить ширину диапазона из которого берутся случайные значения + прописать N акторов от лица которых вызываются транзакции.
Как внедрять:
- Hardhat можно использовать специализированный fuzzer Echidna, но с 2025 года имеет встроенный fuzzer
- Foundry имеет встроенный fuzzer

7 слой. Formal Verification
Если фаззеры закидывают функции случайными данными и пытаются таким образом вызвать сбой, то методы формальной верификации пытаются найти математическое доказательство корректности функции. Крайне мощный инструмент, обладающий своей спецификой и ограничениями по применению, но по сути не имеющий аналогов. На Cyfrin его изучение закинули в отдельный курс
Как внедрять:
- Такой анализатор есть прямо в solc (компилятор Solidity), использует SMT-солверы, вызывать через консоль
- Использовать стороннее ПО, такое как Halmos, Certora

Этот пост конечно не является железным требованием ко всем кодовым базам, но чем больше слоев, тем лучше. Так же стоит понимать, что каких-то слоев в случайном порядке может не быть и это нормально

Каждая команда исходит из того, сколько у них времени и ресурсов и разные способы проверки кода требуют кратно разных затрат

https://t.me/web3securityresearch

Закончил Assembly and Formal Verification курс от Cyfrin

Таким образом закрыл ветку по треку Smart Contract Security Auditor!

Хотя этот курс несколько короче, всего 15 часов (первый 24 часа) проходил я его дольше, потому что поэтапно, после ознакомления с assembly и opcodes брал перерыв

Материал сложнее, но подача по прежнему на уровне, так что учиться интересно

Много "уроков" по 2-3 минуты, но проходятся они сильно дольше, если делать сразу конспект и отмечать какие-то непонятные места, так что 15 часов - это очень номинально, по факту, конечно, больше

Из курсов, которые меня интересуют на изучение в качестве следующих - это конечно курсы по Zero-Knowledge Proofs, их там 2, курс по Rust, либо закрыть Advanced Foundry, но пока конечно планирую сделать Formal Verification на текущем проекте

Про Formal Verification, часть 1

Упоминал про этот метод анализа кода здесь

Рассказывать буду на примере Certora, так как сам пользуюсь их сервисом. Это будет серией постов неопределенной длины, поскольку нюансов работы множество.

Формальная верификация - это метод, при котором корректность кода подтверждается математически. Идея в том, что доказывается соответствие анализируемой кодовой базы заявленным свойствам.

Именно соответствие свойствам и является уникальной чертой формальной верификации, так как остальное тестирование по сути проверяет только работу системы в частных случаях, что не дает полной картины даже если этих частных случаев десятки тысяч.

Certora (произносится как «сертора») как система состоит из двух частей:
- Certora Verification Language
- Certora Prover

Certora Verification Language - CVL
Это специальный язык, который используется для написания спецификаций для смарт контрактов

Certora Prover
Прувер (в переводе с англ. проверяющий/доказывающий) основывается на общеизвестных техниках формальной верификации. По сути это широкое понятие, которое включает в себя несколько частей, включающее в себя компилятор, декомпилятор, статический анализатор и прочее, подробно его устройство разбирается вот здесь, на 57 слайдах

В спецификациях определяются правила анализируемого контракта, которые несут в себе некоторые предположения о его поведении. Эти правила компилируются в логические формулы, которые называются verification condition. Обычно их создается некоторое множество, которое затем отправляется на анализ в SMT Solver

SMT Solver - Satisfiability Modulo Theories Solver. Проверяет могут ли быть удовлетворены условия выражения

Для написания теста формальной верификации по стандарту создается в корне проекта папка certora с двумя подпасками: conf и spec и в них соответственно два файла с расширениями .spec и .conf

На этом сегодня закончу, хороших выходных!

https://t.me/web3securityresearch

Formal Verification, часть 2
.conf файл

Конфигурационный файл и этим все сказано. Хранит в себе пути к исследуемым контрактам, к файлу спецификации, содержит настройки прувера

Имеет расширение .conf, пишется как JSON

Типичный файл выглядит так

{
    "files": [
        "./src/OurContract.sol:OurContract",
        "./src/AnotherContract.sol:AnotherContract"
    ],
    "verify": "OurContract:certora/spec/OurContractInvariant.spec",
    "wait_for_results": "all",
    "rule_sanity": "basic",
    "optimistic_loop": true,
    "msg":"Verification of OurContractInvariant"
}

После разделов files и verify находятся настройки анализа, альтернативно их можно писать в CLI при вызове команды certoraRun, которая запускает верификацию

То есть можно было бы написать

 certoraRun ./certora/conf/OurContract.conf --verify OurContract:certora/spec/OurContractInvariant.spec --wait_for_results all --rule_sanity basic --optimistic_loop true --msg Verification of OurContractInvariant

Кроме прочего таким образом могут быть заданы настройки самого прувера

После запуска команды certoraRun компилируются контракты, затем проверяется корректность локально, если все ок, то задача уходит в работу на сервер, когда будет готово - вам пришлют ссылку на отчет

Потому что Certora работает по freemium модели и вам доступны 2000 минут работы сервиса в месяц

https://t.me/web3securityresearch

Интересный пост в Сиолошной, про то как AI модели могут находить и эксплуатировать уязвимости в смарт-контрактах уже сейчас

оригинал статьи на английском от Антропик

В статье указаны две уязвимости в коде:
- в первом случае в контракте все пользователи имели доступ к функции калькулятора, меняющей storage переменные и модель смогла провести inflation attack, про которые я писал
- во втором случае в контракте, выпускающем токены в один клик, можно было задеплоить токен без указания адреса для приема комиссий. Зато его можно было добавить позже

Круто, что атакующие скрипты в исходной статье тоже показаны

https://t.me/web3securityresearch

Formal Verification, часть 4

Правило для проверки transfer в ERC-20

Сегодня разбираем как написать правило на примере стандартной реализации ERC-20

Проверяемое правило:
Баланс бенефициара увеличивается соответствующим образом

Правило простое, в общих чертах похожее на то, что стоило бы написать в обычном тесте

/** @title Transfer must move `amount` tokens from the caller's
 *  account to `recipient`
 */
rule transferSpec(address recipient, uint amount) {

    env e;
    
    // `mathint` is a type that represents an integer of any size
    mathint balance_sender_before = balanceOf(e.msg.sender);
    mathint balance_recip_before = balanceOf(recipient);

    transfer(e, recipient, amount);

    mathint balance_sender_after = balanceOf(e.msg.sender);
    mathint balance_recip_after = balanceOf(recipient);

    // Operations on mathints can never overflow nor underflow
    assert balance_sender_after == balance_sender_before - amount,
        "transfer must decrease sender's balance by amount";

    assert balance_recip_after == balance_recip_before + amount,
        "transfer must increase recipient's balance by amount";
}

Необычных вещей здесь несколько:
1) env e. Главное отличие ФВ от тестов в том, что она учитывает все возможные входные данные и все возможные контексты вызова. Как раз контекст передается через переменную env. Достаточно объявить одну, но можно использовать больше. Соответственно, она содержит/предоставляет такую информацию как: e.msg.sender, e.block.number и так далее. Передавать e следует первой из аргументов
2) mathint. Это собственный тип CVL для целых чисел произвольного размера. Позволяет не беспокоиться о переполнении и знаке
3) в CVL можно использовать только assert, а вот assertEq не поддерживается

Выполнение проверки этого правила завершится с ошибкой, отчет об этом на прикрепленном изображении

...
Finished verification request
ERROR: Prover found violations:

[rule] transferSpec: FAIL
report url: https://prover.certora.com/output/...

Violations were found

Ошибка возникает в случае, когда пользователь отправляет токены сам себе, так что assert'ы неверны

На экране отчета мы видим 4 столбца:
- слева мы видим проверяемые правила
- второй столбец содержит проверяемый код
- в третьем call trace вызова, в котором обнаружено нарушение
- в четвертом значения переменных и параметров

Для того, чтобы обрабатывать этот случай следует добавить следующий assert

    assert recipient == sender => balance_sender_after == balance_sender_before,
        "transfer must not change sender's balancer when transferring to self";

То есть отдельно обработать случай, когда отправитель и получатель - один и тот же адрес. После этого правило должно выполняться во всех случаях

Ссылки:
- Туториал, взятый за основу
- Исследуемая реализация ERC-20, код
- Исходная спецификация
- Исправленная спецификация

https://t.me/web3securityresearch

Вышел Solidity 0.8.31

Команда Solidity объявила о выходе компилятора Solidity версии 0.8.31. Обновление приносит поддержку новых возможностей EVM, представленных в сетевом апгрейде Fusaka, расширяет функциональность спецификаторов раскладки хранилища и запускает первый этап отказа от устаревших возможностей, которые будут окончательно удалены в версии 0.9.0. Кроме того, теперь официально публикуются сборки компилятора для Linux на архитектуре ARM.

Одним из ключевых изменений стало то, что версия EVM с кодовым названием osaka теперь используется по умолчанию. При необходимости разработчики по-прежнему могут указать более старую версию виртуальной машины через настройки компилятора. В новой версии также добавлена поддержка опкода CLZ, реализующего стандарт EIP-7939. Эта инструкция позволяет считать количество ведущих нулей в 256-битном слове и открывает новые возможности для оптимизаций, битовых операций, алгоритмов сжатия и работы со структурами данных на уровне приложений.

В ближайшее время этот опкод найдет активное применение в популярных библиотеках, включая solady и OpenZeppelin, где сможет заменить существующие реализации вроде Math.clz(). Пока в самом компиляторе область применения CLZ ограничена, но команда изучает способы использовать его для будущих оптимизаций генерации байткода.

С точки зрения инфраструктуры релиза произошло важное обновление: начиная с этой версии, Solidity официально выпускается в виде бинарных сборок для Linux на ARM. Ранее такие версии существовали либо в виде сборок под macOS, либо в виде самостоятельной компиляции из исходников. Теперь ARM-билды встроены в систему CI и проходят тот же цикл тестирования, что и остальные платформы, гарантируя идентичность байткода и метаданных на всех архитектурах.

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

Одновременно команда начала оптимизировать каналы распространения компилятора. В частности, официально прекращена поддержка Ubuntu PPA, так как этот канал оказался маловостребованным. Docker-сборки пока сохраняются, но в будущем тоже могут быть убраны, если их использование останется незначительным. При этом контейнеры уже перенесены из DockerHub в реестр GitHub, и новые версии будут публиковаться именно там.

Наконец, версия 0.8.31 открывает фазу активной подготовки к релизу 0.9.0, который станет несовместимым с предыдущими версиями. В компилятор добавлены предупреждения об устаревании send() и transfer(), устаревшего ABI coder v1, виртуальных модификаторов, сравнений контрактов без явного приведения к адресу и специального комментария memory-safe-assembly. Всё это сигнализирует о переходе Solidity к более строгой типизации, более прозрачной семантике и сокращению исторически сложных и небезопасных конструкций, которые долгое время тянулись из ранних версий языка.

#solidity

Formal Verification, часть 4.1

Правило для проверки total supply в ERC-20

Проверяемое правило:
Total supply токена > баланс любого пользователя

Правило несложное, выглядит так. Сминтили токены на аккаунт, проверяем

/// @title Total supply after mint is at least the balance of the receiving account
rule totalSupplyAfterMint(address account, uint256 amount) {
    env e; 
    
    mint(e, account, amount);
    
    uint256 userBalanceAfter = balanceOf(account);
    uint256 totalAfter = totalSupply();
    
    // Verify that the total supply of the system is at least the current balance of the account.
    assert totalAfter >=  userBalanceAfter, "total supply is less than a user's balance";
}

Вот только по отчету certora это правило будет нарушено/violated

Потому что Certora работает так, что проверяет все возможные пути, даже те, которые невероятны/недостижимы. В данном случае один из таких путей это когда totalSuplly() вернет значение меньше, чем balanceOf()

Потому что Certora не запускает код, она проверяет его математически, для нее нет значения в чем суть той или иной функции, она делает over-approximation, т.е. чрезмерные предположения. И эта часть наверное наиболее сложная, потому что требует изменить логику работы с кодом, который требуется написать

Поэтому существуют

Preconditions - условия, которые мы задаем явно

В данном случае после строчки с env e следует добавить:

    // Assume that in the current state before calling mint, the total supply of the 
    // system is at least the user balance.
    uint256 userBalanceBefore =  balanceOf(account);
    uint256 totalBefore = totalSupply();
    require totalBefore >= userBalanceBefore; 

То есть обозначить, что total supply до операции был больше, чем user balance до операции

Про переменные надо еще сказать следующее:
- неинициализированная переменная может принимать любое значение
- require тем не менее может ограничить ее каким-либо образом
- переменные внутри правила immutable
- а вот ghost переменные могут меняться

Ссылки:
- Туториал, взятый за основу
- Спецификация

https://t.me/web3securityresearch

Formal Verification, часть 5

Parametric rules - Параметрические правила

Тот момент, где начинает раскрываться мощь инструмента

Многие свойства могут быть обобщены для всех функций контракта

Проверяемое правило:
Allowance может меняться только владельцем

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

К тому же подобных правил под проверку может быть несколько

Как выглядит параметрическое правило

rule someParametricRule(method f) {
    ...
    env e;  // The env for f
    calldataarg args;  // Any possible arguments for f
    f(e, args);  // Calling the contract method f
    ...
}

То есть мы в правило передаем некий method f в качестве параметра. Прувер будет передавать все возможные методы для исполнения в правило, а поскольку это имитация вызовов, то каждому вызову метода f положено передавать контекст вызова через env e и данные вызова через calldataarg args. При этом calldataarg автоматически подстроится под сигнатуры функций

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

Выглядит так:

f.selector == sig:approve(address, uint).selector

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

Полный пример кода:

/**
 * # ERC20 Parametric Example
 *
 * Another example specification for an ERC20 contract. This one using a parametric rule,
 * which is a rule that encompasses all the methods in the current contract. It is called
 * parametric since one of the rule's parameters is the current contract method.
 * To run enter:
 * 
 * certoraRun ERC20.sol --verify ERC20:Parametric.spec --solc solc8.0 --msg "Parametric rule"
 *
 * The `onlyHolderCanChangeAllowance` fails for one of the methods. Look at the Prover
 * results and understand the counter example - which discovers a weakness in the
 * current contract.
 */

// The methods block below gives various declarations regarding solidity methods.
methods
{
    // When a function is not using the environment (e.g., `msg.sender`), it can be
    // declared as `envfree`
    function balanceOf(address) external returns (uint) envfree;
    function allowance(address,address) external returns(uint) envfree;
    function totalSupply() external returns (uint) envfree;
}

/// @title If `approve` changes a holder's allowance, then it was called by the holder
rule onlyHolderCanChangeAllowance(address holder, address spender, method f) {

    // The allowance before the method was called
    mathint allowance_before = allowance(holder, spender);

    env e;
    calldataarg args;  // Arguments for the method f
    f(e, args);                        

    // The allowance after the method was called
    mathint allowance_after = allowance(holder, spender);

    assert allowance_after > allowance_before => e.msg.sender == holder,
        "only the sender can change its own allowance";

    // Assert that if the allowance changed then `approve` or `increaseAllowance` was called.
    assert (
        allowance_after > allowance_before =>
        (
            f.selector == sig:approve(address, uint).selector ||
            f.selector == sig:increaseAllowance(address, uint).selector
        )
    ),
    "only approve and increaseAllowance can increase allowances";
}

К этому моменту может появиться ощущение, что все не так уж сложно, но это до тех пор, пока вы не запустите ФВ на своем коде

Ссылки:
- Туториал, взятый за основу
- Спецификация на github

https://t.me/web3securityresearch