Riepilogo Tecnico: Verifica Integrale dell'Elaborazione dei Pacchetti

Definizione del Problema

Gli attuali sforzi di verifica formale per i programmi P4 in esecuzione su switch di rete programmabili (come Intel Tofino) e smart NIC si sono concentrati principalmente sul "blocco di controllo" (il pipeline match-action). Tuttavia, dimostrare la correttezza del solo blocco di controllo è insufficiente per garantire che uno switch gestisca i pacchetti secondo una specifica desiderata. Un'architettura di switch completa include componenti critici non-P4 — come parser, deparser e motori configurabili (ad esempio, motori multicast, generatori di pacchetti, percorsi di resubmission e traffic manager) — che vengono attivati dal programma P4 impostando specifici campi di header o metadati.

Gli strumenti di verifica esistenti mancano di modelli formali di alto livello per questi componenti non-P4. Di conseguenza, non possono verificare il comportamento end-to-end dello stream di pacchetti. Questa lacuna porta a bug non rilevabili; ad esempio, un bug in cui un campo non è stato inizializzato potrebbe essere mascherato da una zero-inizializzazione predefinita del compilatore, ma si manifesterebbe come un fallimento sotto diversi comportamenti del compilatore o nel contesto del sistema di switch completo. Senza un framework per verificare l'interazione tra il programma P4 e questi motori configurabili, i sistemi di verifica rimangono incompleti.

Metodologia

Gli autori propongono un framework completo per specificare formalmente e dimostrare la correttezza dell'intero data plane dello switch, integrando i programmi P4 con i componenti non-P4. La metodologia si basa sul proof assistant Coq e si appoggia sull'esistente strumento Verifiable P4.

1. Modellazione Formale dei Componenti

Il framework decompone lo switch in componenti modulari, ciascuno dei quali è specificato come una relazione di transizione di stato input-output:

