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

이더리움 클라이언트의 신뢰 컴퓨팅 기반(TCB)을 줄이기 위한 형식 검증 설계와 구현 경로 5가지가 공개됐다.

조지 카디아나키스(George Kadianakis) 이더리움재단 멤버와 케브 웨더번(Kev Wedderburn) 이더리움재단 멤버는 25일 이더리움 연구 포럼에 관련 글을 게시했다. 형식 검증으로 이더리움 클라이언트의 신뢰 대상 범위를 줄이는 방안을 설명했다.

TCB는 검증된 대상이 아니라 신뢰를 전제로 사용하는 구성 요소와 규격, 도구, 가정을 뜻한다. 형식 검증이 TCB를 완전히 없애지는 못하지만 사람이 직접 신뢰해야 하는 범위를 줄일 수 있다는 것이 글의 출발점이다.

연구진은 추상화한 클라이언트를 여러 모듈로 나눠 각 모듈의 역할과 보장 범위를 따로 검증하는 접근을 제시했다. 모듈별 보장을 인터페이스로 연결하면 전체 클라이언트의 보안 속성을 확인할 수 있다는 설명이다.

핵심 구분은 ‘순수 모듈’과 ‘비순수 모듈’이다. 암호학과 SSZ, 포크 선택 규칙처럼 부작용이 적고 수학적 구조가 명확한 영역은 형식 검증에 적합한 순수 모듈로 분류했다. 네트워크처럼 입출력과 외부 상태가 많고 메시지 순서, 연결 단절, 지연 등을 고려해야 하는 영역은 비순수 모듈로 봤다.

연구진은 비순수 모듈을 처음부터 신뢰하지 않는 구조로 설계할 것을 제안했다. 예를 들어 네트워크 모듈이 전달하는 서명을 그대로 신뢰하지 않고 순수한 서명 검증 모듈에서 다시 처리하면 네트워크 모듈의 버그도 악의적인 외부 입력과 같은 방식으로 다룰 수 있다.

장기적으로는 검증 경계를 네트워크에 더 가깝게 옮기는 방안도 제시했다. 네트워크 전체를 모델링하기보다 파서와 가십 규칙, 동기화 로직을 우선 검증해 잘못된 메시지가 시스템을 중단시키거나 과도한 자원을 사용하게 만드는 상황을 막는 방식이다.

글은 사양과 실제 실행 파일 사이의 연결도 별도 과제로 제시했다. 연구진은 Lean4로 형식 사양을 작성하고 속성을 증명하는 일과 실제 구현이 해당 사양을 따르는지 증명하는 일을 구분했다. 이용자는 Lean4의 정리보다 자신의 컴퓨터에서 실행되는 코드의 안전성을 중요하게 보기 때문에 두 단계가 모두 필요하다는 설명이다.

구현 경로로는 △Rust 등으로 작성된 코드를 Lean4로 자동 변환하는 방식 △Lean4로 작성한 모듈을 C 코드로 추출하는 방식 △클라이언트 자체를 Lean4로 작성하고 부작용이 큰 모듈만 다른 언어로 연결하는 방식 △RISC-V 어셈블리로 핵심 모듈을 직접 작성하는 방식 △검증된 컴파일러를 사용하는 방식이 제시됐다.

Rust 코드를 Lean4로 변환하면 변환기와 최종 바이너리를 만드는 Rust 컴파일러가 TCB에 남는다. Lean4 코드를 C로 추출하거나 클라이언트 대부분을 Lean4로 작성하는 경우에는 추출기와 C 컴파일러, 외부 함수 인터페이스가 신뢰 대상에 포함된다.

RISC-V 어셈블리로 핵심 모듈을 작성하면 일반 컴파일러를 TCB에서 제외할 수 있지만 RISC-V 명령어 집합의 형식 모델과 어셈블리를 다른 프로세서용 코드로 바꾸는 도구가 새로운 신뢰 대상이 된다. 검증된 컴파일러를 사용하면 추출기와 C 컴파일러를 TCB에서 제외할 수 있다.

연구진은 모든 모듈에 하나의 방식을 적용할 필요는 없다고 봤다. 수학적 구조가 강한 모듈은 Lean4로 검증하고 자료구조가 복잡하거나 규모가 큰 모듈은 변환기나 검증된 컴파일러를 활용하는 혼합 방식도 가능하다고 제시했다.

이번 글은 이더리움 클라이언트 전체가 이미 형식 검증을 마쳤다는 발표가 아니다. 형식 사양과 구현, 컴파일 과정까지 이어지는 검증을 어떤 단위로 나누고 어디까지 확대할지에 대한 설계 방향을 제시한 연구다.