Introdução
Métodos formais costumam aparecer em discussões de segurança cercados por exemplos acadêmicos: protocolos simplificados, máquinas de estado artificiais, propriedades matemáticas elegantes e sistemas construídos especificamente para serem verificados.
Mas o que acontece quando aplicamos essa forma de raciocínio a uma biblioteca criptográfica real?
Foi exatamente esse o objetivo deste trabalho.
Partimos de uma biblioteca TypeScript/JavaScript existente, analisamos sua arquitetura criptográfica, formulamos propriedades de segurança, construímos experimentos controlados e utilizamos Lean 4 para formalizar partes relevantes do comportamento observado.
Durante esse processo, chegamos a um candidate finding particularmente interessante:
Um ciphertext pequeno e não autenticado pode controlar parâmetros do Argon2id e provocar consumo significativo de recursos antes que a autenticação AES-GCM finalmente rejeite o ciphertext.
Em nossos experimentos, duas operações concorrentes com ciphertexts adulterados levaram o processo Node.js a um pico observado de aproximadamente 8 GB de working set, embora ambas terminassem posteriormente em DECRYPTION_FAILED.
Mais interessante que o finding isoladamente, porém, é como chegamos até ele.
Este artigo apresenta esse caminho.
1. O objetivo não era “caçar vulnerabilidades”
O projeto começou com uma pergunta diferente:
Podemos pegar uma biblioteca criptográfica real e transformar suas garantias de segurança em propriedades que possam ser investigadas experimentalmente e formalizadas?
Essa diferença de abordagem é importante.
Em vez de começar procurando padrões conhecidos de vulnerabilidade, começamos identificando as propriedades que deveriam permanecer verdadeiras.
Por exemplo:Decryptk(Encryptk(m))=m
Essa é uma propriedade funcional básica.
Mas também podemos formular propriedades de segurança:Tamper(C)⇒Reject(C)
ou:WrongKey⇒Reject
e:WrongAAD⇒Reject
A mudança conceitual é pequena, mas poderosa.
Em vez de perguntar:
“Existe um bug aqui?”
passamos a perguntar:
“Quais propriedades precisam permanecer verdadeiras para que esse sistema seja seguro?”
E então tentamos quebrá-las.
2. O alvo da análise
O laboratório foi realizado sobre uma pequena biblioteca criptográfica TypeScript/JavaScript.
A versão analisada implementava, entre outros mecanismos:
- AES-256-GCM;
- Argon2id;
- ciphertexts versionados;
- parâmetros KDF armazenados no próprio ciphertext;
- AAD;
- autenticação de ciphertext;
- suporte a Node.js e browser;
- compatibilidade com formatos anteriores.
A arquitetura conceitual que nos interessava inicialmente era aproximadamente:
Application │ ▼Crypto API │ ▼KDF │ ▼AES-GCM │ ▼Ciphertext container ┌──┼────┬─────┐salt IV tag ciphertext
Nosso primeiro objetivo era entender quatro coisas:
Onde a chave chega ao AES-GCM?De onde vem o IV?Onde o authentication tag é produzido e verificado?O que acontece quando a autenticação falha?
Isso nos levou diretamente ao código responsável pela decriptação.
3. Primeiro princípio: transformar documentação em propriedades
Uma biblioteca criptográfica normalmente apresenta afirmações como:
ciphertext adulterado deve ser rejeitado.
Isso pode ser transformado em uma propriedade:C′=C⇒Decrypt(C′)=Failure
Claro que essa formulação ainda é simplificada demais para representar AES-GCM corretamente.
Mas ela nos dá algo extremamente útil:
uma propriedade testável.
Começamos então pelos casos mais óbvios.
4. Experimento 1 — adulterando o ciphertext
Produzimos um ciphertext válido e modificamos um byte.
Conceitualmente:
Original:66 77 61 2f ...Tampered:67 77 61 2f ...
A alteração foi mínima:0x66⊕0x01=0x67
A biblioteca rejeitou o resultado:
Decryption rejected.Type: DECRYPTION_FAILEDCode: DECRYPTION_FAILED
Primeira propriedade observada:TamperedCiphertext⇒Reject
Até aqui, comportamento esperado.
Mas então fizemos algo diferente.
Formalizamos a ideia.
5. Levando a propriedade para Lean
Criamos uma representação mínima de ciphertext:
abbrev Ciphertext := List UInt8
E uma operação de adulteração:
def tamperFirstByte (c : Ciphertext) : Ciphertext := match c with | [] => [] | b :: rest => (b ^^^ 1) :: rest
Primeiro provamos que a operação realmente altera um ciphertext não vazio:
theorem tamper_changes_nonempty (b : UInt8) (rest : List UInt8) : tamperFirstByte (b :: rest) ≠ (b :: rest) := by intro h simp [tamperFirstByte] at h bv_decide
Depois construímos um modelo abstrato de rejeição.
A ideia era simples:
received == expected ↓ successreceived != expected ↓ failure
E provamos no modelo:Tamper(C)⇒Reject(C)
Isso não prova AES-GCM.
Também não prova a implementação JavaScript.
Prova uma propriedade do modelo que construímos.
Essa distinção se tornaria fundamental posteriormente.
6. Construindo evidência em várias camadas
Repetimos o processo para diferentes componentes autenticados.
Testamos:
ciphertext alterado → rejeitadotag alterada → rejeitadachave incorreta → rejeitadaAAD incorreto → rejeitadoIV incorreto → rejeitado
Cada experimento produzia evidência concreta da implementação.
Paralelamente, criamos modelos em Lean para representar as propriedades correspondentes.
O resultado começou a formar uma cadeia:
Documentação ↓Propriedade esperada ↓Código ↓Experimento ↓Modelo ↓Teorema
E foi justamente seguindo essa cadeia que encontramos algo mais interessante.
7. O primeiro comportamento inesperado: compatibilidade legada
Durante a análise dos testes do próprio projeto, encontramos referências a uma configuração relacionada à autenticação do header v1.
O comportamento legado existia para permitir compatibilidade com ciphertexts antigos.
No modo atual, o header era incorporado ao AAD.
Conceitualmente:AAD=Context∥Header
No modo legado:AAD=Context
O header deixava de participar diretamente da autenticação AES-GCM.
Isso imediatamente levantou uma pergunta:
O modo legado serve apenas para ler ciphertexts antigos ou também afeta a criação de novos ciphertexts?
Seguimos o fluxo no código.
E encontramos que a mesma decisão era utilizada no caminho de encryption.
Em termos simplificados:
legacyHeaderAad = falseAAD = context || header
enquanto:
legacyHeaderAad = trueAAD = context
Isso significava que o modo de compatibilidade também poderia produzir novos ciphertexts utilizando a semântica legada.
8. Reproduzindo o comportamento
Criamos então um novo ciphertext com o modo legado habilitado.
Depois modificamos o primeiro byte reservado do header:
Byte original: 0Byte adulterado: 255
O resultado foi particularmente interessante.
No modo legado:
Legacy decrypt ACCEPTED tampered ciphertext
No modo atual/default:
Default decrypt REJECTEDCode: DECRYPTION_FAILED
Mas ainda não tínhamos necessariamente uma vulnerabilidade.
Precisávamos entender por quê.
9. O parser mudou completamente a interpretação
Inspecionando o parser do formato v1, identificamos o layout relevante:
0–3 magic4 version5 KDF ID6–9 memoryCost10–13 timeCost14–15 parallelism16–21 reserved
O detalhe crucial:
os bytes reservados não eram utilizados semanticamente pelo parser.
Portanto, modificar:
byte 16
não alterava:
- a chave;
- o KDF;
- os parâmetros;
- o IV;
- o ciphertext.
No modo legado, aquele byte também não participava do AAD.
Consequentemente:
reserved byte modified ↓parser ignores it ↓AAD does not contain it ↓same key ↓same authentication relation ↓decryption succeeds
No modo seguro:
reserved byte modified ↓header participates in AAD ↓AAD changes ↓GCM authentication fails
Agora tínhamos uma explicação estrutural.
10. Formalizando os dois modos
Representamos essa diferença em Lean:
inductive HeaderMode where | secure | legacy
O estado abstrato possuía duas propriedades:
structure AuthenticatedState where payloadAuthenticated : Bool headerMatches : Bool
No modo seguro:Success⟺PayloadAuthenticated∧HeaderMatches
No modo legado:Success⟺PayloadAuthenticated
Isso permitiu provar:Secure∧HeaderModified⇒Failure
e:Legacy∧PayloadValid∧HeaderModified⇒Success
Novamente:
Lean não estava descobrindo o comportamento do JavaScript.
Ele estava nos obrigando a escrever precisamente qual propriedade acreditávamos que o sistema possuía.
Essa disciplina acabou sendo extremamente útil.
11. Nem toda adulteração do header funcionava
Aqui aconteceu uma parte particularmente importante da investigação.
Poderíamos ter parado no primeiro comportamento interessante e concluído:
“O header não é protegido no modo legado.”
Mas isso seria uma simplificação excessiva.
Decidimos modificar outro campo.
Desta vez:
memoryCost
Original:
4096
Adulterado:
8192
Resultado:
DECRYPTION_FAILED
Por quê?
Porque memoryCost não é apenas metadata.
Ele participa da derivação da chave.
Assim:memoryCost′=memoryCost
faz com que:KDF(password,salt,params′)=KDF(password,salt,params)
e consequentemente:K′=K
A autenticação AES-GCM falha.
Isso nos deu uma distinção muito mais precisa:
Alguns campos do header não estavam diretamente vinculados ao AAD no modo legado, mas alterações em campos semanticamente utilizados pelo KDF ainda poderiam ser detectadas indiretamente por produzirem uma chave diferente.
Esse tipo de refinamento é exatamente o que uma análise séria precisa fazer.
12. E então apareceu uma pergunta diferente
Enquanto investigávamos memoryCost, percebemos algo.
Para descobrir que a chave estava errada, o sistema precisava primeiro calcular a chave.
Ou seja:
ciphertext ↓parse header ↓read memoryCost ↓execute Argon2id ↓derive key ↓AES-GCM ↓authentication failure
Então fizemos uma nova pergunta:
Quem controla o custo do Argon2id antes da autenticação?
A resposta era:
o próprio ciphertext.
Esse foi o ponto em que a investigação mudou de direção.
13. Da integridade para disponibilidade
Até aquele momento estávamos essencialmente estudando:Integrity
Agora surgiu uma propriedade relacionada a:Availability
Poderíamos formulá-la informalmente como:UntrustedInput⇒ExcessivePreAuthenticationWork
Mas o fluxo parecia permitir:UnauthenticatedHeader→KDFParameters→ExpensiveKDF→Authentication
Ou seja, o sistema precisava gastar recursos antes de saber se aquele ciphertext era legítimo.
14. Mas havia limites
A implementação não aceitava qualquer valor.
Testamos:
memoryCost = 4,294,967,295
Resultado:
INVALID_INPUTKDF_PARAMS_OUT_OF_BOUNDS
O próprio erro revelou os limites:
memoryCost <= 4,194,304timeCost <= 100parallelism <= 64
Isso é importante.
Não seria correto escrever:
“A biblioteca permite memoryCost arbitrário.”
Ela não permite.
Existe uma mitigação explícita.
A pergunta correta passou a ser:
O maior valor permitido ainda é perigoso em um contexto de input não confiável?
15. Testando exatamente o boundary
Alteramos então:
memoryCost = 4,194,304
Ou seja:memoryCost=MAX
O parser aceitou.
O Argon2id foi executado.
Somente depois a autenticação falhou:
DECRYPTION_FAILED
Tempo observado:
3.97 segundos
Em outra execução:
3.26 segundos
Um ciphertext inválido conseguia, portanto, provocar vários segundos de processamento antes de ser rejeitado.
E o ciphertext tinha aproximadamente:
103 bytes
Esse detalhe seria crucial posteriormente.
16. Pequeno input, grande trabalho
Esse comportamento é diferente do caso trivial:
100 GB de input→ muito consumo de recursos
Aqui temos:
~103 bytes ↓alguns bytes controlam memoryCost ↓4,194,304 ↓Argon2id ↓grande consumo de recursos
Ou seja, existe uma relação de amplificação:SmallInput→LargeResourceCost
O custo não é proporcional ao tamanho do ciphertext.
É determinado por metadata controlável antes da autenticação.
17. Medindo memória: o primeiro resultado enganou
Primeiro utilizamos:
process.memoryUsage()
Antes:
RSS: 40.16 MB
Depois:
RSS: 40.39 MB
À primeira vista parecia que praticamente nenhuma memória tinha sido utilizada.
Mas havia um problema metodológico.
O Argon2id utiliza memória nativa, e uma medição realizada depois da operação pode acontecer quando a alocação relevante já foi liberada.
Então mudamos o método.
Passamos a observar externamente o processo Node.js durante a execução.
Em uma amostragem de uma operação, observamos working set acima de 1 GB.
Mas ainda queríamos entender o comportamento sob concorrência.
18. Duas operações
Executamos duas decriptações simultaneamente.
Ambas continham:
memoryCost = 4,194,304
Resultado:
Attempt 1:4.06 secondsDECRYPTION_FAILEDAttempt 2:4.07 secondsDECRYPTION_FAILED
Tempo total:
4.07 seconds
Esse resultado era particularmente relevante.
Se fossem completamente serializadas, esperaríamos aproximadamente:T≈4+4=8s
Mas observamos:Ttotal≈T1≈T2
E isso era consistente com processamento concorrente das operações custosas.
19. O número que chamou nossa atenção
Enquanto as duas operações executavam, monitoramos o processo externamente.
As amostras mostraram:
WorkingSetMB PeakWorkingSetMB1701.53 1701.536008.97 6008.977780.09 7780.092367.04 8232.07
O maior PeakWorkingSet observado foi:8232.07 MB
aproximadamente:8.0 GiB
E tudo isso havia sido provocado por dois ciphertexts pequenos que seriam posteriormente rejeitados.
Nesse ponto interrompemos deliberadamente os testes de escala.
Não havia justificativa técnica para executar quatro, oito ou dezenas de operações e arriscar derrubar a própria máquina.
Já tínhamos evidência suficiente da amplificação.
20. Voltando ao Lean
Agora tínhamos uma propriedade muito mais interessante para formalizar.
Criamos:
inductive KdfParameterStatus where | withinBounds | outOfBounds
E:
inductive ProcessingDecision where | rejectBeforeKdf | executeKdf
Modelamos:
def decideKdfProcessing (status : KdfParameterStatus) : ProcessingDecision := match status with | KdfParameterStatus.outOfBounds => ProcessingDecision.rejectBeforeKdf | KdfParameterStatus.withinBounds => ProcessingDecision.executeKdf
E provamos:
theorem out_of_bounds_rejected_before_kdf : decideKdfProcessing KdfParameterStatus.outOfBounds = ProcessingDecision.rejectBeforeKdf := by rfl
assim como:
theorem within_bounds_executes_kdf : decideKdfProcessing KdfParameterStatus.withinBounds = ProcessingDecision.executeKdf := by rfl
Depois refinamos o estado.
21. O ponto central da propriedade formal
Criamos três estágios:
inductive ProcessingStage where | beforeKdf | afterKdfBeforeAuthentication | authenticated
E então provamos:
theorem within_bounds_reaches_pre_authentication_stage : stageAfterKdfDecision (decideKdfProcessing KdfParameterStatus.withinBounds) = ProcessingStage.afterKdfBeforeAuthentication := by rfl
A interpretação é:WithinBounds⇒ExecuteKDF⇒AfterKDFBeforeAuthentication
Isso captura exatamente a propriedade arquitetural que nos interessava.
22. O que Lean provou — e o que ele NÃO provou
Essa talvez seja a parte mais importante deste artigo.
Lean não provou:Hiprax/crypto eˊ vulneraˊvel
Também não provou:
memoryCost = 4194304→ 8 GB de RAM
Nem provou a implementação do Argon2id.
Nem verificou automaticamente o TypeScript.
O que provamos foi uma propriedade do nosso modelo abstrato:
Quando os parâmetros estão dentro dos limites aceitos, o modelo permite que o KDF seja executado antes do estágio de autenticação.
A ligação com o sistema real veio de outra fonte:
evidência empírica e análise de código.
Isso produz uma estrutura muito mais intelectualmente honesta:
┌─────────────────┐ │ Source analysis │ └────────┬────────┘ │ ▼ comportamento observado │ ┌────────────┴────────────┐ ▼ ▼ Experimentos Modelo formal │ │ ▼ ▼tempo / memória propriedades │ │ └────────────┬────────────┘ ▼ Security Finding
Nenhuma dessas camadas substitui a outra.
Elas se complementam.
23. A causa arquitetural
O problema é particularmente interessante porque não existe uma solução trivial como:
“Autentique o header antes.”
Para verificar AES-GCM, precisamos da chave.
Mas:Authentication⇒Key
e:Key⇒KDF
enquanto:KDF⇒ParametersFromHeader
Logo:Header→KDF→Key→Authentication
Não podemos simplesmente inverter para:Authentication→KDF
porque ainda não temos a chave necessária para realizar aquela autenticação.
Isso transforma o problema de um simples bug de implementação em uma questão de design de protocolo e resource governance.
24. A mitigação correta é limitar trabalho não confiável
Uma defesa mais apropriada é separar dois conceitos:MaximumSupportedKdfCost
de:MaximumAcceptedUntrustedDecryptCost
Esses limites não precisam ser iguais.
Uma biblioteca pode tecnicamente suportar um ciphertext com parâmetros extremamente altos sem necessariamente permitir que qualquer aplicação processe esse custo vindo de uma origem não confiável.
Controles possíveis incluem:
KDF ceilings configuráveis +limites específicos para decrypt +controle de concorrência +rate limiting +isolamento de workers/processos
Isso transforma a questão em:
Quanto trabalho uma entrada ainda não autenticada tem permissão para provocar?
Essa pergunta é aplicável muito além de criptografia.
25. O que tornou o finding interessante
O finding não surgiu porque encontramos uma linha obviamente insegura como:
eval(userInput)
Ele surgiu de uma composição de comportamentos individualmente razoáveis:
1. O formato precisa armazenar parâmetros KDF.
2. O decrypt precisa ler esses parâmetros.
3. Parâmetros inválidos precisam ter limites.
4. Parâmetros válidos precisam chegar ao KDF.
5. O KDF precisa executar antes que exista uma chave.
6. A chave é necessária para autenticar o ciphertext.
7. Operações podem ocorrer concorrentemente.
Separadamente, cada decisão parece perfeitamente compreensível.
Compostas:1+2+3+4+5+6+7
produzem uma propriedade de segurança emergente.
É exatamente aqui que métodos formais e raciocínio baseado em propriedades se tornam interessantes.
26. O papel dos contraexemplos
Durante a investigação, várias hipóteses nossas estavam erradas ou incompletas.
Por exemplo, poderíamos pensar:
“Se o header não estiver autenticado, qualquer campo pode ser modificado.”
Falso.
O experimento com memoryCost mostrou um contraexemplo.
O campo não estava diretamente protegido pelo AAD no modo legado, mas alterá-lo mudava a derivação da chave e fazia o AES-GCM falhar.
Também investigamos alterações no KDF ID e na versão.
Esses testes mostraram outros caminhos de parser, validação e compatibilidade.
Cada contraexemplo refinava o modelo mental.
Isso sugere uma metodologia poderosa:Hypothesis→CounterexampleSearch→Refinement
que é extremamente próxima da maneira como trabalhamos com especificações formais.
27. Formal methods não significa necessariamente provar o sistema inteiro
Existe uma percepção comum de que usar métodos formais significa necessariamente:
reescrever aplicação em linguagem formal
↓modelar cada função
↓provar centenas de teoremas
↓só então encontrar alguma coisa
Esse é um uso possível.
Mas não é o único.
Neste trabalho utilizamos Lean como uma ferramenta de precisão do raciocínio de segurança.
O processo foi:Implementation→SecurityProperty→MinimalModel→Proof
Quando o modelo não correspondia ao comportamento observado, precisávamos refiná-lo.
E esse ciclo fazia surgir novas perguntas sobre a implementação.
28. O modelo formal funcionou como uma lupa
A maior contribuição do Lean neste trabalho talvez não tenha sido o No goals.
Foi nos obrigar a decidir exatamente o que cada conceito significava.
O que significa:
tampered?
O que significa:
authenticated?
O que significa:
headerMatches?
O que significa:
withinBounds?
E principalmente:
em que estágio do processamento estamos?
Em segurança, ambiguidades escondem bugs.
Formalização força essas ambiguidades a aparecerem.
29. A cadeia de evidências
Ao final, não dependíamos de uma única técnica.
Tínhamos:
| Camada | Evidência |
|---|---|
| Documentação | Garantias e comportamento esperado |
| Source review | Ordem real de processamento |
| Unit tests existentes | Comportamentos conhecidos pelo projeto |
| Experimentos próprios | Reprodução independente |
| Boundary analysis | Diferença entre rejeitado e permitido |
| Timing | ~3–4 segundos por operação |
| OS monitoring | Consumo de memória nativa |
| Concurrency | Amplificação observada |
| Lean | Propriedades do modelo mecanicamente provadas |
Isso é muito mais forte do que dizer simplesmente:
“Executei um script e consumiu muita RAM.”
30. Responsible disclosure
Depois de consolidar a evidência, consultamos a política de segurança do projeto.
Ela explicitamente solicita que problemas de segurança não sejam publicados em Issues, Pull Requests ou Discussions, preferindo canais privados.
Também encontramos uma distinção importante na política.
O projeto considera Denial of Service via large input fora do escopo — por exemplo, passar arquivos patologicamente grandes e esperar que a criptografia não consuma recursos.
Nosso cenário, entretanto, é diferente:
Large-input DoS:gigabytes de input ↓gigabytes de trabalho
versus:
Nosso caso:~103 bytes ↓KDF cost metadata ↓gigabytes de memória observada
Por isso descrevemos o comportamento como:
Pre-Authentication Argon2id Resource Amplification via v1 Ciphertext Header
e não simplesmente como “large input DoS”.
O relatório foi submetido privadamente ao mantenedor em conformidade com a política de responsible disclosure.
Até que o processo de triagem seja concluído, a classificação final pertence ao mantenedor.
31. O finding
A hipótese submetida pode ser resumida como:
Pre-Authentication Resource Exhaustion via Attacker-Controlled Argon2id Parameters
A condição estrutural é:SmallUnauthenticatedCiphertext→AttackerInfluencedKDFParameters→ExpensiveArgon2id→AuthenticationFailure
Em nossos experimentos:
memoryCost máximo aceito:4,194,304tempo por operação:~3–4 segundosduas operações concorrentes:~4.07 segundos totalPeakWorkingSet observado:~8.23 GBresultado final:DECRYPTION_FAILED
A explorabilidade real depende do sistema consumidor.
Se somente dados confiáveis chegam ao decrypt, o risco é muito menor.
Se uma aplicação permite:
Internet ↓ciphertext controlado ↓decrypt()
o cenário muda substancialmente.
Por isso submetemos a severidade como preliminar e deployment-dependent, em vez de apresentar uma classificação absoluta.
32. A principal lição
O resultado mais importante deste estudo não é:
“Lean encontrou um DoS.”
Isso seria tecnicamente incorreto.
A conclusão mais interessante é:
Métodos formais podem mudar a maneira como fazemos security research.
Em vez de procurar somente padrões vulneráveis, podemos procurar violações de propriedades.
A metodologia passa a ser:Understand→Specify→Experiment→Formalize→Challenge→Refine
O código fornece a implementação.
Os experimentos fornecem evidência concreta.
Os contraexemplos quebram nossas hipóteses.
O monitoramento fornece impacto quantitativo.
E o sistema formal nos obriga a dizer precisamente o que estamos afirmando.
33. Segurança como problema matemático e experimental
Há algo particularmente interessante nessa abordagem.
Security research tradicionalmente mistura:
- engenharia reversa;
- conhecimento de sistemas;
- criatividade adversarial;
- experimentação.
Métodos formais adicionam uma nova dimensão:precisa˜o loˊgica
A pergunta deixa de ser apenas:
“Consigo quebrar isso?”
e passa a incluir:
“Qual propriedade deveria impedir que eu quebrasse isso?”
Depois:
“Essa propriedade realmente vale?”
E finalmente:
“Sob quais hipóteses conseguimos prová-la?”
Essa sequência aproxima segurança de áreas como matemática aplicada, verificação de software e ciência experimental.
34. Conclusão
Começamos com uma biblioteca criptográfica e uma propriedade simples:TamperedCiphertext⇒Reject
Adulteramos ciphertext.
Depois tag.
Depois chave.
Depois AAD.
Depois IV.
Investigamos headers.
Descobrimos diferenças entre modos atuais e legados.
Alteramos campos semanticamente relevantes.
Seguimos o caminho da derivação da chave.
Percebemos que o custo do KDF era determinado antes da autenticação.
Testamos os limites.
Medimos tempo.
Medimos memória.
Testamos concorrência.
E formalizamos a propriedade estrutural em Lean.
O caminho completo foi:
Cryptographic library
↓Security claims
↓Security properties
↓Source-code analysis
↓Concrete experiments
↓Counterexamples
↓Model refinement
↓Formal specification
↓Lean proofs
↓Resource measurements
↓Candidate security finding
↓Responsible disclosure
Talvez essa seja a melhor demonstração do valor de métodos formais aplicados à segurança:
eles não substituem o pesquisador, o teste ou a análise do código.
Eles tornam nossas afirmações mais precisas.
E, quando combinamos precisão matemática com experimentação adversarial, começamos a enxergar propriedades do sistema que uma leitura puramente sintática do código dificilmente revelaria.
Nota sobre disclosure
Este artigo descreve a metodologia de pesquisa e os resultados experimentais obtidos durante a análise. O comportamento foi reportado privadamente ao mantenedor para triagem de segurança.
A política do projeto prevê reconhecimento inicial em até 72 horas, decisão de triagem/severidade posteriormente e divulgação pública coordenada após eventual correção.
Até a conclusão desse processo, termos como candidate finding e potential security issue são deliberados: evidência técnica reproduzível não deve ser confundida com uma classificação final unilateral de vulnerabilidade.