Proving Circuit Functional Equivalence in Zero Knowledge

O artigo apresenta o ZK-CEC, o primeiro framework de verificação formal de hardware com privacidade que utiliza provas de conhecimento zero para garantir a equivalência funcional de IPs proprietários em relação a especificações públicas sem revelar o design subjacente.

O essencial

Imagine que você é um chef de cozinha famoso (o Fornecedor de IP) que criou uma receita secreta e incrível para um prato novo. Você quer vender essa receita para um grande restaurante (o Integrador do Sistema), mas tem um problema:

1. Se você mostrar a receita inteira, o restaurante pode roubá-la e copiá-la.
2. Se você não mostrar nada, o restaurante tem medo de que você esteja tentando vender uma receita falsificada ou que tenha escondido um ingrediente estranho (como uma "bomba" ou um bug) que vai explodir na cozinha.

Como resolver esse impasse? Como provar que a receita é perfeita e segura sem revelar os ingredientes secretos?

É exatamente isso que o artigo "Provar a Equivalência Funcional de Circuitos em Conhecimento Zero" (ZK-CEC) propõe.

Aqui está a explicação simplificada, usando analogias do dia a dia:

1. O Problema: A Desconfiança na Cadeia de Suprimentos

Hoje, quase todos os chips de computador são feitos juntando peças de diferentes fabricantes. Isso é eficiente, mas perigoso. Um fabricante mal-intencionado pode colocar um "Cavalo de Troia" (um vírus de hardware) no chip, ou um comprador pode tentar roubar a tecnologia.

As soluções antigas eram como pedir para o chef cozinhar o prato na frente do cliente para provar que é bom. O problema? O cliente só vê o prato pronto (simulação). Se o chef escondeu um veneno que só aparece em uma situação muito específica (um "caso de canto"), o cliente nunca vai notar.

2. A Solução: A Mágica do "Conhecimento Zero"

Os autores criaram um novo método chamado ZK-CEC. Pense nele como um truque de mágica matemática.

O objetivo é provar que a "receita secreta" (o chip do fornecedor) funciona exatamente igual a uma "receita padrão pública" (a especificação que o comprador quer), sem nunca mostrar os ingredientes secretos.

3. A Analogia do Quebra-Cabeça Secreto

Imagine que a receita secreta é um quebra-cabeça gigante e complexo.

• O Fornecedor tem as peças secretas.
• O Comprador tem o desenho da caixa (a especificação pública) e quer saber se as peças do fornecedor formam exatamente aquele desenho.

O Truque:
Em vez de mostrar as peças, o fornecedor monta o quebra-cabeça dentro de uma caixa de vidro inquebrável e trancada. Ele então prova matematicamente que, se você tentar montar o desenho da caixa com as peças lá dentro, é impossível que elas fiquem diferentes do desenho.

Se fosse possível que elas ficassem diferentes, significaria que o chip tem um erro ou um truque. Como o fornecedor prova que é impossível que haja diferença, o comprador fica convencido de que o chip é perfeito, sem nunca ver as peças.

4. O Desafio da "Falsa Prova" (O Pulo do Gato)

O artigo descobre um problema nas técnicas antigas de mágica (chamadas ZKUNSAT). Se o mágico (fornecedor) pudesse inventar a própria regra do jogo, ele poderia dizer: "Olhe, eu provei que meu truque secreto funciona!" mas na verdade ele estaria provando algo falso sobre um truque que ele inventou na hora.

Para resolver isso, os autores criaram um Novo Plano (Blueprint):

• Eles dividem a prova em duas partes: a parte pública (o que o comprador conhece) e a parte secreta (o chip).
• Eles criam regras rígidas para garantir que a parte secreta não seja "colada" de qualquer jeito. É como se o mágico tivesse que provar que a caixa de vidro está vazia antes de colocar o quebra-cabeça, e que as peças não têm cores estranhas escondidas.

5. O Resultado: Rápido e Eficiente

Os autores testaram essa ideia em computadores reais. Eles provaram que é possível verificar chips complexos (como os usados em criptografia de segurança) em um tempo razoável.

