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.
Emplacement des modèles
Les modèles sont maintenus dans un dépôt distinct : vignesh07/openclaw-formal-models.Ce dépôt est actuellement inaccessible (GitHub renvoie « Repository not found » au moment de la rédaction). S’il est toujours inaccessible pour vous, demandez son emplacement actuel dans les canaux des responsables d’OpenClaw avant de supposer que les modèles ont été supprimés.
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 :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 appliqueMaxPending 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.