Maude-HCS: Model Checking the Undetectability-Performance Tradeoffs of Hidden Communication Systems

1. 문제 정의 (Problem)

• 배경: 은폐 통신 시스템 (HCS) 은 일반 네트워크 활동 속에 은밀한 메시지를 숨겨 통신의 존재 자체를 감추는 기술입니다. 이는 인터넷 자유와 국가 안보 (예: 검열 우회, 작전 수행) 에 필수적이지만, 탐지될 경우 치명적인 위험을 초래할 수 있습니다.
• 현황의 한계: 기존 HCS 의 탐지 불가능성은 주로 임의의 트래픽 통계나 특정 탐지기를 사용한 실험적 (Ad hoc) 평가에 의존합니다. 이는 실험 설정과 암묵적인 적대적 가정에 밀접하게 묶여 있어, 설계 공간의 체계적인 탐색, 설계의 진화, 또는 다른 설계 간의 비교가 어렵습니다.
• 필요성: HCS 설계의 성능과 탐지 불가능성을 검증하기 위해, 실험실 테스트베드나 시뮬레이션에 의존하지 않고 형식적 (Formal) 으로 모델링하고 추론할 수 있는 확장 가능한 프레임워크가 부재했습니다.

2. 방법론 (Methodology)

Maude-HCS 는 재작성 논리 (Rewriting Logic) 기반의 형식 도구인 Maude 와 **통계적 모델 체킹 (Statistical Model Checking, SMC)**을 결합하여 다음과 같은 워크플로우를 제공합니다.

A. 형식적 정의: 탐지 불가능성 (Formalizing Undetectability)

• 관측 가능한 실행 궤적 (Observable Execution Traces): HCS 가 적용된 상태와 일반 시스템 (HCS 가 없는 상태) 의 실행 궤적 분포를 정의합니다.
• 수학적 정의: 탐지 불가능성을 두 분포 간의 **통계적 구별 불가능성 (Statistical Indistinguishability)**으로 정의합니다. 이는 두 분포 간의 거리 측정치 (예: KL 발산, Kullback-Leibler Divergence) 에 상한 (Bound) 을 두는 것으로 표현됩니다.
  • $M(View_{HCS}, View_{Ord}) \le d$
  • 여기서 $M$은 발산 측정치, $d$는 허용 가능한 상한값입니다.

B. 분석 도구: Maude-HCS 프레임워크

1. 모델링:
   • 일반 네트워크 시스템 ($N$) 을 Maude 의 '일반화된 액터 (Generalized Actor)' 재작성 이론으로 모델링합니다.
   • Weird Network 변환: HCS 패턴 (예: 터널링, 위장) 을 적용하여 일반 시스템을 은폐 통신 시스템 ($W(N, p)$) 으로 변환합니다. 이 과정에서 원본 시스템의 행동을 변경하지 않고 은폐 기능을 감싸는 (wrapping) 방식으로 모듈성을 유지합니다.
   • 확률적 변환: 결정론적/비결정론적 모델을 확률적 재작성 이론으로 변환하여 메시지 지연, 패킷 손실, 배경 트래픽 등을 확률 분포로 모델링합니다.
2. 통계적 모델 체킹 (SMC):
   • QMaude 도구를 사용하여 몬테카를로 (Monte Carlo) 시뮬레이션을 수행합니다.
   • 적대자 모델: 패시브 (수동) 적대자가 관측하는 트래픽 통계 (패킷 크기, 타이밍 등) 를 기반으로 탐지기 (Detector) 를 정의합니다.
   • 정량적 속성: QuaTeX 논리를 사용하여 탐지기의 **진양성률 (TPR)**과 **거짓양성률 (FPR)**을 추정합니다.
3. 감사 (Auditing) 프로세스:
   • 추정된 TPR 과 FPR 을 사용하여 KL 발산의 **하한 (Lower Bound)**을 계산합니다.
   • 데이터 처리 부등식 (Data Processing Inequality) 을 활용하여, 특정 탐지기에 대한 발산 하한을 도출함으로써 "이 시스템은 $d$만큼의 탐지 불가능성을 가진다"는 주장이 타당한지 검증합니다.

3. 주요 기여 (Key Contributions)

