M\u00e9todos formais costumam aparecer em discuss\u00f5es de seguran\u00e7a cercados por exemplos acad\u00eamicos: protocolos simplificados, m\u00e1quinas de estado artificiais, propriedades matem\u00e1ticas elegantes e sistemas constru\u00eddos especificamente para serem verificados.<\/p>\n\n\n\n
Mas o que acontece quando aplicamos essa forma de racioc\u00ednio a uma biblioteca criptogr\u00e1fica real?<\/p>\n\n\n\n
Foi exatamente esse o objetivo deste trabalho.<\/p>\n\n\n\n
Partimos de uma biblioteca TypeScript\/JavaScript existente, analisamos sua arquitetura criptogr\u00e1fica, formulamos propriedades de seguran\u00e7a, constru\u00edmos experimentos controlados e utilizamos Lean 4<\/strong> para formalizar partes relevantes do comportamento observado.<\/p>\n\n\n\n Durante esse processo, chegamos a um candidate finding particularmente interessante:<\/p>\n\n\n\n Um ciphertext pequeno e n\u00e3o autenticado pode controlar par\u00e2metros do Argon2id e provocar consumo significativo de recursos antes que a autentica\u00e7\u00e3o AES-GCM finalmente rejeite o ciphertext.<\/strong><\/p>\n<\/blockquote>\n\n\n\n Em nossos experimentos, duas opera\u00e7\u00f5es concorrentes com ciphertexts adulterados levaram o processo Node.js a um pico observado de aproximadamente 8 GB de working set<\/strong>, embora ambas terminassem posteriormente em Mais interessante que o finding isoladamente, por\u00e9m, \u00e9 como chegamos at\u00e9 ele<\/strong>.<\/p>\n\n\n\n Este artigo apresenta esse caminho.<\/p>\n\n\n\n O projeto come\u00e7ou com uma pergunta diferente:<\/p>\n\n\n\n Podemos pegar uma biblioteca criptogr\u00e1fica real e transformar suas garantias de seguran\u00e7a em propriedades que possam ser investigadas experimentalmente e formalizadas?<\/p>\n<\/blockquote>\n\n\n\n Essa diferen\u00e7a de abordagem \u00e9 importante.<\/p>\n\n\n\n Em vez de come\u00e7ar procurando padr\u00f5es conhecidos de vulnerabilidade, come\u00e7amos identificando as propriedades que deveriam permanecer verdadeiras<\/strong>.<\/p>\n\n\n\n Por exemplo:Decryptk\u200b(Encryptk\u200b(m))=m<\/p>\n\n\n\n Essa \u00e9 uma propriedade funcional b\u00e1sica.<\/p>\n\n\n\n Mas tamb\u00e9m podemos formular propriedades de seguran\u00e7a:Tamper(C)\u21d2Reject(C)<\/p>\n\n\n\n ou:WrongKey\u21d2Reject<\/p>\n\n\n\n e:WrongAAD\u21d2Reject<\/p>\n\n\n\n A mudan\u00e7a conceitual \u00e9 pequena, mas poderosa.<\/p>\n\n\n\n Em vez de perguntar:<\/p>\n\n\n\n \u201cExiste um bug aqui?\u201d<\/p>\n<\/blockquote>\n\n\n\n passamos a perguntar:<\/p>\n\n\n\n \u201cQuais propriedades precisam permanecer verdadeiras para que esse sistema seja seguro?\u201d<\/p>\n<\/blockquote>\n\n\n\n E ent\u00e3o tentamos quebr\u00e1-las.<\/p>\n\n\n\n O laborat\u00f3rio foi realizado sobre uma pequena biblioteca criptogr\u00e1fica TypeScript\/JavaScript.<\/p>\n\n\n\n A vers\u00e3o analisada implementava, entre outros mecanismos:<\/p>\n\n\n\n A arquitetura conceitual que nos interessava inicialmente era aproximadamente:<\/p>\n\n\n\n Nosso primeiro objetivo era entender quatro coisas:<\/p>\n\n\n\n Isso nos levou diretamente ao c\u00f3digo respons\u00e1vel pela decripta\u00e7\u00e3o.<\/p>\n\n\n\n Uma biblioteca criptogr\u00e1fica normalmente apresenta afirma\u00e7\u00f5es como:<\/p>\n\n\n\n ciphertext adulterado deve ser rejeitado.<\/p>\n<\/blockquote>\n\n\n\n Isso pode ser transformado em uma propriedade:C\u2032\ue020=C\u21d2Decrypt(C\u2032)=Failure<\/p>\n\n\n\n Claro que essa formula\u00e7\u00e3o ainda \u00e9 simplificada demais para representar AES-GCM corretamente.<\/p>\n\n\n\n Mas ela nos d\u00e1 algo extremamente \u00fatil:<\/p>\n\n\n\n uma propriedade test\u00e1vel.<\/strong><\/p>\n\n\n\n Come\u00e7amos ent\u00e3o pelos casos mais \u00f3bvios.<\/p>\n\n\n\n Produzimos um ciphertext v\u00e1lido e modificamos um byte.<\/p>\n\n\n\n Conceitualmente:<\/p>\n\n\n\n A altera\u00e7\u00e3o foi m\u00ednima:0x66\u22950x01=0x67<\/p>\n\n\n\n A biblioteca rejeitou o resultado:<\/p>\n\n\n\n Primeira propriedade observada:TamperedCiphertext\u21d2Reject<\/p>\n\n\n\n At\u00e9 aqui, comportamento esperado.<\/p>\n\n\n\n Mas ent\u00e3o fizemos algo diferente.<\/p>\n\n\n\n Formalizamos a ideia.<\/p>\n\n\n\n Criamos uma representa\u00e7\u00e3o m\u00ednima de ciphertext:<\/p>\n\n\n\n E uma opera\u00e7\u00e3o de adultera\u00e7\u00e3o:<\/p>\n\n\n\n Primeiro provamos que a opera\u00e7\u00e3o realmente altera um ciphertext n\u00e3o vazio:<\/p>\n\n\n\n Depois constru\u00edmos um modelo abstrato de rejei\u00e7\u00e3o.<\/p>\n\n\n\n A ideia era simples:<\/p>\n\n\n\n E provamos no modelo:Tamper(C)\u21d2Reject(C)<\/p>\n\n\n\n Isso n\u00e3o prova AES-GCM.<\/p>\n\n\n\n Tamb\u00e9m n\u00e3o prova a implementa\u00e7\u00e3o JavaScript.<\/p>\n\n\n\n Prova uma propriedade do modelo que constru\u00edmos<\/strong>.<\/p>\n\n\n\n Essa distin\u00e7\u00e3o se tornaria fundamental posteriormente.<\/p>\n\n\n\n Repetimos o processo para diferentes componentes autenticados.<\/p>\n\n\n\n Testamos:<\/p>\n\n\n\n Cada experimento produzia evid\u00eancia concreta da implementa\u00e7\u00e3o.<\/p>\n\n\n\n Paralelamente, criamos modelos em Lean para representar as propriedades correspondentes.<\/p>\n\n\n\n O resultado come\u00e7ou a formar uma cadeia:<\/p>\n\n\n\n E foi justamente seguindo essa cadeia que encontramos algo mais interessante.<\/p>\n\n\n\n Durante a an\u00e1lise dos testes do pr\u00f3prio projeto, encontramos refer\u00eancias a uma configura\u00e7\u00e3o relacionada \u00e0 autentica\u00e7\u00e3o do header v1.<\/p>\n\n\n\n O comportamento legado existia para permitir compatibilidade com ciphertexts antigos.<\/p>\n\n\n\n No modo atual, o header era incorporado ao AAD.<\/p>\n\n\n\n Conceitualmente:AAD=Context\u2225Header<\/p>\n\n\n\n No modo legado:AAD=Context<\/p>\n\n\n\n O header deixava de participar diretamente da autentica\u00e7\u00e3o AES-GCM.<\/p>\n\n\n\n Isso imediatamente levantou uma pergunta:<\/p>\n\n\n\n O modo legado serve apenas para ler<\/strong> ciphertexts antigos ou tamb\u00e9m afeta a cria\u00e7\u00e3o de novos<\/strong> ciphertexts?<\/p>\n<\/blockquote>\n\n\n\n Seguimos o fluxo no c\u00f3digo.<\/p>\n\n\n\n E encontramos que a mesma decis\u00e3o era utilizada no caminho de encryption.<\/p>\n\n\n\n Em termos simplificados:<\/p>\n\n\n\n enquanto:<\/p>\n\n\n\n Isso significava que o modo de compatibilidade tamb\u00e9m poderia produzir novos ciphertexts utilizando a sem\u00e2ntica legada.<\/p>\n\n\n\n Criamos ent\u00e3o um novo ciphertext com o modo legado habilitado.<\/p>\n\n\n\n Depois modificamos o primeiro byte reservado do header:<\/p>\n\n\n\n O resultado foi particularmente interessante.<\/p>\n\n\n\n No modo legado:<\/p>\n\n\n\n No modo atual\/default:<\/p>\n\n\n\n Mas ainda n\u00e3o t\u00ednhamos necessariamente uma vulnerabilidade.<\/p>\n\n\n\n Precis\u00e1vamos entender por qu\u00ea<\/strong>.<\/p>\n\n\n\n Inspecionando o parser do formato v1, identificamos o layout relevante:<\/p>\n\n\n\n O detalhe crucial:<\/p>\n\n\n\n os bytes reservados n\u00e3o eram utilizados semanticamente pelo parser.<\/strong><\/p>\n\n\n\n Portanto, modificar:<\/p>\n\n\n\n n\u00e3o alterava:<\/p>\n\n\n\n No modo legado, aquele byte tamb\u00e9m n\u00e3o participava do AAD.<\/p>\n\n\n\n Consequentemente:<\/p>\n\n\n\n No modo seguro:<\/p>\n\n\n\n Agora t\u00ednhamos uma explica\u00e7\u00e3o estrutural.<\/p>\n\n\n\n Representamos essa diferen\u00e7a em Lean:<\/p>\n\n\n\n O estado abstrato possu\u00eda duas propriedades:<\/p>\n\n\n\n No modo seguro:Success\u27faPayloadAuthenticated\u2227HeaderMatches<\/p>\n\n\n\n No modo legado:Success\u27faPayloadAuthenticated<\/p>\n\n\n\n Isso permitiu provar:Secure\u2227HeaderModified\u21d2Failure<\/p>\n\n\n\n e:Legacy\u2227PayloadValid\u2227HeaderModified\u21d2Success<\/p>\n\n\n\n Novamente:<\/p>\n\n\n\n Lean n\u00e3o estava descobrindo o comportamento do JavaScript.<\/strong><\/p>\n\n\n\n Ele estava nos obrigando a escrever precisamente qual propriedade acredit\u00e1vamos que o sistema possu\u00eda.<\/p>\n\n\n\n Essa disciplina acabou sendo extremamente \u00fatil.<\/p>\n\n\n\n Aqui aconteceu uma parte particularmente importante da investiga\u00e7\u00e3o.<\/p>\n\n\n\n Poder\u00edamos ter parado no primeiro comportamento interessante e conclu\u00eddo:<\/p>\n\n\n\n \u201cO header n\u00e3o \u00e9 protegido no modo legado.\u201d<\/p>\n<\/blockquote>\n\n\n\n Mas isso seria uma simplifica\u00e7\u00e3o excessiva.<\/p>\n\n\n\n Decidimos modificar outro campo.<\/p>\n\n\n\n Desta vez:<\/p>\n\n\n\n Original:<\/p>\n\n\n\n Adulterado:<\/p>\n\n\n\n Resultado:<\/p>\n\n\n\n Por qu\u00ea?<\/p>\n\n\n\n Porque Ele participa da deriva\u00e7\u00e3o da chave.<\/p>\n\n\n\n Assim:memoryCost\u2032\ue020=memoryCost<\/p>\n\n\n\n faz com que:KDF(password,salt,params\u2032)\ue020=KDF(password,salt,params)<\/p>\n\n\n\n e consequentemente:K\u2032\ue020=K<\/p>\n\n\n\n A autentica\u00e7\u00e3o AES-GCM falha.<\/p>\n\n\n\n Isso nos deu uma distin\u00e7\u00e3o muito mais precisa:<\/p>\n\n\n\n Alguns campos do header n\u00e3o estavam diretamente vinculados ao AAD no modo legado, mas altera\u00e7\u00f5es em campos semanticamente utilizados pelo KDF ainda poderiam ser detectadas indiretamente por produzirem uma chave diferente.<\/p>\n<\/blockquote>\n\n\n\n Esse tipo de refinamento \u00e9 exatamente o que uma an\u00e1lise s\u00e9ria precisa fazer.<\/p>\n\n\n\n Enquanto investig\u00e1vamos Para descobrir que a chave estava errada, o sistema precisava primeiro calcular a chave<\/strong>.<\/p>\n\n\n\n Ou seja:<\/p>\n\n\n\n Ent\u00e3o fizemos uma nova pergunta:<\/p>\n\n\n\n Quem controla o custo do Argon2id antes da autentica\u00e7\u00e3o?<\/p>\n<\/blockquote>\n\n\n\n A resposta era:<\/p>\n\n\n\n o pr\u00f3prio ciphertext.<\/strong><\/p>\n\n\n\n Esse foi o ponto em que a investiga\u00e7\u00e3o mudou de dire\u00e7\u00e3o.<\/p>\n\n\n\n At\u00e9 aquele momento est\u00e1vamos essencialmente estudando:Integrity<\/p>\n\n\n\n Agora surgiu uma propriedade relacionada a:Availability<\/p>\n\n\n\n Poder\u00edamos formul\u00e1-la informalmente como:UntrustedInput\ue020\u21d2ExcessivePreAuthenticationWork<\/p>\n\n\n\n Mas o fluxo parecia permitir:UnauthenticatedHeader\u2192KDFParameters\u2192ExpensiveKDF\u2192Authentication<\/p>\n\n\n\n Ou seja, o sistema precisava gastar recursos antes de saber se aquele ciphertext era leg\u00edtimo.<\/p>\n\n\n\n A implementa\u00e7\u00e3o n\u00e3o aceitava qualquer valor.<\/p>\n\n\n\n Testamos:<\/p>\n\n\n\n Resultado:<\/p>\n\n\n\n O pr\u00f3prio erro revelou os limites:<\/p>\n\n\n\n Isso \u00e9 importante.<\/p>\n\n\n\n N\u00e3o seria correto escrever:<\/p>\n\n\n\n \u201cA biblioteca permite memoryCost arbitr\u00e1rio.\u201d<\/p>\n<\/blockquote>\n\n\n\n Ela n\u00e3o permite.<\/p>\n\n\n\n Existe uma mitiga\u00e7\u00e3o expl\u00edcita.<\/p>\n\n\n\n A pergunta correta passou a ser:<\/p>\n\n\n\n O maior valor permitido<\/strong> ainda \u00e9 perigoso em um contexto de input n\u00e3o confi\u00e1vel?<\/p>\n<\/blockquote>\n\n\n\n Alteramos ent\u00e3o:<\/p>\n\n\n\n Ou seja:memoryCost=MAX<\/p>\n\n\n\n O parser aceitou.<\/p>\n\n\n\n O Argon2id foi executado.<\/p>\n\n\n\n Somente depois a autentica\u00e7\u00e3o falhou:<\/p>\n\n\n\n Tempo observado:<\/p>\n\n\n\n Em outra execu\u00e7\u00e3o:<\/p>\n\n\n\n Um ciphertext inv\u00e1lido conseguia, portanto, provocar v\u00e1rios segundos de processamento antes de ser rejeitado<\/strong>.<\/p>\n\n\n\n E o ciphertext tinha aproximadamente:<\/p>\n\n\n\n Esse detalhe seria crucial posteriormente.<\/p>\n\n\n\n Esse comportamento \u00e9 diferente do caso trivial:<\/p>\n\n\n\n Aqui temos:<\/p>\n\n\n\n Ou seja, existe uma rela\u00e7\u00e3o de amplifica\u00e7\u00e3o<\/strong>:SmallInput\u2192LargeResourceCost<\/p>\n\n\n\n O custo n\u00e3o \u00e9 proporcional ao tamanho do ciphertext.<\/p>\n\n\n\n \u00c9 determinado por metadata control\u00e1vel antes da autentica\u00e7\u00e3o.<\/p>\n\n\n\n Primeiro utilizamos:<\/p>\n\n\n\n Antes:<\/p>\n\n\n\n Depois:<\/p>\n\n\n\n \u00c0 primeira vista parecia que praticamente nenhuma mem\u00f3ria tinha sido utilizada.<\/p>\n\n\n\n Mas havia um problema metodol\u00f3gico.<\/p>\n\n\n\n O Argon2id utiliza mem\u00f3ria nativa, e uma medi\u00e7\u00e3o realizada depois<\/strong> da opera\u00e7\u00e3o pode acontecer quando a aloca\u00e7\u00e3o relevante j\u00e1 foi liberada.<\/p>\n\n\n\n Ent\u00e3o mudamos o m\u00e9todo.<\/p>\n\n\n\n Passamos a observar externamente o processo Node.js durante a execu\u00e7\u00e3o.<\/p>\n\n\n\n Em uma amostragem de uma opera\u00e7\u00e3o, observamos working set acima de 1 GB<\/strong>.<\/p>\n\n\n\n Mas ainda quer\u00edamos entender o comportamento sob concorr\u00eancia.<\/p>\n\n\n\n Executamos duas decripta\u00e7\u00f5es simultaneamente.<\/p>\n\n\n\n Ambas continham:<\/p>\n\n\n\n Resultado:<\/p>\n\n\n\n Tempo total:<\/p>\n\n\n\n Esse resultado era particularmente relevante.<\/p>\n\n\n\n Se fossem completamente serializadas, esperar\u00edamos aproximadamente:T\u22484+4=8s<\/p>\n\n\n\n Mas observamos:Ttotal\u200b\u2248T1\u200b\u2248T2\u200b<\/p>\n\n\n\n E isso era consistente com processamento concorrente das opera\u00e7\u00f5es custosas.<\/p>\n\n\n\n Enquanto as duas opera\u00e7\u00f5es executavam, monitoramos o processo externamente.<\/p>\n\n\n\n As amostras mostraram:<\/p>\n\n\n\n O maior aproximadamente:8.0 GiB<\/p>\n\n\n\n E tudo isso havia sido provocado por dois ciphertexts pequenos que seriam posteriormente rejeitados<\/strong>.<\/p>\n\n\n\n Nesse ponto interrompemos deliberadamente os testes de escala.<\/p>\n\n\n\n N\u00e3o havia justificativa t\u00e9cnica para executar quatro, oito ou dezenas de opera\u00e7\u00f5es e arriscar derrubar a pr\u00f3pria m\u00e1quina.<\/p>\n\n\n\n J\u00e1 t\u00ednhamos evid\u00eancia suficiente da amplifica\u00e7\u00e3o.<\/p>\n\n\n\n Agora t\u00ednhamos uma propriedade muito mais interessante para formalizar.<\/p>\n\n\n\n Criamos:<\/p>\n\n\n\n E:<\/p>\n\n\n\n Modelamos:<\/p>\n\n\n\n E provamos:<\/p>\n\n\n\n assim como:<\/p>\n\n\n\n Depois refinamos o estado.<\/p>\n\n\n\n Criamos tr\u00eas est\u00e1gios:<\/p>\n\n\n\n E ent\u00e3o provamos:<\/p>\n\n\n\n A interpreta\u00e7\u00e3o \u00e9:WithinBounds\u21d2ExecuteKDF\u21d2AfterKDFBeforeAuthentication<\/p>\n\n\n\n Isso captura exatamente a propriedade arquitetural que nos interessava.<\/p>\n\n\n\n Essa talvez seja a parte mais importante deste artigo.<\/p>\n\n\n\n Lean n\u00e3o provou<\/strong>:Hiprax\/crypto e\u02ca vulnera\u02cavel<\/p>\n\n\n\n Tamb\u00e9m n\u00e3o provou:<\/p>\n\n\n\n Nem provou a implementa\u00e7\u00e3o do Argon2id.<\/p>\n\n\n\n Nem verificou automaticamente o TypeScript.<\/p>\n\n\n\n O que provamos foi uma propriedade do nosso modelo abstrato<\/strong>:<\/p>\n\n\n\n Quando os par\u00e2metros est\u00e3o dentro dos limites aceitos, o modelo permite que o KDF seja executado antes do est\u00e1gio de autentica\u00e7\u00e3o.<\/p>\n<\/blockquote>\n\n\n\n A liga\u00e7\u00e3o com o sistema real veio de outra fonte:<\/p>\n\n\n\n evid\u00eancia emp\u00edrica e an\u00e1lise de c\u00f3digo.<\/strong><\/p>\n\n\n\n Isso produz uma estrutura muito mais intelectualmente honesta:<\/p>\n\n\n\n Nenhuma dessas camadas substitui a outra.<\/p>\n\n\n\n Elas se complementam.<\/p>\n\n\n\n O problema \u00e9 particularmente interessante porque n\u00e3o existe uma solu\u00e7\u00e3o trivial como:<\/p>\n\n\n\n \u201cAutentique o header antes.\u201d<\/p>\n<\/blockquote>\n\n\n\n Para verificar AES-GCM, precisamos da chave.<\/p>\n\n\n\n Mas:Authentication\u21d2Key<\/p>\n\n\n\n e:Key\u21d2KDF<\/p>\n\n\n\n enquanto:KDF\u21d2ParametersFromHeader<\/p>\n\n\n\n Logo:Header\u2192KDF\u2192Key\u2192Authentication<\/p>\n\n\n\n N\u00e3o podemos simplesmente inverter para:Authentication\u2192KDF<\/p>\n\n\n\n porque ainda n\u00e3o temos a chave necess\u00e1ria para realizar aquela autentica\u00e7\u00e3o.<\/p>\n\n\n\n Isso transforma o problema de um simples bug de implementa\u00e7\u00e3o em uma quest\u00e3o de design de protocolo e resource governance<\/strong>.<\/p>\n\n\n\n Uma defesa mais apropriada \u00e9 separar dois conceitos:MaximumSupportedKdfCost<\/p>\n\n\n\n de:MaximumAcceptedUntrustedDecryptCost<\/p>\n\n\n\n Esses limites n\u00e3o precisam ser iguais.<\/p>\n\n\n\n Uma biblioteca pode tecnicamente suportar um ciphertext com par\u00e2metros extremamente altos sem necessariamente permitir que qualquer aplica\u00e7\u00e3o processe esse custo vindo de uma origem n\u00e3o confi\u00e1vel.<\/p>\n\n\n\n Controles poss\u00edveis incluem:<\/p>\n\n\n\n Isso transforma a quest\u00e3o em:<\/p>\n\n\n\n Quanto trabalho uma entrada ainda n\u00e3o autenticada tem permiss\u00e3o para provocar?<\/p>\n<\/blockquote>\n\n\n\n Essa pergunta \u00e9 aplic\u00e1vel muito al\u00e9m de criptografia.<\/p>\n\n\n\n O finding n\u00e3o surgiu porque encontramos uma linha obviamente insegura como:<\/p>\n\n\n\n Ele surgiu de uma composi\u00e7\u00e3o de comportamentos individualmente razo\u00e1veis:<\/p>\n\n\n\n Separadamente, cada decis\u00e3o parece perfeitamente compreens\u00edvel.<\/p>\n\n\n\n Compostas:1+2+3+4+5+6+7<\/p>\n\n\n\n produzem uma propriedade de seguran\u00e7a emergente.<\/p>\n\n\n\n \u00c9 exatamente aqui que m\u00e9todos formais e racioc\u00ednio baseado em propriedades se tornam interessantes.<\/p>\n\n\n\n Durante a investiga\u00e7\u00e3o, v\u00e1rias hip\u00f3teses nossas estavam erradas ou incompletas.<\/p>\n\n\n\n Por exemplo, poder\u00edamos pensar:<\/p>\n\n\n\n \u201cSe o header n\u00e3o estiver autenticado, qualquer campo pode ser modificado.\u201d<\/p>\n<\/blockquote>\n\n\n\n Falso.<\/p>\n\n\n\n O experimento com O campo n\u00e3o estava diretamente protegido pelo AAD no modo legado, mas alter\u00e1-lo mudava a deriva\u00e7\u00e3o da chave e fazia o AES-GCM falhar.<\/p>\n\n\n\n Tamb\u00e9m investigamos altera\u00e7\u00f5es no KDF ID e na vers\u00e3o.<\/p>\n\n\n\n Esses testes mostraram outros caminhos de parser, valida\u00e7\u00e3o e compatibilidade.<\/p>\n\n\n\n Cada contraexemplo refinava o modelo mental.<\/p>\n\n\n\n Isso sugere uma metodologia poderosa:Hypothesis\u2192CounterexampleSearch\u2192Refinement<\/p>\n\n\n\n que \u00e9 extremamente pr\u00f3xima da maneira como trabalhamos com especifica\u00e7\u00f5es formais.<\/p>\n\n\n\n Existe uma percep\u00e7\u00e3o comum de que usar m\u00e9todos formais significa necessariamente:<\/p>\n\n\n\n Esse \u00e9 um uso poss\u00edvel.<\/p>\n\n\n\n Mas n\u00e3o \u00e9 o \u00fanico.<\/p>\n\n\n\n Neste trabalho utilizamos Lean como uma ferramenta de precis\u00e3o do racioc\u00ednio de seguran\u00e7a<\/strong>.<\/p>\n\n\n\n O processo foi:Implementation\u2192SecurityProperty\u2192MinimalModel\u2192Proof<\/p>\n\n\n\n Quando o modelo n\u00e3o correspondia ao comportamento observado, precis\u00e1vamos refin\u00e1-lo.<\/p>\n\n\n\n E esse ciclo fazia surgir novas perguntas sobre a implementa\u00e7\u00e3o.<\/p>\n\n\n\n A maior contribui\u00e7\u00e3o do Lean neste trabalho talvez n\u00e3o tenha sido o Foi nos obrigar a decidir exatamente o que cada conceito significava.<\/p>\n\n\n\n O que significa:<\/p>\n\n\n\n O que significa:<\/p>\n\n\n\n O que significa:<\/p>\n\n\n\n O que significa:<\/p>\n\n\n\n E principalmente:<\/p>\n\n\n\n Em seguran\u00e7a, ambiguidades escondem bugs.<\/p>\n\n\n\n Formaliza\u00e7\u00e3o for\u00e7a essas ambiguidades a aparecerem.<\/p>\n\n\n\n Ao final, n\u00e3o depend\u00edamos de uma \u00fanica t\u00e9cnica.<\/p>\n\n\n\n T\u00ednhamos:<\/p>\n\n\n\n Isso \u00e9 muito mais forte do que dizer simplesmente:<\/p>\n\n\n\n \u201cExecutei um script e consumiu muita RAM.\u201d<\/p>\n<\/blockquote>\n\n\n\n Depois de consolidar a evid\u00eancia, consultamos a pol\u00edtica de seguran\u00e7a do projeto.<\/p>\n\n\n\n Ela explicitamente solicita que problemas de seguran\u00e7a n\u00e3o sejam publicados em Issues, Pull Requests ou Discussions<\/strong>, preferindo canais privados.<\/p>\n\n\n\n Tamb\u00e9m encontramos uma distin\u00e7\u00e3o importante na pol\u00edtica.<\/p>\n\n\n\n O projeto considera Denial of Service via large input<\/strong> fora do escopo \u2014 por exemplo, passar arquivos patologicamente grandes e esperar que a criptografia n\u00e3o consuma recursos.<\/p>\n\n\n\n Nosso cen\u00e1rio, entretanto, \u00e9 diferente:<\/p>\n\n\n\n versus:<\/p>\n\n\n\n Por isso descrevemos o comportamento como:<\/p>\n\n\n\n Pre-Authentication Argon2id Resource Amplification via v1 Ciphertext Header<\/strong><\/p>\n<\/blockquote>\n\n\n\n e n\u00e3o simplesmente como \u201clarge input DoS\u201d.<\/p>\n\n\n\n O relat\u00f3rio foi submetido privadamente ao mantenedor em conformidade com a pol\u00edtica de responsible disclosure.<\/p>\n\n\n\n At\u00e9 que o processo de triagem seja conclu\u00eddo, a classifica\u00e7\u00e3o final pertence ao mantenedor.<\/strong><\/p>\n\n\n\n A hip\u00f3tese submetida pode ser resumida como:<\/p>\n\n\n\n A condi\u00e7\u00e3o estrutural \u00e9:SmallUnauthenticatedCiphertext\u2192AttackerInfluencedKDFParameters\u2192ExpensiveArgon2id\u2192AuthenticationFailure<\/p>\n\n\n\n Em nossos experimentos:<\/p>\n\n\n\n A explorabilidade real depende do sistema consumidor.<\/p>\n\n\n\n Se somente dados confi\u00e1veis chegam ao decrypt, o risco \u00e9 muito menor.<\/p>\n\n\n\n Se uma aplica\u00e7\u00e3o permite:<\/p>\n\n\n\n o cen\u00e1rio muda substancialmente.<\/p>\n\n\n\n Por isso submetemos a severidade como preliminar e deployment-dependent<\/strong>, em vez de apresentar uma classifica\u00e7\u00e3o absoluta.<\/p>\n\n\n\n O resultado mais importante deste estudo n\u00e3o \u00e9:<\/p>\n\n\n\n \u201cLean encontrou um DoS.\u201d<\/p>\n<\/blockquote>\n\n\n\n Isso seria tecnicamente incorreto.<\/p>\n\n\n\n A conclus\u00e3o mais interessante \u00e9:<\/p>\n\n\n\n M\u00e9todos formais podem mudar a maneira como fazemos security research.<\/strong><\/p>\n<\/blockquote>\n\n\n\n Em vez de procurar somente padr\u00f5es vulner\u00e1veis, podemos procurar viola\u00e7\u00f5es de propriedades.<\/p>\n\n\n\n A metodologia passa a ser:Understand\u2192Specify\u2192Experiment\u2192Formalize\u2192Challenge\u2192Refine\u200b<\/p>\n\n\n\n O c\u00f3digo fornece a implementa\u00e7\u00e3o.<\/p>\n\n\n\n Os experimentos fornecem evid\u00eancia concreta.<\/p>\n\n\n\n Os contraexemplos quebram nossas hip\u00f3teses.<\/p>\n\n\n\n O monitoramento fornece impacto quantitativo.<\/p>\n\n\n\n E o sistema formal nos obriga a dizer precisamente o que estamos afirmando<\/strong>.<\/p>\n\n\n\n H\u00e1 algo particularmente interessante nessa abordagem.<\/p>\n\n\n\n Security research tradicionalmente mistura:<\/p>\n\n\n\n M\u00e9todos formais adicionam uma nova dimens\u00e3o:precisa\u02dco lo\u02cagica<\/p>\n\n\n\n A pergunta deixa de ser apenas:<\/p>\n\n\n\n \u201cConsigo quebrar isso?\u201d<\/p>\n<\/blockquote>\n\n\n\n e passa a incluir:<\/p>\n\n\n\n \u201cQual propriedade deveria impedir que eu quebrasse isso?\u201d<\/p>\n<\/blockquote>\n\n\n\n Depois:<\/p>\n\n\n\n \u201cEssa propriedade realmente vale?\u201d<\/p>\n<\/blockquote>\n\n\n\n E finalmente:<\/p>\n\n\n\n \u201cSob quais hip\u00f3teses conseguimos prov\u00e1-la?\u201d<\/p>\n<\/blockquote>\n\n\n\n Essa sequ\u00eancia aproxima seguran\u00e7a de \u00e1reas como matem\u00e1tica aplicada, verifica\u00e7\u00e3o de software e ci\u00eancia experimental.<\/p>\n\n\n\n Come\u00e7amos com uma biblioteca criptogr\u00e1fica e uma propriedade simples:TamperedCiphertext\u21d2Reject<\/p>\n\n\n\n Adulteramos ciphertext.<\/p>\n\n\n\n Depois tag.<\/p>\n\n\n\n Depois chave.<\/p>\n\n\n\n Depois AAD.<\/p>\n\n\n\n Depois IV.<\/p>\n\n\n\n Investigamos headers.<\/p>\n\n\n\n Descobrimos diferen\u00e7as entre modos atuais e legados.<\/p>\n\n\n\n Alteramos campos semanticamente relevantes.<\/p>\n\n\n\n Seguimos o caminho da deriva\u00e7\u00e3o da chave.<\/p>\n\n\n\n Percebemos que o custo do KDF era determinado antes da autentica\u00e7\u00e3o.<\/p>\n\n\n\n Testamos os limites.<\/p>\n\n\n\n Medimos tempo.<\/p>\n\n\n\n Medimos mem\u00f3ria.<\/p>\n\n\n\n Testamos concorr\u00eancia.<\/p>\n\n\n\n E formalizamos a propriedade estrutural em Lean.<\/p>\n\n\n\n O caminho completo foi:<\/p>\n\n\n\n Talvez essa seja a melhor demonstra\u00e7\u00e3o do valor de m\u00e9todos formais aplicados \u00e0 seguran\u00e7a:<\/p>\n\n\n\n eles n\u00e3o substituem o pesquisador, o teste ou a an\u00e1lise do c\u00f3digo.<\/strong><\/p>\n\n\n\n Eles tornam nossas afirma\u00e7\u00f5es mais precisas.<\/p>\n\n\n\n E, quando combinamos precis\u00e3o matem\u00e1tica com experimenta\u00e7\u00e3o adversarial, come\u00e7amos a enxergar propriedades do sistema que uma leitura puramente sint\u00e1tica do c\u00f3digo dificilmente revelaria.<\/p>\n\n\n\n Este artigo descreve a metodologia de pesquisa e os resultados experimentais obtidos durante a an\u00e1lise<\/strong>. O comportamento foi reportado privadamente ao mantenedor para triagem de seguran\u00e7a.<\/p>\n\n\n\n A pol\u00edtica do projeto prev\u00ea reconhecimento inicial em at\u00e9 72 horas, decis\u00e3o de triagem\/severidade posteriormente e divulga\u00e7\u00e3o p\u00fablica coordenada ap\u00f3s eventual corre\u00e7\u00e3o.<\/p>\n\n\n\n At\u00e9 a conclus\u00e3o desse processo, termos como candidate finding<\/em> e potential security issue<\/em> s\u00e3o deliberados: evid\u00eancia t\u00e9cnica reproduz\u00edvel n\u00e3o deve ser confundida com uma classifica\u00e7\u00e3o final unilateral de vulnerabilidade.<\/strong><\/p>\n","protected":false},"excerpt":{"rendered":" Introdu\u00e7\u00e3o M\u00e9todos formais costumam aparecer em discuss\u00f5es de […]<\/p>\n","protected":false},"author":1,"featured_media":315,"comment_status":"open","ping_status":"open","sticky":false,"template":"","format":"standard","meta":{"footnotes":""},"categories":[37,17,29,13,10],"tags":[],"class_list":["post-314","post","type-post","status-publish","format-standard","has-post-thumbnail","hentry","category-criptografia","category-fikresekhel","category-pesquisa","category-research","category-secure-coding"],"_links":{"self":[{"href":"https:\/\/fikresekhel.com\/blog\/wp-json\/wp\/v2\/posts\/314","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/fikresekhel.com\/blog\/wp-json\/wp\/v2\/posts"}],"about":[{"href":"https:\/\/fikresekhel.com\/blog\/wp-json\/wp\/v2\/types\/post"}],"author":[{"embeddable":true,"href":"https:\/\/fikresekhel.com\/blog\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/fikresekhel.com\/blog\/wp-json\/wp\/v2\/comments?post=314"}],"version-history":[{"count":1,"href":"https:\/\/fikresekhel.com\/blog\/wp-json\/wp\/v2\/posts\/314\/revisions"}],"predecessor-version":[{"id":316,"href":"https:\/\/fikresekhel.com\/blog\/wp-json\/wp\/v2\/posts\/314\/revisions\/316"}],"wp:featuredmedia":[{"embeddable":true,"href":"https:\/\/fikresekhel.com\/blog\/wp-json\/wp\/v2\/media\/315"}],"wp:attachment":[{"href":"https:\/\/fikresekhel.com\/blog\/wp-json\/wp\/v2\/media?parent=314"}],"wp:term":[{"taxonomy":"category","embeddable":true,"href":"https:\/\/fikresekhel.com\/blog\/wp-json\/wp\/v2\/categories?post=314"},{"taxonomy":"post_tag","embeddable":true,"href":"https:\/\/fikresekhel.com\/blog\/wp-json\/wp\/v2\/tags?post=314"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}\n
DECRYPTION_FAILED<\/code>.<\/p>\n\n\n\n
\n\n\n\n1. O objetivo n\u00e3o era \u201cca\u00e7ar vulnerabilidades\u201d<\/h1>\n\n\n\n
\n
\n
\n
\n\n\n\n2. O alvo da an\u00e1lise<\/h1>\n\n\n\n
\n
Application \u2502 \u25bcCrypto API \u2502 \u25bcKDF \u2502 \u25bcAES-GCM \u2502 \u25bcCiphertext container \u250c\u2500\u2500\u253c\u2500\u2500\u2500\u2500\u252c\u2500\u2500\u2500\u2500\u2500\u2510salt IV tag ciphertext<\/pre>\n\n\n\n
Onde a chave chega ao AES-GCM?De onde vem o IV?Onde o authentication tag \u00e9 produzido e verificado?O que acontece quando a autentica\u00e7\u00e3o falha?<\/pre>\n\n\n\n
\n\n\n\n3. Primeiro princ\u00edpio: transformar documenta\u00e7\u00e3o em propriedades<\/h1>\n\n\n\n
\n
\n\n\n\n4. Experimento 1 \u2014 adulterando o ciphertext<\/h1>\n\n\n\n
Original:66 77 61 2f ...Tampered:67 77 61 2f ...<\/pre>\n\n\n\n
Decryption rejected.Type: DECRYPTION_FAILEDCode: DECRYPTION_FAILED<\/pre>\n\n\n\n
\n\n\n\n5. Levando a propriedade para Lean<\/h1>\n\n\n\n
abbrev Ciphertext := List UInt8<\/pre>\n\n\n\n
def tamperFirstByte (c : Ciphertext) : Ciphertext := match c with | [] => [] | b :: rest => (b ^^^ 1) :: rest<\/pre>\n\n\n\n
theorem tamper_changes_nonempty (b : UInt8) (rest : List UInt8) : tamperFirstByte (b :: rest) \u2260 (b :: rest) := by intro h simp [tamperFirstByte] at h bv_decide<\/pre>\n\n\n\n
received == expected \u2193 successreceived != expected \u2193 failure<\/pre>\n\n\n\n
\n\n\n\n6. Construindo evid\u00eancia em v\u00e1rias camadas<\/h1>\n\n\n\n
ciphertext alterado \u2192 rejeitadotag alterada \u2192 rejeitadachave incorreta \u2192 rejeitadaAAD incorreto \u2192 rejeitadoIV incorreto \u2192 rejeitado<\/pre>\n\n\n\n
Documenta\u00e7\u00e3o \u2193Propriedade esperada \u2193C\u00f3digo \u2193Experimento \u2193Modelo \u2193Teorema<\/pre>\n\n\n\n
\n\n\n\n7. O primeiro comportamento inesperado: compatibilidade legada<\/h1>\n\n\n\n
\n
legacyHeaderAad = falseAAD = context || header<\/pre>\n\n\n\n
legacyHeaderAad = trueAAD = context<\/pre>\n\n\n\n
\n\n\n\n8. Reproduzindo o comportamento<\/h1>\n\n\n\n
Byte original: 0Byte adulterado: 255<\/pre>\n\n\n\n
Legacy decrypt ACCEPTED tampered ciphertext<\/pre>\n\n\n\n
Default decrypt REJECTEDCode: DECRYPTION_FAILED<\/pre>\n\n\n\n
\n\n\n\n9. O parser mudou completamente a interpreta\u00e7\u00e3o<\/h1>\n\n\n\n
0\u20133 magic4 version5 KDF ID6\u20139 memoryCost10\u201313 timeCost14\u201315 parallelism16\u201321 reserved<\/pre>\n\n\n\n
byte 16<\/pre>\n\n\n\n
\n
reserved byte modified \u2193parser ignores it \u2193AAD does not contain it \u2193same key \u2193same authentication relation \u2193decryption succeeds<\/pre>\n\n\n\n
reserved byte modified \u2193header participates in AAD \u2193AAD changes \u2193GCM authentication fails<\/pre>\n\n\n\n
\n\n\n\n10. Formalizando os dois modos<\/h1>\n\n\n\n
inductive HeaderMode where | secure | legacy<\/pre>\n\n\n\n
structure AuthenticatedState where payloadAuthenticated : Bool headerMatches : Bool<\/pre>\n\n\n\n
\n\n\n\n11. Nem toda adultera\u00e7\u00e3o do header funcionava<\/h1>\n\n\n\n
\n
memoryCost<\/pre>\n\n\n\n
4096<\/pre>\n\n\n\n
8192<\/pre>\n\n\n\n
DECRYPTION_FAILED<\/pre>\n\n\n\n
memoryCost<\/code> n\u00e3o \u00e9 apenas metadata.<\/p>\n\n\n\n\n
\n\n\n\n12. E ent\u00e3o apareceu uma pergunta diferente<\/h1>\n\n\n\n
memoryCost<\/code>, percebemos algo.<\/p>\n\n\n\nciphertext \u2193parse header \u2193read memoryCost \u2193execute Argon2id \u2193derive key \u2193AES-GCM \u2193authentication failure<\/pre>\n\n\n\n
\n
\n\n\n\n13. Da integridade para disponibilidade<\/h1>\n\n\n\n
\n\n\n\n14. Mas havia limites<\/h1>\n\n\n\n
memoryCost = 4,294,967,295<\/pre>\n\n\n\n
INVALID_INPUTKDF_PARAMS_OUT_OF_BOUNDS<\/pre>\n\n\n\n
memoryCost <= 4,194,304timeCost <= 100parallelism <= 64<\/pre>\n\n\n\n
\n
\n
\n\n\n\n15. Testando exatamente o boundary<\/h1>\n\n\n\n
memoryCost = 4,194,304<\/pre>\n\n\n\n
DECRYPTION_FAILED<\/pre>\n\n\n\n
3.97 segundos<\/pre>\n\n\n\n
3.26 segundos<\/pre>\n\n\n\n
103 bytes<\/pre>\n\n\n\n
\n\n\n\n16. Pequeno input, grande trabalho<\/h1>\n\n\n\n
100 GB de input\u2192 muito consumo de recursos<\/pre>\n\n\n\n
~103 bytes \u2193alguns bytes controlam memoryCost \u21934,194,304 \u2193Argon2id \u2193grande consumo de recursos<\/pre>\n\n\n\n
\n\n\n\n17. Medindo mem\u00f3ria: o primeiro resultado enganou<\/h1>\n\n\n\n
process.memoryUsage()<\/pre>\n\n\n\n
RSS: 40.16 MB<\/pre>\n\n\n\n
RSS: 40.39 MB<\/pre>\n\n\n\n
\n\n\n\n18. Duas opera\u00e7\u00f5es<\/h1>\n\n\n\n
memoryCost = 4,194,304<\/pre>\n\n\n\n
Attempt 1:4.06 secondsDECRYPTION_FAILEDAttempt 2:4.07 secondsDECRYPTION_FAILED<\/pre>\n\n\n\n
4.07 seconds<\/pre>\n\n\n\n
\n\n\n\n19. O n\u00famero que chamou nossa aten\u00e7\u00e3o<\/h1>\n\n\n\n
WorkingSetMB PeakWorkingSetMB1701.53 1701.536008.97 6008.977780.09 7780.092367.04 8232.07<\/pre>\n\n\n\n
PeakWorkingSet<\/code> observado foi:8232.07 MB<\/p>\n\n\n\n
\n\n\n\n20. Voltando ao Lean<\/h1>\n\n\n\n
inductive KdfParameterStatus where | withinBounds | outOfBounds<\/pre>\n\n\n\n
inductive ProcessingDecision where | rejectBeforeKdf | executeKdf<\/pre>\n\n\n\n
def decideKdfProcessing (status : KdfParameterStatus) : ProcessingDecision := match status with | KdfParameterStatus.outOfBounds => ProcessingDecision.rejectBeforeKdf | KdfParameterStatus.withinBounds => ProcessingDecision.executeKdf<\/pre>\n\n\n\n
theorem out_of_bounds_rejected_before_kdf : decideKdfProcessing KdfParameterStatus.outOfBounds = ProcessingDecision.rejectBeforeKdf := by rfl<\/pre>\n\n\n\n
theorem within_bounds_executes_kdf : decideKdfProcessing KdfParameterStatus.withinBounds = ProcessingDecision.executeKdf := by rfl<\/pre>\n\n\n\n
\n\n\n\n21. O ponto central da propriedade formal<\/h1>\n\n\n\n
inductive ProcessingStage where | beforeKdf | afterKdfBeforeAuthentication | authenticated<\/pre>\n\n\n\n
theorem within_bounds_reaches_pre_authentication_stage : stageAfterKdfDecision (decideKdfProcessing KdfParameterStatus.withinBounds) = ProcessingStage.afterKdfBeforeAuthentication := by rfl<\/pre>\n\n\n\n
\n\n\n\n22. O que Lean provou \u2014 e o que ele N\u00c3O provou<\/h1>\n\n\n\n
memoryCost = 4194304\u2192 8 GB de RAM<\/pre>\n\n\n\n
\n
\u250c\u2500\u2500\u2500\u2500\u2500\u2500\u2500\u2500\u2500\u2500\u2500\u2500\u2500\u2500\u2500\u2500\u2500\u2510 \u2502 Source analysis \u2502 \u2514\u2500\u2500\u2500\u2500\u2500\u2500\u2500\u2500\u252c\u2500\u2500\u2500\u2500\u2500\u2500\u2500\u2500\u2518 \u2502 \u25bc comportamento observado \u2502 \u250c\u2500\u2500\u2500\u2500\u2500\u2500\u2500\u2500\u2500\u2500\u2500\u2500\u2534\u2500\u2500\u2500\u2500\u2500\u2500\u2500\u2500\u2500\u2500\u2500\u2500\u2510 \u25bc \u25bc Experimentos Modelo formal \u2502 \u2502 \u25bc \u25bctempo \/ mem\u00f3ria propriedades \u2502 \u2502 \u2514\u2500\u2500\u2500\u2500\u2500\u2500\u2500\u2500\u2500\u2500\u2500\u2500\u252c\u2500\u2500\u2500\u2500\u2500\u2500\u2500\u2500\u2500\u2500\u2500\u2500\u2518 \u25bc Security Finding<\/pre>\n\n\n\n
\n\n\n\n23. A causa arquitetural<\/h1>\n\n\n\n
\n
\n\n\n\n24. A mitiga\u00e7\u00e3o correta \u00e9 limitar trabalho n\u00e3o confi\u00e1vel<\/h1>\n\n\n\n
KDF ceilings configur\u00e1veis +limites espec\u00edficos para decrypt +controle de concorr\u00eancia +rate limiting +isolamento de workers\/processos<\/pre>\n\n\n\n
\n
\n\n\n\n25. O que tornou o finding interessante<\/h1>\n\n\n\n
eval(userInput)<\/pre>\n\n\n\n
1. O formato precisa armazenar par\u00e2metros KDF.
2. O decrypt precisa ler esses par\u00e2metros.
3. Par\u00e2metros inv\u00e1lidos precisam ter limites.
4. Par\u00e2metros v\u00e1lidos precisam chegar ao KDF.
5. O KDF precisa executar antes que exista uma chave.
6. A chave \u00e9 necess\u00e1ria para autenticar o ciphertext.
7. Opera\u00e7\u00f5es podem ocorrer concorrentemente.<\/pre>\n\n\n\n
\n\n\n\n26. O papel dos contraexemplos<\/h1>\n\n\n\n
\n
memoryCost<\/code> mostrou um contraexemplo.<\/p>\n\n\n\n
\n\n\n\n27. Formal methods n\u00e3o significa necessariamente provar o sistema inteiro<\/h1>\n\n\n\n
reescrever aplica\u00e7\u00e3o em linguagem formal
\u2193modelar cada fun\u00e7\u00e3o
\u2193provar centenas de teoremas
\u2193s\u00f3 ent\u00e3o encontrar alguma coisa<\/pre>\n\n\n\n
\n\n\n\n28. O modelo formal funcionou como uma lupa<\/h1>\n\n\n\n
No goals<\/code>.<\/p>\n\n\n\ntampered?<\/pre>\n\n\n\n
authenticated?<\/pre>\n\n\n\n
headerMatches?<\/pre>\n\n\n\n
withinBounds?<\/pre>\n\n\n\n
em que est\u00e1gio do processamento estamos?<\/pre>\n\n\n\n
\n\n\n\n29. A cadeia de evid\u00eancias<\/h1>\n\n\n\n
Camada<\/th> Evid\u00eancia<\/th><\/tr><\/thead> Documenta\u00e7\u00e3o<\/td> Garantias e comportamento esperado<\/td><\/tr> Source review<\/td> Ordem real de processamento<\/td><\/tr> Unit tests existentes<\/td> Comportamentos conhecidos pelo projeto<\/td><\/tr> Experimentos pr\u00f3prios<\/td> Reprodu\u00e7\u00e3o independente<\/td><\/tr> Boundary analysis<\/td> Diferen\u00e7a entre rejeitado e permitido<\/td><\/tr> Timing<\/td> ~3\u20134 segundos por opera\u00e7\u00e3o<\/td><\/tr> OS monitoring<\/td> Consumo de mem\u00f3ria nativa<\/td><\/tr> Concurrency<\/td> Amplifica\u00e7\u00e3o observada<\/td><\/tr> Lean<\/td> Propriedades do modelo mecanicamente provadas<\/td><\/tr><\/tbody><\/table><\/figure>\n\n\n\n \n
\n\n\n\n30. Responsible disclosure<\/h1>\n\n\n\n
Large-input DoS:gigabytes de input \u2193gigabytes de trabalho<\/pre>\n\n\n\n
Nosso caso:~103 bytes \u2193KDF cost metadata \u2193gigabytes de mem\u00f3ria observada<\/pre>\n\n\n\n
\n
\n\n\n\n31. O finding<\/h1>\n\n\n\n
Pre-Authentication Resource Exhaustion via Attacker-Controlled Argon2id Parameters<\/h2>\n\n\n\n
memoryCost m\u00e1ximo aceito:4,194,304tempo por opera\u00e7\u00e3o:~3\u20134 segundosduas opera\u00e7\u00f5es concorrentes:~4.07 segundos totalPeakWorkingSet observado:~8.23 GBresultado final:DECRYPTION_FAILED<\/pre>\n\n\n\n
Internet \u2193ciphertext controlado \u2193decrypt()<\/pre>\n\n\n\n
\n\n\n\n32. A principal li\u00e7\u00e3o<\/h1>\n\n\n\n
\n
\n
\n\n\n\n33. Seguran\u00e7a como problema matem\u00e1tico e experimental<\/h1>\n\n\n\n
\n
\n
\n
\n
\n
\n\n\n\n34. Conclus\u00e3o<\/h1>\n\n\n\n
Cryptographic library
\u2193Security claims
\u2193Security properties
\u2193Source-code analysis
\u2193Concrete experiments
\u2193Counterexamples
\u2193Model refinement
\u2193Formal specification
\u2193Lean proofs
\u2193Resource measurements
\u2193Candidate security finding
\u2193Responsible disclosure<\/pre>\n\n\n\n
\n\n\n\nNota sobre disclosure<\/h2>\n\n\n\n