Разработчики Ethereum предложили пять путей формальной верификации клиентов
- —TCB — компоненты и допущения, которые принимаются на веру без проверки
- —Чистые модули (криптография, SSZ, выбор форка) подходят для формальной верификации
- —Нечистые модули (сеть, I/O) предлагается проектировать без доверия к их выводам
- —Пять путей: конвертация Rust в Lean4, экстракция Lean4 в C, клиент на Lean4, RISC-V, верифицированный компилятор
Почему важно: Снижение TCB уменьшит поверхность атак на клиенты Ethereum, но это пока исследование, а не готовое решение.
Источник: TokenPost