Secure Conformance Checking using Token-based Replay and Homomorphic Encryption

1. Enunciato del Problema

Il controllo di conformità è un'operazione fondamentale nel process mining che confronta un registro eventi (comportamento effettivo) con un modello di processo (comportamento atteso) per identificare le deviazioni. Tradizionalmente, ciò richiede che sia il proprietario del modello che il proprietario del registro condividano i propri dati in chiaro con un analista di business.

Tuttavia, in scenari come la produzione su misura o le collaborazioni inter-organizzative, le parti spesso desiderano proteggere informazioni sensibili:

• I Proprietari del Modello potrebbero voler mantenere segreti i loro processi proprietari (ad esempio, flussi di lavoro produttivi).
• I Proprietari del Registro potrebbero voler proteggere dati sensibili di esecuzione (ad esempio, dettagli degli ordini dei clienti) dal proprietario del modello.

La sfida consiste nell'eseguire il controllo di conformità (nello specifico il replay basato su token) su dati cifrati senza rivelare il modello di processo sottostante o il registro eventi all'altra parte, mantenendo al contempo la capacità di calcolare metriche di adattamento (deviazioni).

2. Metodologia

Gli autori propongono un framework sicuro utilizzando la Crittografia Omomorfica (HE) e una riformulazione dell'algoritmo di replay basato su token mediante algebra lineare (operazioni su matrici e vettori).

Concetti Chiave

• Replay Basato su Token: Un algoritmo che "riproduce" le tracce del registro eventi su una rete di Petri. Tiene traccia dei token consumati, prodotti, mancanti (per abilitare le transizioni) e residui (rimasti alla fine).
• Crittografia Omomorfica (HE): Nello specifico, gli autori utilizzano Concrete di Zama (basato su TFHE), che supporta operazioni aritmetiche (addizione, sottrazione, moltiplicazione) e confronti (min/max) su interi cifrati senza decifrazione.
• Architettura Client-Server:
  • Client (Proprietario del Registro): Detiene il registro eventi. Cifra la marcatura corrente e il prossimo evento (transizione) da attivare. Invia questi dati al server.
  • Server (Proprietario del Modello): Detiene il modello della rete di Petri. Esegue il passo di replay sui dati cifrati utilizzando matrici precalcolate. Restituisce la nuova marcatura cifrata e i contatori locali.
  • Privacy: Il server non vede mai il registro in chiaro; il client non vede la struttura del modello in chiaro oltre a quanto deducibile dal replay.

Riformulazione Algoritmica

Per rendere il replay basato su token compatibile con l'HE, gli autori hanno sostituito il tradizionale "gioco dei token" (che si basa su logica condizionale e diramazioni) con moltiplicazione di matrici e operazioni vettoriali.

1. Precomputazione (Lato Server):

   • La rete di Petri viene convertita in una Matrice di Incidenza ($N$).
   • Viene costruita una Matrice di Dinamica ($E$) per rappresentare tutte le possibili "abilitazioni" (combinazioni di marcature correnti e transizioni).
   • Una Matrice di Sequenze di Attivazione ($S$) memorizza i vettori di Parikh (conteggi delle transizioni) per le sequenze di attivazione valide.
   • Una Matrice di Preset ($P$) memorizza i luoghi di ingresso per ogni transizione.

2. Passo di Replay (Esecuzione Sicura):

   • Controllo di Abilitazione: Il client invia la marcatura corrente cifrata ($M$) e il prossimo evento cifrato ($t$). Il server calcola un vettore selettore ($sel$) utilizzando la moltiplicazione di matrici: $E \cdot [M, t]^T$. Ciò determina se la transizione è abilitata direttamente o richiede transizioni silenziose ($\tau$).
   • Gestione dei Token Mancanti: Se la transizione non è abilitata, l'algoritmo calcola i "token mancanti" ($\pi$) richiesti dalla matrice di preset $P$.
   • Aggiornamento Unificato della Marcatura: Per evitare istruzioni condizionali if/else (che rivelano informazioni nell'HE), gli autori combinano la logica di "adattamento" e "non adattamento" in un'unica equazione:
     $$M' = (M + N \cdot \sigma^T) \cdot \text{sum}(sel) + (M + \pi^T + N \cdot t^T) \cdot (1 - \text{sum}(sel))$$
     Qui, $\text{sum}(sel)$ agisce come un interruttore binario (1 se abilitato, 0 se non abilitato).
   • Calcolo dei Contatori: L'algoritmo calcola i token mancanti ($m$), consumati ($c$), prodotti ($p$) e residui ($r$) utilizzando differenze vettoriali e mascheramento condizionale (moltiplicando per 0 o 1 in base all'interruttore).

