💻 computer science

Safety and Liveness of Cross-Domain State Preservation under Byzantine Faults: A Mechanized Proof in Isabelle/HOL

이 논문은 글로벌 금융 규제 요구사항의 포괄적인 모델에 대응하여 인스턴스화된 7개의 범용 로케일(locale)로 구성된 재사용 가능한 프레임워크를 활용하여, 비잔틴 결함(Byzantine faults) 상황 하에서의 교차 도메인 규제 상태 보존에 대한 안전성(safety) 및 활성(liveness) 보장을 확립하는 기계화된 Isabelle/HOL 증명을 제시한다.

원저자: Jinwook Kim

게시일 2026-06-01

📖 4 분 읽기☕ 가벼운 읽기

CC BY 4.0

원저자: Jinwook Kim

원본 논문은 CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/) 라이선스로 제공됩니다. ✨ 이것은 아래 논문에 대한 AI 생성 설명입니다. 저자가 작성하거나 승인한 것이 아닙니다. 기술적 정확성을 위해서는 원본 논문을 참조하세요. 전체 면책 조항 읽기

디지털 자산(토큰화된 주식이나 부동산 등)이 서로 다른 "이웃 동네"(블록체인)와 "종이 장부"(오프체인 시스템) 사이를 자유롭게 이동할 수 있는 세상을 상상해 보십시오. 문제는 다음과 같습니다. 만약 A라는 동네의 판사가 자산을 동결한다면, 이 동서 동결 조치는 B, C 동네와 종이 장부에서도 즉각적이고 완벽하게 일어나야 합니다. 만약 그렇지 않다면, 악의적인 행위자들이 규칙이 집행되지 않는 곳으로 자산을 숨기는 "규제 차익(regulatory arbitrage)"을 노릴 수 있습니다.

이 논문은 이러한 자산을 이동시키는 특정 시스템이 (일부 참여자가 방해하더라도) **안전(safe)**하며(실수를 저지르지 않음), **활성(alive)**하다는(멈추지 않음) 것에 대한 수학적 증명입니다.

다음은 쉬운 비유를 사용한 상세 설명입니다:

1. 목표: "완벽한 릴레이 경주"

이 시스템을 릴레이 경주라고 생각해 보십시오. 여기서 바톤은 "규제 상태"(예: "동결됨" 또는 "활성 상태")를 나타냅니다.

도전 과제: 한 명의 주자(블록체인)가 바톤의 색깔을 바꿀 때, 팀의 다른 모든 주자도 즉시 동일한 색깔을 보아야 합니다.
리스크: 만약 한 명의 주자가 거짓말을 하거나, 잊어버리거나, 혹은 멈춰버린다면, 전체 경주가 중단되거나 바톤이 동시에 두 가지 색깔을 띠게 될 수도 있습니다 있습니다.

2. 두 가지 큰 성과 (안전성과 활성성)

저자들은 자신들의 시스템에 대해 두 가지를 증명했습니다:

A. 안전성(Safety): "깨지지 않는 거울"

의미: 시스템이 작동한다면 결과는 항상 일관됩니다. 만약 A 체인이 "동결"이라고 말한다면, B 체인도 반드시 "동결"이라고 말해야 합니다. 모호함은 존재할 수 없습니다.
비유: 마법 거울 세트가 있다고 상상해 보십시오. 거울 A 앞에 빨간 공을 놓으면, 거울 B, C, 그리고 종이 기록 모두가 빨간 공을 보여줍니다. 그들은 결코 파란 공을 보여주지 않으며, 서로 의견이 일치하지 않는 일도 없습니다.
증명: 저자들은 이 거울링(mirroring)이 완벽하게 일어난다는 것을 증명하는 "지도"(이를 locale이라 부름)를 구축했습니다. 이는 체인들이 서로 다른 언어(기술적 어휘)를 사용하거나, 자산이 블록체인과 종이 데이터베이스 사이를 이동하는 경우에도 마찬가지입니다. 저자들은 작업 순서를 어떻게 섞더라도 최종적인 모습은 항상 동일하다는 것을 증명했습니다.

B. 활성성(Liveness): "멈춤 방지 메커리즘"

