> ## Documentation Index
> Fetch the complete documentation index at: https://docs2.openclaw.ai/llms.txt
> Use this file to discover all available pages before exploring further.

# 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](https://github.com/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:

```bash theme={"theme":{"light":"min-light","dark":"min-dark"}}
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](/it/security/THREAT-MODEL-ATLAS)
* [Contribuire al modello di minaccia](/it/security/CONTRIBUTING-THREAT-MODEL)