Formal Verification, часть 7.1
про _safeTransfer()

На прошлой неделе я участвовал в коротком аудит контесте, который решил "взять" с помощью формальной верификации

Спойлер: я ничего не нашел, но зато вернулся к ФВ и мне есть чем поделиться

Речь сегодня пойдет про поведение SMT-solver при контакте с assembly блоками кода. Я не нашел статей на эту тему, Claude не нашел статей на эту тему, возможно плохо искали, есть вероятность, что их нет, тк тема достаточно узкоспециальная. В этой статье я хочу изложить последовательное решение задачи, включая части, не давшие результата, но важные для понимания. Для тех, кто занимается ФВ постоянно и давно многие вещи должны быть известны, для всех остальных будет полезно.

В июле 2025 OpenZeppellin обновили код SafeERC20 так, что теперь _safeTransfer(), _safeTransferFrom(), _safeApprove() используют низкоуровневые вызовы через assembly. Так что речь идет о пятой версии контрактов, OZ v5

Для формальной верификации это существенное изменение, потому что происходящее в блоке assembly для SMT-solver'a фактически является слепой зоной. Когда солвер не может определить последствий вызова какой либо функции внешнего контракта, он применяет HAVOC_ECF - havoc external contract fields (подстановка случайных значений во все storage слоты). В моем случае, когда Stacking контракт обращался к контракту Token, это приводило к полной перезаписи всей информации в Token -> консистентность нарушена, проверка не работает

Более того, поскольку вызов внутри SafeERC20 не может быть отслежен, то Prover видел его как [?].[?], то есть неизвестно ни к кому обращается вызов, ни к какой функции

1. Было решено применить DISPATCHER(true), который позволяет явно указать на реализации, которые ожидаемо должны быть вызваны.

function _.transfer(address, uint256) external => DISPATCHER(true);
function _.transferFrom(address, address, uint256) external => DISPATCHER(true);

В случае OZ v5 важно понимать, что сам по себе диспетчер не вызывает тело функции, он проверяет, что функция по "адресу" существует, что её вызов не вызывает revert, а в ответ возвращает произвольное значение, которое НЕ записывается в storage. Это называется режимом подмены, он используется, если sighash (селектор функции) недоступен. Если же sighash доступен, то возвращаемое значение запишется в storage
Итог: [?].[?] сменилось на [Token.transferFrom]/, но это не помогло, потому что дальше вызов все равно идет из assembly блока -> HAVOC -> нарушение маппинга балансов токена

2. Попробовал конкретизировать место возникновения с помощью unresolver external in Staking (неопределенные вызовы из контракта стейкинга), DISPATCH должен был эти вызовы сопоставить с конкретными методами контракта Token и возвращаемое значение поменял на NONDET, т.е. любое произвольное. Это должно было ограничить HAVOC токена,

unresolved external in Staking._ => DISPATCH [
    Token.transfer, 
    Token.transferFrom
] default NONDET

Это в какой-то мере сработало, система перестала погружаться в хаос, но NONDET значения тоже не записываются в storage, потому что NONDET тоже работает в режиме подмены, если неизвестен sighash. DISPATCH находил функцию, но unresolved external заставляет Prover оценивать функции внутри как view-only.
Поэтому внутренний маппинг стейкинга увеличивался, а вот баланс контракта стейкинга в контракте токена не обновлялся -> ложное нарушение инварианта

3. Следующим шагом я решил отслеживать изменения балансов ghost переменной, чтобы обойти view-only ограничение + прописать явную суммаризацию. План надежный, как швейцарские часы:
- создаем ghost переменную ghostBalance
- меняем её через специально написанную функцию tokenTransferFromSummary()
- tokenTransferFromSummary() через блок methods привязывается к Token.transferFrom()

Но оказалось, что при входе в unresolved external происходит перехват вызова на уровне опкода CALL раньше, чем применяется суммаризация метода.

https://t.me/web3securityresearch