이더리움 클라이언트 신뢰 기반 줄일 검증 경로 5가지

본문

이더리움 연구 포럼이 클라이언트의 신뢰 컴퓨팅 기반(TCB)을 줄이는 형식 검증 설계와 구현 경로를 공개했다. 순수·비순수 모듈을 나누고 구현과 컴파일 과정까지 검증하는 방안이 담겼다. 이더리움 클라이언트의 신뢰 컴퓨팅 기반(TCB)을 줄이기 위한 형식 검증 설계와 구현 경로 5가지가 공개됐다. 조지 카디아나키스(George Kadianakis) 이더리움재단 멤버와 케브 웨더번(Kev Wedderburn) 이더리움재단 멤버는 25일 이더리움 연구 포럼에 관련 글을 게시했다. 형식 검증으로 이더리움 클라이언트의 신뢰 대상 범위를 줄이는 방안을 설명했다. 형식 검증이 TCB를 완전히 없애지는 못하지만 사람이 직접 신뢰해야 하는 범위를 줄일 수 있다는 것이 글의 출발점이다. 예를 들어 네트워크 모듈이 전달하는 서명을 그대로 신뢰하지 않고 순수한 서명 검증 모듈에서 다시 처리하면 네트워크 모듈의 버그도 악의적인 외부 입력과 같은 방식으로 다룰 수 있다.

장기적으로는 검증 경계를 네트워크에 더 가깝게 옮기는 방안도 제시했다.

구현 경로로는 △Rust 등으로 작성된 코드를 Lean4로 자동 변환하는 방식 △Lean4로 작성한 모듈을 C 코드로 추출하는 방식 △클라이언트 자체를 Lean4로 작성하고 부작용이 큰 모듈만 다른 언어로 연결하는 방식 △RISC-V 어셈블리로 핵심 모듈을 직접 작성하는 방식 △검증된 컴파일러를 사용하는 방식이 제시됐다. Lean4 코드를 C로 추출하거나 클라이언트 대부분을 Lean4로 작성하는 경우에는 추출기와 C 컴파일러, 외부 함수 인터페이스가 신뢰 대상에 포함된다. RISC-V 어셈블리로 핵심 모듈을 작성하면 일반 컴파일러를 TCB에서 제외할 수 있지만 RISC-V 명령어 집합의 형식 모델과 어셈블리를 다른 프로세서용 코드로 바꾸는 도구가 새로운 신뢰 대상이 된다. 이번 글은 이더리움 클라이언트 전체가 이미 형식 검증을 마쳤다는 발표가 아니다.