• Sem o truque: Verificar tudo manualmente levaria anos ou exigiria ver a receita secreta.
• Com o ZK-CEC: A verificação é feita em segundos ou minutos, e o segredo permanece seguro.

Resumo em uma Frase

O ZK-CEC é como um selo de garantia matemático que permite a um vendedor provar que seu produto secreto é perfeito e seguro, sem nunca precisar abrir a caixa e mostrar o que tem dentro, resolvendo o impasse entre quem vende e quem compra na indústria de chips.

Por que isso importa?
Isso permite que a tecnologia avance mais rápido, com mais segurança e sem medo de roubo de propriedade intelectual, criando confiança onde antes só havia desconfiança.

Resumo técnico

1. Problema e Motivação

O ecossistema moderno de Circuitos Integrados (IC) depende cada vez mais da integração de Propriedade Intelectual de Terceiros (3PIP). Isso cria um "impasse de confiança":

• Riscos de Segurança: Vendedores maliciosos podem inserir Hardware Trojans, backdoors ou bugs intencionais nos IPs.
• Privacidade de IP: Se o comprador exigir transparência total para verificar o design, o vendedor corre o risco de ter sua propriedade intelectual (IP) pirateada.

Limitações das Soluções Atuais:

• Métodos existentes de verificação de hardware com privacidade são baseados em simulação (usando Criptografia Homomórfica ou ZKVMs). A simulação não oferece garantias formais exaustivas e pode falhar em detectar Trojans que só são ativados em condições raras ou específicas.
• Métodos de Verificação Formal (como Combinational Equivalence Checking - CEC) oferecem garantias matemáticas, mas as abordagens atuais de prova em conhecimento zero (ZKP) para verificação formal (como o ZKUNSAT) exigem que a fórmula lógica seja pública. Se a fórmula for tratada como entrada secreta nesses protocolos, a sonoridade (soundness) é comprometida, permitindo que um provador malicioso prove propriedades sobre uma fórmula forjada.

2. Metodologia Proposta: ZK-CEC

Os autores propõem o ZK-CEC, o primeiro framework de verificação formal de hardware com privacidade, que combina verificação formal e provas de conhecimento zero (ZKP).

2.1. O Dilema e a Solução (Blueprint)

O artigo identifica que o protocolo ZKUNSAT (estado da arte para provar insatisfiabilidade em ZKP) falha quando a fórmula é secreta, pois o verificador não pode garantir que a fórmula secreta representa o sistema real.

Para resolver isso, os autores propõem um Blueprint (Modelo Geral) para verificação de propriedades com fórmulas secretas:

1. Divisão da Fórmula: A fórmula total é dividida em duas partes:
   • $\Phi_{sys}$ (Sistema): Mantido secreto pelo vendedor (o IP).
   • $\Phi_{prop}$ (Propriedade): Mantido público pelo comprador (a especificação).
2. Objetivo: Provar que a conjunção $\Phi_{sys} \land \Phi_{prop}$ é insatisfiável (UNSAT). Isso significa que não existe nenhuma entrada que faça o sistema secreto violar a propriedade pública.
3. Garantias de Sonoridade: Para evitar fraudes, o protocolo verifica três propriedades adicionais:
   • A propriedade pública é correta e satisfiável.
   • O sistema secreto é satisfiável (não contém contradições internas).
   • As variáveis do sistema secreto e da propriedade pública são isoladas, exceto na interface definida (variáveis de entrada/saída).

2.2. O Protocolo ZK-CEC

O protocolo verifica a equivalência funcional entre um circuito de implementação secreto ($C_{impl}$) e uma especificação pública ($C_{spec}$) provando que o circuito miter (que compara as saídas) é insatisfiável. O protocolo é composto por quatro sub-protocolos baseados em aritmetização sobre um campo finito e compromissos VOLE (Vector Oblivious Linear Evaluation):

