OpenClaw 보안 모델 검증: TLA+로 취약점 즉시 확인하기

보안 로직을 짤 때마다 “정말 모든 케이스를 다 고려했을까?” 하는 불안감이 들 때가 있죠. 특히 복잡한 권한 부여나 세션 격리 로직은 코드 리뷰만으로는 놓치기 쉬운 빈틈이 생기기 마련이에요. 이런 문제를 해결하기 위해 OpenClaw는 수학적으로 보안 모델을 검증하는 방법을 사용하고 있어요.

이 페이지에서는 OpenClaw의 공식 보안 모델(현재 TLA+/TLC 기준)을 관리하고 있어요.

참고: 일부 오래된 링크는 이전 프로젝트 이름을 참조할 수 있어요.

목표 (지향점): 명시적인 가정 아래 OpenClaw가 의도한 보안 정책(권한 부여, 세션 격리, 도구 게이팅, 오설정 안전성)을 강제한다는 것을 기계적으로 검증된 논거로 제공하는 것이에요.

현재 제공하는 것: 실행 가능하고 공격자 중심인 보안 회귀 테스트 세트예요.

• 각 클레임은 유한한 상태 공간에서 실행 가능한 모델 체크를 거쳐요.
• 많은 클레임이 실제 발생 가능한 버그 클래스에 대해 카운터이그잼플(반례) 트레이스를 생성하는 **부정 모델(negative model)**과 쌍을 이뤄요.

아직 제공하지 않는 것: “OpenClaw가 모든 측면에서 안전하다”거나 전체 TypeScript 구현이 완벽하게 정확하다는 증명은 아니에요.

모델 저장소 위치

모델은 별도의 저장소에서 관리되고 있어요: vignesh07/openclaw-formal-models.

중요한 주의 사항

• 이것은 모델일 뿐이며, 전체 TypeScript 구현체가 아니에요. 모델과 코드 사이에 차이가 발생할 수 있어요.
• 결과는 TLC가 탐색한 상태 공간 범위 내로 제한돼요. “Green” 결과가 모델링된 가정과 범위를 벗어난 보안까지 보장하는 것은 아니에요.
• 일부 클레임은 명시적인 환경적 가정(예: 올바른 배포, 올바른 설정 입력)에 의존해요.

결과 재현하기

현재는 모델 저장소를 로컬에 클론하고 TLC를 실행하여 결과를 재현할 수 있어요(아래 참고). 향후에는 다음과 같은 기능을 제공할 예정이에요.

• 공개 아티팩트(반례 트레이스, 실행 로그)가 포함된 CI 실행 모델
• 작고 제한된 체크를 위한 호스팅 방식의 “모델 실행” 워크플로우

시작하기:

git clone https://github.com/vignesh07/openclaw-formal-models
cd openclaw-formal-models

# Java 11+ required (TLC runs on the JVM).
# The repo vendors a pinned `tla2tools.jar` (TLA+ tools) and provides `bin/tlc` + Make targets.

make <target>

Gateway 노출 및 오픈 Gateway 오설정

클레임: 인증 없이 루프백을 넘어 바인딩하면 원격 침해 가능성이 생기거나 노출이 증가해요. 토큰/패스워드는 인증되지 않은 공격자를 차단해요(모델 가정 기준).

• Green 실행:
  • make gateway-exposure-v2
  • make gateway-exposure-v2-protected
• Red (예상된 결과):
  • make gateway-exposure-v2-negative

모델 저장소의 docs/gateway-exposure-matrix.md 문서도 함께 확인해 보세요.

Node exec 파이프라인 (가장 위험도가 높은 기능)

클레임: exec host=node를 사용하려면 (a) Node 명령 allowlist와 선언된 명령이 필요하며, (b) 설정된 경우 실시간 승인이 필요해요. 승인은 재전송 공격을 방지하기 위해 토큰화돼요(모델 기준).

• Green 실행:
  • make nodes-pipeline
  • make approvals-token
• Red (예상된 결과):
  • make nodes-pipeline-negative
  • make approvals-token-negative

Pairing 저장소 (DM 게이팅)

