Towards System-Oriented Formal Verification of Local-First Access Control

Resumo Técnico: Em Direção à Verificação Formal Orientada a Sistemas de Controle de Acesso Local-First

1. O Problema

Sistemas "local-first" (como Matrix e Keyhive) utilizam Tipos de Dados Replicados sem Conflitos (CRDTs) para permitir colaboração descentralizada com baixa latência e alta disponibilidade. No entanto, à medida que esses sistemas escalam de pequenos grupos de confiança mútua para grandes redes públicas, surgem dois desafios críticos:

• Falta de Confiança e Tolerância a Falhas Bizantinas: Em sistemas de larga escala, participantes podem agir de forma maliciosa (equivocação, omissão ou retrocesso de data/ backdating), tentando manipular a ordem dos eventos ou contornar permissões.
• Lacuna entre Teoria e Prática: Atualmente, protocolos como o Matrix baseiam-se em especificações informais e implementações de referência não verificadas, o que pode levar a vulnerabilidades de segurança (como violações de invariantes de autorização).

O desafio central é projetar algoritmos de controle de acesso que sejam Byzantine Fault-Tolerant (BFT), garantam a consistência eventual e permitam revogação de permissões sem a necessidade de coordenação centralizada.

2. Metodologia

Os autores adotam uma abordagem "bottom-up" (de baixo para cima). Em vez de tentar verificar o complexo sistema Matrix diretamente, eles constroem e verificam formalmente um modelo simplificado de um tipo de dado replicado para gestão de grupos de colaboração.

A metodologia baseia-se em:

• Modelagem Matemática: Definição de semânticas para um tipo de dado que utiliza capacidades (capabilities) para controle de acesso e hash chronicles (grafos acíclicos dirigidos baseados em hashes) para replicação resiliente a falhas bizantinas.
• Verificação Formal com Verus: Utilização do framework Verus, que estende a linguagem Rust. O Verus permite escrever a especificação, a implementação e a prova de correção no mesmo arquivo de código-fonte, utilizando o provador de teoremas Z3. Isso garante que a verificação ocorra com "custo zero" em tempo de execução, unindo a performance do Rust com o rigor da lógica formal.
• Abstração de Falhas Bizantinas: O modelo assume que o log de eventos (chronicle) é eventualmente consistente, mas permite que entidades maliciosas tentem manipular a causalidade através de backdating e equivocation.

3. Principais Contribuições

• Especificação de Semântica de Autorização: Definição de um modelo de controle de acesso baseado em capacidades no estilo "granted-present-revoke" (concedido-presente-revogado), que é adequado para a natureza não-monotônica de sistemas distribuídos.
• Definição de Invariantes de Segurança:
  • Segurança de Autorização (Authorization Safety): Garante que a autorização causal de um evento permaneça invariante, exceto por revogações autorizadas.
  • Segurança de Consulta (Query Safety): Garante que mudanças nos resultados de consultas só ocorram se o novo evento for devidamente autorizado.
  • Segurança de Revogação (Revocation Safety): Garante que, se um evento for desautorizado em um determinado timestamp, ele também seja considerado desautorizado em qualquer timestamp anterior (proteção contra backdating).
• Implementação e Verificação em Rust: Um estudo de caso demonstrando a aplicação de três níveis de complexidade de algoritmos (desde modelos puramente monotônicos até modelos que suportam revogação não-monotônica).

4. Resultados

Os autores demonstraram que é possível utilizar o Verus para provar que seus algoritmos simplificados satisfazem os invariantes de segurança propostos, mesmo sob a ameaça de ataques bizantinos (como o uso de eventos retroativos para tentar ignorar uma revogação).

Eles confirmaram que:

• A implementação é total (não causa panics ou travamentos inesperados).
• As consultas são puras e garantem a convergência forte (todos os nós corretos chegarão ao mesmo estado de autorização).
• O uso do Verus permite que engenheiros de sistemas utilizem ferramentas de verificação formal sem abandonar a linguagem Rust de alto desempenho.

5. Significância

Este trabalho é significativo por preencher a lacuna entre a teoria de métodos formais e a engenharia de sistemas distribuídos. Ele fornece um roteiro para a construção de sistemas de controle de acesso "local-first" que são, por design, seguros contra atores maliciosos. Embora o modelo testado seja simplificado, a prova de conceito demonstra que a verificação formal de sistemas de larga escala (como o Matrix) é tecnicamente viável através de ferramentas modernas como o Verus, pavimentando o caminho para infraestruturas de comunicação descentralizadas mais robustas e confiáveis.