Resumo Técnico: Segurança e Liveness de Preservação de Estado entre Domínios sob Falhas Bizantinas

1. Definição do Problema

O artigo aborda o desafio crítico de garantir a consistência dos estados de conformidade regulatória para ativos tokenizados operando através de redes blockchain heterogêneas e livros contábeis off-chain. Sem garantias formais, a arbitragem regulatória torna-se estruturalmente possível; por exemplo, uma ordem de congelamento emitida em uma jurisdição deve ser imediatamente e deterministicamente refletida em todos os domínios conectados.

O problema é decomposto em duas dimensões:

1. Segurança (Safety): Garantir que, se uma sincronização for realizada, o estado resultante seja consistente em todos os domínios com preservação estrutural.
2. Liveness (Vivacidade): Garantir que, em um ambiente descentralizado contendo nós bizantinos (atores maliciosos), o processo de sincronização realmente proceda, evitando deadlocks e inanição (starvation).

Trabalhos anteriores não verificaram formalmente ambas as propriedades simultaneamente em um único framework, nem verificaram propriedades de consenso específicas de regulação (como determinismo de prioridade e ausência de deadlock de ativos) usando Isabelle/HOL.

2. Metodologia

Os autores empregam uma abordagem de prova mecanizada usando Isabelle/HOL. O desenvolvimento consiste em 3.215 linhas de código distribuídas em quatro arquivos de teoria, construídos sem o uso de sorry ou oops (suposições não provadas).

2.1 Modelos de Sistema e de Ameaça

• Modelo de Sistema: O sistema compreende um conjunto finito de domínios (chains/ledgers) que compartilham uma estrutura de máquina de estados. A sincronização é modelada como uma operação atômica envolvendo verificação, validação, aquisição de lock, atualização de estado e liberação de lock.
• Modelo de Ameaça:
  • Propriedade 1 (Segurança): Inicialmente assume nós honestos e canais confiáveis.
  • Propriedade 2 (Liveness): Relaxa a suposição de nós honestos para permitir até $f < n/3$ nós bizantinos. Nós bizantinos podem reter liberações de lock ou agir de forma maliciosa.
  • Combinado: A Propriedade 2 descarta a suposição de "nós honestos" da Propriedade 1, resultando em uma garantia incondicional.

2.2 Modelo de Transição de Estado Regulatório

O modelo formal baseia-se no framework do Protocolo de Conformidade Regulatória (RCP), que sistematiza 31 requisitos de 15 autoridades financeiras globais.

• Estados: Cinco estados regulatórios (ACTIVE, FROZEN, SEIZED, CONFISCATED, RESTRICTED).
• Ações: Sete ações regulatórias (FREEZE, SEIZE, CONFISCATE, RESTRICT, UNFREEZE, UNRESTRICT, RELEASE).
• Restrições: O modelo impõe restrições legais específicas, como a exclusão de transições "SEIZED → FROZEN" (visto que a apreensão é uma restrição legal mais forte do que o congelamento) e a natureza terminal do estado CONFISCATED.

2.3 Infraestrutura de Verificação: Locales Genéricos

A metodologia central baseia-se na definição de sete locales genéricos e independentes de domínio no Isabelle/HOL. Esses locales servem como uma infraestrutura de verificação reutilizável. Teoremas provados dentro desses locales são automaticamente herdados por qualquer domínio concreto que os instancie via o mecanismo de interpretação do Isabelle.

• Locales de Segurança (4):
  1. state_machine: Define estados finitos, ações e transições determinísticas.
  2. state_preservation: Estabelece uma condição de naturalidade onde a sincronização comuta com as transições de estado (homomorfismo).
  3. symmetric_state_preservation: Adiciona mapas inversos para garantir a preservação de ida e volta (roundtrip) bidirecional.
  4. multi_domain_preservation: Generaliza a consistência para um conjunto arbitrário de domínios finitos (consistência de N-domínios) e garante o isolamento por ativo.
• Locales de Liveness (3):
  1. priority_system: Garante a seleção determinística de ações via prioridades injetivas.
  2. deadlock_free_locking: Garante que nenhum recurso fique travado indefinidamente via liberação forçada baseada em timeout.
  3. fair_leader_system: Garante a ausência de inanição sob um escalonamento periódico de líder honesto.

3. Principais Contribuições

3.1 Prova de Segurança Mecanizada (Propriedade 1)

O artigo estende o padrão Merkle Functor (anteriormente limitado à integridade de dados unidirecional em um único domínio) para um framework cross-domain, bidirecional e multi-domínio.

