소개: Gasper 합의 메커니즘의 최종성에 대한 공식 검증

以太坊爱好者

特邀专栏作者

2020-07-21 05:46

이 기사는 약 4672자로, 전체를 읽는 데 약 7분이 소요됩니다

Gasper를 공식화하고 핵심 세 가지 속성을 증명합니다.

AI 요약

펼치기

Gasper를 공식화하고 핵심 세 가지 속성을 증명합니다.

편집자 주: 이 기사의 출처는이더리움 애호가(ID: ethfans)편집자 주: 이 기사의 출처는

이더리움 애호가(ID: ethfans)

Gasper는 비콘 체인 프로토콜(다가올 이더리움 2.0 네트워크의 기본 프로토콜)에 의해 구현되는 추상 지분 증명 프로토콜 계층입니다. Gasper의 핵심 부분은 트랜잭션의 내구성을 보장하고 시스템의 중단 없는 작동이 공격에 의해 손상되지 않도록 하는 일련의 완결성 메커니즘입니다.

Gasper

Runtime Verification과 Ethereum Foundation 간의 장기적인 협력에서 또 다른 이정표를 발표하게 되어 기쁩니다: 우리는 비콘 체인 프로토콜을 시뮬레이션하고 검증하기 위한 공식 프레임워크를 개발했으며 Gasper 최종성 정확성을 공식적으로 성공적으로 증명했습니다. 비콘 체인의 Gasper 추상화 구현도 이러한 속성을 가지고 있음을 입증합니다. 모델과 증명 스크립트는 모두 여기에서 찾을 수 있습니다.

첫 번째 레벨 제목

비콘 체인 프로토콜은 이더리움의 향후 주요 업그레이드인 "이더리움 2.0"의 핵심인 새로운 지분 증명 프로토콜 세트입니다. 비콘 체인 프로토콜에서 참여 노드(또는 "검증자")는 모두 시스템에 예금(ETH 형태의 지분)을 가지고 있습니다. 유효성 검사기는 블록의 유효성을 확인하고 네트워크에 "증명"을 제출하여 다양한 속성에 투표합니다. 비콘 체인 프로토콜 자체에는 검증자가 블록체인의 최신 상태에 대한 합의에 도달하는 데 도움이 되는 여러 도구가 포함되어 있습니다.

개스퍼는 비콘 체인 프로토콜의 파이널리티 가젯에 대한 추상적이지만 정확한 설명을 제안하고 포크 선택 규칙도 정의합니다. 체인이 포크될 때 메인 체인. Gasper의 Finality는 "Casper Friendly Finality Gadget(Casper FFG)" 문서에서 시작된 개념을 일반화하여 "종료"에 보다 일반적인 형식을 부여합니다.

보조 제목

정당화 및 확정

완결성의 개념은 "체크포인트 블록"(에포크 시작 부분의 블록인 "에포크 경계 블록"이라고도 함)에만 관련됩니다. 증명 메시지의 일부를 "합리화 투표"라고 합니다. 합리화 투표에서 검증자는 원본 체크포인트 블록을 이후의 대상 체크포인트 블록과 연결하여 증명을 시작한 검증자가 "우리는 소스 체크포인트를 대상 체크포인트의 상태로". 결과적으로 정당성 투표는 (1) 투표를 시작한 유효성 검사기, (2) 소스 체크포인트 및 정당성 높이, (3) 목표 체크포인트 및 정당성 높이를 보여줍니다.

조건이 충족되는 경우에만: (1) 소스 체크포인트 B0이 합리화되었습니다. 대상 체크포인트 B1 소스 체크포인트 B0을 통해 합리화됩니다.

B0은 순서-K 최종성(k > 0)을 달성하고 B0과 Bk 사이의 모든 체크포인트는 대부분의 유효성 검사기가 B0을 K 세대 자손 체크포인트 Bk와 연결하는 경우에만 완료됩니다. 제네시스 블록 자체는 합리화되고 최종적인 것으로 간주됩니다. 아래 다이어그램은 Gasper의 합리화 및 종료 개념을 보여줍니다.
검증자가 프로토콜에서 벗어나서 모순된 투표를 제출하려고 하면 검증자는 불이익을 받습니다. 예치금의 상당 부분이 차감됩니다. 개스퍼는 모순된 투표를 구성하는 요소를 정의하기 위해 두 가지 조건(슬래싱 조건이라고도 함)을 정의합니다.

