El verificador de modelo acotado de C: criminalmente infrautilizado

Artículo original ↗ Discusión en Hacker News ↗

Herramientas de verificación formal como CBMC, un verificador de modelo acotado para C (y backend de Kani de Amazon para Rust), son elogiadas por detectar errores sutiles como desbordamientos de búfer y fallos lógicos al explorar exhaustivamente las rutas del programa dentro de límites dados. Los comentaristas debaten hasta qué punto estas herramientas escalan más allá de código pequeño, estilo pruebas unitarias, cómo se comparan con alternativas como Frama-C, KLEE y los sanitizers, y si el esfuerzo que requieren es preferible a cambiar a lenguajes más seguros. La conversación se amplía hacia problemas de larga data en C —comportamiento indefinido, falta de información sobre la longitud de los arrays y garantías de seguridad débiles— y si la evolución del lenguaje o las herramientas externas son la vía más realista hacia un software de bajo nivel más seguro.

Adopción y casos de uso de CBMC

  • Varios comentaristas sostienen que CBMC está infrautilizado y abogan por llevar la verificación formal, al estilo del hardware, al software convencional.
  • Ejemplos citados: verificación de código criptográfico, bibliotecas C de AWS, componentes de FreeRTOS, funciones de clientes HTTP y grandes proyectos comerciales en C (~500K LOC).
  • Algunos usuarios informan haber encontrado errores reales como desbordamientos de búfer, bucles de denegación de servicio y problemas en analizadores y código de red.

Escalabilidad y estilo de verificación

  • Consenso: CBMC funciona mejor a nivel de unidad o de módulo pequeño, no en sistemas grandes completos.
  • El uso eficaz requiere:
    • Diseño basado en contratos: precondiciones/postcondiciones explícitas y aserciones.
    • Funciones “sombra” que sustituyen a los llamados complejos con modelos simplificados y no deterministas que respetan el mismo contrato.
    • Mantener la profundidad de búsqueda baja para que cada ejecución termine rápidamente.
  • Adaptarlo a código heredado, mal estructurado, se considera más difícil que usarlo desde el principio.

Comparación con otras herramientas

  • Frama-C, Coq VST, enfoque de seL4: más potentes, pero requieren más experiencia y no escalan fácilmente al código cotidiano.
  • KLEE: bueno en herramientas simples como GNU text/coreutils; tiene dificultades con entradas estructuradas complejas (p. ej., protobufs, contenedores de C++).
  • Los analizadores estáticos (p. ej., analizadores del compilador más anotaciones) pueden cubrir algunos problemas de búfer; CBMC sigue valorándose como otra capa de seguridad.
  • CBMC también se usa como backend para Kani, una herramienta de verificación de Rust.

Arrays de C, límites y diseño del lenguaje

  • Debate ampliado sobre la pérdida del tamaño de los arrays en C al decaer a punteros y los consiguientes errores de búfer.
  • Propuestas discutidas: punteros con metadatos/slices, arrays de tamaño no propietario y parámetros puntero-a-array; algunas implementadas en otros lenguajes.
  • Frustración porque los estándares de C no han adoptado estas características, mientras sí han incorporado otras más oscuras (p. ej., identificadores Unicode).

Comportamiento indefinido y memoria no inicializada

  • CBMC modela las variables locales no inicializadas como valores no deterministas, lo que puede apartarse de la semántica de UB de C.
  • Algunos sostienen que un verificador debería tratar cualquier UB (como leer variables no inicializadas) como un error inmediato; otros señalan que el enfoque actual de CBMC es de modelos “parecidos a C”, no de semántica exacta de C.
  • Un largo subhilo sobre UB, optimizaciones del compilador, “C amigable/aburrido”, sanitizers y comportamiento del sistema operativo muestra una profunda preocupación por las descompilaciones inducidas por UB y los fallos de seguridad.
  • Se coincide en que CBMC debería usarse junto con advertencias del compilador y sanitizers como parte de una defensa en profundidad.