Verificación formal: una prueba matemática no garantiza software perfecto

La verificación formal de software usa lógica y matemáticas para demostrar que un modelo o una implementación satisface una propiedad definida con precisión. El resultado no significa que el programa sea perfecto: establece que, bajo determinados supuestos y dentro del alcance analizado, el comportamiento cumple la especificación formulada.

Una demostración puede ser correcta y dejar fuera requisitos equivocados, interacciones no modeladas, errores de configuración, dependencias vulnerables o ataques que la propiedad nunca contempló. Por eso la verificación formal aporta una garantía delimitada y no sustituye las pruebas dinámicas, la revisión de código ni el análisis de amenazas.

Qué demuestra realmente una prueba formal

El glosario de métodos formales del NIST los define como técnicas matemáticamente rigurosas para especificar, desarrollar y verificar sistemas de software. Especificar es esencial: antes de demostrar una propiedad hay que expresar sin ambigüedad qué estados, entradas, resultados y transiciones se consideran válidos.

Una propiedad puede adoptar una forma como «para toda ejecución que satisfaga estas precondiciones, nunca aparece este estado prohibido». La herramienta comprueba la relación entre la propiedad y el modelo o programa; no convierte automáticamente todas las expectativas humanas sobre el producto en obligaciones matemáticas.

El alcance puede ser una función, un protocolo, una máquina de estados o un componente. No incluye necesariamente el sistema desplegado con su compilador, bibliotecas, red, configuración, operadores y servicios externos. Una afirmación precisa debe identificar el artefacto verificado, la propiedad demostrada, los supuestos aceptados y las partes excluidas.

Un ejemplo mínimo: propiedad correcta, requisito insuficiente

Consideremos un ejemplo hipotético de transferencias bancarias. La especificación permite una operación solo cuando el saldo de origen es igual o superior al importe; la propiedad exige que el saldo nunca quede por debajo de cero. Si la demostración es válida, puede concluirse que, dentro de ese modelo y bajo sus supuestos, ninguna transferencia autorizada produce un saldo negativo.

La conclusión no abarca todo lo que hace segura o correcta una transferencia. No demuestra que el destinatario sea legítimo, que el usuario haya consentido la operación, que el importe no se alterara antes de llegar al componente o que una credencial robada no permita iniciarla. Tampoco establece propiedades de disponibilidad, privacidad o resistencia a canales laterales que no aparezcan en la especificación.

El requisito inicial también puede estar mal formulado. Si el producto permite un descubierto limitado, prohibir cualquier saldo negativo no describe el comportamiento deseado. Si el modelo representa importes con enteros matemáticos, pero el programa usa un tipo numérico con límites, la abstracción puede omitir un desbordamiento. La prueba seguiría siendo válida para el modelo, no necesariamente para la intención del negocio o para cada detalle de la implementación.

Demostración, comprobación de modelos, análisis estático y testing

La demostración de teoremas construye o comprueba un argumento lógico que deriva una propiedad de axiomas, supuestos y una representación formal del sistema. Puede requerir intervención humana aunque un asistente automatice numerosos pasos. Su fuerza es la garantía deductiva; su frontera es lo que se formalizó.

La comprobación de modelos examina los estados alcanzables de un modelo para decidir si cumplen una propiedad y puede devolver un contraejemplo cuando encuentra una violación. La página del NIST sobre verificación de diseño y modelado enumera entre las funciones posibles la simulación, la verificación exhaustiva y la prueba del diseño. La palabra «exhaustiva» se refiere al espacio definido por el modelo, no a todas las condiciones posibles del entorno real.

El análisis estático inspecciona código sin ejecutarlo. Puede seguir flujos, aplicar reglas o emplear abstracciones formales, pero el aviso de un escáner convencional es un hallazgo potencial, no una demostración de ausencia o presencia de todos los defectos. El alcance de su resultado depende de las reglas, las aproximaciones y el código que pudo examinar.

El testing ejecuta software real con entradas concretas y observa resultados concretos. Una prueba superada acredita esa ejecución, no todas las ejecuciones posibles; a cambio, puede exponer problemas de integración, configuración, rendimiento o recursos que el modelo formal no representó. Las cuatro técnicas responden preguntas distintas y sus resultados no expresan el mismo tipo de garantía.

Por qué sigue haciendo falta evidencia empírica

Un artículo académico de 1996 alojado por el NIST explica que los métodos formales complementan métodos empíricos e informales y estudia la correspondencia entre especificaciones y modelos de implementación en el diseño de hardware. El principio aplicable al software es el mismo: una prueba sobre una representación no aporta por sí sola evidencia sobre los elementos que esa representación omite.

Las pruebas unitarias y de integración ejercitan componentes reales y sus interfaces. El fuzzing explora entradas imprevistas; las pruebas de carga observan límites de recursos; la revisión humana puede descubrir supuestos dudosos, requisitos contradictorios y errores en el propio modelo. Cuando son parte de la superficie evaluada, también deben examinarse la compilación, el empaquetado, la configuración y las dependencias.

El análisis de amenazas añade activos, adversarios, capacidades y rutas de ataque a la evaluación. Si omite a un administrador malicioso, un canal lateral o la manipulación de la cadena de suministro, demostrar una propiedad limitada al control de acceso no cubre esos riesgos. El análisis sirve además para decidir qué propiedades conviene formalizar, en lugar de asumir que cualquier propiedad demostrada equivale a seguridad general.

Los límites que debe declarar una verificación

La frase «formalmente verificado» solo resulta informativa cuando va acompañada de límites concretos. Como mínimo, la afirmación debería permitir identificar:

• Propiedad: la afirmación exacta demostrada y el requisito que pretende representar.
• Artefacto: si se verificó un modelo, código fuente, bytecode, hardware o una combinación determinada.
• Supuestos: qué elementos se dieron por correctos, como el compilador, la aritmética, el sistema operativo o servicios externos.
• Cobertura: qué entradas, estados, comportamientos concurrentes y fallos del entorno están incluidos.
• Correspondencia: cómo se relaciona el artefacto verificado con la versión que llega a producción.
• Evidencia complementaria: qué testing, revisión, análisis estático y evaluación de amenazas acompañan la demostración.

Estos límites no invalidan la verificación formal. Delimitan su valor: una garantía rigurosa y auditable sobre propiedades concretas. Hablar de corrección o seguridad del sistema completo exige, además, comprobar que la especificación representa los requisitos adecuados y reunir evidencia sobre aquello que quedó fuera de la abstracción.

Lee también:

• Pagar Suno Pro no garantiza el copyright de una canción creada con IA
• Cómo aislar agentes de IA sin falsear una prueba de ciberseguridad
• El ordenador cuántico de 128 cúbits aún no tiene una prueba independiente