Skip to main content
I modelli formali di sicurezza di OpenClaw (attualmente TLA+/TLC) forniscono un’argomentazione verificata automaticamente secondo cui specifici percorsi a rischio massimo — autorizzazione, isolamento delle sessioni, controllo dell’accesso agli strumenti e sicurezza in caso di configurazione errata — applicano i criteri previsti, sulla base di presupposti esplicitamente dichiarati.
Nota: alcuni collegamenti meno recenti potrebbero fare riferimento al nome precedente del progetto.

​
Che cos’è

Una suite eseguibile di test di regressione della sicurezza basata su scenari di attacco:
  • Ogni affermazione dispone di una verifica del modello eseguibile su uno spazio degli stati finito.
  • Molte affermazioni dispongono di un modello negativo associato che produce una traccia di controesempio per una classe realistica di bug.
Questa non è una prova che OpenClaw sia sicuro sotto ogni aspetto e non verifica l’intera implementazione TypeScript.

​
Dove si trovano i modelli

I modelli sono gestiti in un repository separato: vignesh07/openclaw-formal-models.
Al momento tale repository non è raggiungibile (GitHub restituisce “Repository not found” al momento della stesura). Se risulta ancora non disponibile, chiedi nei canali dei manutentori di OpenClaw quale sia la posizione attuale prima di supporre che i modelli siano stati rimossi.

​
Avvertenze

  • Si tratta di modelli, non dell’intera implementazione TypeScript: è possibile che il modello e il codice divergano.
  • I risultati sono limitati dallo spazio degli stati esplorato da TLC. Un risultato positivo non implica sicurezza oltre i presupposti e i limiti modellati.
  • Alcune affermazioni dipendono da presupposti espliciti sull’ambiente, ad esempio una distribuzione corretta e dati di configurazione corretti.

​
Riproduzione dei risultati

Clona il repository dei modelli ed esegui TLC:
Non esiste ancora un’integrazione CI con questo repository; un’iterazione futura potrebbe aggiungere modelli eseguiti dalla CI con artefatti pubblici (tracce di controesempio, registri di esecuzione) oppure un flusso ospitato “esegui questo modello” per piccole verifiche limitate.

​
Affermazioni e target

​
Esposizione del Gateway e configurazione errata di un Gateway aperto

Affermazione: l’associazione a interfacce diverse da loopback senza autenticazione può rendere possibile una compromissione remota e aumentare l’esposizione; un token o una password blocca gli autori di attacchi non autenticati, secondo i presupposti del modello. Consulta anche docs/gateway-exposure-matrix.md nel repository dei modelli.

​
Pipeline di esecuzione del Node (funzionalità a rischio massimo)

Affermazione: exec host=node richiede (a) un elenco di comandi consentiti per il Node insieme ai comandi dichiarati e (b) un’approvazione in tempo reale, se configurata; nel modello, le approvazioni vengono associate a token per impedirne il riutilizzo.

​
Archivio di associazione (controllo dell’accesso ai messaggi diretti)

Affermazione: le richieste di associazione rispettano il TTL e i limiti delle richieste in sospeso.

​
Controllo dell’ingresso (menzioni e aggiramento tramite comandi di controllo)

Affermazione: nei contesti di gruppo che richiedono una menzione, un comando di controllo non autorizzato non può aggirare il controllo basato sulle menzioni.

​
Instradamento e isolamento delle chiavi di sessione

Affermazione: i messaggi diretti provenienti da interlocutori distinti non vengono accorpati nella stessa sessione, a meno che non siano esplicitamente collegati o configurati.

​
Modelli v1++: concorrenza, nuovi tentativi e correttezza delle tracce

Modelli successivi che migliorano la fedeltà rispetto alle modalità di errore del mondo reale: aggiornamenti non atomici, nuovi tentativi e distribuzione dei messaggi.

​
Concorrenza e idempotenza dell’archivio di associazione

Affermazione: l’archivio di associazione applica MaxPending e l’idempotenza anche in presenza di intercalamenti: la sequenza di verifica e scrittura deve essere atomica o protetta da blocco e l’aggiornamento non deve creare duplicati. In concreto: le richieste simultanee non possono superare MaxPending per un canale e richieste o aggiornamenti ripetuti per la stessa coppia (channel, sender) non creano righe in sospeso attive duplicate.

​
Correlazione delle tracce e idempotenza dell’ingresso

Affermazione: l’acquisizione conserva la correlazione delle tracce durante la distribuzione ed è idempotente in caso di nuovi tentativi da parte del fornitore. Quando un evento esterno viene trasformato in più messaggi interni, ogni parte mantiene la stessa identità di traccia o evento; i nuovi tentativi non causano una doppia elaborazione; se mancano gli ID evento del fornitore, la deduplicazione ricorre a una chiave sicura, ad esempio l’ID traccia, per evitare di eliminare eventi distinti. Affermazione: l’instradamento mantiene isolate per impostazione predefinita le sessioni dei messaggi diretti e accorpa le sessioni soltanto quando è configurato esplicitamente, mediante la precedenza dei canali e i collegamenti di identità. Le impostazioni dmScope specifiche del canale prevalgono sui valori predefiniti globali; identityLinks accorpa le sessioni soltanto all’interno di gruppi collegati esplicitamente, non tra interlocutori non correlati.

​
Contenuti correlati