Тут разбор, пусть останется для истории ссылка

Атака: Inflation Attack

Инфляционная атака - это распространенная атака, характерная для Vault’ов стандарта ERC-4626

Этот стандарт вам знаком, если вы хоть раз депонировали средства в протоколы-обёртки под процент или поинты

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

Огромное количество протоколов использует этот стандарт, здесь список

Когда возникает
На ранних стадиях этому подвержен любой пул, который предлагает обмен активов на долю в этом пуле.
То есть, если ваш протокол в том или ином виде предлагает функцию минта долей (mint shares), то вы под ударом

Формула минта обычно выглядит примерно так

sharesAmount = totalShares * assetAmount / asset.balanceOf(address(this))

Атакующий может манипулировать делителем, что может привести к получению очень малой доли токенов пула, вплоть до нулевой

Пример кода, подверженного атаке

abstract contract ERC4626 is ERC20 {
    IERC20 asset;

    constructor(IERC20 asset_) {
        asset = asset_;
    }

    function totalAssets() public view returns (uint256) {
        return asset.balanceOf(address(this));
    }

    function convertToShares(uint256 assets) public view returns (uint256) {
        if (totalAssets() == 0) {
            return assets;
        }
        return totalSupply() * assets / totalAssets();
    }

    function convertToAssets(uint256 shares) public view returns (uint256) {
        return totalAssets() * shares / totalSupply();
    }

    function deposit(uint256 assets) public {
        asset.transferFrom(msg.sender, address(this), assets);
        _mint(msg.sender, convertToShares(assets));
    }

    function burn(uint256 shares) public {
        _burn(msg.sender, shares);
        asset.transfer(msg.sender, convertToAssets(shares));
    }
}

Сценарий атаки
1. Атакующий делает back-run создаваемого пула. Бэк раннинг - это когда хакер увидел транзакцию еще в мемпуле, до включения в блок, и закинул свою транзакцию так, чтобы она шла сразу же за транзакцией создания пула. Буквально «дышит в спину», если переводить по смыслу
2. Атакующий минтит себе один share пула, одну долю то есть
3. Атакующий фронтраннит депозит жертвы на 20_000 USDT
4. Атакующий раздувает делитель в формуле расчета долей до 20_000, для этого можно использовать прямой депозит в обход функции минта
5. Из-за того что в Solidity по умолчанию деление целочисленное, а хакер делает фактически


sharesAmount = 1 * 20_000 / (1 + 20_000), где в верхней части дроби средства жертвы, а внизу то что
внес хакер двумя транзакциями, то есть результат меньше 1 и он округляется до 0

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

Что можно предпринять:
1. Учет баланса контракта лучше вести созданными для этого переменными, а не полагаться на asset.balanceOf(address(this));
2. Использовать ERC4626 Router
3. Использовать "dead shares"

При подготовке поста использовалась статья от MixBytes()

https://t.me/web3securityresearch

Как заработать сотни тысяч долларов на NFT

Речь пойдет про вчерашнюю ситуацию/инцидент с контрактами группы Strategy

Коротко, для тех кто всё пропустил, в общих чертах. Сейчас в крипте появилась новая «мета» strategy (нарратив, тема, мода, идея - называйте как угодно), суть которой заключается в следующем:

1. У нас есть NFT проекты со своей аудиторией, с богатой историей и достаточно высокой ценой за одну NFT
2. NFT рынок живет волнами активности, у многих коллекций на фоне роста эфира просели цены, потому что люди продают NFT и фиксируют эфир
3. Что если откупать эти NFT на комиссии, которые были собраны с торговли определенным токеном? Будет расти цена коллекции, потому что никто не хочет продавать дешево, когда у тебя есть гарантия выкупа
4. Купленная NFT продается в рынок, вырученные средства идут теперь уже на выкуп токена с последующим сжиганием. Цена токена растет, NFT дорожают и все такое.

Мы не будем останавливаться на том кто же платит за вечеринку, это просто механизм, вот тут про тайминги и имена написано
https://t.me/MMPRTVNFT/3614

Что произошло?
Произошел деплой контракта, который должен этот механизм осуществлять, помимо прочего там есть функция

function buyTargetNFT(uint256 value, bytes calldata data, uint256 expectedId, address target) external nonReentrant {
        // Store both balance and nft amount before calling external 
        uint256 ethBalanceBefore = address(this).balance;
        uint256 nftBalanceBefore = collection.balanceOf(address(this));

        // Make sure we are not owner of the expected id
        if (collection.ownerOf(expectedId) == address(this)) {
            revert AlreadyNFTOwner();
        }

        // Ensure value is not more than currentFees
        if (value > currentFees) {
            revert NotEnoughEth();
        }

        // Call external
        (bool success, bytes memory reason) = target.call{value: value}(data);
        if (!success) {
            revert ExternalCallFailed(reason);
        }

        // Ensure we now have one more NFT
        uint256 nftBalanceAfter = collection.balanceOf(address(this));

        if (nftBalanceAfter != nftBalanceBefore + 1) {
            revert NeedToBuyNFT();
        }

        // Ensure we are now owner of expectedId
        if (collection.ownerOf(expectedId) != address(this)) {
            revert NotNFTOwner();
        }

        // Calculate actual cost of the NFT to base new price on
        uint256 cost = ethBalanceBefore - address(this).balance;
        currentFees -= cost;

        // List NFT for sale at priceMultiplier times the cost
        uint256 salePrice = cost * priceMultiplier / 1000;
        nftForSale[expectedId] = salePrice;
        
        emit NFTBoughtByProtocol(expectedId, cost, salePrice);
    }

Она позволяет указать контракту какую NFT и по какой цене покупать, это ок

Ну и она в общем то не отслеживает то, кто ее вызывает, то есть мог её вызвать кто угодно

Соответственно, нашелся человек, который начал контракту продавать свои NFT по x3 цене, затем откупать, потом снова продавать, до тех пор, пока на контракте не кончились деньги

Эта уязвимость называется Missing Access Control, это одна из первых уязвимостей, которую вам показывают на курсах по безопасности

Неужели разрабы контрактов настолько не шарят?

Есть вариант, что это была не уязвимость, а недоделанная система

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

И есть парень, который вчера, через пару часов после инцидента, написал бота, который теперь следит за количеством средств + за ценами на NFT и инициирует покупку, вот он

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

https://t.me/web3securityresearch

А что такое deadshares?

Для того, чтобы атакующий не мог размыть долю вкладчика, используются так называемые dead shares, т.е. мертвые доли

Например, при инициализации пула мы можем сминтить 1000 shares и отправить их на нулевой адрес

function initialize() public {
    uint256 deadAmount = 1000; // Или 1e6, в зависимости от decimals
    _mint(address(0), deadAmount); // Минтим и "сжигаем" на нулевом адресе
}

Размыть 1000 долей намного сложнее, чем манипулировать отправной точкой 0, то есть мы не закрываем уязвимость, но делаем эксплуатацию сильно дороже, потому что в

sharesAmount = totalShares * assetAmount / asset.balanceOf(address(this))

totalShares теперь равен 1000, а не 1, как было показано в примере атаки

UPD. Мне попалась классная атака с обходом deadshares, так что этот пост нужен для контекста разбора

https://t.me/web3securityresearch

Метамаск выкатил в ранний доступ 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