기술 요약: iSMC – 대화형 인증을 구현한 BDD 기반 심볼릭 모델 체커

1. 문제 제기

모델 체킹은 하드웨어 및 소프트웨어 시스템의 정확성을 검증하는 근본적인 기법입니다. 그러나 모델 체커 자체의 신뢰성을 보장하는 것은 중요한 과제입니다. 전통적인 인증 패러다임은 비대화형 프로토콜에 의존합니다. 즉, 증명자 (모델 체커) 가 증명서 (예: 만족하는 할당 또는 해결 증명) 를 생성하고, 검증자가 이를 독립적으로 검사합니다.

이 논문은 이 접근법에서 근본적인 이론적 한계를 지적합니다. 일반 CTL 모델 체킹을 포함한 많은 문제들에 대해, 증명서는 인스턴스 크기에 대해 최악의 경우 지수적 길이를 가질 수 있습니다. 결과적으로 검증자는 이를 확인하는 데 지수 시간이 필요하게 되어, $NP = coNP$가 아닌 한 대규모 시스템에 대한 인증 과정은 실용적이지 않게 됩니다.

저자들은 대화형 인증을 제안합니다. 이는 증명자와 검증자가 다중 라운드 프로토콜에 참여하는 대화형 증명 시스템 (IP) 에 기반한 패러다임입니다. 검증자는 적응적으로 질문을 하여, 내부 계산이 복잡하더라도 다항 시간 내에 높은 확률로 오류를 탐지할 수 있습니다. CTL 모델 체킹과 같은 PSPACE 문제에 대한 대화형 증명은 이론적으로 확립되어 있습니다 (Shamir 의 $IP=PSPACE$). 그러나 이진 결정 다이어그램 (BDD) 을 사용한 심볼릭 모델 체킹에 이를 실용화하는 것은 여전히 열린 과제로 남아 있었습니다.

2. 방법론

이 논문은 정의 요구사항이 있는 CTL 모델 체킹을 위한 대화형 인증을 구현한 최초의 자기 인증형 모델 체커인 iSMC를 제시합니다. 이 시스템은 세 가지 핵심 모듈을 기반으로 구축되었습니다.

2.1 아키텍처

• 솔버 (Solver): CTL 명세를 만족하는 도달 가능 상태 집합을 계산하는 심볼릭 BDD 기반 모델 체커입니다. 평탄화된 불 모델 (SMV 형식) 에서 작동하며 clic BDD 라이브러리를 사용합니다.
• 증명자 (Prover): 솔버와 동일한 머신에서 실행됩니다. 모델 체킹 인스턴스를 실행하고 계산 중 수행된 BDD 라이브러리 호출 및 어설션의 시퀀스로 구성된 실행 trace를 생성합니다.
• 검증자 (Verifier): 제한된 리소스를 가진 클라이언트에서 실행할 수 있는 경량 모듈입니다. 모델 체킹 알고리즘을 다시 실행하지 않습니다. 대신 증명자와 대화형 프로토콜을 통해 실행 trace 를 검증합니다.

2.2 TraceCert 프로토콜

핵심 혁신은 Couillard 등 [11] 의 QBF 인증 작업에서 적응된 대화형 증명 프로토콜인 TraceCert입니다.

1. Trace 를 회로로 변환: 실행 trace 는 **일반화된 불 회로 (GBC)**로 변환됩니다. trace 의 각 명령은 게이트가 되고, 어설션 (예: "상태 집합 $C_1$은 $C_0$과 동등하지 않다") 은 동등성 주장이 됩니다.
2. 산술화: 불 함수는 유한 체 $\mathbb{F}_p$ 위의 다변수 다항식으로 인코딩됩니다. 이를 통해 검증자는 전체 회로를 탐색하는 대신 무작위 지점에서 다항식을 평가하여 계산의 속성을 확인할 수 있습니다.
3. 차수 축소: 다항식이 다항 시간 검증을 위해 낮은 차수를 갖도록 보장하기 위해, 프로토콜은 불 입력에서 함수의 값을 변경하지 않고 지수를 1 로 줄이는 차수 축소 게이트 ($\delta_x$) 를 도입합니다.
4. 대화형 라운드: 프로토콜은 회로를 탐색하며 라운드로 진행됩니다. 증명자가 게이트의 값을 주장하면, 검증자는 해당 게이트의 입력에 대한 무작위 할당으로 증명자에게 도전을 가합니다. 증명자는 주장과 일관된 다항식을 제공해야 합니다. 증명자가 거짓말을 할 경우, Schwartz-Zippel 보조정리에 의해 잡힐 확률이 제한됩니다.

2.3 기존 작업 대비 주요 기술적 개선

저자들은 QBF 에 초점을 맞춘 [11] 의 기술을 CTL 모델 체킹의 특정 요구사항을 처리하도록 확장하여 세 가지 주요 병목 현상을 해결했습니다.

