Verifikasi formal (model keamanan)

Model keamanan formal OpenClaw (saat ini TLA+/TLC) 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 yang dinyatakan secara eksplisit.

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

Apa ini

Rangkaian pengujian regresi keamanan yang dapat dijalankan 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 dikelola dalam repositori terpisah: vignesh07/openclaw-formal-models.

Catatan penting

• Ini adalah model, bukan keseluruhan implementasi TypeScript — ketidaksesuaian antara model dan kode mungkin terjadi.
• Hasil dibatasi oleh ruang keadaan yang dieksplorasi TLC. Hasil hijau tidak menyiratkan keamanan di luar asumsi dan batas yang dimodelkan.
• Beberapa klaim bergantung pada asumsi lingkungan yang eksplisit (misalnya, deployment 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 dikunci serta menyediakan bin/tlc dan target Make. make <target>

Belum ada integrasi CI kembali ke repositori ini; iterasi mendatang dapat menambahkan model yang dijalankan oleh 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 penyusupan 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.

Alur eksekusi Node (kapabilitas dengan risiko tertinggi)

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

Penyimpanan pemasangan (pembatasan DM)

Klaim: permintaan pemasangan mematuhi TTL dan batas permintaan tertunda.

Pembatasan masukan (penyebutan dan pengelakan perintah kontrol)

Klaim: dalam konteks grup yang mewajibkan penyebutan, perintah kontrol yang tidak diotorisasi tidak dapat mengelakkan 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 ketepatan seputar mode kegagalan di dunia nyata: pembaruan nonatomik, percobaan ulang, dan penyebaran pesan.

Konkurensi dan idempotensi penyimpanan pemasangan

Klaim: penyimpanan pemasangan menegakkan MaxPending dan idempotensi bahkan dalam kondisi operasi yang saling berselang-seling — pemeriksaan-lalu-penulisan harus bersifat atomik/dikunci, dan penyegaran tidak boleh membuat duplikat. Secara konkret: permintaan bersamaan 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 masukan

Klaim: proses pemasukan mempertahankan korelasi jejak selama penyebaran dan bersifat idempoten ketika 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 beralih ke kunci yang aman (misalnya ID jejak) untuk menghindari penghapusan peristiwa yang berbeda.

Prioritas dmScope perutean dan identityLinks

Klaim: perutean menjaga sesi DM tetap terisolasi secara default dan hanya menggabungkan sesi ketika dikonfigurasi secara eksplisit, melalui prioritas kanal dan tautan identitas. Penggantian dmScope khusus kanal lebih diprioritaskan daripada nilai default global; identityLinks menggabungkan sesi hanya di dalam grup tertaut yang eksplisit, bukan di antara rekan yang tidak berkaitan.

Terkait

• Model ancaman
• Berkontribusi pada model ancaman
• Respons insiden