CertiK формально доказала корректность zkVM zkWasm в Coq

CertiK завершила формальную верификацию zkWasm — zero-knowledge виртуальной машины от Delphinus Lab для доказательства корректного исполнения WebAssembly. В Coq доказаны soundness и knowledge soundness для всего набора инструкций; около 6 000 строк Rust-схем потребовали 33 080 строк определений и доказательств.

• Доказаны soundness и knowledge soundness для всех инструкций zkWasm
• 6 000 строк Rust-схем потребовали 33 080 строк Coq-доказательств
• Формальные методы выявили баг с подделкой возврата из функции
• Исследование USENIX 2024: 99 из 141 уязвимости zk-систем — в схемах