의 의미: 일부 참여자가 "비잔틴(Byzantine)"(거짓말을 하거나, 메시지를 지연시키거나, 자산 인도를 거부하는 악의적이거나 고장 난 노드라는 뜻의 전문 용어) 상태일지라도 시스템은 멈추지 않습니다.
비유: 사람들이 좁은 복도를 통해 무거운 상자를 전달하려고 하는 상황을 상해 보십시오.
- 문제: 악의적인 행위자가 상자를 움켜쥐고 놓아주지 않아 다른 모든 사람의 진행을 막을 수 있습니다.
- 해결책: 시스템에는 내장된 "타임아웃"(스프링이 달린 트랩도어 같은 것)이 있습니다. 누군가 상자를 너무 오래 잡고 있으면, 시스템이 자동으로 그 사람의 손에서 상자를 떼어내어 다음 사람에게 전달합니다.
- 증명: 저자들은 악의적인 참여자가 전체의 1/3에 달하더라도, 상자가 언젠가는 반드시 통과할 것임을 수학적으로 증명했습니다. 어떤 자산도 영원히 갇혀 있지 않을 것입니다.

3. "마법의 기술": 두 가지의 결합

보통 안전성 증명은 모든 사람이 정직하다고 가정하고, 활성성 증명은 일부 사람들이 나쁘다고 가정합니다.

논문의 기술: 그들은 이 둘을 결합했습니다. "안전성"을 위해 필요한 "정직한 사람들"이라는 가정을 "활성성(Anti-Stuck Mechanism)"이 해결할 만큼 강력하다는 것을 보여준 것입니다.
결과: 당신은 아무도 신뢰할 필요가 없습니다. 악의적인 행위자가 있더라도, 시스템은 일관성을 유지하면서도 계속 움직일 것이라는 점이 보장됩니다.

4. 도구 상자: 수학을 위한 "레고 블록"

저자들은 단순히 이 시스템만을 위해 증명한 것이 아닙니다. 그들은 7개의 재사용 가능한 "레고 블록"(Isabelle/HOL에서의 locale)을 만들었습니다.

작동 방식: 이 블록들은 범용적입니다. 이 블록들을 어떤 시스템(은행, 공급망, 게임 등)에도 끼워 맞출 수 있으며, 즉시 동일한 안전성과 활성 보장을 얻을 수 있습니다.
실제 테스트: 그들은 블록을 상자에 넣어두기만 하지 않았습니다. 그들은 이 블록들을 세 가지 매우 다른 실제 시나리오에 적용하여 제대로 작동함을 증명했습니다:
1. 서로 다른 언어: "동결"만 말하는 체인 vs "동결"과 "해제"를 모두 말하는 체인.
2. 서로 다른 세계: 블록체인 vs 복잡한 오프체인 법적 문서(DAML).
3. 합의 엔진: 다음 순서를 결정하기 위해 사용되는 구체적인 투표 메커니즘.

5. 이것이 "아닌" 것들

논문의 한계를 명확히 하기 위해 다음을 밝힙니다:

이 논문은 특정 판사가 실제로 자산을 동결할 법적 권한이 있는지 여부를 검사하는 것이 아닙니다. 단지 만약 동결 명령이 내려진다면, 그것이 모든 곳에서 올바르게 발생하는지를 검사합니다.
이 논문은 특정 컴퓨터 코드(Rust/Solidity)에 버그가 없음을 증명하는 것이 아니라, 시스템의 수학적 모델이 건전함을 증证明하는 것입니다.
이 논문은 실행 중에 새로운 체인이 끊임없이 추가되거나 제거되는 네트워크의 혼돈 상황을 다루지는 않습니다(이는 향후 연구 과제입니다).

요약

이 논문은 신뢰에 대한 수학적 인증서입니다. 이 논문은 다음과 같이 말합니다: "우리는 규제 규칙(예: 자산 동결)이 서로 다른 세계에서 걸쳐 완벽하게 집행되는 시스템을 구축했습니다. 일부 참여자가 이를 방해하려 하더라도, 시스템은 규칙이 준수되고 시스템이 멈추지 않도록 보장하는 자기 교정 메커니즘을 갖추고 있습니다."

저자들은 단계별로 논리적 허점이 없는지 컴퓨터가 검증할 수 있도록 Isabelle/HOL이라는 증명 보조 도구를 사용하여 3,215줄의 코드를 작성함으로써 이를 수행했습니다.

기술 요약: 비잔틴 결함 하에서의 교차 도메인 상태 보존에 대한 안전성 및 활성성

1. 문제 정의

본 논문은 이종 블록체인 네트워크와 오프체인 원장 간에서 운영되는 토큰화된 자산의 규제 준수 상태(regulatory compliance states)에 대한 일관성을 보장하는 핵심 과제를 다룬다. 형식적 보증이 없다면 규제 차익 거래(regulatory arbitrage)가 구조적으로 가능해진다. 예를 들어, 한 관할 구역에서 발행된 동결 명령은 연결된 모든 도메인에 즉각적이고 결정론적으로 반영되어야 한다.

문제는 두 가지 차원으로 분해된다:

