Ideias & Insights

Explorando desenvolvimento AI-first, guardrails de código e a arquitetura da descartabilidade.

abstract-interpretationstatic-analysismetainfer

Meta Encontrou 100.000 Bugs em Código de Produção com um analyzer Estático que Nunca Executa o Programa

O Infer da Meta usa interpretação abstrata e bi-abdução para encontrar desreferências nulas, vazamentos de memória e race conditions ao raciocinar sobre a estrutura do código, não sobre sua execução. Veja como funciona e como usá-lo em sua própria codebase.

A Meta enviou mais de 100.000 correções de bugs que foram capturadas por um analyzer estático antes que o código chegasse a um usuário. A ferramenta se chama…
abstract-interpretationstatic-analysissafety-criticalaviation

A Análise Estática Não Pode Provar Que Seu Avião Não Vai Cair. Ela Pode Provar Algo Mais Útil.

A interpretação abstrata superaproxima todo estado possível do programa. Se uma divisão por zero é inalcançável na abstração, ela é inalcançável no código real. Veja como funciona e onde deixa de funcionar.

A análise estática não pode provar que um avião não vai cair. Ela pode provar que o loop de controle do altímetro nunca vai dividir por zero, nunca vai acessar…
abstract-interpretationstatic-analysisruntime-errorsverification

Como provar que seu código não tem erros de execução (e por que você provavelmente desistirá de tentar)

A interpretação abstrata permite provar que erros de execução são impossíveis antes da execução. Veja como ela funciona na prática, por que é difícil e onde se encaixa na sua cadeia de ferramentas.

Sua suíte de testes passa. Seu verificador de tipos está verde. Você faz o deploy. Duas horas depois, a produção lança um em um caso extremo que ninguém pensou…
hardware-assisted-safetycapability-hardwarecherisoftware-history

O hardware de capabilities não falhou. Chegou 40 anos cedo demais.

A segurança de memória no nível de hardware é possível desde os anos 1970. Aqui está o porquê de as arquiteturas de capabilities terem perdido repetidamente para os modelos de memória plana, e por que o CHERI está finalmente mudando a conta.

Setenta por cento dos CVEs são bugs de memory safety. Buffer overflows, use-after-free, double frees. O tipo de vulnerabilidades que permitem a um atacante…
hardware-assisted-safetysandboxingcwebassembly

Sua dependência em C pode derrubar todo o seu processo. WebAssembly pode impedir isso.

Containers são exagerados para isolar uma única biblioteca C. Compile-a para WebAssembly e execute-a dentro de um sandbox WASI para memory safety, acesso ao filesystem baseado em capabilities e contenção de crashes sem Docker.

Um único null pointer dereference dentro de uma biblioteca em C pode derrubar toda a sua aplicação. Se essa biblioteca faz parse de input do usuário,…
hardware-assisted-safetymemory-corruptionmobileasan

Seu celular já tem hardware que detecta corrupção de memória

ARM Memory Tagging Extension e GWP-ASan tornam possível a detecção de segurança de memória em produção em dispositivos móveis modernos. Veja como funcionam e quais são as compensações.

Seu celular pode detectar corrupção de memória em produção. Não com a instrumentação completa que você executa em CI, e não em cada alocação. Mas o hardware no…
hardware-assisted-safetybuffer-overflowmemory-safetycheri

Buffer Overflows Continuam Acontecendo Porque nodes Os Corrigimos em Software

CHERI é uma extensão de hardware que transforma cada pointer em uma bounded capability. Veja como ela impede buffer overflows no nível da CPU, o que custa e como testá-la em hardware real.

Buffer overflows estão no CWE Top 25 há vinte anos. Temos stack canaries, ASLR, DEP, control-flow integrity e linguagens memory-safe, e ainda assim eles…
cleanroom-correctnessllmformal-proofsautomation

LLMs Não Conseguem Provar que Seu Código Está Correto, Mas Podem Escrever o Boilerplate que Faz Isso

A verificação Cleanroom exige gerar e descarregar obrigações de prova. Veja como os LLMs automatizam a anotação e a geração de VC para que você possa se concentrar nas provas realmente difíceis.

A engenharia de software Cleanroom exige que você prove que seu código está correto antes de compilá-lo. Isso soa nobre até você passar três horas escrevendo…
cleanroom-correctnessprocessefficiencypragmatism

Cleanroom Entrega 0,1 Defeitos por KLOC. Você Não Precisa do Ritual Completo para Chegar Lá.

A engenharia de software Cleanroom reduz as taxas de defeitos em 100×, mas a adoção completa exige equipes de teste separadas e provas formais. Aqui está um subconjunto pragmático que captura a maior parte do benefício sem o overhead.

A engenharia de software Cleanroom entrega 0,1 defeitos por mil linhas de código. A média da indústria é de 10 a 50. O problema é que o Cleanroom completo…