이더리움, 린 4로 3개 업그레이드 합의 검증

본문

Etheorem 프로젝트가 린 4로 이더리움의 Fulu·Gloas·Heze 합의 규격을 구현하고 수학적으로 검증하고 있다. 이더리움(ETH) 연구팀이 린 4(Lean 4)로 Fulu·Gloas·Heze 업그레이드의 합의 규격을 구현하고 수학적으로 검증하는 프로젝트를 추진하고 있다. 이더리움 프로토콜 펠로십(EPF)과 인비저블 가든(Invisible Garden) 연구팀은 21일 이더리움 리서치 포럼 게시글을 통해 프로젝트 ‘Etheorem’의 진행 상황을 공개했다. Etheorem은 정리 증명 언어인 린 4로 이더리움 합의 규격을 실행 가능한 형태로 구현하고, 코드 테스트를 넘어 핵심 논리를 수학적으로 검증하는 것을 목표로 한다. 이더리움은 여러 개발팀이 만든 합의 클라이언트를 함께 사용하는 구조다. 프로젝트는 Fulu·Gloas·Heze 업그레이드에 해당하는 합의 규격을 구현했다.

상태 전환과 포크 선택 로직을 실행할 수 있으며, 이더리움 공식 합의 테스트 벡터와 대조해 구현 결과를 확인하고 있다.

이 라이브러리는 합의 데이터의 직렬화·역직렬화와 머클 트리 계산에 필요한 일부 속성을 린 커널에서 검증한다. 검증 대상에는 직렬화된 데이터가 원래 값으로 되돌아오는지, 서로 다른 값이 같은 인코딩을 갖지 않는지, 인코딩 크기가 사전에 계산된 한도를 넘지 않는지가 포함된다. 같은 규격 정의를 검증 환경과 실행 환경에서 함께 사용해 증명에 쓰인 로직과 실제 클라이언트의 로직이 달라지는 문제를 줄이겠다는 구상이다. 형식 검증이 적용 범위 안의 논리를 점검하는 방식인 만큼, 전체 이더리움 클라이언트를 대체하는 단계는 아니다. 블록체인 프로토콜의 린 4 형식 검증 사례 도 핵심 로직을 모델로 재현해 검증 범위를 설정하는 방식으로 진행됐다.