• Roundtrip Bidirecional: Prova que as transições de estado são fielmente refletidas em ambas as direções entre os domínios.
• Consistência de N-Domínios: Prova que, após uma sincronização em um domínio, todos os domínios conectados alcançam o mesmo estado resultante.
• Isolamento por Ativo: Prova que a sincronização em um ativo não afeta o estado de outros ativos.
• Instanciações Concretas: Os autores fornecem testemunhas concretas para garantir que os locales não sejam satisfeitos de forma vazia:
  • Instância de Escalada: Uma instância de ações heterogêneas onde uma chain suporta apenas ações de escalada (FREEZE, SEIZE, etc.) enquanto a outra suporta o conjunto completo, provando a preservação estrutural através de vocabulários distintos.
  • Instância de Cruzamento de Camadas: Uma ponte bidirecional entre um enum reg_state on-chain e um registro de permissão DAML off-chain, provando a injetividade e a ausência de perda de informação.

3.2 Prova de Liveness Mecanizada (Propriedade 2)

Este é o primeiro uso do Isabelle/HOL sozinho para verificar o liveness de consenso BFT em um contexto de blockchain.

• Determinismo: Ações regulatórias conflitantes são resolvidas via uma ordem total de chaves de prioridade (nível de autoridade, timestamp, severidade, ID do nó).
• Ausência de Deadlock: Prova que, mesmo que nós bizantinos retenham liberações de lock, o mecanismo de timeout garante que o lock expire dentro de um tempo delimitado.
• Ausência de Inanição (Starvation Freedom): Prova que, sob um limite de justiça (garantindo um líder honesto dentro de $k$ épocas), todas as requisições pendentes são eventualmente processadas.

3.3 Descarga de Suposições (Garantia Combinada)

O artigo demonstra um padrão de raciocínio assume-guarantee. A Propriedade 2 descarta a suposição de "nós honestos" exigida pela Propriedade 1. Ao provar que o sistema permanece vivo e determinístico mesmo com falhas bizantinas ($f < n/3$), a garantia de segurança condicional é promovida a uma garantia incondicional: a preservação de estado cross-domain mantém-se mesmo na presença de nós bizantinos.

4. Resultados e Artefatos

• Artefatos de Prova: O desenvolvimento inclui oito interpretações concretas de locales (cobrindo todos os sete locales genéricos) ao lado de uma instanciação paramétrica multi-domínio.
• Modelo Regulatório: O modelo cobre 31 requisitos regulatórios mapeados para 5 estados e 7 ações.
• Disponibilidade: Todos os artefatos estão publicamente disponíveis no GitHub e foram submetidos ao Archive of Formal Proofs (AFP) para revisão.
• Guia de Design: As provas geram restrições de parâmetros específicas para implementação (ex: $n \ge 3f + 1$, timeouts positivos, limites de justiça) que se traduzem diretamente em um racional de design matemático para sequenciadores descentralizados.

5. Significância e Alegações

O artigo alega significância em três áreas principais:

1. Novidade em Verificação Formal: É o primeiro trabalho a verificar formalmente tanto a segurança quanto a liveness simultaneamente para transições de estado regulatório cross-domain. É também o primeiro a verificar propriedades de consenso específicas de regulação (determinismo de prioridade, ausência de deadlock de ativos regulatórios) em qualquer ferramenta.
2. Avanço Metodológico: Ao utilizar uma hierarquia de locales genéricos, os autores fornecem uma infraestrutura de verificação reutilizável que é independente de domínio. Isso permite que as mesmas provas de segurança e liveness sejam aplicadas a domínios arbitrários (ex: DeFi, bancos de dados distribuídos) simplesmente instanciando os locales.
3. Ponte entre Teoria e Prática: O trabalho vai além da verificação de consenso abstrato (como acordo/validade) para abordar restrições regulatórias de domínio específico. Ele estabelece explicitamente a ponte entre uma máquina de estados teórica e um modelo de conformidade regulatória, fornecendo um "guia de design" para parâmetros de implementação derivados diretamente das provas.

Os autores explicitamente notam limitações: o modelo não verifica características específicas de cada chain (gas, tempos de bloco), não prova o refinamento formal para código Rust/Solidity, e assume um sistema fechado (a chegada dinâmica de requisições é um trabalho futuro). O framework atual estabelece os locales e instâncias fundamentais, mas ainda não formaliza as leis de funtor da teoria das categorias, que estão reservadas para trabalhos futuros para alcançar o status pleno de "functor".