기술 요약: Tofu 를 활용한 자동화된 채널 결함 분석

문제 제기

분산 프로토콜은 현대 인터넷 서비스의 핵심을 이루지만, 그 통신 채널은 본질적으로 불완전합니다. 메시지는 혼잡으로 인해 손실되거나, 적대자에 의해 재전송되거나, 다중 경로 라우팅을 통해 순서가 바뀔 수 있습니다. 이러한 채널 수준의 결함은 미묘한 버그, 서비스 거부 취약점, 안전성 위반의 주요 원인입니다.

이러한 결함을 분석하는 현재의 접근 방식은 다음과 같은 중대한 이분법에 시달립니다:

1. 실용적 테스트 도구: Scapy, Linux netem, PacketDrill 과 같은 도구는 수동 결함 주입과 퍼징을 허용합니다. 그러나 이들은 완전성 보장을 제공하지 못합니다. 버그를 찾지 못했다고 해서 그 부재를 증명하는 것은 아닙니다.
2. 형식적 검증: 기존 형식 방법 (예: Tamarin, ProVerif, Spin, TLA+) 은 종종 공격자 능력을 수동으로 정의하거나 채널 수준의 결함보다는 암호학적 속성에 초점을 맞춥니다. 일부 프레임워크가 자동화된 공격 합성을 위해 존재하지만, 이들은 종종 특정 메시지 유형을 대상으로 하거나 채널 결함에 대한 임의적 (ad-hoc) 모델링을 요구하며, 임의의 선형 시간 논리 (LTL) 명세에 대한 체계적이고 일반화 가능한 접근 방식이 부족합니다.

문헌에는 임의의 분산 프로토콜 명세에 걸쳐 (손실, 재전송, 순서 변경) 채널 결함에 대한 정연하고 완전한 자동화된 분석을 제공하는 방법론의 공백이 존재합니다.

방법론

저자들은 결함이 있는 통신 채널을 악용하여 LTL 프로토콜 명세를 위반하는 공격 궤적을 자동으로 합성하는 엄격한 방법론을 제안합니다. 이는 다음과 같은 핵심 구성 요소를 구현한 Tofu라는 도구를 통해 실현됩니다:

1. 형식적 기초

이 방법론은 **선형 시간 논리 (LTL)**와 뷔히 자동자 (Büchi Automata) 사이의 동등성에 의존합니다.

• 프로세스: 분산 프로토콜은 버퍼링된 채널을 통해 상호작용하는 통신 프로세스 (레이블된 전이 시스템) 로 모델링됩니다.
• 공격 합성: 이 문제는 프로토콜 $P$와 공격자 $A$의 합성이 속성 $\phi$를 위반하는 (즉, $(P \parallel A) \not\models \phi$) "공격자 프로세스" $A$를 찾는 것으로 공식화됩니다.
• 복잡도: 이 문제는 뷔히 자동자 언어 포함 문제로 축소되어 PSPACE에 속합니다.

2. 채널 결함 가젯

Tofu 는 사용자가 지정한 결함 한도 $\ell$을 가진 피해자 채널 $c$에 대해 세 가지 구별된 공격자 능력을 모델링하는 특정 "가젯" (프로세스) 을 합성합니다:

• 손실 가젯 ($D_\ell$): 채널에서 최대 $\ell$개의 메시지를 조용히 소비합니다. 메시지를 손실할지, 전달할지, 아니면 종료할지 결정하기 위해 비결정적 선택을 사용하여 수신자를 기아 상태로 만들어 생명성을 trivial 하게 위반하지 않도록 합니다.
• 재전송 가젯 ($R_\ell$): 비파괴적 읽기를 통해 메시지를 관찰하고 로컬 버퍼에 저장한 후 비결정적으로 재전송합니다. 버퍼에서 메시지를 제거하거나 제거하지 않고 재전송하는 것을 지원하며, 메시지를 폐기할 수도 있습니다.
• 순서 변경 가젯 ($O_\ell$): 파괴적 읽기를 통해 메시지를 가로채 버퍼에 저장한 후 다른 순서로 재전송합니다. 올바른 가로채기 의미론을 보장하기 위해 이 가젯은 합성 시스템에서 가장 높은 우선순위를 부여받습니다.

이러한 가젯들은 일반화 가능하도록 설계되었습니다: 특정 메시지 유형에 무관하며 임의의 프로토콜 모델과 결합될 수 있습니다.

3. 구현 (Tofu 도구)

