Secure Conformance Checking using Token-based Replay and Homomorphic Encryption

1. Énoncé du problème

La vérification de conformité est une opération centrale dans l'exploration de processus (process mining) qui compare un journal d'événements (comportement réel) à un modèle de processus (comportement attendu) pour identifier les écarts. Traditionnellement, cela nécessite que le propriétaire du modèle et le propriétaire du journal partagent leurs données en clair avec un analyste d'affaires.

Cependant, dans des scénarios tels que la fabrication sur mesure ou les collaborations inter-organisationnelles, les parties souhaitent souvent protéger des informations sensibles :

• Les propriétaires de modèles peuvent souhaiter garder leur logique de processus propriétaire (par exemple, les flux de travail de production) secrète.
• Les propriétaires de journaux peuvent souhaiter protéger les données d'exécution sensibles (par exemple, les détails des commandes clients) du propriétaire du modèle.

Le défi consiste à effectuer une vérification de conformité (spécifiquement la rejouissance basée sur les jetons) sur des données chiffrées sans révéler le modèle de processus sous-jacent ou le journal d'événements à l'autre partie, tout en conservant la capacité de calculer des métriques de fitness (écarts).

2. Méthodologie

Les auteurs proposent un cadre sécurisé utilisant le chiffrement homomorphe (HE) et une reformulation de l'algorithme de rejouissance basée sur les jetons utilisant l'algèbre linéaire (opérations matricielles et vectorielles).

Concepts de base

• Rejouissance basée sur les jetons : Un algorithme qui « rejoue » les traces du journal d'événements sur un réseau de Petri. Il suit les jetons consommés, produits, manquants (pour permettre les transitions) et restants (excédentaires à la fin).
• Chiffrement homomorphe (HE) : Plus précisément, les auteurs utilisent Concrete de Zama (basé sur TFHE), qui prend en charge les opérations arithmétiques (addition, soustraction, multiplication) et les comparaisons (min/max) sur des entiers chiffrés sans déchiffrement.
• Architecture client-serveur :
  • Client (propriétaire du journal) : Détient le journal d'événements. Chiffre le marquage actuel et l'événement suivant (transition) à déclencher. Envoie ces éléments au serveur.
  • Serveur (propriétaire du modèle) : Détient le modèle de réseau de Petri. Effectue l'étape de rejouissance sur des données chiffrées en utilisant des matrices précalculées. Retourne le nouveau marquage chiffré et les compteurs locaux.
  • Confidentialité : Le serveur ne voit jamais le journal en clair ; le client ne voit jamais la structure du modèle en clair au-delà de ce qui est déduit de la rejouissance.

Reformulation algorithmique

Pour rendre la rejouissance basée sur les jetons compatible avec le HE, les auteurs ont remplacé le « jeu de jetons » traditionnel (qui repose sur une logique conditionnelle et des branchements) par des multiplications matricielles et des opérations vectorielles.

1. Précalcul (côté serveur) :

   • Le réseau de Petri est converti en une matrice d'incidence ($N$).
   • Une matrice de dynamique ($E$) est construite pour représenter toutes les « autorisations » possibles (combinaisons de marquages actuels et de transitions).
   • Une matrice de séquences de déclenchement ($S$) stocke les vecteurs de Parikh (comptages de transitions) pour les séquences de déclenchement valides.
   • Une matrice de préensemble ($P$) stocke les places d'entrée pour chaque transition.

2. Étape de rejouissance (exécution sécurisée) :

   • Vérification d'autorisation : Le client envoie le marquage actuel chiffré ($M$) et l'événement suivant chiffré ($t$). Le serveur calcule un vecteur sélecteur ($sel$) en utilisant une multiplication matricielle : $E \cdot [M, t]^T$. Cela détermine si la transition est autorisée directement ou si elle nécessite des transitions silencieuses ($\tau$).
   • Gestion des jetons manquants : Si la transition n'est pas autorisée, l'algorithme calcule les « jetons manquants » ($\pi$) requis à partir de la matrice de préensemble $P$.
   • Mise à jour unifiée du marquage : Pour éviter les instructions conditionnelles if/else (qui fuient des informations dans le HE), les auteurs combinent la logique « conforme » et « non conforme » en une seule équation :
     $$M' = (M + N \cdot \sigma^T) \cdot \text{sum}(sel) + (M + \pi^T + N \cdot t^T) \cdot (1 - \text{sum}(sel))$$
     Ici, $\text{sum}(sel)$ agit comme un interrupteur binaire (1 si autorisé, 0 sinon).
   • Calcul des compteurs : L'algorithme calcule les jetons manquants ($m$), consommés ($c$), produits ($p$) et restants ($r$) en utilisant des différences vectorielles et un masquage conditionnel (multiplication par 0 ou 1 basé sur l'interrupteur).