클레임: Pairing 요청은 TTL 및 대기 중인 요청 제한(caps)을 준수해요.

• Green 실행:
  • make pairing
  • make pairing-cap
• Red (예상된 결과):
  • make pairing-negative
  • make pairing-cap-negative

Ingress 게이팅 (멘션 + 제어 명령 우회)

클레임: 멘션이 필요한 그룹 컨텍스트에서, 권한이 없는 “제어 명령”은 멘션 게이팅을 우회할 수 없어요.

• Green:
  • make ingress-gating
• Red (예상된 결과):
  • make ingress-gating-negative

라우팅/세션 키 격리

클레임: 서로 다른 피어(peer)로부터 온 DM은 명시적으로 연결되거나 설정되지 않는 한 동일한 세션으로 합쳐지지 않아요.

• Green:
  • make routing-isolation
• Red (예상된 결과):
  • make routing-isolation-negative

v1++: 추가 바운디드 모델 (동시성, 재시도, 추적 정확성)

이것들은 실제 환경의 실패 모드(비원자적 업데이트, 재시도, 메시지 팬아웃)에 대한 정확도를 높이기 위한 후속 모델들이에요.

Pairing 저장소 동시성 / 멱등성

클레임: Pairing 저장소는 인터리빙(interleaving) 상황에서도 MaxPending 및 멱등성을 강제해야 해요(즉, “check-then-write”는 원자적이어야 하거나 잠금 처리되어야 하며, 새로고침이 중복 항목을 생성해서는 안 돼요).

의미하는 바:

• 동시 요청이 발생해도 채널에 대한 MaxPending을 초과할 수 없어요.

• 동일한 (channel, sender)에 대한 반복적인 요청이나 새로고침은 중복된 대기 행을 생성하지 않아야 해요.

• Green 실행:

  • make pairing-race (원자적/잠금 제한 체크)
  • make pairing-idempotency
  • make pairing-refresh
  • make pairing-refresh-race

• Red (예상된 결과):

  • make pairing-race-negative (비원자적 시작/커밋 제한 레이스)
  • make pairing-idempotency-negative
  • make pairing-refresh-negative
  • make pairing-refresh-race-negative

Ingress 추적 상관관계 / 멱등성

클레임: 수집(ingestion) 프로세스는 팬아웃 전체에서 추적 상관관계를 유지해야 하며, 프로바이더 재시도 시에도 멱등성을 유지해야 해요.

의미하는 바:

• 하나의 외부 이벤트가 여러 내부 메시지가 될 때, 모든 부분은 동일한 추적/이벤트 ID를 유지해요.

• 재시도로 인해 중복 처리가 발생하지 않아요.

• 프로바이더 이벤트 ID가 없는 경우, 고유한 이벤트를 누락하지 않도록 안전한 키(예: 추적 ID)로 중복 제거를 수행해요.

• Green:

  • make ingress-trace
  • make ingress-trace2
  • make ingress-idempotency
  • make ingress-dedupe-fallback

• Red (예상된 결과):

  • make ingress-trace-negative
  • make ingress-trace2-negative
  • make ingress-idempotency-negative
  • make ingress-dedupe-fallback-negative

라우팅 dmScope 우선순위 + identityLinks

클레임: 라우팅은 기본적으로 DM 세션을 격리된 상태로 유지해야 하며, 명시적으로 설정된 경우(채널 우선순위 + ID 링크)에만 세션을 합쳐야 해요.

의미하는 바:

• 채널별 dmScope 설정은 글로벌 기본값보다 우선순위가 높아야 해요.

• identityLinks는 관련 없는 피어 간이 아니라, 명시적으로 연결된 그룹 내에서만 합쳐져야 해요.

• Green:

  • make routing-precedence
  • make routing-identitylinks

• Red (예상된 결과):

  • make routing-precedence-negative
  • make routing-identitylinks-negative

궁금한 점이 있거나 설정에 도움이 필요하면 언제든 물어봐 주세요! AI Setup Assistant

다음 단계

• 보안 아키텍처 개요
• Gateway 설정 가이드