이더리움 연구

[이더리움 연구] ePBS 형식 보안 분석 — EIP-7732 이더리움 연구팀이 ePBS(EIP-7732)의 보안 속성을 스펙 코드 수준에서 형식적으로 추적하는 분석 문서를 공개했습니다. 핵심은 P1 P5, 5개의 외부 관측 가능한 속성을 정의하고, 각 속성이 어떤 가정 하에 스펙 코드 어느 줄에서 강제되는지를 명시적으로 추적하는 것입니다. 아직 증명되지 않은 가정은 열거해두고, 동반 형식 증명 작업을 통해 라인 단위로 완성할 예정입니다. 주목할 부분은 속성이 성립하기 위해 필요한 강화 전제조건과 그 한계를 명확히 드러낸다는 점입니다. 예컨대 "빌더가 페이로드를 숨겨도 결제를 피할 수 없다(P5)"가 성립하려면 부모 블록이 직전 슬롯에 있어야 하고, 이 조건이 깨지는 구체적인 공격 시나리오(비잔틴 제안자 쌍이 슬롯을 비워 리오그를 유도하는 경우 등)까지 열거합니다. 직관적으로 그럴 듯한 보안 주장이 실제로 어떤 조건에서만 성립하는지를 코드와 함께 추적하는 작업입니다. 현재 초안(WIP) 상태이며 확정된 스펙이 아닙니다. 그럼에도 이 작업은 이더리움 프로토콜 변경이 복잡해지는 상황에서, 설계의 직관과 실제 코드 사이의 간극을 메우는 형식 검증 방법론을 연구팀이 어떻게 구축하는지를 보여줍니다. https://github.com/ethereum/epbs-security-analysis