Noobing Security Research

Mastering Ethereum
https://masteringethereum.xyz/

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

Читаю её последние пару недель, очень цельный и последовательный источник, по сути полное описание того, что следует знать о сети эфира

Смело могу советовать, но надо быть готовым к тому, что материал местами непростой и возникает соблазн глубже провалиться в кроличью нору, либо наоборот бросить текст и это одновременно (привет главе о криптографии)

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

https://t.me/web3securityresearch

Formal Verification, часть 6

Vacuity

Одна из ошибок, с которой я столкнулся (и многие до и после меня), гласит rule is vacuous

Что можно перевести как правило бездумное/бессодержательное

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

Например, наше бездумное требование выглядит так:

rule simpleVacuousRule(uint256 x, uint256 y) {
    // Contradictory requirement
    require (x > y) && (y > x);
    assert false;  // Should always fail
}

У Prover есть свойство rule_sanity, которое может быть задано в .conf файле. Если будет указано, что rule_sanity basic, то прувер пометит это правило как неисполнимое, потому что оно не прошло проверку на корректность. Но если задать rule_sanity none, то правило будет помечено как верифицированное, потому что контрпримера не существует в том плане, что assert недостижим и значит не завершается ошибкой

Происходит это потому, что прувер по умолчанию игнорирует пути, которые завершаются revert'ом симулируемой транзакции

Для включения таких путей в анализ используется оператор @withrevert, который добавляется после названия функции, например someFunction@withrevert(args)

При этом, если someFunction будет ревертнута, то она вернет какое-то случайное значение, а остальные переменные откатятся к своим значениям до транзакции

CVL так же имеет встроенную bool lastReverted, которая изменяется в зависимости от того, была ли последняя вызываемая функция reverted

Зачем это вообще нужно? Чтобы проверять, что некоторые пути действительно всегда недостижимы

Если наша @withRevert функция была ревертнута, то lastReverted становится true и возможно проверить что assert lastReverted. Потому что он теперь во-первых достижим, во-вторых true

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

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

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

Вышел 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

Правило для проверки 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

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

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

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

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

https://t.me/web3securityresearch

Formal Verification, часть 3.2

Что содержит .spec файл

👨‍💻 Sorts: Uninterpreted Sorts по сути своей являются абстрактными типами данных, которые можно сравнивать друг с другом. А неинтерпретируемыми они называются, потому что существуют интерпретируемые: в текущем контексте это все Solidity типы
Пример

sort Foo;

ghost bar(Foo, Foo) returns Foo;

rule myRule {
   Foo x;
   Foo y;
   Foo z = bar(x, y);
   assert x == y && y == z;
}

Создаем тип данных Foo, привязываем его к призрачной переменной bar и используем в правиле. Пока не использовал на практике, но пишут что в некоторых ситуациях проще делать так, ладно


👨‍💻 Ghosts: Призрачные/гост/ghost переменные это почти как обычные переменные, но они могут передавать информацию между rules/правилами и hooks/хуками, и использоваться в саммари методов. Во втором случае это уже ghost function
Пример

ghost uint x;
ghost mapping(address => mathint) balances;

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


👨‍💻 Hooks: Хуки позволяют привязаться кодом к низкоуровневым операциям, например к чтению/записи в STORAGE. Их определенное количество и каждый имеет свой шаблон применения, работают в связке с ghost переменными
Пример

ghost mathint sum_of_balances {
    init_state axiom sum_of_balances == 0;
}

hook Sstore _balances[KEY address a] uint new_value (uint old_value) STORAGE {
    // when balance changes, update ghost
    sum_of_balances = sum_of_balances + new_value - old_value;
}

Такая вот верхушка айсберга. Сложность формальной верификации отчасти в том, что она использует свой язык (но другого пути нет), который содержит огромное количество ньюансов. У меня на данный момент исписано около 20 страниц формата а4 с разбором тех ошибок, которые мне выдавал prover и это я можно сказать только начал

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

https://t.me/web3securityresearch