안전성(Safety): 동기화가 수행될 경우, 결과 상태가 구조적 보존을 유지하며 모든 도와 일관성을 갖는지 보장한다.
활성성(Liveness): 비잔틴 노드(악의적 행위자)를 포함하는 탈중앙화 환경에서, 동기화 프로세스가 데드락(deadlock)이나 기아(starvation) 현상 없이 실제로 진행되는지 보장한다.

기존 연구들은 단일 프레임워크 내에서 두 속성을 동시에 형식적으로 검증하지 못했으며, Isabelle/HOL을 사용하여 규제 특유의 합의 속성(예: 우선순위 결정론 및 자산 데드락 자유)을 검증한 사례도 없다.

2. 방법론

저자들은 Isabelle/HOL을 사용하는 기계화된 증명 접근법을 채택하였다. 본 개발물은 4개의 이론(theory) 파일에 걸쳐 3,215줄의 코드로 구성되며, sorry나 oops(증명되지 않은 가정) 없이 빌드된다.

2.1 시스템 및 위협 모델

시스템 모델: 시스템은 상태 머신 구조를 공유하는 유한한 도메인(체인/원장) 집합으로 구성된다. 동기화는 검증, 유효성 확인, 락 획득, 상태 업데이트, 락 해제를 포함하는 원자적 연산으로 모델링된다.
위협 모델:
- 속성 1 (안전성): 초기에는 정직한 노드와 신뢰할 수 있는 채널을 가정한다.
- 속성 2 (활성성): 정직한 노드 가정을 완화하여 최대 $f < n/3$ 개의 비잔틴 노드를 허용한다. 비잔틴 노드는 락 해제를 보류하거나 악의적으로 행동할 수 있다.
- 결합: 속성 2가 속성 1의 정직한 노드 가정을 해소함으로써, 무조건적인 보증을 도출한다.

2.2 규제 상태 전이 모델

형식 모델은 15개 글로벌 금융 당국의 31개 요구사항을 체계화한 규제 준수 프로토콜(Regulatory Compliance Protocol, RCP) 프레임워크를 기반으로 한다.

상태(States): 5가지 규제 상태 (ACTIVE, FROZEN, SEIZED, CONFISCATED, RESTRICTED).
동작(Actions): 7가지 규제 동작 (FREEZE, SEIZE, CONFISCATE, RESTRICT, UNFREEZE, UNRESTRICT, RELEASE).
제약 조건(Constraints): 모델은 특정 법적 제약 조건을 강제한다. 예를 들어, "SEIZED → FROZEN" 전이는 금지된다(압류는 동결보다 강력한 법적 제약이므로). 또한 CONFISCATED 상태는 종단적(terminal) 성격을 갖는다.

2.3 검증 인프라: 제네릭 로케일(Generic Locales)

핵심 방법론은 Isabelle/HOL에서 정의된 7개의 제네릭, 도메인 독립적 로케일에 의존한다. 이 로케일들은 재사용 가능한 검증 인프라 역할을 한다. 이 로케일 내에서 증명된 정리들은 Isabelle의 해석(interpretation) 메커니즘을 통해 해당 로케일을 인스턴스화하는 모든 구체적인 도메인에 자동으로 상속된다.

안전성 로케일 (4개):
1. state_machine: 유한 상태, 동작 및 결정론적 전이를 정의한다.
2. state_preservation: 동기화가 상태 전이와 교환(commute)된다는 자연성 조건(homomorphism)을 확립한다.
3. symmetric_state_preservation: 양방향 라운드트립 보존을 보장하기 위해 역함수를 추가한다.
4. multi_domain_preservation: 일관성을 임의의 유한한 도메인 집합( $N$ -도메인 일관성)으로 일반화하고 자산별 격리를 보장한다.
활성성 로케일 (3개):
1. priority_system: 주입적 우선순위를 통해 동작의 결정론적 선택을 보장한다.
2. deadlock_free_locking: 타임아웃 기반의 강제 해제를 통해 리소스가 무기한 잠기는 것을 방지한다.
3. fair_leader_system: 주기적인 정직한 리더 스케줄링 하에서 기아 방지를 보장한다.

3. 주요 기여

3.1 기계화된 안전성 증명 (속성 1)

본 논문은 메르클 펑터(Merkle Functor) 패턴(기존에는 단일 도메인의 단방향 데이터 무결성에 국한됨)을 교차 도메인, 양방향 및 다중 도메인 프레임워크로 확장한다.