3. Calcolo dell'Adattamento (Fitness):

   • Dopo aver elaborato tutti gli eventi in una traccia, il client decifra i contatori finali e calcola il punteggio di adattamento utilizzando la formula standard:
     $$f = \frac{1}{2}\left(1 - \frac{m}{c}\right) + \frac{1}{2}\left(1 - \frac{r}{p}\right)$$

3. Contributi Chiave

1. Primo Replay Basato su Token Sicuro: Questo è il primo lavoro ad applicare la crittografia omomorfica specificamente all'algoritmo di controllo di conformità basato su replay di token.
2. Riformulazione Basata su Matrici: Gli autori hanno trasformato con successo il gioco dei token non lineare e dipendente dallo stato in una formulazione algebrica lineare adatta alla crittografia omomorfica, eliminando la necessità di logica di diramazione.
3. Architettura che Preserva la Privacy: Un protocollo client-server in cui il proprietario del modello elabora tracce cifrate senza apprendere il contenuto della traccia, e il proprietario del registro non apprende nulla sulla struttura del modello oltre ai risultati del replay.
4. Implementazione e Valutazione: Un prototipo funzionante implementato in Python utilizzando il framework Concrete di Zama, che dimostra la fattibilità dell'approccio.

4. Risultati

Gli autori hanno valutato il prototipo utilizzando un registro eventi sintetico e un modello di rete di Petri (dal libro Process Mining e dai tutorial PM4Py).

• Prestazioni (Dati in Chiaro vs. Cifrati):
  • Dati in Chiaro (CLR): Il tempo di esecuzione era nell'ordine dei millisecondi.
  • Dati Cifrati (SEC): I tempi di esecuzione variavano da 7,8 a 15,8 secondi per tracce senza calcoli dei contatori di token.
  • Cifrati con Contatori (SEC+): I tempi di esecuzione variavano da 19,3 a 37,4 secondi.
• Insight sull'Ottimizzazione:
  • Una versione iniziale che calcolava i contatori ($p, c, m, r$) all'interno della funzione lato server richiedeva da 35 a 84 minuti.
  • Gli autori hanno identificato che questo rallentamento era dovuto al fatto che il compilatore HE (Concrete) utilizzava di default interi a 16 bit per i valori di ritorno, causando un sovraccarico massiccio. Spostando l'accumulo dei contatori lato client (decifrando i risultati intermedi), hanno ridotto il tempo a meno di 40 secondi.
• Scalabilità: Il metodo ha gestito con successo tracce di lunghezze variabili (da 4 a 13 eventi) e sia tracce adattate che non adattate.

5. Significato e Lavori Futuri

• Significato: Il documento dimostra che il controllo di conformità sicuro è praticamente fattibile. Consente alle organizzazioni di verificare la conformità dei processi (ad esempio, nelle catene di approvvigionamento o nell'assistenza sanitaria) senza compromettere segreti commerciali o la privacy dei pazienti. Il passaggio dalla logica di diramazione alle operazioni su matrici è un contributo teorico critico per l'applicazione dell'HE al process mining.
• Limitazioni:
  • Prestazioni: Sebbene sotto un minuto, l'esecuzione cifrata è significativamente più lenta rispetto ai dati in chiaro (di ordini di grandezza).
  • Inondazione di Token (Token Flooding): L'implementazione attuale non affronta pienamente il problema dell'"inondazione di token" (dove i luoghi accumulano >1 token) nel dominio cifrato.
  • Precisione: La dipendenza dalla precisione intera nei framework HE limita la complessità delle operazioni.
• Direzioni Future:
  • Test con registri eventi reali.
  • Affrontare l'inondazione di token nel dominio cifrato.
  • Esplorare altre piattaforme HE per ottimizzare il compromesso tra precisione e prestazioni.
  • Implementare una versione completa di rete client-server per analizzare i costi di comunicazione.

In conclusione, il documento fornisce una solida prova di concetto per il process mining sicuro, dimostrando che la crittografia omomorfica può essere efficacemente adattata a compiti algoritmici complessi come il replay basato su token attraverso una riformulazione algebrica.