비탈릭, 형식 검증 발전·한계 분석

비탈릭 부테린 이더리움 공동창업자가 형식 검증이 이더리움과 더 넓은 컴퓨팅 영역에서 보안성을 높일 수 있지만, 모든 문제를 해결하는 수단은 아니라고 밝혔다.

오데일리에 따르면 비탈릭은 글을 통해 개발자가 EVM 바이트코드, 어셈블리, 린(Lean) 등 저수준 언어나 증명 도구를 활용해 코드의 정확성을 수학적으로 검증하는 흐름이 이더리움 연구 진영에서 확산하고 있다고 설명했다.

그는 형식 검증이 프로그램의 성질을 기계가 확인할 수 있는 수학적 증명으로 검증하는 방식이라며, 암호 통신·암호 프로토콜·영지식증명·합의 메커니즘 등 핵심 시스템의 신뢰성을 높이는 데 활용될 수 있다고 했다.

다만 보안 정의가 사람의 모델링에 의존하고, 일부 시스템은 완전한 형식화가 어려우며, 하드웨어나 검증되지 않은 모듈이 여전히 공격 지점이 될 수 있다고 지적했다. 사양 오류나 검증 범위 밖의 가정도 취약점으로 이어질 수 있다는 설명이다.

비탈릭은 향후 형식 검증을 AI 보조 프로그래밍, 타입 시스템, 테스트 프레임워크와 함께 적용하는 것이 현실적이라고 밝혔다. 앞서 이더리움 생태계는 EVM 구현, STARK 증명 시스템, 양자내성 서명 등 주요 인프라의 검증 가능성을 연구해왔다.