양방향 라운드트립: 상태 전이가 도메인 간 양방향으로 충실하게 반영됨을 증명한다.
N-도메인 일관성: 한 도메인에서 동기화가 발생한 후, 연결된 모든 도메인이 동일한 결과 상태에 도달함을 증명한다.
자산별 격리: 한 자산에 대한 동기화가 다른 자산의 상태에 영향을 미치지 않음을 증명한다.
구체적 인스턴스화: 저자들은 로케일이 공허하게 만족되지 않음을 보장하기 위해 구체적인 증거(witness)를 제공한다:
- 에스컬레이션 인스턴스: 한 체인은 에스컬레이션 동작(FREEZE, SEIZE 등)만 지원하고 다른 체인은 전체 세트를 지원하는 이종 동작 인스턴스로, 서로 다른 어휘(vocabulary) 간의 구조적 보존을 증명한다.
- 레이어 교차 인스턴스: 온체인의 reg_state 열거형과 오프체인 DAML 권한 레코드 간의 양방향 브릿지로, 단사성(injectivity)과 정보 손실 없음을 증명한다.

3.2 기계화된 활성성 증명 (속성 2)

이는 블록체인 맥락에서 BFT 합의의 활성을 검증하기 위해 Isabelle/HOL만을 사용한 첫 번째 사례이다.

결정론: 충돌하는 규제 동작은 우선순위 키(권한 수준, 타임스탬프, 심각도, 노드 ID)의 총 순서(total order)를 통해 해결된다.
데드락 자유: 비잔틴 노드가 락 해제를 보류하더라도, 타임아웃 메커니즘이 제한된 시간 내에 락을 만료시킴을 증명한다.
기아 방지: 공정성 경계(정직한 리더가 $k$ 에포크 내에 존재함을 보장) 하에서, 모든 대기 중인 요청이 결국 처리됨을 증명한다.

3.3 가정 해소 (결합된 보증)

본 논문은 가정-보증 추론(assume-guarantee reasoning) 패턴을 보여준다. 속성 2는 속성 1에 필요한 "정직한 노드" 가정을 해소한다. 비잔틴 결함( $f < n/3$ )이 있는 상황에서도 시스템이 활성 및 결정론적 상태를 유지함을 증명함으로써, 조건부 안전성 보증을 무조건적 보증으로 승격시킨다.

4. 결과 및 산출물

증명 산출물: 개발물에는 (7개의 제네릭 로케일을 모두 포함하는) 8개의 구체적인 로케일 해석과 파라미터화된 다중 도메인 인스턴스가 포함되어 있다.
규제 모델: 모델은 5개 상태와 7개 동작에 매핑된 31개 규제 요구사항을 다룬다.
가용성: 모든 산출물은 GitHub에 공개되어 있으며, 검토를 위해 AFP(Archive of Formal Proofs)에 제출되었다.
설계 가이드: 증명은 구현을 위한 구체적인 파라미터 제약 조건(예: $n \ge 3f + 1$ , 양수 타임아웃, 공정성 경계)을 도출하며, 이는 탈중앙화 시퀀서의 수학적 설계 근거로 직접 변환된다.

5. 의의 및 주장

본 논문은 세 가지 주요 영역에서 의의를 갖는다:

형식 검증의 참신함: 교차 도메인 규제 상태 전이를 위해 안전성과 활성을 동시에 형식적으로 검증한 최초의 연구이다. 또한 규제 특유의 합의 속성(우선순위 결정론, 규제 자산 데드락 자유)을 도구로 검증한 최초의 사례이다.
방법론적 발전: 제네릭 로케일 계층 구조를 활용함으로써, 도메인에 독립적인 재사용 가능한 검증 인프라를 제공한다. 이를 통해 동일한 안전성 및 활성 증명을 로케일 인스턴스화를 통해 DeFi, 분산 데이터베이스 등 임의의 도메인에 적용할 수 있다.
이론과 실제의 가교: 추상적인 합의 검증(합의/유효성 등)을 넘어 도메인 특화된 규제 제약을 다룬다. 이론적인 상태 머신과 규제 준수 모델 사이의 간극을 명확히 메우며, 증명에서 직접 도출된 구현 파라미터를 통해 "설계 가이드"를 제공한다.

저자들은 다음과 같은 한계점을 명시한다: 모델은 체인 특유의 특성(가스, 블록 시간)을 검증하지 않으며, Rust/Solidity 코드로의 형식적 정제(refinement)를 증명하지 않고, 폐쇄형 시스템을 가정한다(동적 요청 도착은 향후 과제임). 현재 프레임워크는 기초적인 로케일과 인스턴스를 구축하였으나, 완전한 "펑터(functor)" 상태를 달성하기 위한 범주론적 펑터 법칙(항등 및 합성)의 형식화는 향후 과제로 남겨두었다.