Formal Verification, часть 3.1

Что содержит .spec файл

Здесь мы на языке CVL (Certora Verification Language) пишем спецификацию

Что может быть указано в .spec файле:

👨‍💻 Import statements: файлы CVL могут импортировать содержимое других файлов CVL
Пример

import "base.spec";

Такое объявление импортирует все элементы из base.spec за исключением правил и инвариантов

👨‍💻 Use statements: оператор use позволяет использовать правила и инварианты из других файлов/встроенных правил
Пример

use rule ruleInBase;

Импортирует правило ruleInBase из base.spec. Может использоваться в связке с фильтрами (о них как-нибудь позже), может переписывать импортированные фильтры

👨‍💻 Using statements: Позволяет получить ссылки на различные контракты
Пример

using Asset as underlying;

Если дальше по файлу писать что-то вроде "underlying.someFunc()", то это равносильно вызову функции на экземпляр контракта

👨‍💻Methods blocks: methods блок содержит информацию о том, как должны вести себя методы, какие из них мы подвергаем суммаризации (summarization). Это вообще один из интересных концептов формальной верификации, про него будет отдельный пост, возможно не один

В блоке методов не надо указывать все проверяемые методы, там необходимы лишь те, про которые мы хотим внести дополнительную информацию
Пример

methods {
    function _.balanceOf(address) external => DISPATCHER(true);
    function _.totalSupply() external => DISPATCHER(true);
    function _.transfer(address, uint256) external => DISPATCHER(true);
    function _.transferFrom(address, address, uint256) external => DISPATCHER(true);
}

👨‍💻 Rules: Правила описывают желаемое поведение методов и контрактов. Корневое понятие, именно правила проверяет prover. Если правило нарушается, то это называется контрпример - counterexample
Пример

/// `deposit` must increase the pool's underlying asset balance
rule integrityOfDeposit {

    mathint balance_before = underlyingBalance();

    env e; 
    uint256 amount;
    safeAssumptions(_, e);

    deposit(e, amount);

    mathint balance_after = underlyingBalance();

    assert balance_after == balance_before + amount,
        "deposit must increase the underlying balance of the pool";
}

Простое правило, которое проверяет, что баланс после всегда равен балансу до плюс вносимая сумма

👨‍💻 Invariants: Инвариант описывает свойство системы, которое всегда должно выполняться. В CVL инвариант может быть сильным или слабым. Первый должен выполняться в "момент покоя", то есть пока контракт не исполняется. Сильный инвариант держится не только между транзакциями, но и до/после вызова unresolved external calls, например call или delegatecall
Пример

/// The ball should never get to player 2 - strenghened invariant
invariant playerTwoNeverReceivesBall() 
    ballPosition() == 1 || ballPosition() == 3;

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

👨‍💻 Functions: CVL функции. Могут использоваться для вычислений, могут переопределять функции из блока methods
Пример

function abs_value_difference(uint256 x, uint256 y) returns uint256 {
    if (x < y) {
      return y - x;
    } else {
      return x - y;
    }
}

👨‍💻 Definitions: CVL определения - это типизированные макросы, предназначаются для упрощения спецификации.
Пример

definition MAX_UINT256() returns uint256 = 0xffffffffffffffffffffffffffffffff;
definition is_even(uint256 x) returns bool = exists uint256 y . 2 * y == x;

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

Про 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

Закончил 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 на текущем проекте

Тесты? Тесты. Часть 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

Тесты? Тесты. Часть 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

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

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

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

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

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

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

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

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

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

https://t.me/web3securityresearch

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

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

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

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

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

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

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

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

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

https://t.me/web3securityresearch

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

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

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

Обновление!

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

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

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

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

https://t.me/web3securityresearch

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

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

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

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

Это было для меня поначалу непривычно, но 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

UPD от 9.04.2026
Crypto Data Bytes
https://read.cryptodatabytes.com/

OurNetwork
https://ournetwork.substack.com/

HashItOut
https://0xknight.substack.com/


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

https://t.me/web3securityresearch