3. Calcul du score de fitness :

   • Après avoir traité tous les événements d'une trace, le client déchiffre les compteurs finaux et calcule le score de fitness en utilisant la formule standard :
     $$f = \frac{1}{2}\left(1 - \frac{m}{c}\right) + \frac{1}{2}\left(1 - \frac{r}{p}\right)$$

3. Contributions clés

1. Première rejouissance basée sur les jetons sécurisée : Il s'agit du premier travail appliquant spécifiquement le chiffrement homomorphe à l'algorithme de vérification de conformité par rejouissance basée sur les jetons.
2. Reformulation basée sur les matrices : Les auteurs ont transformé avec succès le jeu de jetons non linéaire et dépendant de l'état en une formulation algébrique linéaire adaptée au chiffrement homomorphe, éliminant le besoin de logique de branchement.
3. Architecture préservant la vie privée : Un protocole client-serveur où le propriétaire du modèle traite des traces chiffrées sans apprendre le contenu de la trace, et où le propriétaire du journal n'apprend rien sur la structure du modèle au-delà des résultats de la rejouissance.
4. Implémentation et évaluation : Un prototype fonctionnel implémenté en Python utilisant le framework Concrete de Zama, démontrant la faisabilité de l'approche.

4. Résultats

Les auteurs ont évalué le prototype en utilisant un journal d'événements synthétique et un modèle de réseau de Petri (issu du livre Process Mining et des tutoriels PM4Py).

• Performance (Clair vs Chiffré) :
  • Données claires (CLR) : Le temps d'exécution était de l'ordre de la milliseconde.
  • Données chiffrées (SEC) : Les temps d'exécution variaient de 7,8 à 15,8 secondes pour des traces sans calculs de compteurs de jetons.
  • Chiffré avec compteurs (SEC+) : Les temps d'exécution variaient de 19,3 à 37,4 secondes.
• Insights sur l'optimisation :
  • Une version initiale qui calculait les compteurs ($p, c, m, r$) à l'intérieur de la fonction côté serveur prenait 35 à 84 minutes.
  • Les auteurs ont identifié que ce ralentissement était dû au compilateur HE (Concrete) utilisant par défaut des entiers de 16 bits pour les valeurs de retour, causant une surcharge massive. En déplaçant l'accumulation des compteurs côté client (déchiffrant les résultats intermédiaires), ils ont réduit le temps à moins de 40 secondes.
• Évolutivité : La méthode a géré avec succès des traces de longueurs variables (4 à 13 événements) et des traces conformes et non conformes.

5. Importance et travaux futurs

• Importance : L'article prouve que la vérification de conformité sécurisée est pratiquement réalisable. Il permet aux organisations de vérifier la conformité des processus (par exemple, dans les chaînes d'approvisionnement ou les soins de santé) sans compromettre les secrets commerciaux ou la vie privée des patients. Le passage de la logique de branchement aux opérations matricielles est une contribution théorique critique pour l'application du HE à l'exploration de processus.
• Limitations :
  • Performance : Bien que sous la minute, l'exécution chiffrée est considérablement plus lente que le clair (de plusieurs ordres de grandeur).
  • Inondation de jetons : L'implémentation actuelle ne résout pas pleinement le problème de « l'inondation de jetons » (où les places accumulent >1 jeton) dans le domaine chiffré.
  • Précision : La dépendance à la précision des entiers dans les frameworks HE limite la complexité des opérations.
• Directions futures :
  • Tests avec des journaux d'événements réels.
  • Résolution de l'inondation de jetons dans le domaine chiffré.
  • Exploration d'autres plateformes HE pour optimiser le compromis entre précision et performance.
  • Implémentation d'une version complète de réseau client-serveur pour analyser les coûts de communication.

En conclusion, l'article fournit une preuve de concept robuste pour l'exploration de processus sécurisée, démontrant que le chiffrement homomorphe peut être efficacement adapté à des tâches algorithmiques complexes comme la rejouissance basée sur les jetons grâce à une reformulation algébrique.