주변 투표(Surround-voting): 검증자가 발행한 투표와 관련된 두 체크포인트는 검증자가 발행한 다른 투표의 두 체크포인트 높이 범위 내에 정확히 있습니다.

텍스트

이중 투표를 시작한 검증인은 첫 번째 슬래시 조건을 위반한 것으로 간주되며 랩 투표를 시작한 검증인은 두 번째 슬래시 조건을 위반한 것으로 간주됩니다. 두 경우 모두 규칙을 어긴 검증인은 많은 양의 예치금을 차감하게 됩니다.

보조 제목
정확성(정확성 속성)

다른 BFT(Byzantine Fault Tolerance) 프로토콜과 마찬가지로 Gasper 프로토콜의 핵심 기본 가정은 대다수의 검증자(예치 금액으로 정의되는 2/3 이상)가 정직하고 프로토콜의 요구 사항을 따를 것이라는 것입니다. 이 가정 하에서 Gasper에는 두 가지 기본 속성이 있습니다.

책임 있는 안전: 최소 1/3의 유효성 검사기(입금액 기준)가 삭감되지 않는 한 서로 다른 포크에 속하는 두 개의 블록이 완료되지 않습니다.

Plausible Liveness: 과거에 블록체인에 어떤 일이 발생했든 블록의 최종화 프로세스는 절대 교착 상태에 빠지지 않습니다.

또한 검증자 집합이 동적으로 변경되는 환경(검증자가 네트워크를 떠나고 새로운 검증자가 합류함에 따라 활성 검증자 집합이 변경될 수 있음)에서 세 번째 속성은 누군가가 프로토콜의 규칙을 위반할 때 정량화합니다. 압수할 수 있는 것:

Slashable bound: 유효성 검사기 활성화 및 종료 매개변수 조건을 제어하기 위해 추가 프로토콜 조건을 사용할 수 있는 한, (보안을 깨뜨릴 때) 삭감할 수 있는 예치금의 하한선이 있음을 증명할 수 있습니다.

동적 유효성 검사기 집합(비콘 체인 프로토콜이 구현하는 것)은 또 다른 어려운 문제를 야기합니다. 시스템은 더 이상 악의적인 유효성 검사기를 안정적으로 처벌할 수 없습니다. 악의적인 유효성 검사기가 나쁜 일을 한 후 예치되기 전에 그렇게 할 수 있기 때문입니다. 실제로 슬래시됩니다. 네트워크를 떠나십시오. 삭감 가능한 하한 속성을 통해 활성 유효성 검사기 집합의 변수 범위를 조정하고 최소 수준의 책임을 유지할 수 있습니다.

Gasper의 최종성 확인

Gasper는 정확성을 공식적으로 증명하는 데 사용할 수 있는 완결성에 대한 수학적이고 정확한 설명을 제공하는 것을 목표로 합니다. Ethereum 플랫폼은 대규모 금융 거래 시스템의 주가로 점점 더 많이 사용되고 있으며 전례 없는 보안 보장의 중요성을 강조합니다.

Ethereum Foundation과 협력하여 Coq 증명 도우미를 사용하여 동적 유효성 검사기 집합의 일반적인 조건에서 Gasper의 최종성 메커니즘을 공식화했습니다. 우리는 이 조건에서 Gasper의 세 가지 주요 속성인 책임 있는 안전, 우도 활성 및 슬래시 가능한 하한을 모두 지적하고 증명합니다. 모든 증명은 동일한 Coq 모델을 사용합니다.
여기에서는 이 성과에 대해 간략히 설명합니다. 자세한 내용은 다음에서 확인할 수 있습니다.

프로젝트에 대한 기술 보고서

프로젝트의 Github 저장소

보조 제목

모델링 및 검증 방법

