Аналитик Стивен Тонг обнаружил ошибки дизайна Wrapped Ether (WETH)

В исследовании Format Verification of Wrapped ETH (WETH) Стивен Тонг проверил два параметра, имеющих решающее значение для токеномического дизайна Wrapped Ether, токена ERC-20, который отражает эфир (ETH) в приложениях DeFi.

Тонг опубликовал обзор двух функций Wrapped Ethereum (WETH), смарт-контракта в сети Ethereum (ETH), предназначенного для оптимизации использования ETH в DeFi путём «обёртывания» его в обычный ERC-актив.

Ошибка в WETH:

 

Wrapped ETH — это смарт-контракт, который использовался в более чем 125 МИЛЛИОНАХ транзакций Ethereum. В этом году 11,5% всех транзакций использовали Wrapped ETH.

 

Но безопасно ли это? Я проверил два критических свойства безопасности с помощью SMT-решателя Z3.

Он использовал инструменты Constrained Horn Clause (CHC) для моделирования всех возможных состояний Wrapped Ethereum (ETH). В процессе он проверил, действительно ли метрика «общего предложения» смарт-контракта WETH равна количеству выпущенных токенов.

Исследователь также протестировал, можно ли в любое время выкупить ETH у WETH. Тонг назвал эту функцию платёжеспособностью.

Что касается первого пункта, аналитик сообщил, что общее предложение не обязательно равно количеству существующих токенов.

С помощью функции самоуничтожения, которая расторгает контракт или переводит любые контрактные средства на указанный адрес, пользователи смогут выпустить токены WETH, фактически не отправляя ETH для «обёртывания».

Кроме того, Тонг продемонстрировал, что выполнивший депозит эфиров (ETH) пользователь необязательно сможет вывести свои средства со смарт-контрактов в любое время.

Вот результат, который мы хотим видеть!

Таким образом, он предоставил две гипотетические модели, чтобы продемонстрировать отсутствие корреляции между балансом контракта WETH и фактическим количеством выпущенных токенов, а также «недостаток платёжеспособности», который мог повлиять на процесс вывода средств.

Специалист подчеркнул, что обе ситуации являются гипотетическими и моделируются только для эксперимента. Ошибки в исследовании являются «незначительными» и «безвредными».