1. 관측 궤적 분포 기반의 탐지 불가능성 형식화: HCS 의 탐지 불가능성을 단순한 경험적 지표가 아닌, 일반 시스템과 HCS 시스템 간의 관측 궤적 분포 간의 정량적 거리 (KL 발산 등) 로 엄밀하게 정의했습니다.
2. 시맨틱 정렬된 모듈식 모델링 및 확장 가능한 분석: Liu 등 [33] 의 모듈식 접근법을 확장하여, 시간 (Time) 과 확률 (Probability) 을 포함하는 HCS 모델을 자동으로 확률적 버전으로 변환하는 도구를 제공합니다. 이를 통해 설계자는 은폐 메커니즘의 새로운 측면에만 집중할 수 있으며, 전체 모델의 시맨틱 일관성을 보장받습니다.
3. 탐지 불가능성 주장 감사 방법론: 구체적인 HCS 설계에 대해 SMC 를 통해 KL 발산 하한을 추정하고, 이를 통해 설계자가 주장하는 탐지 불가능성 파라미터가 특정 가정 하에서 유효한지 검증하는 방법론을 제시했습니다.
4. 파라미터화된 배포 환경에서의 확장된 감사: 애플리케이션 속도, 네트워크 손실, 배경 트래픽, 탐지기 임계값 등 다양한 파라미터를 변경하며 대규모 설계 공간을 체계적으로 탐색하고, 성능과 탐지 불가능성의 트레이드오프를 정량화했습니다.

4. 실험 결과 (Results)

저자들은 DNS 터널링 (Iodine) 과 Mastodon 소셜 네트워크를 통한 스테가노그래피 (Destini) 를 결합한 개념 증명 (PoC) HCS 를 구현하여 Maude-HCS 를 평가했습니다.

• 실제 테스트베드와의 시맨틱 정렬 (Semantic Alignment):
  • Maude 모델 기반의 예측 (SMC 결과) 과 물리적 테스트베드에서 측정한 실제 성능 (지연 시간, Goodput) 을 비교했습니다.
  • 지연 시간과 Goodput 에 대해 모델과 실험 결과가 약 1 표준편차 이내로 매우 잘 일치함을 확인했습니다 (지연 시간 오차 최대 13.6%, Goodput 오차 최대 17.1%).
  • 이는 모델이 실제 구현의 복잡한 동작 (버그 포함) 을 충실히 반영함을 의미합니다.
• 성능 - 프라이버시 트레이드오프 분석:
  • 트래픽 주입 속도: 전송 속도를 높일수록 (대기 시간 감소) Goodput 은 증가하지만, 탐지기의 TPR 과 FPR 차이가 커져 KL 발산 하한이 증가 (탐지 가능성 증가) 하는 경향을 보였습니다.
  • 네트워크 조건: 패킷 손실률과 배경 트래픽 양에 따라 탐지 불가능성이 크게 달라짐을 확인했습니다.
  • 탐지기 임계값: 탐지기 임계값을 변경하면 KL 발산 하한이 크게 변하며, 이는 설계자가 특정 운영 환경에서 시스템이 얼마나 안전한지 정량적으로 평가할 수 있음을 보여줍니다.

5. 의의 및 결론 (Significance)

• 형식적 검증의 도입: HCS 분야에 처음으로 형식적 모델링과 SMC 기반의 정량적 분석을 도입하여, "검증되지 않은 경험적 주장"을 넘어 "수학적 하한이 보장된 설계"를 가능하게 했습니다.
• 설계 최적화 지원: 실제 구현 전에 모델 기반으로 다양한 파라미터 (지연, 손실, 트래픽 양) 를 변경하며 최적의 성능 - 보안 균형을 찾을 수 있어, 개발 비용과 시간을 절감하고 더 안전한 시스템을 설계할 수 있습니다.
• 실용성 입증: 복잡한 실제 네트워크 환경 (NAT, 다양한 배경 트래픽, 손실) 에서도 모델 예측이 실험 결과와 높은 일치도를 보임으로써, 이 프레임워크가 실제 배포 전 검증 도구로서 유효함을 입증했습니다.
• 미래 전망: 향후에는 이 모델을 기반으로 최적화된 HCS 프로토콜을 자동으로 생성 (Code Generation) 하는 방향으로 발전시켜, "Correct-by-Construction" (구현 단계에서부터 오류가 없는) 은폐 통신 시스템을 구축하는 것을 목표로 합니다.

요약하자면, Maude-HCS는 은폐 통신 시스템의 설계자가 성능과 보안 (탐지 불가능성) 사이의 균형을 정량적으로 이해하고 검증할 수 있는 강력한 형식적 도구이며, 이를 통해 실제 환경에서의 신뢰성을 높이는 데 기여합니다.