• Parser e Deparser P4: Gli autori hanno potenziato Verifiable P4 per verificare le funzioni di parsing e deparsing dei pacchetti. Hanno introdotto una notazione concisa e dichiarativa per specificare i formati dei pacchetti (ispirata a Narcissus) per gestire le dipendenze tra i campi degli header (ad esempio, campi di protocollo che dettano gli header successivi) senza esporre i risultati intermedi del parsing. Questa notazione supporta match di codifica esatta, concatenazione e branching.
• Motori Configurabili: Gli autori hanno decodificato la documentazione del produttore (specificamente per l'architettura Intel Tofino) per creare modelli formali per i motori configurabili.
  • Packet Replication Engine (PRE): Modellato come una funzione che gestisce la replicazione unicast e multicast basata su una ricerca in tabella a due livelli.
  • Generatore di Pacchetti: Modellato come una funzione basata su timer periodici che inietta pacchetti nel flusso.
  • Componenti del Traffic Manager: Per componenti come la ricerca delle sessioni di mirroring, il controllo di ammissione e lo scheduling, gli autori hanno fornito specifiche assiomatiche. Queste spaziano da assiomi minimi (ad esempio, i pacchetti nelle code non vengono persi) ad assiomi più forti (ad esempio, i pacchetti destinati a porte "sempre pronte" non vengono mai scartati).
• Integrazione del Sistema ("Plumbing"): Il framework collega questi componenti in un modello olistico. Definisce le relazioni per le pipeline Ingress ed Egress e modella il "plumbing" (code, mirror, percorsi di ricircolo) che li collega. Il sistema modella lo stato dello switch come una tupla di tempo, stato del generatore, stati del pipeline e cronologie delle code.

2. Strategia di Verifica

Il processo di verifica prevede due fasi:

1. Verifica a livello di componente: Dimostrare che specifici programmi P4 (parser, blocchi di controllo, deparser) soddisfano le loro specifiche locali utilizzando la logica del programma Verifiable P4.
2. Composizione End-to-End: Comporre i lemmi dei componenti verificati con i modelli assiomatici dei motori configurabili. Collegando le postcondizioni di un componente alle precondizioni del successivo, il framework dimostra le proprietà dell'intero stream di pacchetti dall'ingresso alle uscite.

Contributi Chiave

1. Verifica del Data-Plane End-to-End: Il documento introduce il primo framework per convalidare le proprietà dei pacchetti dall'ingresso all'uscita, fondando la verifica su specifiche semantiche per ogni componente programmabile, configurabile e a funzione fissa.
2. Verifica Potenziata di Parser/Deparser: Gli autori hanno esteso Verifiable P4 per supportare la verifica di parser e deparser programmabili in P4, introducendo una notazione formale e verificabile tramite macchina per i formati dei pacchetti che migliora la leggibilità e l'automazione.
3. Modelli Formali di Motori Configurabili: Il documento presenta modelli formali (funzioni e assiomi) per i principali motori configurabili di Tofino, inclusi un Packet Replication Engine completamente modellato e subset funzionali del Packet Generator e di altri componenti del traffic manager.
4. Casi Studio: Il framework è stato dimostrato attraverso due applicazioni:
   • Packet Sampler: Un'applicazione stateful che campiona ogni 1024° pacchetto. La verifica ha dimostrato che il sampler produce correttamente un digest degli header per ogni 1024° pacchetto, integrando le prove del programma P4 con le prove del motore multicast e del comportamento del parser/deparser.
   • Firewall Stateful: Una verifica potenziata di un firewall stateful. Gli autori hanno utilizzato il modello formale del Packet Generator per dimostrare che il generatore può iniettare pacchetti periodici per garantire un "flusso denso", eliminando la precedente assunzione che i flussi di ingresso debbano naturalmente non avere gap superiori a 10 millisecondi.

Risultati

Gli autori hanno verificato con successo la correttezza dei due casi studio all'interno del proof assistant Coq.

• Per il Packet Sampler, hanno dimostrato che lo switch, quando configurato con il particolare programma P4 e le impostazioni del motore, soddisfa una specifica che mette in relazione lo stream di input con lo stream di output (assicurando che ogni 1024° pacchetto venga campionato e gli altri siano inoltrati normalmente).
• Per il Firewall Stateful, hanno dimostrato che la combinazione del programma P4 e della configurazione del Packet Generator soddisfa il teorema di correttezza del firewall, eliminando l'assunzione del "flusso denso" e provando efficacemente che il generatore garantisce la densità di flusso necessaria.
• Il framework ha rilevato con successo un bug in un esempio precedente in cui un campo non era stato inizializzato; questo bug era rilevabile solo verificando il comportamento end-to-end contro tutti i possibili comportamenti del compilatore e degli input, un compito impossibile con la sola verifica del blocco di controllo.

Significato e Rivendicazioni

Il documento afferma di essere il primo a permettere che la prova di correttezza di un programma P4 sia composta con le prove di correttezza dei componenti non-P4 dello switch (parser, deparser e motori configurabili) per verificare il sistema di programmazione dello switch nel suo insieme.

Gli autori sottolineano che, sebbene i loro modelli specifici siano adattati all'architettura Intel Tofino, la metodologia generale è applicabile ad altre architetture P4. Notano che l'approccio si basa sulla modularità: separare la prova del programma P4 dalle specifiche del motore permette di convalidare le proprietà dei pacchetti attraverso l'intero data plane.

Tuttoveglià, gli autori sono modesti riguardo all'ambito delle loro rivendicazioni:

• Riconoscono che i loro modelli dei motori configurabili sono "approssimazioni conservative" (sotto-approssimazioni) che non coprono tutte le funzionalità o i dettagli interni delle dimensioni delle code, il che significa che non possono provare garanzie sui tassi di perdita dei pacchetti in tutti gli scenari.
• Notano che, mentre il linguaggio P4 è standardizzato, i "motori configurabili" non lo sono, il che significa che le specifiche e le prove specifiche per applicazioni come il packet sampler non sono direttamente portabili ad altre architetture senza una nuova specificazione.
• Evidenziano che il processo di verifica può essere laborioso, in particolare per quanto riguarda le proprietà di inizializzazione e la gestione dei bit non inizializzati nei record P4.