Verifikasi formal (model keamanan)

Model keamanan formal OpenClaw (TLA+/TLC saat ini) memberikan argumen yang diperiksa mesin bahwa jalur tertentu dengan risiko tertinggi — otorisasi, isolasi sesi, pembatasan alat, dan keamanan terhadap kesalahan konfigurasi — menegakkan kebijakan yang dimaksud, berdasarkan asumsi eksplisit yang dinyatakan.

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

Apa ini

Rangkaian regresi keamanan yang dapat dieksekusi dan digerakkan oleh penyerang:

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

Ini bukan bukti bahwa OpenClaw aman dalam segala aspek, dan tidak memverifikasi keseluruhan implementasi TypeScript.

Lokasi model

Model dipelihara dalam repositori terpisah: vignesh07/openclaw-formal-models.

Batasan

• Ini adalah model, bukan keseluruhan implementasi TypeScript — perbedaan antara model dan kode mungkin terjadi.
• Hasil dibatasi oleh ruang keadaan yang dijelajahi TLC. Status hijau tidak menyiratkan keamanan di luar asumsi dan batas yang dimodelkan.
• Beberapa klaim bergantung pada asumsi lingkungan yang eksplisit (misalnya, penerapan dan masukan konfigurasi yang benar).

Mereproduksi hasil

Kloning repositori model dan jalankan TLC:

git clone https://github.com/vignesh07/openclaw-formal-modelscd openclaw-formal-models # Memerlukan Java 11+ (TLC berjalan pada JVM).# Repositori menyertakan tla2tools.jar dengan versi yang dipatok serta menyediakan bin/tlc dan target Make. make <target>

Belum ada integrasi Pipeline CI kembali ke repositori ini; iterasi mendatang dapat menambahkan model yang dijalankan melalui CI dengan artefak publik (jejak contoh tandingan, log eksekusi) atau alur kerja "jalankan model ini" yang dihosting untuk pemeriksaan terbatas berskala kecil.

Klaim dan target

Paparan Gateway dan kesalahan konfigurasi Gateway terbuka

Klaim: pengikatan di luar loopback tanpa autentikasi dapat memungkinkan kompromi jarak jauh dan meningkatkan paparan; token/kata sandi memblokir penyerang yang tidak terautentikasi, berdasarkan asumsi model.

Lihat juga docs/gateway-exposure-matrix.md dalam repositori model.

Pipeline eksekusi Node (kapabilitas dengan risiko tertinggi)

Klaim: exec host=node memerlukan (a) daftar izin perintah Node beserta perintah yang dideklarasikan dan (b) persetujuan langsung jika dikonfigurasi; dalam model, persetujuan diberi token untuk mencegah pemutaran ulang.

Penyimpanan pemasangan (pembatasan DM)

Klaim: permintaan pemasangan mematuhi TTL dan batas permintaan tertunda.

Pembatasan ingress (penyebutan dan penerobosan perintah kontrol)

Klaim: dalam konteks grup yang mewajibkan penyebutan, perintah kontrol yang tidak diotorisasi tidak dapat menerobos pembatasan penyebutan.

Perutean dan isolasi kunci sesi

Klaim: DM dari rekan yang berbeda tidak digabungkan ke dalam sesi yang sama kecuali ditautkan atau dikonfigurasi secara eksplisit.

Model v1++: konkurensi, percobaan ulang, dan ketepatan jejak

Model lanjutan yang meningkatkan kesesuaian terhadap mode kegagalan dunia nyata: pembaruan nonatomik, percobaan ulang, dan fan-out pesan.

Konkurensi dan idempotensi penyimpanan pemasangan

Klaim: penyimpanan pemasangan menegakkan MaxPending dan idempotensi bahkan dalam operasi yang berselang-seling — periksa-lalu-tulis harus bersifat atomik/terkunci, dan penyegaran tidak boleh membuat duplikat. Secara konkret: permintaan serentak tidak dapat melampaui MaxPending untuk suatu kanal, dan permintaan/penyegaran berulang untuk (channel, sender) yang sama tidak membuat baris tertunda aktif yang duplikat.

Korelasi jejak dan idempotensi ingress

Klaim: proses ingest mempertahankan korelasi jejak selama fan-out dan bersifat idempoten saat penyedia melakukan percobaan ulang. Ketika satu peristiwa eksternal menjadi beberapa pesan internal, setiap bagian mempertahankan identitas jejak/peristiwa yang sama; percobaan ulang tidak menyebabkan pemrosesan ganda; jika ID peristiwa penyedia tidak tersedia, deduplikasi menggunakan kunci aman sebagai cadangan (misalnya ID jejak) agar tidak membuang peristiwa yang berbeda.

Perutean prioritas dmScope dan identityLinks

Klaim: prioritas dmScope dan tautan identitas berperilaku secara deterministik: cakupan default main berbagi satu sesi berjalan di seluruh DM milik satu pemilik (default agen pribadi), sedangkan setiap cakupan isolasi yang dikonfigurasi (per-peer, per-channel-peer, per-account-channel-peer) menjaga sesi DM tetap terpisah secara ketat. Penimpaan dmScope khusus kanal lebih diutamakan daripada default global; identityLinks menggabungkan sesi hanya dalam grup yang ditautkan secara eksplisit, bukan di antara rekan yang tidak terkait. Kotak masuk multi-pengguna diharapkan memilih cakupan isolasi (audit keamanan runtime merekomendasikan hal ini ketika mendeteksi lalu lintas DM multi-pengguna).

Terkait

• Model ancaman
• Berkontribusi pada model ancaman
• Respons insiden