Resumo Técnico: Verificação Formal de Segurança contra Probing via Independência Condicional

Declaração do Problema

Ataques de canal lateral representam uma ameaça significativa à segurança de esquemas criptográficos, motivando a adoção generalizada de mascaramento como contramedida. O mascaramento divide valores secretos em compartilhamentos para garantir que o vazamento de qualquer subconjunto de valores intermediários não revele o segredo subjacente. No entanto, provar a segurança de algoritmos mascarados, particularmente sob o modelo de probing ISW (onde um adversário pode sondar até $t$ valores intermediários), é notoriamente propenso a erros quando realizado manualmente. Diversas falhas foram identificadas em provas de segurança manuais, tornando necessária a verificação formal.

Embora a lógica de separação probabilística tenha sido aplicada com sucesso para verificar propriedades como independência de entrada (por exemplo, em one-time pads), ela ainda não foi utilizada para verificar a segurança contra probing (especificamente a não-interferência $t$) de algoritmos mascarados. Ferramentas existentes de verificação formal frequentemente dependem de métodos baseados em substituição ou inferência de tipos, que podem carecer da modularidade ou expressividade necessárias para o raciocínio condicional complexo inerente ao mascaramento.

Metodologia

Este trabalho propõe uma abordagem inovadora para a verificação formal, estabelecendo uma conexão rigorosa entre definições de segurança baseadas em simuladores e independência condicional. A metodologia baseia-se no Lilac, uma lógica de separação probabilística projetada para raciocinar sobre independência condicional.

1. Fundamento Teórico: Simuladores e Independência Condicional

Os autores reformulam a definição padrão de não-interferência baseada em simuladores em termos de independência condicional.

• Visão baseada em simuladores: Um algoritmo mascarado é seguro se, para qualquer conjunto de sondas $O$ (observado por um adversário), existir um simulador capaz de gerar a distribuição de $O$ usando apenas um subconjunto de compartilhamentos de entrada $I$, sem acesso aos demais compartilhamentos secretos.
• Visão de independência condicional: Este requisito de segurança é equivalente à afirmação de que os valores observados $O$ são condicionalmente independentes dos compartilhamentos de entrada secretos ($\Delta \setminus I$) dados os compartilhamentos de entrada públicos $I$. Formalmente, isso é expresso como $O \perp (\Delta \setminus I) \mid I$.

O artigo demonstra que essa equivalência vale dentro do framework semântico do Lilac, que modela independência probabilística usando combinações independentes de espaços de probabilidade e condicionamento via desagregação.

2. Extensão do Lilac

Para aplicar o Lilac à segurança contra probing, os autores estendem a lógica com regras de prova específicas que não estavam presentes na formulação original do Lilac:

• Axiomas Semi-Graphoid: O artigo prova que os axiomas semi-graphoid para independência condicional (Simetria, Decomposição, União Fraca e Contração) valem na semântica do Lilac. Esses axiomas são cruciais para manipular afirmações de independência condicional durante as provas.
• Regras de Composabilidade: Novas regras são introduzidas para lidar com a composição de propriedades de não-interferência, especificamente para composição sequencial e loops for. Essas regras permitem a verificação modular de algoritmos complexos construídos a partir de gadgets menores.
• Propriedade e Enfraquecimento: Regras adicionais facilitam o raciocínio sobre a propriedade de variáveis aleatórias e o enfraquecimento de propriedades de não-interferência ao lidar com entradas não compartilhadas ou subconjuntos de variáveis.

3. Framework de Verificação

O processo de verificação envolve:

1. Traduzir algoritmos mascarados (escritos na linguagem de programação probabilística APPL) em triplas de Hoare dentro do Lilac.
2. Utilizar a equivalência estabelecida (Teorema V.1) para reduzir a verificação da não-interferência $(I, O)$ à prova de uma tripla de Hoare específica de independência condicional:
   $$\{ \text{own } \Delta \} \ M \ \{ Y. \ C_{x \leftarrow I}(\text{own}(\Delta \setminus I) * \text{own } O) \}$$
3. Aplicar o conjunto estendido de regras de prova (incluindo as novas regras semi-graphoid e de composabilidade) para derivar as implicações necessárias.

Contribuições Principais

1. Conexão Formal: O artigo estabelece uma equivalência formal entre definições de segurança contra probing baseadas em simuladores e propriedades de independência condicional expressáveis no Lilac. Isso preenche a lacuna entre noções de segurança criptográfica e lógica de separação probabilística.
2. Extensão do Lilac: Os autores fornecem um conjunto de regras de prova adicionais necessárias para verificar algoritmos mascarados, incluindo os axiomas semi-graphoid para independência condicional e regras de composabilidade para composição sequencial e loops.
3. Estudos de Caso: A eficácia da abordagem é demonstrada pela verificação formal da segurança contra probing de três algoritmos críticos usando o Lilac:
   • MINIADDREPNOISE: Uma sub-rotina para adicionar ruído uniforme a valores mascarados.
   • REFRESH: Um algoritmo fundamental para refrescar compartilhamentos, prevenindo o acúmulo de vazamentos.
   • SECMULT: Um algoritmo padrão de multiplicação mascarada.
   • ADDREPNOISEER: Uma variante usada no esquema de assinatura Raccoon (um candidato para a padronização de Criptografia Pós-Quântica do NIST), provando que ele satisfaz a propriedade de Não-Interferência Forte $t$ com Entrada Não Compartilhada ($t$-SNIU).

Resultados

O artigo deriva com sucesso triplas de Hoare para os algoritmos-alvo, confirmando suas propriedades de não-interferência.

• Para MINIADDREPNOISE, a prova mostra que os compartilhamentos de saída são condicionalmente independentes dos compartilhamentos de entrada não observados, dados os inputs observados.
• Para REFRESH, a prova verifica que o algoritmo satisfaz a Não-Interferência Forte $t$ ($t$-SNI), uma propriedade mais forte que a não-interferência padrão, essencial para a composabilidade em mascaramento de ordem superior.
• Para SECMULT e ADDREPNOISEER, as provas aproveitam as novas regras de composabilidade para lidar com os loops aninhados e dependências de dados complexas inerentes a esses algoritmos.

A verificação de ADDREPNOISEER é particularmente significativa, pois valida um componente chave da prova de segurança do esquema de assinatura Raccoon, que depende da propriedade $t$-SNIU.

Significado e Alegações

Os autores afirmam que este trabalho fornece a primeira aplicação de lógica de separação probabilística (especificamente o Lilac) à verificação formal de segurança contra probing para algoritmos mascarados. Ao traduzir provas de segurança em raciocínio de independência condicional, a abordagem oferece uma alternativa modular e logicamente rigorosa às ferramentas existentes baseadas em substituição ou inferência de tipos.

O artigo enfatiza que, embora a ideia subjacente de conectar simuladores à independência condicional seja conceitualmente simples, sua formalização no Lilac é tecnicamente não trivial devido à dependência da lógica em combinações independentes em vez de espaços de probabilidade de produto padrão. A derivação bem-sucedida do teorema principal e a aplicação a componentes criptográficos do mundo real (Raccoon) demonstram que este framework é viável para verificar esquemas complexos de mascaramento de alta ordem.

O trabalho mantém-se modesto quanto ao seu escopo, observando que os resultados atuais são limitados ao cenário de teoria da informação da segurança contra probing. Os autores identificam a extensão da abordagem para o cenário computacional e a implementação do método em um provador de teoremas interativo como direções importantes para trabalhos futuros. Eles também sugerem que o framework poderia ser aplicado a outras propriedades de segurança baseadas em simuladores, como as encontradas em computação segura multipartidária.