Secure Conformance Checking using Token-based Replay and Homomorphic Encryption

1. Declaração do Problema

A verificação de conformidade é uma operação central na mineração de processos que compara um registro de eventos (comportamento real) contra um modelo de processo (comportamento esperado) para identificar desvios. Tradicionalmente, isso exige que tanto o proprietário do modelo quanto o proprietário do registro compartilhem seus dados em texto claro com um analista de negócios.

No entanto, em cenários como manufatura sob medida ou colaborações interorganizacionais, as partes frequentemente desejam proteger informações sensíveis:

• Proprietários de Modelos podem querer manter seu lógica de processo proprietária (por exemplo, fluxos de trabalho de produção) em segredo.
• Proprietários de Registros podem querer proteger dados de execução sensíveis (por exemplo, detalhes de pedidos de clientes) do proprietário do modelo.

O desafio é realizar a verificação de conformidade (especificamente o replay baseado em tokens) sobre dados criptografados sem revelar o modelo de processo subjacente ou o registro de eventos à outra parte, mantendo a capacidade de calcular métricas de adequação (desvios).

2. Metodologia

Os autores propõem um framework seguro usando Criptografia Homomórfica (HE) e uma reformulação do algoritmo de replay baseado em tokens usando álgebra linear (operações de matriz e vetor).

Conceitos Principais

• Replay Baseado em Tokens: Um algoritmo que "reproduz" traços de registro de eventos em uma Rede de Petri. Ele rastreia tokens consumidos, produzidos, faltantes (para habilitar transições) e remanescentes (sobrantes no final).
• Criptografia Homomórfica (HE): Especificamente, os autores utilizam o Concrete da Zama (baseado em TFHE), que suporta operações aritméticas (adição, subtração, multiplicação) e comparações (mínimo/máximo) em inteiros criptografados sem descriptografia.
• Arquitetura Cliente-Servidor:
  • Cliente (Proprietário do Registro): Segura o registro de eventos. Criptografa a marcação atual e o próximo evento (transição) a ser disparado. Envia estes ao servidor.
  • Servidor (Proprietário do Modelo): Segura o modelo da Rede de Petri. Realiza o passo de replay sobre dados criptografados usando matrizes pré-calculadas. Retorna a nova marcação criptografada e contadores locais.
  • Privacidade: O servidor nunca vê o registro em texto claro; o cliente nunca vê a estrutura do modelo em texto claro além do que é inferido a partir do replay.

Reformulação Algorítmica

Para tornar o replay baseado em tokens compatível com HE, os autores substituíram o tradicional "jogo de tokens" (que depende de lógica condicional e ramificação) por multiplicação de matrizes e operações vetoriais.

1. Pré-cálculo (Lado do Servidor):

   • A Rede de Petri é convertida em uma Matriz de Incidência ($N$).
   • Uma Matriz de Dinâmica ($E$) é construída para representar todas as possíveis "habilitações" (combinações de marcações atuais e transições).
   • Uma Matriz de Sequências de Disparo ($S$) armazena os vetores de Parikh (contagens de transições) para sequências de disparo válidas.
   • Uma Matriz de Pré-ajuste ($P$) armazena os lugares de entrada para cada transição.

2. Passo de Replay (Execução Segura):

   • Verificação de Habilitação: O cliente envia a marcação atual criptografada ($M$) e o próximo evento criptografado ($t$). O servidor calcula um vetor seletor ($sel$) usando multiplicação de matriz: $E \cdot [M, t]^T$. Isso determina se a transição está habilitada diretamente ou requer transições silenciosas ($\tau$).
   • Tratamento de Tokens Faltantes: Se a transição não estiver habilitada, o algoritmo calcula os "tokens faltantes" ($\pi$) necessários a partir da matriz de pré-ajuste $P$.
   • Atualização Unificada de Marcação: Para evitar declarações condicionais if/else (que vazam informações em HE), os autores combinam a lógica de "adequado" e "inadequado" em uma única equação:
     $$M' = (M + N \cdot \sigma^T) \cdot \text{sum}(sel) + (M + \pi^T + N \cdot t^T) \cdot (1 - \text{sum}(sel))$$
     Aqui, $\text{sum}(sel)$ atua como um interruptor binário (1 se habilitado, 0 se não).
   • Cálculo de Contadores: O algoritmo calcula tokens faltantes ($m$), consumidos ($c$), produzidos ($p$) e remanescentes ($r$) usando diferenças vetoriais e mascaramento condicional (multiplicando por 0 ou 1 com base no interruptor).