1. 효율적인 이름 변경 및 동등성: 원래 프로토콜 (CPCertify) 은 동등성 및 이름 변경 게이트를 비효율적으로 처리했습니다 ($O(n^2)$ 및 $O(n^k)$). TraceCert 는 이러한 라운드를 각각 $O(1)$ 및 $O(n)$으로 최적화했습니다.
2. 가비지 컬렉션 호환성: 표준 BDD 라이브러리는 전역 계산 캐시와 가비지 컬렉션을 사용합니다. 이전 접근법은 증명자가 모든 중간 BDD 를 저장하도록 요구하여 가비지 컬렉션을 불가능하게 했습니다. 저자들은 증명자가 과거 도전을 악의적으로 기억하기만 하지 않는 한, 증명자가 중간 결과를 폐기 (오라클 역할) 하더라도 건전성을 훼손하지 않는 프로토콜의 하향식 변형인 TraceCertRev를 도입했습니다.
3. 전역 계산 캐시: 이전 구현 (blic) 은 캐싱과 호환되지 않는 방식으로 확장된 BDD(eBDD) 를 조작하여 전역 캐시를 사용할 수 없었습니다. 저자들은 노드를 버전 관리하기 위해 링크 필드를 사용하는 새로운 불변 eBDD 표현을 도입하여 전역 고유 테이블의 사용을 가능하게 하고 성능을 크게 향상시켰습니다.

3. 주요 기여

1. iSMC 시스템: 정의 요구사항이 있는 임의의 CTL 속성을 위한 대화형 인증을 구현한 최초의 자기 인증형 모델 체커입니다.
2. TraceCert 프로토콜: 모델 체킹 trace 에서 일반적으로 발생하는 변수 이름 변경 및 동등성 어설션을 효율적으로 처리하는 새로운 대화형 증명 프로토콜로, 특정 게이트 라운드의 복잡성을 줄였습니다.
3. 최적화된 eBDD 구현: 전역 계산 캐시 및 가비지 컬렉션 사용을 가능하게 하는 새로운 알고리즘 (ApplyEBDD) 및 데이터 구조로, 이전 blic 라이브러리의 비효율성을 극복했습니다.
4. TraceCertRev: 인증 중 가비지 컬렉션을 허용하는 프로토콜 변형으로, 메모리가 제약인 대규모 모델 체킹에서 시스템의 실용성을 가능하게 합니다.

4. 실험 결과

저자들은 HWMCC'25 liveness 트랙의 53 개 벤치마크에 대해 iSMC 를 평가했습니다.

• 솔버 성능: 성숙한 도구인 NuSMV 와 비교하여 iSMC 의 솔버는 평균적으로 5.84 배 느립니다. 저자들은 이를 주로 현재 프로토타입에서 관계형 곱 (BDD 최적화) 에 대한 지원이 부족하기 때문이라고 설명하며, 이를 대화형으로 인증하는 것은 여전히 열린 문제라고 덧붙였습니다.
• 증명자 오버헤드: 증명자는 솔버의 시간 $S$에 대해 $O(S)$ 시간으로 실행됩니다. 상수 인자는 약 2.00으로, 인증 오버헤드는 해결 시간의 약 두 배입니다.
• 검증자 효율성: 검증자는 매우 효율적입니다. 증명자에 15 분 타임아웃을 적용했을 때, 검증자는 3.6 초를 초과한 적이 없었습니다 (증명자 대비 평균 33.4 배 속도 향상). 검증자의 실행 시간은 계산 시간이 아닌 실행 trace 의 길이에 선형적으로 비례합니다.
• 최적화의 영향: 개선 사항 (TraceCert, clic 라이브러리, 전역 캐시) 은 CPCertify 와 blic을 사용한 기준 구현 대비 실행 시간에서 평균 2.26 배 속도 향상과 메모리 사용량에서 16.12 배 감소를 가져왔습니다.

5. 중요성 및 주장

이 논문은 iSMC 가 모델 체킹을 위한 실용적인 대화형 인증을 향한 중요한 걸음이라고 주장합니다.

• 신뢰할 수 없는 서버에 대한 신뢰: 이 시스템은 제한된 리소스를 가진 클라이언트가 강력한 하지만 신뢰할 수 없는 서버에 모델 체킹을 위임할 수 있는 시나리오를 가능하게 합니다. 서버 (솔버 + 증명자) 는 무거운 계산을 수행하고, 클라이언트 (검증자) 는 다항 시간 내에 높은 확률로 결과를 인증합니다.
• 다항 시간 검증: 일반적인 CTL 속성에 대해 지수 시간이 필요한 비대화형 인증 방법과 달리, iSMC 의 검증자는 변수 수와 trace 길이에 대해 다항 시간으로 실행됩니다.
• 확장성: 저자들은 최적화를 통해 대화형 인증의 오버헤드가 관리 가능하고 메모리 풋프린트가 크게 감소하여 비단순한 벤치마크에 대해 이 접근법이 실현 가능함을 입증했습니다.

저자들은 iSMC 가 최초의 프로토타입임을 겸손하게 언급합니다. 솔버는 현재 관계형 곱과 같은 최적화가 부족하여 NuSMV 와 같은 최첨단 도구보다 느리고, 현재 구현은 CTL 을 대상으로 하지만, 기본 프레임워크는 이론적으로 전체 모달 $\mu$-계산으로 확장될 수 있음을 인정합니다.