🔢 mathematics

Canonical Byte-String Encoding for Finite-Ring Cryptosystems

Este artigo apresenta um codec de mapeamento base-m canônico, formalizado e verificado em Lean 4 com uma implementação em Rust, que converte strings de bytes em resíduos módulo *m* para criptografia de anéis finitos, garantindo decodificação exata e tolerância a sufixos válidos.

Autores originais: Kyrylo Riabov, Serhii Kryvyi

Publicado 2026-03-25

📖 4 min de leitura🧠 Leitura aprofundada

CC BY 4.0

Autores originais: Kyrylo Riabov, Serhii Kryvyi

Artigo original sob licença CC BY 4.0 (http://creativecommons.org/licenses/by/4.0/). ✨ Esta é uma explicação gerada por IA do artigo abaixo. Não foi escrita nem endossada pelos autores. Para precisão técnica, consulte o artigo original. Ler aviso legal completo

Imagine que você precisa enviar uma carta secreta para um amigo, mas o correio só aceita envelopes que contêm números, e não letras ou palavras. Além disso, o seu amigo só entende números que são menores que um certo limite (digamos, números de 0 a 49).

Se você tentar escrever "Olá" diretamente, o correio vai rejeitar. Você precisa transformar cada letra em um número, mas de uma forma que seu amigo possa reverter exatamente para "Olá" quando receber.

É exatamente esse o problema que este artigo resolve. Os autores, Kyrylo e Serhii, criaram um "tradutor universal" chamado Base-m-len.

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

1. O Problema: A Barreira da Linguagem

Em criptografia moderna (especialmente a que usa "anéis" matemáticos), os computadores precisam trabalhar com números. Mas nossos dados (textos, fotos, senhas) são feitos de bytes (sequências de números de 0 a 255).
O desafio é: como transformar uma mensagem longa e complexa em uma sequência de números menores, sem perder nenhuma informação e sem que o destinatário fique confuso sobre onde a mensagem termina?

2. A Solução: O "Selo de Endereço" Inteligente

Os autores criaram um sistema chamado Base-m-len. Pense nele como um envelope inteligente com três partes:

Parte 1: O Rótulo de Tamanho (O "Selo")
Antes de colocar a mensagem, o sistema escreve em um pequeno cartão: "Esta carta tem X bytes de comprimento".
- Por que isso é legal? O destinatário olha o cartão, sabe exatamente quantas letras ler. Se houver um rabisco extra no final do envelope (ruído ou dados extras), ele simplesmente ignora, porque já sabe onde a mensagem acabou.
Parte 2: O "Estado de Segurança" (O "Cofre")
Há um segundo cartão que diz: "O número final que ficou na minha calculadora foi Y". Isso ajuda a garantir que a matemática foi feita corretamente e permite que o destinatário comece a decodificar do jeito certo.
Parte 3: A Mensagem em Números (O "Conteúdo")
A mensagem em si é transformada em uma corrente de números menores. O sistema usa uma técnica inteligente (baseada em um método chamado rANS) para empurrar os bytes para dentro desses números menores, como se estivesse espremendo uma esponja para caber em um copo pequeno, mas sem perder uma gota de água.

3. Como Funciona a Mágica (A Analogia da Esteira)

Imagine uma esteira rolante de fábrica:

Encaixotamento (Codificação): O sistema pega seus bytes (letras), um por um, de trás para frente. Ele os mistura com um número grande. Sempre que o número fica muito grande, ele "corta" um pedaço (um dígito menor) e joga na esteira de saída.
O Resultado: No final, você tem uma lista de números pequenos e dois cartões de tamanho fixo no início.
Desencaixotamento (Decodificação): O destinatário pega os cartões, sabe o tamanho, e começa a reconstruir a esteira. Ele pega os números pequenos, devolve-os ao "cofre" matemático e extrai os bytes originais.

4. Por que isso é tão especial? (A Prova de Segurança)

O que torna este artigo realmente impressionante não é apenas a ideia, mas a garantia matemática.

Os autores não apenas escreveram o código em Rust (uma linguagem de programação segura).
Eles usaram um assistente matemático chamado Lean 4 para provar, linha por linha, que o sistema nunca falha.
É como se eles não apenas construíssem uma ponte, mas contrataram um engenheiro que, usando lógica pura, provou que a ponte não vai cair, não importa o peso ou o vento, desde que você siga as regras de tamanho.

5. O Que Isso Significa para o Futuro?

Este sistema é como um "adaptador de tomada" universal para criptografia.

Para os desenvolvedores: Agora eles têm uma maneira padrão, rápida e comprovada de transformar qualquer texto ou arquivo em números para usar em sistemas de criptografia avançados.
Para a segurança: Como o sistema é determinístico (sempre faz a mesma coisa com a mesma entrada) e público, ele não esconde a mensagem por si só. Ele apenas prepara a mensagem para que a criptografia real (o "cadeado") possa ser aplicada depois.

Resumo em uma frase:
Os autores criaram um tradutor matemático infalível que transforma qualquer texto em uma sequência de números menores, garantindo que a mensagem possa ser lida de volta perfeitamente, mesmo que chegue com "sujeira" extra no final, tudo isso provado matematicamente para não deixar brechas.

Título: Codificação Canônica de Strings de Bytes para Criptossistemas de Anel Finito

Autores: Kyrylo Riabov e Serhii Kryvyi (Universidade Nacional Taras Shevchenko de Kiev, Ucrânia)
Data: 25 de março de 2026

1. O Problema

Os criptossistemas baseados em anéis (ring-mapping cryptosystems), como aqueles utilizados em criptografia de reticulados (ex: NTRU, ML-KEM) e primitivas simétricas sobre anéis inteiros, exigem que as mensagens sejam representadas como elementos do anel $\mathbb{Z}_m$ (inteiros módulo $m$ ) antes da aplicação de transformações algébricas de criptografia ou descriptografia.

O problema identificado é a falta de uma camada de representação canônica e genérica para dados arbitrários (texto UTF-8 ou dados binários). Trabalhos anteriores frequentemente utilizavam tabelas de símbolos fixas e manuais, o que é suficiente para demonstrações algébricas, mas inadequado para protocolos gerais que lidam com dados reais. Existe a necessidade de um codec (codificador/decodificador) que mapeie strings de bytes para resíduos em $\mathbb{Z}_m$ de forma determinística, auto-delimitada e verificável.

2. Metodologia: O Codec `base-m-len`

Os autores propõem um codec chamado base-m-len, que atua como uma camada de transporte entre bytes e resíduos. A abordagem baseia-se em adaptar conceitos de codificação de entropia (especificamente rANS - range Asymmetric Numeral Systems de Duda), mas com objetivos diferentes: em vez de compressão estatística, o foco é a representação determinística e auto-delimitada.

Estrutura do Formato de Transmissão (Wire Format)

O formato codificado consiste em três componentes concatenados:

Prefixo de Comprimento Fixo: Codifica o tamanho da string de bytes original ( $L$ ) usando $k$ dígitos em base- $m$ , onde $k$ é o menor inteiro tal que $m^k \ge 2^{64}$ .
Prefixo de Estado Final: Codifica o estado final do processamento do payload, também usando $k$ dígitos em base- $m$ .
Payload (Carga Útil): Um fluxo de dígitos em base- $m$ gerado por uma transdução uniforme dos bytes de entrada.

Algoritmo de Codificação

O codificador processa os bytes de entrada de trás para frente (reverso).
Mantém um estado $x$ inicializado no limite inferior do decodificador ( $L$ ).
Para cada byte $b$ , atualiza o estado com $x \leftarrow 256x + b$ .
Enquanto o estado exceder um limiar de codificação, emite dígitos ( $x \mod m$ ) e renormaliza o estado ( $x \leftarrow \lfloor x/m \rfloor$ ).
O fluxo de saída é revertido para ordem FIFO (First-In-First-Out) para o decodificador.

Algoritmo de Decodificação

Lê o prefixo de comprimento para saber quantos bytes recuperar.
Lê o prefixo de estado para inicializar a variável de estado.
Recupera os bytes original através de divisões e multiplicações inversas, consumindo dígitos do payload conforme necessário.
Tolerância a Sufixos: O decodificador para exatamente após recuperar o número declarado de bytes, ignorando qualquer dígito válido adicional no final da stream. Isso permite a concatenação segura de mensagens.

3. Principais Contribuições

O artigo oferece três contribuições fundamentais:

Definição Canônica: Estabelece um codec byte-para-resíduo parametrizado pelo módulo $m$ , centrado no formato base-m-len, que suporta strings de até $2^{64}$ bytes.
Garantias de Correção Formal:
- Decodificação Exata: Prova que a decodificação recupera exatamente a string de bytes original para todos os módulos suportados.
- Inversão de Prefixo Fixo: Garante que o comprimento e o estado podem ser recuperados sem ambiguidade.
- Tolerância a Sufixos: Prova formalmente que dígitos extras no final não corrompem a decodificação.
Implementação e Verificação Formal:
- Rust: Uma biblioteca de referência (sym-adv-encoding) com interfaces para bytes e UTF-8.
- Lean 4: Uma formalização completa da especificação abstrata com provas verificadas por máquina. Isso inclui a verificação de limites de estado, inversão de prefixos e correção de ponta a ponta da stream.

4. Resultados e Avaliação

Complexidade e Custo de Representação

Tempo: A codificação e decodificação são lineares $O(n)$ em relação ao tamanho da entrada.
Custo de Cabeçalho: O tamanho fixo do cabeçalho é $2k$ dígitos. Para módulos pequenos (ex: $m=25$ ), o cabeçalho é grande (28 dígitos), mas diminui para módulos maiores (16 dígitos para $m=257$ ).
Taxa de Payload: O número de dígitos por byte é aproximadamente $\log_m 256$ . Módulos maiores resultam em taxas mais próximas de 1 dígito por byte.

Desempenho Prático (Benchmarks)

Testes realizados em hardware Apple M3 Pro mostraram:

O codec nativo em Rust é significativamente mais rápido do que conversões de radix completas usando BigUint (aritmética de precisão arbitrária), especialmente em grandes volumes de dados.
Exemplo: Para 64 KiB, a codificação nativa com $m=257$ atingiu ~236 MiB/s, enquanto a abordagem BigUint caiu para ~1,2 MiB/s.
A configuração com $m=257$ é particularmente eficiente, aproximando-se de 1 resíduo por byte, mantendo a recuperação explícita do comprimento.

5. Significado e Limitações

Significado

Camada de Representação: O trabalho preenche uma lacuna crítica em protocolos de criptografia de anel, fornecendo uma camada de serialização padronizada que pode ser integrada diretamente em sistemas como SYMPZON (primitivas simétricas sobre anéis inteiros).
Verificabilidade: A presença de provas formais em Lean 4 oferece um alto nível de confiança na correção do algoritmo, algo raro em implementações de criptografia de baixo nível.
Flexibilidade: A tolerância a sufixos permite o uso em protocolos de streaming ou concatenação de mensagens sem necessidade de reestruturação complexa.

Limitações e Considerações de Segurança

Não é uma Primitiva de Segurança: O codec é determinístico e público. Ele não fornece confidencialidade, integridade ou autenticidade. Essas propriedades devem ser fornecidas pelo protocolo criptográfico que o envolve.
Vazamento de Comprimento: O formato expõe o tamanho exato da mensagem original. Se o ocultamento de comprimento for necessário, o protocolo de nível superior deve aplicar preenchimento (padding).
Escopo da Verificação: As provas formais cobrem a especificação abstrata, não a implementação Rust linha por linha. Detalhes de engenharia como limites de alocação e endurecimento de analisadores sintáticos (parsers) são responsabilidade da implementação.

Conclusão

O artigo apresenta uma solução robusta e matematicamente verificada para o problema de mapear dados binários arbitrários para anéis finitos. Ao combinar eficiência prática (via Rust) com rigor formal (via Lean 4), o codec base-m-len estabelece um padrão para a representação de mensagens em criptossistemas modernos baseados em anéis, facilitando a interoperabilidade e a segurança em aplicações como criptografia homomórfica e computação multipartidária.