3. Cálculo de Adequação:

   • Após processar todos os eventos em um traço, o cliente descriptografa os contadores finais e calcula a pontuação de adequação usando a fórmula padrão:
     $$f = \frac{1}{2}\left(1 - \frac{m}{c}\right) + \frac{1}{2}\left(1 - \frac{r}{p}\right)$$

3. Contribuições Principais

1. Primeiro Replay Baseado em Tokens Seguro: Este é o primeiro trabalho a aplicar criptografia homomórfica especificamente ao algoritmo de verificação de conformidade de replay baseado em tokens.
2. Reformulação Baseada em Matrizes: Os autores transformaram com sucesso o jogo de tokens não linear e dependente de estado em uma formulação algébrica linear adequada para criptografia homomórfica, eliminando a necessidade de lógica de ramificação.
3. Arquitetura de Preservação de Privacidade: Um protocolo cliente-servidor onde o proprietário do modelo processa traços criptografados sem aprender o conteúdo do traço, e o proprietário do registro não aprende nada sobre a estrutura do modelo além dos resultados do replay.
4. Implementação e Avaliação: Um protótipo funcional implementado em Python usando o framework Concrete da Zama, demonstrando a viabilidade da abordagem.

4. Resultados

Os autores avaliaram o protótipo usando um registro de eventos sintético e um modelo de Rede de Petri (do livro Process Mining e tutoriais do PM4Py).

• Desempenho (Claro vs. Criptografado):
  • Dados Claros (CLR): O tempo de execução foi em milissegundos.
  • Dados Criptografados (SEC): Os tempos de execução variaram de 7,8 a 15,8 segundos para traços sem cálculos de contadores de tokens.
  • Criptografado com Contadores (SEC+): Os tempos de execução variaram de 19,3 a 37,4 segundos.
• Insights de Otimização:
  • Uma versão inicial que calculava contadores ($p, c, m, r$) dentro da função do lado do servidor levou de 35 a 84 minutos.
  • Os autores identificaram que essa lentidão era devida ao compilador HE (Concrete) padrão usando inteiros de 16 bits para valores de retorno, causando sobrecarga massiva. Ao mover a acumulação de contadores para o lado do cliente (descriptografando resultados intermediários), reduziram o tempo para menos de 40 segundos.
• Escalabilidade: O método lidou com sucesso com traços de comprimentos variados (4 a 13 eventos) e tanto traços adequados quanto inadequados.

5. Significado e Trabalho Futuro

• Significado: O artigo prova que a verificação de conformidade segura é praticamente viável. Permite que organizações verifiquem a conformidade de processos (por exemplo, em cadeias de suprimentos ou saúde) sem comprometer segredos comerciais ou a privacidade dos pacientes. A mudança da lógica de ramificação para operações de matriz é uma contribuição teórica crítica para aplicar HE à mineração de processos.
• Limitações:
  • Desempenho: Embora abaixo de um minuto, a execução criptografada é significativamente mais lenta que o texto claro (ordens de magnitude).
  • Inundação de Tokens: A implementação atual não aborda completamente o problema de "inundação de tokens" (onde lugares acumulam >1 token) no domínio criptografado.
  • Precisão: A dependência de precisão inteira em frameworks HE limita a complexidade das operações.
• Direções Futuras:
  • Testes com registros de eventos do mundo real.
  • Abordar a inundação de tokens no domínio criptografado.
  • Explorar outras plataformas HE para otimizar o compromisso entre precisão e desempenho.
  • Implementar uma versão completa de rede cliente-servidor para analisar custos de comunicação.

Em conclusão, o artigo fornece uma prova de conceito robusta para mineração de processos segura, demonstrando que a criptografia homomórfica pode ser efetivamente adaptada a tarefas algorítmicas complexas como o replay baseado em tokens através de reformulação algébrica.