Verifikasi formal (model keamanan)

Halaman ini melacak model keamanan formal OpenClaw (TLA+/TLC saat ini; lainnya sesuai kebutuhan).

Catatan: beberapa tautan lama mungkin merujuk ke nama proyek sebelumnya.

Tujuan (arah utama): menyediakan argumen yang diperiksa mesin bahwa OpenClaw menegakkan kebijakan keamanan yang dimaksudkan (otorisasi, isolasi sesi, pembatasan tool, dan keamanan terhadap salah konfigurasi), dengan asumsi yang eksplisit.

Apa ini (saat ini): rangkaian regresi keamanan yang dapat dieksekusi dan digerakkan oleh penyerang:

• Setiap klaim memiliki pemeriksaan model yang dapat dijalankan pada ruang status terbatas.
• Banyak klaim memiliki pasangan model negatif yang menghasilkan trace contoh tandingan untuk kelas bug yang realistis.

Apa ini bukan (belum): bukti bahwa "OpenClaw aman dalam segala aspek" atau bahwa implementasi TypeScript penuh sudah benar.

# Tempat model berada

Model dikelola di repo terpisah: vignesh07/openclaw-formal-models.

# Catatan penting

• Ini adalah model, bukan implementasi TypeScript penuh. Drift antara model dan kode dapat terjadi.
• Hasil dibatasi oleh ruang status yang dieksplorasi oleh TLC; status "hijau" tidak menyiratkan keamanan di luar asumsi dan batas yang dimodelkan.
• Beberapa klaim bergantung pada asumsi lingkungan yang eksplisit (misalnya, deployment yang benar, input konfigurasi yang benar).

# Mereproduksi hasil

Saat ini, hasil direproduksi dengan meng-clone repo model secara lokal dan menjalankan TLC (lihat di bawah). Iterasi mendatang dapat menawarkan:

• model yang dijalankan CI dengan artefak publik (trace contoh tandingan, log eksekusi)
• workflow "jalankan model ini" yang di-host untuk pemeriksaan kecil dan terbatas

Memulai:

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>

# Eksposur Gateway dan salah konfigurasi Gateway terbuka

Klaim: binding di luar loopback tanpa auth dapat membuat kompromi jarak jauh menjadi mungkin / meningkatkan eksposur; token/password memblokir penyerang tanpa auth (sesuai asumsi model).

• Eksekusi hijau:
  • make gateway-exposure-v2
  • make gateway-exposure-v2-protected
• Merah (diharapkan):
  • make gateway-exposure-v2-negative

Lihat juga: docs/gateway-exposure-matrix.md di repo model.

# Pipeline exec Node (kapabilitas berisiko tertinggi)

Klaim: exec host=node memerlukan (a) allowlist perintah Node plus perintah yang dideklarasikan dan (b) persetujuan live saat dikonfigurasi; persetujuan diberi token untuk mencegah replay (dalam model).

• Eksekusi hijau:
  • make nodes-pipeline
  • make approvals-token
• Merah (diharapkan):
  • make nodes-pipeline-negative
  • make approvals-token-negative

# Penyimpanan pairing (pembatasan DM)

Klaim: permintaan pairing mematuhi TTL dan batas permintaan tertunda.

• Eksekusi hijau:
  • make pairing
  • make pairing-cap
• Merah (diharapkan):
  • make pairing-negative
  • make pairing-cap-negative

# Pembatasan ingress (mention + bypass perintah kontrol)

Klaim: dalam konteks grup yang memerlukan mention, "perintah kontrol" tanpa otorisasi tidak dapat melewati pembatasan mention.

• Hijau:
  • make ingress-gating
• Merah (diharapkan):
  • make ingress-gating-negative

# Isolasi routing/kunci sesi

Klaim: DM dari peer berbeda tidak digabungkan ke sesi yang sama kecuali ditautkan/dikonfigurasi secara eksplisit.

• Hijau:
  • make routing-isolation
• Merah (diharapkan):
  • make routing-isolation-negative

# v1++: model terbatas tambahan (konkurensi, retry, kebenaran trace)

Ini adalah model lanjutan yang memperketat fidelitas seputar mode kegagalan dunia nyata (pembaruan non-atomik, retry, dan fan-out pesan).

# Konkurensi / idempotensi penyimpanan pairing

Klaim: penyimpanan pairing harus menegakkan MaxPending dan idempotensi bahkan dalam interleaving (yaitu, "check-then-write" harus atomik / terkunci; refresh tidak boleh membuat duplikat).

Artinya:

• Dalam permintaan konkuren, Anda tidak bisa melampaui MaxPending untuk sebuah channel.

• Permintaan/refresh berulang untuk (channel, sender) yang sama tidak boleh membuat baris pending live duplikat.

• Eksekusi hijau:

  • make pairing-race (pemeriksaan batas atomik/terkunci)
  • make pairing-idempotency
  • make pairing-refresh
  • make pairing-refresh-race

• Merah (diharapkan):

  • make pairing-race-negative (race batas begin/commit non-atomik)
  • make pairing-idempotency-negative
  • make pairing-refresh-negative
  • make pairing-refresh-race-negative

# Korelasi trace / idempotensi ingress

Klaim: ingestion harus mempertahankan korelasi trace di seluruh fan-out dan bersifat idempoten saat terjadi retry provider.

Artinya:

• Saat satu event eksternal menjadi beberapa pesan internal, setiap bagian mempertahankan identitas trace/event yang sama.

• Retry tidak mengakibatkan pemrosesan ganda.

• Jika ID event provider tidak ada, dedupe menggunakan kunci aman sebagai fallback (misalnya, ID trace) untuk menghindari penghapusan event yang berbeda.

• Hijau:

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

• Merah (diharapkan):

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

# Presedensi dmScope routing + identityLinks

Klaim: routing harus menjaga sesi DM tetap terisolasi secara default, dan hanya menggabungkan sesi saat dikonfigurasi secara eksplisit (presedensi channel + tautan identitas).

Artinya:

• Override dmScope khusus channel harus mengalahkan default global.

• identityLinks hanya boleh menggabungkan dalam grup yang ditautkan secara eksplisit, bukan lintas peer yang tidak terkait.

• Hijau:

  • make routing-precedence
  • make routing-identitylinks

• Merah (diharapkan):

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

# Terkait

• Model ancaman
• Berkontribusi pada model ancaman