Tofu 는 Promela 언어를 사용하여 Spin 모델 체커 위에 구현되었습니다.

• 작업 흐름: 사용자는 프로토콜의 Promela 모델을 제공하고, 피해자 채널을 선택하며, 공격자 모델 (손실, 재전송, 순서 변경) 을 선택하고 LTL 속성을 지정합니다.
• 주입: Tofu 는 모델을 구문 분석하고 채널을 식별한 후 해당 가젯 코드를 합성하여 모델에 주입합니다.
• 검증: 수정된 모델은 Spin 에 전달됩니다. Spin 은 철저한 상태 공간 탐색을 수행합니다. 공격이 존재하면 반례 궤적을 반환하고, 그렇지 않으면 공격 부재를 인증합니다.

주요 기여

본 논문은 다음과 같은 기여를 제시합니다:

1. 일반화 가능한 가젯: 분산 프로토콜의 임의의 통신 채널에 적용 가능한 손실, 재전송, 순서 변경 가젯에 대한 형식적 정의 및 구성.
2. Tofu 도구: 분산 통신 프로토콜에 대한 공격을 합성하는 일반화 가능한 도구로, 위에서 언급한 세 가지 공격자 모델을 지원합니다. Tofu 는 정연합니다 (거짓 양성 없음) 그리고 완전합니다 (결함 한도 내에서 공격이 존재하면 이를 발견함).
3. TCP 에 대한 사례 연구: 그 유용성을 입증하기 위해 전송 제어 프로토콜 (TCP) 의 형식 모델에 Tofu 를 적용한 사례.

결과: TCP 사례 연구

저자들은 연결 설정 및 해지에 초점을 맞춘 TCP 의 Promela 모델을 구축했으며, 채널 결함의 영향을 격리하기 위해 의도적으로 재전송 시간 초과, 시퀀스 번호와 같은 구현 수준의 복원력 기능을 생략했습니다. 그들은 손실, 재전송, 순서 변경 공격 하에서 6 가지 LTL 속성 (안전성 및 생명성 포함) 을 검증했습니다.

결과:

• 손실 및 재전송 공격: Tofu 는 6 개 중 5 개의 속성을 위반하는 공격을 성공적으로 발견했습니다.
  • 예시: FIN 메시지를 손실하면 한 엔드포인트는 타임아웃되어 종료하는 반면 다른 엔드포인트는 Established 상태에 머무르게 되어 "반개방 연결 없음" 안전 속성을 위반했습니다.
  • 예시: 구식 SYN 을 재전송하면 수신기가 불필요한 핸드셰이크 상태로 진입하게 되었습니다.
  • 생명성: 공격자가 중요한 제어 메시지를 소비하거나 홍수 공격하여 진행을 막고 수용 사이클을 생성했습니다.
• 순서 변경 공격: 순서 변경 공격자는 어떤 속성도 위반하지 못했습니다. TCP 상태 기계는 순서가 바뀐 패킷을 단순히 건너뛰어 오류 상태가 아닌 타임아웃 및 종료로 이어졌습니다.
• 결론: 이 분석은 재전송 및 시퀀스 확인과 같은 복원력 메커니즘 없이는 기본 수준의 TCP 상태 기계가 채널 결함을 처리하기에 불충분함을 기계적으로 확인했습니다.

중요성 및 주장

이 논문은 채널 결함에 대한 추론을 위한 체계적이고 자동화된 지원을 제공함으로써 형식적 검증 환경의 특정 공백을 메운다고 주장합니다.

• 완전성: 테스트 도구와 달리 Tofu 는 완전성 보장을 제공합니다: 도구가 버그를 찾지 않고 종료하면, 지정된 결함 한도에 대해 그러한 버그의 부재가 증명됩니다.
• 자동화: 공격자 능력에 대한 임의적, 수동적 모델링의 필요성을 제거하여 사용자가 단순히 채널과 결함 유형을 선택할 수 있게 합니다.
• 정연성: 이 도구는 LTL 과 뷔히 자동자 사이의 엄격한 동등성에 의존하므로, 발견된 모든 반례는 진정한 공격 궤적입니다.

저자들은 Tofu 를 기존 구현 수준 테스트 도구의 보완재로 위치시킵니다: Scapy 와 같은 도구는 실제 공격 확인에 귀중하지만, Tofu 는 형식 모델에 대한 포괄성의 이론적 보장을 제공합니다. 코드와 모델은 오픈 소스로 공개되었습니다.