PANews에 따르면 비탈릭 부테린은 이더리움 커뮤니티가 Lean 등 형식 검증 도구를 활용해 EVM 바이트코드와 RISC-V 어셈블리 같은 저수준 언어 코드의 정확성과 보안을 검증하는 실험을 진행하고 있다고 밝혔다.
부테린은 형식 검증이 암호화 통신 프로토콜, 합의 알고리즘, EVM 구현 등 핵심 인프라의 보안을 확인하는 데 활용될 수 있으며, AI가 버그를 자동으로 찾아내는 환경에서 방어 측의 이점을 키울 수 있다고 설명했다.
다만 그는 형식 검증이 만능은 아니며, 모델링되지 않은 가정이나 사이드 채널, 검증 범위 밖 모듈 등은 여전히 위험 요인으로 남는다고 지적했다. 그는 향후 소프트웨어가 소수의 보안 핵심 구조를 중심으로 구축되고, AI가 코드 생성을 맡는 방식으로 발전할 수 있다고 전망했다.
<저작권자 ⓒ TokenPost, 무단전재 및 재배포 금지>
많이 본 기사