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 las matemáticas . [1] La verificación formal es un incentivo clave para la especificación formal de sistemas y es el núcleo de los métodos formales . Representa una dimensión importante de análisis y 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 criterios comunes para la certificación de seguridad informática .
La verificación formal puede ser útil para demostrar la exactitud 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 . Ejemplos destacados de sistemas de software verificados incluyen el compilador C verificado por CompCert y el kernel 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 suma de vectores , autómatas cronometrados , autómatas híbridos , álgebra de procesos , semántica formal de lenguajes de programación como la semántica operativa , semántica denotacional , semántica axiomática y lógica de Hoare . [3]
Un enfoque y formación es la verificació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 se pueden representar efectivamente de manera finita mediante el uso de abstracción o aprovechando 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 de dominio para considerar grupos completos de estados en una sola operación y reducir el tiempo de computación. Las técnicas de implementación incluyen enumeración del espacio de estados , enumeración del espacio de estados simbólico, interpretación abstracta , simulación simbólica y refinamiento de la abstracción. [ cita necesaria ] 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 SystemVerilog (SVA), [4] o la lógica de árbol computacional (CTL). La gran ventaja de la verificación de modelos es que suele ser completamente automática; su principal desventaja es que, en general, no se adapta 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 estas obligaciones utilizando asistentes de prueba (demostradores de teoremas interactivos) ( como HOL , ACL2 , Isabelle , Coq o PVS ), o demostradores automáticos de teoremas , incluidos en particular los solucionadores de teorías del módulo de satisfacibilidad (SMT). Este enfoque tiene la desventaja de que puede requerir que el usuario comprenda en detalle por qué el sistema funciona correctamente y que 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, condiciones previas, condiciones posteriores) de los 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 demostrar que un programa satisface una especificación formal de su comportamiento. Las subáreas de verificación formal incluyen verificación deductiva (ver arriba), interpretación abstracta , demostración automatizada de teoremas , sistemas de tipos y métodos formales ligeros . Un enfoque prometedor de verificación basada en tipos es la programación con 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 exactitud con respecto a esas especificaciones. Los lenguajes escritos de forma dependiente con todas las funciones admiten la verificación deductiva como caso especial.
Otro enfoque complementario es la derivación de programas , en la que se produce 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 , y este enfoque puede verse 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 sólo cuando ha cubierto todo el espacio de posibilidades. Un ejemplo de una técnica errónea es aquella que cubre sólo un subconjunto de posibilidades, por ejemplo sólo 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 poco sólidas que sean decidibles cuando no se dispone de técnicas sólidas y decidibles.
La verificación es un aspecto de probar la idoneidad de un producto para su propósito. La validación es el aspecto complementario. A menudo nos referimos al proceso de verificación general como V & V.
El proceso de verificación consta de aspectos estáticos/estructurales y dinámicos/comportamentales. Por ejemplo, para un producto de software se puede inspeccionar el código fuente (estático) y ejecutarlo en casos de prueba específicos (dinámico). Por lo general, la validación sólo puede realizarse dinámicamente, es decir, el producto se prueba sometiéndolo a usos típicos y atípicos ("¿Cumple satisfactoriamente con todos los casos de uso ?").
La reparación del programa se realiza con respecto a un Oracle , abarcando 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 una variedad de técnicas, en particular el uso de solucionadores de teorías de módulo de satisfacibilidad (SMT) y programación genética , [5] utilizando computación evolutiva para generar y evaluar posibles candidatos para 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, a los que pueden apuntar los módulos de síntesis. Los sistemas de reparación a menudo se centran en una pequeña clase de errores predefinida 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 mayoría o todas las empresas líderes de hardware utilizan la verificación formal, [8] pero su uso en la industria del software aún languidece. [ cita necesaria ] Esto podría atribuirse a la mayor necesidad en la industria del hardware, donde los errores tienen una mayor importancia comercial. [ cita necesaria ] Debido a las posibles interacciones sutiles entre componentes, es cada vez más difícil ejercer un conjunto realista de posibilidades mediante simulación. 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], se han verificado formalmente varios sistemas operativos: el micronúcleo Secure Embedded L4 de NICTA , vendido comercialmente como seL4 por OK Labs; [10] Sistema operativo en tiempo real basado en OSEK/VDX ORIENTAIS de la Universidad Normal del Este de China ; [ cita requerida ] 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, redes basadas en intenciones. [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 necesaria ]
El compilador CompCert C es un compilador de C verificado formalmente que implementa la mayoría de ISO C. [21] [22]
