Formal Verification (Security Models)

이 페이지는 OpenClaw의 형식 보안 모델 (현재 TLA+/TLC; 필요에 따라 추가)을 추적합니다.

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

목표 (north star): OpenClaw가 명시적 가정 하에서 의도된 보안 정책 (권한 부여, 세션 격리, 도구 게이팅 및 구성 오류 안전)을 시행한다는 기계 검증 인수를 제공합니다.

현재 상태: 실행 가능한 공격자 주도 보안 회귀 테스트 스위트:

  • 각 주장은 유한 상태 공간에 대한 실행 가능한 모델 검사를 가지고 있습니다.
  • 많은 주장은 현실적인 버그 클래스에 대한 반례 추적을 생성하는 부정 모델을 쌍으로 가지고 있습니다.

아직 아닌 것: "OpenClaw가 모든 측면에서 안전하다"는 증명 또는 전체 TypeScript 구현이 올바르다는 증명.

모델의 위치

모델은 별도의 저장소에서 유지 관리됩니다: vignesh07/openclaw-formal-models.

중요한 주의 사항

  • 이것들은 모델이지 전체 TypeScript 구현이 아닙니다. 모델과 코드 간의 차이가 가능합니다.
  • 결과는 TLC가 탐색한 상태 공간에 의해 제한됩니다; "녹색"은 모델링된 가정과 경계를 넘어서는 보안을 의미하지 않습니다.
  • 일부 주장은 명시적 환경 가정에 의존합니다 (예: 올바른 배포, 올바른 설정 입력).

결과 재현

현재 결과는 모델 저장소를 로컬로 복제하고 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 exposure and open gateway misconfiguration

주장: 인증 없이 루프백을 넘어서 바인딩하면 원격 침해가 가능해질 수 있음 / 노출이 증가합니다; token/password는 인증되지 않은 공격자를 차단합니다 (모델 가정에 따라).

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

참조: 모델 저장소의 docs/gateway-exposure-matrix.md.

Nodes.run pipeline (highest-risk capability)

주장: nodes.run은 (a) node 명령 허용 목록과 선언된 명령 및 (b) 설정된 경우 실시간 승인이 필요합니다; 승인은 재생을 방지하기 위해 토큰화됩니다 (모델에서).

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

Pairing store (DM gating)

주장: 페어링 요청은 TTL 및 대기 중인 요청 제한을 준수합니다.

  • Green 실행:
    • make pairing
    • make pairing-cap
  • Red (예상됨):
    • make pairing-negative
    • make pairing-cap-negative

Ingress gating (mentions + control-command bypass)

주장: 멘션이 필요한 그룹 컨텍스트에서 권한이 없는 "control command"는 멘션 게이팅을 우회할 수 없습니다.

  • Green:
    • make ingress-gating
  • Red (예상됨):
    • make ingress-gating-negative

Routing/session-key isolation

주장: 명시적으로 연결/설정되지 않는 한 서로 다른 피어의 DM은 동일한 세션으로 축소되지 않습니다.

  • Green:
    • make routing-isolation
  • Red (예상됨):
    • make routing-isolation-negative

v1++: additional bounded models (concurrency, retries, trace correctness)

이것들은 실제 실패 모드 (비원자적 업데이트, 재시도 및 메시지 팬아웃) 주변의 충실도를 강화하는 후속 모델입니다.

Pairing store concurrency / idempotency

주장: 페어링 저장소는 인터리빙 하에서도 MaxPending 및 멱등성을 시행해야 합니다 (즉, "check-then-write"는 원자적 / 잠금되어야 함; refresh는 중복을 생성하지 않아야 함).

의미:

  • 동시 요청 하에서 채널에 대해 MaxPending을 초과할 수 없습니다.

  • 동일한 (channel, sender)에 대한 반복된 요청/새로 고침은 중복 라이브 대기 행을 생성하지 않아야 합니다.

  • Green 실행:

    • make pairing-race (원자적/잠금된 cap 확인)
    • make pairing-idempotency
    • make pairing-refresh
    • make pairing-refresh-race

  • Red (예상됨):

    • make pairing-race-negative (비원자적 begin/commit cap 경합)
    • make pairing-idempotency-negative
    • make pairing-refresh-negative
    • make pairing-refresh-race-negative

Ingress trace correlation / idempotency

주장: 수집은 팬아웃 전반에 걸쳐 추적 상관 관계를 보존하고 제공자 재시도 하에서 멱등적이어야 합니다.

의미:

  • 하나의 외부 이벤트가 여러 내부 메시지가 될 때 모든 부분이 동일한 추적/이벤트 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

Routing dmScope precedence + identityLinks

주장: 라우팅은 기본적으로 DM 세션을 격리된 상태로 유지해야 하며 명시적으로 설정된 경우에만 세션을 축소해야 합니다 (채널 우선 순위 + ID 링크).

의미:

  • 채널별 dmScope 재정의는 전역 기본값보다 우선해야 합니다.

  • identityLinks는 명시적 연결 그룹 내에서만 축소해야 하며 관련 없는 피어 간에는 축소하지 않습니다.

  • Green:

    • make routing-precedence
    • make routing-identitylinks

  • Red (예상됨):

    • make routing-precedence-negative
    • make routing-identitylinks-negative
← 문서로 돌아가기