Verifica formale (modelli di sicurezza)

Questa pagina tiene traccia dei modelli formali di sicurezza di OpenClaw (TLA+/TLC oggi; altri secondo necessità).

Nota: alcuni link meno recenti potrebbero fare riferimento al nome precedente del progetto.

Obiettivo (guida): fornire un'argomentazione verificata automaticamente secondo cui OpenClaw applica la sua policy di sicurezza prevista (autorizzazione, isolamento delle sessioni, controllo di accesso agli strumenti e sicurezza contro configurazioni errate), in base ad assunzioni esplicite.

Che cos'è (oggi): una suite di regressione di sicurezza eseguibile e guidata dall'attaccante:

• Ogni affermazione ha un controllo del modello eseguibile su uno spazio di stati finito.
• Molte affermazioni hanno un modello negativo abbinato che produce una traccia di controesempio per una classe di bug realistica.

Che cosa non è (ancora): una prova che "OpenClaw è sicuro sotto ogni aspetto" o che l'implementazione TypeScript completa è corretta.

# Dove risiedono i modelli

I modelli sono mantenuti in un repo separato: vignesh07/openclaw-formal-models.

# Avvertenze importanti

• Questi sono modelli, non l'implementazione TypeScript completa. È possibile una divergenza tra modello e codice.
• I risultati sono limitati dallo spazio di stati esplorato da TLC; "verde" non implica sicurezza oltre le assunzioni e i limiti modellati.
• Alcune affermazioni si basano su assunzioni ambientali esplicite (ad esempio, distribuzione corretta, input di configurazione corretti).

# Riprodurre i risultati

Oggi i risultati si riproducono clonando localmente il repo dei modelli ed eseguendo TLC (vedi sotto). Un'iterazione futura potrebbe offrire:

• modelli eseguiti in CI con artefatti pubblici (tracce di controesempio, log di esecuzione)
• un flusso di lavoro ospitato "esegui questo modello" per controlli piccoli e limitati

Per iniziare:

git clone https://github.com/vignesh07/openclaw-formal-models
cd openclaw-formal-models

# Java 11+ required (TLC runs on the JVM).
# The repo vendors a pinned `tla2tools.jar` (TLA+ tools) and provides `bin/tlc` + Make targets.

make <target>

# Esposizione del Gateway e configurazione errata di Gateway aperto

Affermazione: eseguire il binding oltre il loopback senza autenticazione può rendere possibile una compromissione remota / aumenta l'esposizione; token/password bloccano gli attaccanti non autenticati (secondo le assunzioni del modello).

• Esecuzioni verdi:
  • make gateway-exposure-v2
  • make gateway-exposure-v2-protected
• Rosso (previsto):
  • make gateway-exposure-v2-negative

Vedi anche: docs/gateway-exposure-matrix.md nel repo dei modelli.

# Pipeline di esecuzione Node (capacità a rischio più elevato)

Affermazione: exec host=node richiede (a) un elenco di comandi Node consentiti più comandi dichiarati e (b) approvazione live quando configurata; le approvazioni sono tokenizzate per impedire la riproduzione (nel modello).

• Esecuzioni verdi:
  • make nodes-pipeline
  • make approvals-token
• Rosso (previsto):
  • make nodes-pipeline-negative
  • make approvals-token-negative

# Archivio di pairing (controllo di accesso dei DM)

Affermazione: le richieste di pairing rispettano TTL e limiti delle richieste in sospeso.

• Esecuzioni verdi:
  • make pairing
  • make pairing-cap
• Rosso (previsto):
  • make pairing-negative
  • make pairing-cap-negative

# Controllo di accesso in ingresso (menzioni + bypass dei comandi di controllo)

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

• Verde:
  • make ingress-gating
• Rosso (previsto):
  • make ingress-gating-negative

# Isolamento del routing/della chiave di sessione

Affermazione: i DM provenienti da peer distinti non confluiscono nella stessa sessione, salvo collegamento/configurazione espliciti.

• Verde:
  • make routing-isolation
• Rosso (previsto):
  • make routing-isolation-negative

# v1++: modelli limitati aggiuntivi (concorrenza, tentativi, correttezza della traccia)

Questi sono modelli successivi che rafforzano la fedeltà rispetto a modalità di errore reali (aggiornamenti non atomici, tentativi e fan-out dei messaggi).

# Concorrenza / idempotenza dell'archivio di pairing

Affermazione: un archivio di pairing dovrebbe applicare MaxPending e l'idempotenza anche in caso di interleaving (cioè, "check-then-write" deve essere atomico / protetto da lock; il refresh non dovrebbe creare duplicati).

Che cosa significa:

• In presenza di richieste concorrenti, non puoi superare MaxPending per un canale.

• Richieste/refresh ripetuti per la stessa coppia (channel, sender) non dovrebbero creare righe live in sospeso duplicate.

• Esecuzioni verdi:

  • make pairing-race (controllo del limite atomico/protetto da lock)
  • make pairing-idempotency
  • make pairing-refresh
  • make pairing-refresh-race

• Rosso (previsto):

  • make pairing-race-negative (race non atomica del limite begin/commit)
  • make pairing-idempotency-negative
  • make pairing-refresh-negative
  • make pairing-refresh-race-negative

# Correlazione della traccia / idempotenza in ingresso

Affermazione: l'ingestione dovrebbe preservare la correlazione della traccia attraverso il fan-out ed essere idempotente in caso di tentativi del provider.

Che cosa significa:

• Quando un evento esterno diventa più messaggi interni, ogni parte mantiene la stessa identità di traccia/evento.

• I tentativi non causano una doppia elaborazione.

• Se mancano gli ID evento del provider, la deduplicazione ripiega su una chiave sicura (ad esempio, ID traccia) per evitare di eliminare eventi distinti.

• Verde:

  • make ingress-trace
  • make ingress-trace2
  • make ingress-idempotency
  • make ingress-dedupe-fallback

• Rosso (previsto):

  • make ingress-trace-negative
  • make ingress-trace2-negative
  • make ingress-idempotency-negative
  • make ingress-dedupe-fallback-negative

# Precedenza dmScope nel routing + identityLinks

Affermazione: il routing deve mantenere isolate per impostazione predefinita le sessioni DM e accorpare le sessioni solo quando configurato esplicitamente (precedenza del canale + link di identità).

Che cosa significa:

• Gli override dmScope specifici del canale devono prevalere sui valori predefiniti globali.

• identityLinks dovrebbe accorpare solo all'interno di gruppi collegati espliciti, non tra peer non correlati.

• Verde:

  • make routing-precedence
  • make routing-identitylinks

• Rosso (previsto):

  • make routing-precedence-negative
  • make routing-identitylinks-negative

# Correlati

• Modello di minaccia
• Contribuire al modello di minaccia