En el contexto de los sistemas de hardware y software , la verificación formal es el acto de probar o refutar la corrección de un sistema con respecto a una determinada especificación o propiedad formal, utilizando métodos formales de matemáticas . [1] La verificación formal es un incentivo clave para la especificación formal de sistemas y está en el núcleo de los métodos formales . Representa una dimensión importante del análisis y la verificación en la automatización del diseño electrónico y es un enfoque para la verificación de software . El uso de la verificación formal permite el más alto Nivel de Garantía de Evaluación ( EAL7 ) en el marco de los criterios comunes para la certificación de seguridad informática .
La verificación formal puede ser útil para demostrar la corrección de sistemas como: protocolos criptográficos , circuitos combinacionales , circuitos digitales con memoria interna y software expresado como código fuente en un lenguaje de programación . Entre los ejemplos destacados de sistemas de software verificados se incluyen el compilador C verificado CompCert y el núcleo del sistema operativo de alta seguridad seL4 .
La verificación de estos sistemas se realiza asegurando la existencia de una prueba formal de un modelo matemático del sistema. [2] Ejemplos de objetos matemáticos utilizados para modelar sistemas son: máquinas de estados finitos , sistemas de transición etiquetados , cláusulas de Horn , redes de Petri , sistemas de adición vectorial , autómatas temporizados , autómatas híbridos , álgebra de procesos , semántica formal de lenguajes de programación como semántica operacional , semántica denotacional , semántica axiomática y lógica de Hoare . [3]
Un enfoque y formación es la comprobación de modelos , que consiste en una exploración sistemáticamente exhaustiva del modelo matemático (esto es posible para modelos finitos , pero también para algunos modelos infinitos donde conjuntos infinitos de estados pueden representarse efectivamente de manera finita mediante el uso de abstracción o aprovechando la simetría). Por lo general, esto consiste en explorar todos los estados y transiciones en el modelo, mediante el uso de técnicas de abstracción inteligentes y específicas del dominio para considerar grupos completos de estados en una sola operación y reducir el tiempo de cálculo. Las técnicas de implementación incluyen enumeración del espacio de estados , enumeración simbólica del espacio de estados, interpretación abstracta , simulación simbólica y refinamiento de abstracción. [ cita requerida ] Las propiedades a verificar a menudo se describen en lógicas temporales , como la lógica temporal lineal (LTL), el lenguaje de especificación de propiedades (PSL), las afirmaciones de SystemVerilog (SVA), [4] o la lógica de árbol computacional (CTL). La gran ventaja de la comprobación de modelos es que a menudo es completamente automática; su principal desventaja es que, en general, no se escala a sistemas grandes; Los modelos simbólicos suelen estar limitados a unos pocos cientos de bits de estado, mientras que la enumeración explícita de estados requiere que el espacio de estados que se explora sea relativamente pequeño.
Otro enfoque es la verificación deductiva. Consiste en generar a partir del sistema y sus especificaciones (y posiblemente otras anotaciones) una colección de obligaciones de prueba matemática , cuya verdad implica la conformidad del sistema con su especificación, y cumplir con estas obligaciones utilizando asistentes de prueba (demostradores de teoremas interactivos) (como HOL , ACL2 , Isabelle , Coq o PVS ), o demostradores de teoremas automáticos , incluyendo en particular solucionadores de teorías de satisfacibilidad módulo (SMT). Este enfoque tiene la desventaja de que puede requerir que el usuario comprenda en detalle por qué el sistema funciona correctamente y transmita esta información al sistema de verificación, ya sea en forma de una secuencia de teoremas a demostrar o en forma de especificaciones (invariantes, precondiciones, poscondiciones) de componentes del sistema (por ejemplo, funciones o procedimientos) y quizás subcomponentes (como bucles o estructuras de datos).
La verificación formal de programas de software implica probar que un programa satisface una especificación formal de su comportamiento. Las subáreas de verificación formal incluyen la verificación deductiva (ver arriba), la interpretación abstracta , la demostración automatizada de teoremas , los sistemas de tipos y los métodos formales ligeros . Un enfoque de verificación basado en tipos prometedor es la programación de tipos dependientes , en la que los tipos de funciones incluyen (al menos parte de) las especificaciones de esas funciones, y la verificación de tipos del código establece su corrección frente a esas especificaciones. Los lenguajes de tipos dependientes con todas las características admiten la verificación deductiva como un caso especial.
Otro enfoque complementario es la derivación de programas , en la que se produce un código eficiente a partir de especificaciones funcionales mediante una serie de pasos que preservan la corrección. Un ejemplo de este enfoque es el formalismo de Bird-Meertens , que puede considerarse como otra forma de corrección por construcción.
Estas técnicas pueden ser sólidas , lo que significa que las propiedades verificadas se pueden deducir lógicamente de la semántica, o no sólidas , lo que significa que no existe tal garantía. Una técnica sólida produce un resultado solo una vez que ha cubierto todo el espacio de posibilidades. Un ejemplo de una técnica no sólida es aquella que cubre solo un subconjunto de las posibilidades, por ejemplo, solo números enteros hasta un cierto número, y da un resultado "suficientemente bueno". Las técnicas también pueden ser decidibles , lo que significa que se garantiza que sus implementaciones algorítmicas terminarán con una respuesta, o indecidibles, lo que significa que es posible que nunca terminen. Al limitar el alcance de las posibilidades, se podrían construir técnicas no sólidas que sean decidibles cuando no haya disponibles técnicas sólidas decidibles.
La verificación es un aspecto de la prueba de la idoneidad de un producto para un fin determinado. La validación es el aspecto complementario. A menudo se hace referencia al proceso de comprobación general como V&V.
El proceso de verificación consta de aspectos estáticos/estructurales y dinámicos/conductuales. Por ejemplo, en el caso de un producto de software, se puede inspeccionar el código fuente (estático) y ejecutarlo en casos de prueba específicos (dinámico). La validación normalmente solo se puede realizar de forma dinámica, es decir, el producto se prueba sometiéndolo a usos típicos y atípicos ("¿Cumple satisfactoriamente todos los casos de uso ?").
La reparación del programa se realiza con respecto a un oráculo , que abarca la funcionalidad deseada del programa que se utiliza para la validación de la solución generada. Un ejemplo sencillo es un conjunto de pruebas: los pares de entrada/salida especifican la funcionalidad del programa. Se emplean diversas técnicas, en particular, el uso de solucionadores de teorías de módulo de satisfacibilidad (SMT) y programación genética [5] , que utiliza la computación evolutiva para generar y evaluar posibles candidatos para las soluciones. El primer método es determinista, mientras que el segundo es aleatorio.
La reparación de programas combina técnicas de verificación formal y síntesis de programas . Las técnicas de localización de fallos en la verificación formal se utilizan para calcular puntos del programa que podrían ser posibles ubicaciones de errores, que pueden ser detectados por los módulos de síntesis. Los sistemas de reparación a menudo se centran en una pequeña clase predefinida de errores para reducir el espacio de búsqueda. El uso industrial es limitado debido al coste computacional de las técnicas existentes.
El aumento de la complejidad de los diseños aumenta la importancia de las técnicas de verificación formal en la industria del hardware . [6] [7] En la actualidad, la verificación formal es utilizada por la mayoría o todas las empresas líderes de hardware, [8] pero su uso en la industria del software aún está languideciendo. [ cita requerida ] Esto podría atribuirse a la mayor necesidad en la industria del hardware, donde los errores tienen una mayor importancia comercial. [ cita requerida ] Debido a las posibles interacciones sutiles entre los componentes, es cada vez más difícil ejercitar un conjunto realista de posibilidades mediante simulación. Los aspectos importantes del diseño de hardware son susceptibles de métodos de prueba automatizados, lo que hace que la verificación formal sea más fácil de introducir y más productiva. [9]
A partir de 2011 [actualizar], varios sistemas operativos han sido verificados formalmente: el microkernel Secure Embedded L4 de NICTA , vendido comercialmente como seL4 por OK Labs; [10] el sistema operativo en tiempo real basado en OSEK/VDX ORIENTAIS de la Universidad Normal del Este de China ; [ cita requerida ] el sistema operativo Integrity de Green Hills Software ; [ cita requerida ] y PikeOS de SYSGO . [11] [12] En 2016, un equipo dirigido por Zhong Shao en Yale desarrolló un núcleo de sistema operativo verificado formalmente llamado CertiKOS. [13] [14]
A partir de 2017, la verificación formal se ha aplicado al diseño de grandes redes informáticas a través de un modelo matemático de la red, [15] y como parte de una nueva categoría de tecnología de red, la red basada en la intención . [16] Los proveedores de software de red que ofrecen soluciones de verificación formal incluyen Cisco [17] Forward Networks [18] [19] y Veriflow Systems. [20]
El lenguaje de programación SPARK proporciona un conjunto de herramientas que permite el desarrollo de software con verificación formal y se utiliza en varios sistemas de alta integridad . [ cita requerida ]
El compilador C CompCert es un compilador C verificado formalmente que implementa la mayoría de ISO C. [21] [22]
