Canonical Byte-String Encoding for Finite-Ring Cryptosystems

Titolo

Codifica Canonica Byte-String per Sistemi Crittografici su Anelli Finiti

1. Il Problema

I sistemi crittografici basati su anelli (ring-mapping cryptosystems), come quelli utilizzati nella crittografia omomorfica, nel calcolo multi-partito sicuro (MPC) e nelle primitive simmetriche su anelli interi, richiedono che i messaggi in chiaro siano rappresentati come elementi di un anello finito $\mathbb{Z}_m$ prima di subire qualsiasi trasformazione algebrica.

Il problema affrontato in questo lavoro è la mancanza di un metodo standardizzato e canonico per mappare dati binari arbitrari (stringhe di byte, inclusi testi UTF-8) in residui modulo $m$. Le soluzioni precedenti spesso si affidavano ad alfabeti costruiti manualmente o tabelle di simboli fisse, adatte solo per illustrazioni teoriche ma insufficienti per gestire dati binari generici in modo sicuro ed efficiente. Esiste quindi la necessità di un livello di rappresentazione robusto che garantisca:

• Una mappatura deterministica da byte a residui.
• La capacità di gestire stringhe di lunghezza variabile (fino a $2^{64}$ byte).
• La decodifica esatta e la tolleranza a suffissi validi aggiunti (self-delimiting).

2. Metodologia: Il Codec Base-$m$-len

Gli autori propongono un nuovo codec canonico denominato base-$m$-len. Questo sistema si basa su una transduzione uniforme dei byte e si ispira ai principi degli algoritmi ANS (Asymmetric Numeral Systems) e rANS di Duda, ma con un obiettivo diverso: non la compressione dell'entropia, ma la creazione di un formato di trasmissione auto-delimitante e deterministico.

La struttura del formato "wire" (trasmissione) è composta da tre parti:

1. Prefisso di Lunghezza (Fixed-width): Codifica la lunghezza in byte della stringa originale utilizzando $k$ cifre in base $m$, dove $k$ è il minimo intero tale che $m^k \ge 2^{64}$. Questo garantisce che qualsiasi lunghezza fino a $2^{64}$ possa essere rappresentata esattamente.
2. Prefisso di Stato (Fixed-width): Codifica lo stato finale del payload (il valore interno dell'algoritmo dopo l'elaborazione) utilizzando anch'esso $k$ cifre in base $m$.
3. Payload (Flusso di residui): Una sequenza di cifre in base $m$ prodotta da una transduzione uniforme. L'encoder elabora i byte in ordine inverso (da destra a sinistra), aggiornando uno stato interno $x$ con la formula $x \leftarrow 256x + b$ ed emettendo cifre modulo $m$ quando lo stato supera una soglia di normalizzazione. Il decoder legge il flusso in ordine FIFO (da sinistra a destra).

Algoritmo Chiave:

• Codifica: Calcola la lunghezza, inizializza lo stato, elabora i byte in reverse, emette cifre di normalizzazione, codifica lo stato finale e inverte l'ordine del payload emesso.
• Decodifica: Legge la lunghezza, legge lo stato iniziale, ricostruisce i byte uno per uno (estendendo lo stato con le cifre del payload quando necessario) e ignora qualsiasi cifra valida rimanente (suffisso).

3. Contributi Chiave

Il lavoro presenta tre contributi principali:

1. Definizione del Codec: Specifica un codec byte-to-residue parametrizzato dal modulo $m$, centrato sul formato wire base-$m$-len, che supporta stringhe di lunghezza inferiore a $2^{64}$.
2. Garanzie di Correttezza Formale: Dimostra matematicamente che la decodifica è esatta per tutti i moduli che soddisfano i vincoli del documento. Viene provato che:
   • L'inversione del prefisso a larghezza fissa è corretta.
   • I limiti dello stato del payload rimangono all'interno di finestre di normalizzazione sicure ($< 2^{64}$).
   • Il sistema è tollerante ai suffissi: se vengono aggiunte cifre valide alla fine del flusso, il decoder si ferma esattamente dopo aver ricostruito la lunghezza dichiarata, ignorando il resto.
3. Implementazione e Verifica:
   • Rust: Una libreria di riferimento (sym-adv-encoding) con implementazioni ottimizzate per la codifica e decodifica di byte e testo UTF-8.
   • Lean 4: Una formalizzazione completa della specifica astratta con prove verificate dalla macchina. Questo include la definizione dei parametri, la logica di transduzione e le proprietà di correttezza del flusso end-to-end.

4. Risultati e Valutazione

L'articolo include un'analisi di complessità e benchmark prestazionali eseguiti su hardware Apple M3 Pro.

• Complessità: Sia la codifica che la decodifica sono lineari rispetto alla lunghezza del flusso ($O(n)$) e richiedono uno stato di lavoro costante ($O(1)$) oltre ai buffer di input/output.
• Costo di Rappresentazione:
  • Il numero di cifre di payload per byte è approssimativamente $\log_m 256$. Moduli più grandi riducono questo costo (avvicinandosi a 1 cifra per byte per $m \approx 257$).
  • L'overhead fisso è dato dai due prefissi ($2k$ cifre). Per $m=257$, $k=16$, risultando in un header di 32 cifre.
• Prestazioni (Throughput):
  • La costruzione nativa in Rust è significativamente più veloce rispetto alle conversioni di radix esatte basate su BigUint (che sono lente su input grandi).
  • Ad esempio, per $m=257$, la codifica di 64 KiB raggiunge circa 236.7 MiB/s, mentre la decodifica tocca 669.1 MiB/s.
  • Il codec è competitivo con i riferimenti ANS generici, pur fornendo funzionalità specifiche per la crittografia ad anello (gestione esplicita della lunghezza).

5. Significato e Implicazioni

Questo lavoro è significativo per l'ecosistema della crittografia moderna per diversi motivi:

• Strato di Rappresentazione Standardizzato: Fornisce un componente fondamentale per protocolli che operano su $\mathbb{Z}_m$, risolvendo il problema della serializzazione dei dati in modo sicuro e verificabile.
• Verifica Formale: L'uso di Lean 4 per provare la correttezza dell'implementazione astratta offre un livello di affidabilità superiore rispetto alla sola verifica tramite test, riducendo il rischio di errori di implementazione in contesti crittografici.
• Flessibilità: La tolleranza ai suffissi permette di concatenare flussi o gestire dati aggiuntivi senza corrompere la decodifica del messaggio originale, una proprietà utile in protocolli di rete complessi.
• Limitazioni di Sicurezza: Gli autori sottolineano che il codec è puramente un meccanismo di serializzazione deterministica. Non fornisce confidenzialità, integrità o autenticità; queste proprietà devono essere garantite dal protocollo crittografico che lo circonda. Inoltre, espone la lunghezza esatta del messaggio, richiedendo padding a livello di protocollo se è necessaria l'occultamento della lunghezza.

In conclusione, il codec base-$m$-len colma un gap pratico nella crittografia su anelli finiti, offrendo una soluzione efficiente, formalmente verificata e pronta per l'uso reale, che può essere integrata direttamente in progetti come SYMPZON e altri schemi di crittografia omomorfica o MPC.