TechFlow 보도에 따르면, 5월 18일 비탈릭(Vitalik)이 「형식 검증(Formal Verification)에 대한 간략한 탐색」이라는 제목의 글을 발표하여 이더리움 최첨단 연구 개발에서 형식 검증의 적용 현황을 소개했다. 이 글에서 그는 개발자들이 린(Lean), EVM 바이트코드 또는 어셈블리 언어로 코드를 작성한 후, 자동으로 검사 가능한 수학적 증명을 통해 해당 코드의 정확성을 검증함으로써 코드의 효율성과 보안성을 동시에 향상시킬 수 있다고 설명했다.
그는 형식 검증이 특히 STARK, 비잔틴 장애 허용(BFT) 합의, ZK-EVM, 양자 내성 서명(quantum-resistant signatures) 등과 같이 복잡하지만 보안 목표가 비교적 명확한 시스템에 적합하다고 지적했으며, 아크라이브(Arklib), VCV-io, evm-asm 등의 관련 프로젝트를 언급했다. 또한 이 글은 형식 검증이 만능이 아니라는 점을 강조하면서, 사양(specification) 정의 오류, 검증되지 않은 코드 영역, 하드웨어 경계, 사이드 채널 공격(side-channel attacks) 등의 한계를 여전히 안고 있음을 지적했다.
즐겨찾기 추가
소셜 미디어 공유