1. $\Pi_{P1}$ (Verificação da Propriedade Pública): O verificador confirma que a fórmula pública ($\Phi_{pub}$) corresponde à especificação e à estrutura do circuito miter, garantindo que ela é satisfiável.
2. $\Pi_{P2}$ (Prova de Insatisfiabilidade): Baseado no ZKUNSAT, prova que o circuito miter completo é insatisfiável. Utiliza uma memória de leitura apenas (ROM) em ZK para verificar a cadeia de derivação de resolução (refutação).
3. $\Pi_{P3}$ (Prova de Satisfiabilidade do Secreto): O provador demonstra que o sistema secreto ($\Phi_{sec}$) é satisfiável (ou seja, é um circuito válido e não contém contradições internas) sem revelar a atribuição de variáveis.
4. $\Pi_{P4}$ (Isolamento de Variáveis): Garante que as variáveis secretas e públicas não se sobrepõem indevidamente, exceto na interface definida, impedindo que o provador "esconda" contradições em variáveis não compartilhadas.

2.3. Otimização

Os autores introduzem uma otimização de compressão de resolventes. Em vez de armazenar todos os passos intermediários da prova de refutação, apenas os "cláusulas aprendidas" (learned clauses) são armazenados. Isso reduz o tamanho da prova e o tempo de verificação, com uma análise de vazamento de informação (leakage) mostrando que a reconstrução da fórmula original pelo verificador permanece computacionalmente inviável (complexidade fatorial).

3. Contribuições Principais

1. Primeiro Framework de Verificação Formal Privada: Introdução do ZK-CEC, que permite provar a equivalência funcional de um IP secreto com uma especificação pública sem revelar o design.
2. Blueprint Geral: Proposição de um modelo para verificação de propriedades com fórmulas secretas, resolvendo o problema de sonoridade do ZKUNSAT ao separar o sistema da propriedade e verificar a consistência de ambos.
3. Protocolo Completo: Design e prova de segurança (completude, sonoridade e conhecimento zero) de quatro sub-protocolos que compõem o sistema.
4. Implementação e Avaliação: Implementação prática usando o EMP-toolkit e avaliação em 37 circuitos combinacionais (incluindo unidades aritméticas, criptográficas como AES S-Box, e lógica de controle).

4. Resultados Experimentais

• Cenário de Teste: Avaliação em servidores com processadores AMD Rome, utilizando uma rede local de 100 Mbps.
• Desempenho:
  • A verificação da insatisfiabilidade ($\Pi_{P1} + \Pi_{P2}$) domina o tempo de execução, conforme esperado para problemas co-NP.
  • O protocolo consegue verificar designs práticos, como o AES S-Box, dentro de limites de tempo viáveis (aprox. 4.9 segundos para o AES S-Box sem otimização).
  • Otimização: A compressão de resolventes resultou em um speedup (aceleração) de até 2.88x no tempo total de prova, dependendo da complexidade do circuito.
• Escalabilidade: O tempo de prova escala quase linearmente com o tamanho da prova de refutação em escala log-log. O principal gargalo é o crescimento exponencial do tamanho da prova de refutação para circuitos muito grandes, o que pode levar a limitações de memória.

5. Significado e Impacto

• Segurança na Cadeia de Suprimentos: O ZK-CEC oferece uma solução viável para o dilema de confiança na cadeia de suprimentos de hardware, permitindo que vendedores de IP provem a ausência de Trojans e a conformidade funcional sem expor o segredo comercial.
• Avanço Teórico: Demonstra que a verificação formal (que é mais forte que a simulação) pode ser realizada em um ambiente de conhecimento zero, superando as limitações de sonoridade de protocolos anteriores quando aplicados a entradas secretas.
• Aplicabilidade Geral: O "Blueprint" proposto não se limita a hardware; pode ser adaptado para verificação de software e sistemas ciber-físicos onde a lógica interna deve permanecer secreta.

Em resumo, o trabalho preenche uma lacuna crítica entre a necessidade de verificação formal rigorosa e a proteção de propriedade intelectual, estabelecendo um novo padrão para a confiança em componentes de hardware de terceiros.