Towards System-Oriented Formal Verification of Local-First Access Control

Riassunto Tecnico: Verso la Verifica Formale Orientata ai Sistemi dell'Access Control Local-First

1. Il Problema (Problem Statement)

I sistemi "local-first" (come Matrix o Keyhive) utilizzano i Conflict-free Replicated Data Types (CRDTs) per garantire bassa latenza e disponibilità in ambienti decentralizzati. Tuttavia, man mano che questi sistemi scalano da piccoli gruppi di utenti fidati a reti globali, emergono due sfide critiche:

• Assenza di fiducia reciproca: In contesti su larga scala, il sistema deve essere resistente ad attacchi Byzantine (entità malevole che possono omettere dati, equivocare o falsificare la cronologia tramite backdating).
• Controllo degli accessi (Access Control): È necessario implementare un controllo degli accessi granulare che funzioni in modo asincrono, senza richiedere coordinamento centrale, garantendo al contempo che le revoche delle autorizzazioni siano sicure e consistenti.

Attualmente, esiste un divario significativo tra la teoria dei metodi formali e la pratica ingegneristica: i protocolli esistenti (come Matrix) si basano su specifiche informali e implementazioni non verificate, il che ha già portato a violazioni di invarianti di sicurezza.

2. Metodologia (Methodology)

Gli autori adottano un approccio bottom-up. Invece di tentare di verificare direttamente sistemi complessi come Matrix, costruiscono e verificano algoritmi di autorizzazione semplificati ma formalmente corretti, per poi estenderne gradualmente la complessità.

La metodologia si basa su tre pilastri:

• Modellazione Semantica: Definizione di un tipo di dato replicato per la gestione di gruppi di collaborazione, basato su capabilities (capacità) per l'autorizzazione e hash chronicles (grafi aciclici diretti o MerkleDAG) per la replica resistente ai guasti Byzantine.
• Verifica Formale con Verus: Utilizzo di Verus, un framework di verifica per il linguaggio Rust. Verus permette di unificare specifica, implementazione e verifica in un unico file sorgente, utilizzando il risolutore SMT Z3. Questo approccio garantisce la verifica a "costo di runtime zero", rendendo il processo accessibile agli ingegneri dei sistemi.
• Modello di Minaccia: Il sistema assume che una frazione $f/n < 1$ di entità sia Byzantine. Gli algoritmi sono testati contro vettori di attacco come l'equivocazione (creazione di eventi concorrenti divergenti) e il backdating (tentativo di inserire eventi in una cronologia passata per aggirare una revoca).

3. Contributi Chiave (Key Contributions)

• Specifiche di Semantica e Invarianti: Il lavoro fornisce una formalizzazione matematica (Spec. 1 e Spec. 2) per un tipo di dato replicato che gestisce:
  • Capabilities: Meccanismo "granted-present-revoke" (concessione, presentazione e revoca).
  • Invarianti di Sicurezza: Definizione di Authorization Safety (l'autorizzazione causale è invariante), Query Safety (i risultati delle query cambiano solo se l'evento è autorizzato) e Revocation Safety (una revoca valida deve invalidare anche eventi con timestamp precedenti/concorrenti per contrastare il backdating).
• Implementazione e Verifica in Rust: Un'implementazione pratica di questi concetti utilizzando Verus, dimostrando come integrare contratti di funzione (ensures, requires) e codice "ghost" (usato solo per la verifica) direttamente nel codice di produzione.
• Studio di Caso su tre livelli di complessità:
  1. Autorizzazione monotica (solo concessione durante la creazione).
  2. Autorizzazione monotica (concessione successiva alla creazione).
  3. Autorizzazione non-monotica (supporto alla revoca), che introduce la complessità maggiore poiché le autorizzazioni possono cambiare nel tempo.

4. Risultati (Results)

• Verifica del Modello Non-Monotico: Gli autori sono riusciti a verificare con successo l'algoritmo che supporta la revoca delle capacità. Nonostante la natura non-monotica (dove un evento può perdere l'autorizzazione a causa di una revoca concorrente), il sistema mantiene la coerenza finale (eventual consistency).
• Resistenza ai Guasti Byzantine: È stato dimostrato che, sotto l'assunzione di una cronologia (chronicle) che garantisce la consistenza finale, i risultati delle query sono puri e totali, rendendo il sistema resistente ai tentativi di manipolazione della cronologia tramite backdating e equivocazione.
• Esperienza con Verus: Il lavoro evidenzia che, sebbene Verus sia potente, la verifica di cicli for (in sostituzione dei combinatori di iteratori di Rust) è una delle attività più onerose in termini di tempo.

5. Significato e Impatto (Significance)

Questo lavoro rappresenta un passo fondamentale verso la sicurezza dei sistemi decentralizzati di nuova generazione. Dimostra che è possibile colmare il divario tra la teoria della verifica formale e l'ingegneria del software ad alte prestazioni utilizzando Rust e Verus.

Il successo della verifica di un sistema di autorizzazione non-monotico apre la strada a implementazioni verificate di protocolli reali come Matrix, riducendo drasticamente il rischio di vulnerabilità di sicurezza critiche derivanti da errori logici nella gestione della concorrenza e della distribuzione dei permessi.