Ideas & Insights

Explorando desarrollo AI-first, guardrails de código y la arquitectura de la descartabilidad.

abstract-interpretationstatic-analysismetainfer

Meta encontró 100,000 bugs en código de producción con un analizador estático que nunca ejecuta el programa

Infer de Meta usa interpretación abstracta y bi-abducción para encontrar desreferencias nulas, fugas de memoria y condiciones de carrera razonando sobre la estructura del código, no sobre su ejecución. Así es como funciona y cómo usarlo en tu propia codebase.

Meta ha enviado más de 100,000 correcciones de bugs que fueron atrapadas por un analizador estático antes de que el código llegara a un usuario. La herramienta…
abstract-interpretationstatic-analysissafety-criticalaviation

El análisis estático no puede demostrar que tu avión no se estrellará. Puede demostrar algo más útil.

La interpretación abstracta sobreaproxima cada posible estado del programa. Si una división por cero es inalcanzable en la abstracción, es inalcanzable en el código real. Así es como funciona y dónde falla.

El análisis estático no puede demostrar que un avión no se estrellará. Sí puede demostrar que el bucle de control del altímetro nunca dividirá por cero, nunca…
abstract-interpretationstatic-analysisruntime-errorsverification

Cómo demostrar que tu código no tiene errores en tiempo de ejecución (y por qué probablemente desistirás)

La interpretación abstracta te permite probar que ciertos errores en tiempo de ejecución son imposibles antes de ejecutar el código. Así es como funciona en realidad, por qué es difícil y dónde encaja en tu cadena de herramientas.

Tu batería de pruebas pasa. Tu verificador de tipos está en verde. Haces el despliegue. Dos horas después, producción lanza un en un caso extremo que nadie…
hardware-assisted-safetychericporting

Tu código en C puede ejecutarse en hardware con capacidades sin rewrite por completo

El ABI híbrido de CHERI te permite portar código en C a hardware con capacidades de forma incremental. Aquí te explicamos cómo compilar, qué se rompe y cómo solucionarlo sin rewrite toda tu codebase.

Tienes una codebase en C que es demasiado grande como para rewrite en Rust y demasiado crítica como para dejarla expuesta a desbordamientos de búfer. El…
hardware-assisted-safetycapability-hardwarecherisoftware-history

El hardware de capabilities no falló. Llegó 40 años antes de tiempo.

La seguridad de memoria a nivel de hardware ha sido posible desde los años 70. Aquí te explicamos por qué las arquitecturas de capabilities siguieron perdiendo contra los modelos de memoria plana, y por qué CHERI está cambiando finalmente las reglas.

El setenta por ciento de los CVEs son bugs de memory safety. Buffer overflows, use-after-free, double frees. El tipo de vulnerabilidades que permiten a un…
hardware-assisted-safetysandboxingcwebassembly

Tu dependencia en C puede hacer fallar todo tu proceso. WebAssembly puede evitarlo.

Los contenedores son excesivos para aislar una sola biblioteca en C. Compílala a WebAssembly y ejecútala dentro de un sandbox WASI para memory safety, acceso al filesystem basado en capabilities y contención de fallos sin Docker.

Un único null pointer dereference dentro de una biblioteca en C puede tumbar toda tu aplicación. Si esa biblioteca parsea input del usuario, descomprime…
hardware-assisted-safetymemory-corruptionmobileasan

Tu teléfono ya tiene hardware que detecta corrupción de memoria

ARM Memory Tagging Extension y GWP-ASan hacen posible la detección de problemas de seguridad de memoria en producción en dispositivos móviles modernos. Así es como funcionan y cómo se ven los compromisos.

Tu teléfono puede detectar corrupción de memoria en producción. No con la instrumentation completa que ejecutas en CI, y no en cada asignación. Pero el…
hardware-assisted-safetybuffer-overflowmemory-safetycheri

Los Buffer Overflows Siguen Ocurriendo Porque Los Arreglamos en Software

CHERI es una extensión de hardware que convierte cada pointer en una bounded capability. Así es como detiene los buffer overflows a nivel de CPU, lo que cuesta y cómo probarlo en hardware real.

Los buffer overflows han estado en el CWE Top 25 durante veinte años. Tenemos stack canaries, ASLR, DEP, control-flow integrity y lenguajes memory-safe, y aún…
cleanroom-correctnessllmformal-proofsautomation

Los LLM no pueden demostrar que tu código es correcto, pero pueden escribir el código repetitivo que lo logra

La verificación Cleanroom requiere generar y descargar obligaciones de prueba. Así es como los LLM automatizan la anotación y la generación de condiciones de verificación (VC) para que puedas centrarte en las pruebas realmente difíciles.

La ingeniería de software Cleanroom exige que demuestres que tu código es correcto antes de compilarlo. Suena noble hasta que pasas tres horas escribiendo…
cleanroom-correctnessprocessefficiencypragmatism

Cleanroom Entrega 0.1 Defectos por KLOC. No Necesitas la Religión Completa para Llegar Ahí.

La ingeniería de software Cleanroom reduce las tasas de defectos 100×, pero la adopción completa requiere equipos de prueba separados y pruebas formales. Aquí tienes un subconjunto pragmático que captura la mayor parte del beneficio sin el overhead.

La ingeniería de software Cleanroom entrega 0.1 defectos por mil líneas de código. El promedio de la industria es de 10 a 50. El problema es que Cleanroom…