첫 번째 단계는 공식적으로 진술하고 증명하고자 하는 모든 주요 속성을 표현할 수 있는 프로토콜 모델을 개발하는 것입니다. 이 모델은 Casper FFG의 안전성과 활성을 검증하는 이전 작업을 기반으로 합니다(이전 모델은 Gasper finality 메커니즘의 초기 버전을 정의했습니다).

이 모델에는 세 가지 주요 구조 모듈이 있습니다.

\sum은 합계 연산자이며 stake.[st_fun v]는 검증자 v에 해당하는 지분의 양을 제공합니다(st_fun은 모든 검증자가 시스템에 지분을 가지고 있어야 한다고 가정합니다).

또한 유효성 검사기의 동적 집합을 시뮬레이션하기를 원하기 때문에 활성 유효성 검사기 집합이 블록에서 블록으로 변경될 수 있으므로 추상(제한된) 매핑 vsset: {fmap Hash -> {set Validator}}를 선언합니다. 블록에서 활성 유효성 검사기 집합이 주어집니다. 이제 vset 및 wt 를 사용하여 압도적 다수 집합이 무엇인지 정의할 수 있습니다.

특정 블록에서 활성 검증자 집합의 하위 집합 가중치가 전체 집합 가중치의 2/3를 초과하면 하위 집합이 절대 다수 집합입니다.

블록 트리. 유한 유형의 블록 해시를 사용하여 블록 Hash:finType을 시뮬레이션하고 제네시스를 사용하여 제네시스 블록을 나타냅니다. 우리는 체크포인트 블록 트리를 시뮬레이트하기 위해 블록 부모-자식 관계(h1은 h2의 부모임)를 나타내기 위해 표기법 h1 <~ h2를 사용합니다.

다음으로 h1 <~* h2를 사용하여 조상 관계를 정의하고, h1은 h2의 조상이고, h2는 h1의 자손입니다(h1과 h2는 같은 블록일 수 있음). 예를 들어 조상관계의 속성을 보면 조상의 조상도 조상이며 이는 부자관계의 속성과 유사하다.

텍스트

보조 제목

이러한 정의와 해당 속성을 기반으로 페널티 조건, 쿼럼 교차 속성, 합리화 및 종료를 포함하여 모델의 다른 모든 구조와 속성을 정의합니다. 예를 들어 프로토콜 위반 시 커뮤니티를 몰수하는 속성은 다음과 같은 추상 멤버십 제약 조건을 사용하여 정의할 수 있습니다.

이 명제는 그룹을 삭감한다는 것은 일부 블록 bL과 bR에 두 개의 절대다수 그룹 vL과 vR이 있음을 의미하며, 이 두 그룹의 교차점은 슬래시 검증자(이중 투표 또는 주변 투표 개시)의 완전한 집합체임을 나타냅니다. 활성 유효성 검사기 집합이 항상 고정되어 있는 특수 조건 하에서 이러한 절대다수 집합의 교차 가중치는 모든 예치금의 1/3 이상입니다.

또 다른 예는 종료 포크(즉, 보안 위반)의 정의입니다.

이 명제는 두 개의 모순된 블록 b1과 b2가 둘 다 완료되었음을 나타냅니다(b1과 b2 모두 다른 블록의 조상 블록이 아니기 때문입니다). 이 두 블록은 임의의 합리화 높이에서 임의로 긴 체인으로 마무리될 수 있습니다.

이러한 정의 및 결과 세트는 책임 보안, 우도 활동 및 슬래시 가능한 하한의 세 가지 정리를 지적하고 증명하는 데 사용됩니다. 명확성을 위해 책임 보안 정리의 공식을 다음과 같이 재정의합니다.

정의는 간단하며 다음과 같이 말합니다. 보안이 깨지면(완성된 포크로) 일부 유효성 검사기 세트가 슬래시됨을 의미해야 합니다. 이 증명은 Gasper가 제공한 비공식적 주장을 기계화하고 분기가 완료된다는 것은 삭감 조건 중 하나를 위반하는 두 개의 압도적 다수 그룹이 있어야 교차가 삭감될 수 있음을 의미하는 이유를 보여줍니다.