비동기 비잔틴 프로토콜의 거의 확실한 종료 검증
블록체인을 포함한 많은 분산 시스템에서 합의 알고리즘은 핵심적인 역할을 수행합니다. 실용적인 합의 알고리즘은 부분 동기 모델에 기반하지만, 메시지 전달 지연이 불확실할 때 활성 상태를 유지할 수 없습니다. 비동기 프로토콜은 유한한 지연 시간에 의존하지 않고 활성 상태를 유지하지만, 여러 계층의 알고리즘으로 구성되어 이해하고 구현하기가 훨씬 어렵습니다. 또한, FLP 불가능성 정리로 인해 확률적 활성 보장만을 제공하며, 이로 인해 비동기 프로토콜의 정확성 검증은 매우 어렵습니다. 실제로 이러한 프로토콜에서 수년간 발견되지 않은 활성 버그가 존재하기도 했습니다. 본 연구는 비동기 분산 프로토콜의 확률적 안전성 및 활성 속성을 명세하고 검증하기 위한 형식 프레임워크인 SureDistrib를 소개합니다. 이 프레임워크는 공통 코인에 의존하는 이진 합의 알고리즘과 같이 다른 확률적 기능에 의존하는 확률적 알고리즘을 명세할 수 있도록 지원합니다. 우리는 이러한 시스템에 대한 정제 관계를 정의하고, 하위 기능을 구현으로 대체하여 구성된 시스템이 추상적인 하위 기능을 가진 원래 시스템을 정제함을 증명하는 구성 보조정리들을 제시합니다. 이 프레임워크를 기반으로, 비동기 비잔틴 결함 허용 이진 합의 알고리즘이 확률 1로 종료함(거의 확실한 종료)을 기계적으로 증명한 최초의 사례를 제시합니다. 이는 복잡한 비동기 프로토콜의 신뢰성을 높이는 데 중요한 진전입니다. SureDistrib는 비동기 분산 시스템의 설계 및 구현에서 발생할 수 있는 잠재적인 활성 문제를 사전에 식별하고 해결하는 데 기여하며, 향후 더욱 견고하고 신뢰할 수 있는 분산 시스템을 구축하는 데 활용될 수 있습니다.