Vérification formelle (modèles de sécurité)

Les modèles de sécurité formels d’OpenClaw (TLA+/TLC actuellement) fournissent un argument vérifié par machine selon lequel certains parcours présentant les risques les plus élevés — autorisation, isolation des sessions, contrôle de l’accès aux outils et sûreté en cas de mauvaise configuration — appliquent la politique prévue, selon des hypothèses explicitement énoncées.

Remarque : certains liens plus anciens peuvent faire référence au précédent nom du projet.

Présentation

Une suite exécutable de tests de non-régression de sécurité pilotés par un attaquant :

• Chaque affirmation dispose d’une vérification de modèle exécutable sur un espace d’états fini.
• De nombreuses affirmations sont associées à un modèle négatif qui produit une trace de contre-exemple pour une catégorie réaliste de bogues.

Il ne s’agit pas d’une preuve qu’OpenClaw est sécurisé à tous égards, et cette suite ne vérifie pas l’intégralité de l’implémentation TypeScript.

Emplacement des modèles

Les modèles sont maintenus dans un dépôt distinct : vignesh07/openclaw-formal-models.

Limites

• Il s’agit de modèles, et non de l’implémentation TypeScript complète : une divergence entre le modèle et le code est possible.
• Les résultats sont limités par l’espace d’états exploré par TLC. Un résultat positif n’implique aucune garantie de sécurité au-delà des hypothèses et limites modélisées.
• Certaines affirmations reposent sur des hypothèses explicites concernant l’environnement, par exemple un déploiement correct et des données de configuration correctes.

Reproduction des résultats

Clonez le dépôt des modèles et exécutez TLC :

git clone https://github.com/vignesh07/openclaw-formal-modelscd openclaw-formal-models # Java 11+ requis (TLC s’exécute sur la JVM).# Le dépôt inclut une version fixe de tla2tools.jar et fournit bin/tlc ainsi que des cibles Make. make <target>

Il n’existe pas encore d’intégration CI avec ce dépôt. Une prochaine version pourrait ajouter des modèles exécutés par la CI avec des artefacts publics (traces de contre-exemples, journaux d’exécution), ou un workflow hébergé « exécuter ce modèle » pour les petites vérifications bornées.

Affirmations et cibles

Exposition du Gateway et mauvaise configuration d’un Gateway ouvert

Affirmation : une liaison au-delà de local loopback sans authentification peut permettre une compromission à distance et accroît l’exposition ; selon les hypothèses du modèle, un jeton ou un mot de passe bloque les attaquants non authentifiés.

Consultez également docs/gateway-exposure-matrix.md dans le dépôt des modèles.

Pipeline d’exécution du Node (capacité présentant le risque le plus élevé)

Affirmation : exec host=node nécessite (a) une liste d’autorisation des commandes du Node ainsi que des commandes déclarées et (b) une approbation en temps réel lorsqu’elle est configurée ; dans le modèle, les approbations utilisent des jetons pour empêcher leur réutilisation.

Stockage des associations (contrôle des messages privés)

Affirmation : les demandes d’association respectent la durée de vie et les limites du nombre de demandes en attente.

Contrôle des entrées (mentions et contournement par des commandes de contrôle)

Affirmation : dans les contextes de groupe nécessitant une mention, une commande de contrôle non autorisée ne peut pas contourner le contrôle des mentions.

Routage et isolation des clés de session

Affirmation : les messages privés provenant d’interlocuteurs distincts ne sont pas regroupés dans la même session, sauf s’ils sont explicitement liés ou configurés ainsi.

Modèles v1++ : concurrence, nouvelles tentatives et exactitude des traces

Modèles complémentaires qui améliorent la fidélité concernant les modes de défaillance réels : mises à jour non atomiques, nouvelles tentatives et diffusion des messages.

Concurrence et idempotence du stockage des associations

Affirmation : le stockage des associations applique MaxPending et l’idempotence, même en cas d’entrelacement des opérations : la vérification suivie de l’écriture doit être atomique ou verrouillée, et l’actualisation ne doit pas créer de doublons. Concrètement, les demandes simultanées ne peuvent pas dépasser MaxPending pour un canal, et les demandes ou actualisations répétées pour la même paire (channel, sender) ne créent pas de lignes actives en attente en double.

Corrélation des traces d’entrée et idempotence

Affirmation : l’ingestion préserve la corrélation des traces pendant la diffusion et reste idempotente lors des nouvelles tentatives du fournisseur. Lorsqu’un événement externe devient plusieurs messages internes, chaque partie conserve la même identité de trace ou d’événement ; les nouvelles tentatives n’entraînent aucun double traitement ; si les identifiants d’événement du fournisseur sont absents, la déduplication utilise une clé de secours sûre, par exemple l’identifiant de trace, afin d’éviter d’écarter des événements distincts.

Priorité de dmScope dans le routage et identityLinks

Affirmation : par défaut, le routage maintient les sessions de messages privés isolées et ne regroupe les sessions qu’en cas de configuration explicite, selon la priorité des canaux et les liens d’identité. Les valeurs de dmScope propres à un canal prévalent sur les valeurs globales par défaut ; identityLinks ne regroupe les sessions qu’au sein de groupes explicitement liés, sans regrouper des interlocuteurs sans rapport.

Voir aussi

• Modèle de menace
• Contribuer au modèle de menace
• Réponse aux incidents