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 los algoritmos previstos que subyacen a 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 puede ser útil para probar la corrección de sistemas como: protocolos criptográficos , circuitos combinacionales , circuitos digitales con memoria interna y software expresado como código fuente.
La verificación de estos sistemas se realiza proporcionando una prueba formal en un modelo matemático abstracto del sistema, siendo la correspondencia entre el modelo matemático y la naturaleza del sistema conocida por construcción. Ejemplos de objetos matemáticos que se utilizan a menudo para modelar sistemas son: máquinas de estados finitos , sistemas de transición etiquetados , redes de Petri , sistemas de adición de vectores , 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 . [2]
Enfoques
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 en los que conjuntos infinitos de estados se pueden representar de manera efectiva 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 cálculo. Las técnicas de implementación incluyen enumeración de espacios de estados, enumeración de espacios de estados simbólicos, interpretación abstracta , simulación simbólica y refinamiento de abstracciones. [ cita requerida ] Las propiedades a verificar se describen a menudo en lógicas temporales , como lógica temporal lineal (LTL), lenguaje de especificación de propiedades (PSL), aserciones SystemVerilog (SVA), [3] o lógica de árbol computacional (CTL). La gran ventaja de la verificación de modelos es que a menudo es completamente automática; su principal desventaja es que, en general, no se escala a grandes sistemas; Los modelos simbólicos generalmente se limitan 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 descargar estas obligaciones utilizando asistentes de prueba (probadores interactivos de teoremas) ( como HOL , ACL2 , Isabelle , Coq o PVS ), probadores automáticos de teoremas , incluidos en particular los solucionadores de teorías de 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 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 los componentes del sistema (por ejemplo, funciones o procedimientos) y quizás subcomponentes (como bucles o estructuras de datos).
Software
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 basado en tipos es la programación de tipificación dependiente , 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 frente a esas especificaciones. Los lenguajes de escritura dependiente con todas las funciones 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 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 pueden deducirse lógicamente de la semántica, o incorrectas , 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 poco sólida es aquella que cubre solo un subconjunto de las posibilidades, por ejemplo, solo números enteros hasta 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. Debido a que están limitadas, las técnicas poco sólidas a menudo tienen más probabilidades de ser decidibles que las sólidas.
Verificación y validación
La verificación es un aspecto de la prueba de la idoneidad de un producto para su propósito. La validación es el aspecto complementario. A menudo, uno se refiere al proceso global de cheques como V & V .
- Validación : "¿Estamos tratando de hacer lo correcto?", Es decir, ¿el producto se especifica según las necesidades reales del usuario?
- Verificación : "¿Hemos hecho lo que estábamos tratando de hacer?", Es decir, ¿el producto se ajusta a las especificaciones?
El proceso de verificación consta de aspectos estáticos / estructurales y dinámicos / de comportamiento. 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 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 con todos los casos de uso ?").
Reparación automatizada del programa
La reparación del programa se realiza con respecto a un oráculo , abarcando la funcionalidad deseada del programa que se utiliza para la validación de la corrección generada. Un ejemplo simple es un conjunto de pruebas: los pares de entrada / salida especifican la funcionalidad del programa. Se emplean una variedad de técnicas, más notablemente usando solucionadores de teorías de módulo de satisfacibilidad (SMT), [4] y programación genética , [5] usando computación evolutiva para generar y evaluar posibles candidatos para arreglos. 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 fallas en la verificación formal se utilizan para calcular los puntos del programa que podrían ser posibles ubicaciones de errores, que pueden ser el objetivo de los módulos de síntesis. Los sistemas de reparación a menudo se centran en una pequeña clase de errores predefinidos para reducir el espacio de búsqueda. El uso industrial es limitado debido al costo computacional de las técnicas existentes.
Uso industrial
El aumento de la complejidad de los diseños aumenta la importancia de las técnicas de verificación formales 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 está languideciendo. [ cita requerida ] Esto podría atribuirse a la mayor necesidad en la industria del hardware, donde los errores tienen 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 la 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], se han verificado formalmente varios sistemas operativos: el microkernel Secure Embedded L4 de NICTA , vendido comercialmente como seL4 por OK Labs; [10] ORIENTAIS, sistema operativo en tiempo real basado en OSEK / VDX de la Universidad Normal de China Oriental ; [ cita requerida ] Sistema operativo Integrity de Green Hills Software ; [ cita requerida ] y PikeOS de SYSGO . [11] [12]
A partir de 2016, los profesores de Yale y Columbia, Zhong Shao y Ronghui Gu, desarrollaron un protocolo de verificación formal para blockchain llamado CertiKOS. [13] El programa es el primer ejemplo de verificación formal en el mundo blockchain, y un ejemplo de verificación formal que se utiliza explícitamente como programa de seguridad. [14]
A partir de 2017, la verificación formal se ha aplicado al diseño de grandes redes informáticas [15] a través de un modelo matemático de la red, [16] y como parte de una nueva categoría de tecnología de red, las redes basadas en la intención. [17] Los proveedores de software de red que ofrecen soluciones formales de verificación incluyen Cisco [18] Forward Networks [19] [20] y Veriflow Systems. [21]
El compilador CompCert C es un compilador C verificado formalmente que implementa la mayoría de ISO C.
Ver también
- Demostración automatizada de teoremas
- Comprobación de modelo
- Lista de herramientas de verificación de modelos
- Comprobación de equivalencia formal
- Comprobador de pruebas
- Idioma de especificación de propiedad
- Bibliografía de verificación formal seleccionada
- Análisis de código estático
- Lógica temporal en la verificación de estados finitos
- Validación posterior al silicio
- Verificación inteligente
- Verificación en tiempo de ejecución
Referencias
- ^ Sanghavi, Alok (21 de mayo de 2010). "¿Qué es la verificación formal?". EE Times Asia .
- ^ Introducción a la verificación formal , Universidad de Berkeley de California, obtenido el 6 de noviembre de 2013
- ^ Cohen, Ben; Venkataramanan, Srinivasan; Kumari, Ajeetha; Piper, Lisa (2015). Manual de afirmaciones de SystemVerilog (4ª ed.). Plataforma de publicación independiente CreateSpace. ISBN 978-1518681448.
- ^ Favio DeMarco; Jifeng Xuan; Daniel Le Berre; Martín Monperrus (2014). Reparación automática de Buggy If Condiciones y condiciones previas faltantes con SMT . Actas del 6º Taller Internacional sobre Restricciones en las Pruebas, Verificación y Análisis de Software (CSTVA 2014) . págs. 30–39. arXiv : 1404.3186 . doi : 10.1145 / 2593735.2593740 . ISBN 9781450328470. S2CID 506586 .
- ^ Le Goues, Claire; Nguyen, ThanhVu; Forrest, Stephanie; Weimer, Westley (enero de 2012). "GenProg: un método genérico para la reparación automática de software" . Transacciones IEEE sobre ingeniería de software . 38 (1): 54–72. doi : 10.1109 / TSE.2011.104 . S2CID 4111307 .
- ^ Harrison, J. (2003). "Verificación formal en Intel". 18º Simposio Anual de Lógica en Ciencias de la Computación del IEEE, 2003. Actas . págs. 45–54. doi : 10.1109 / LICS.2003.1210044 . ISBN 978-0-7695-1884-8. S2CID 44585546 .
- ^ Verificación formal de un diseño de hardware en tiempo real . Portal.acm.org (27 de junio de 1983). Consultado el 30 de abril de 2011.
- ^ "Verificación formal: una herramienta esencial para el diseño VLSI moderno por Erik Seligman, Tom Schubert y MV Achutha Kirankumar" . 2015.
- ^ "Verificación formal en la industria" (PDF) . Consultado el 20 de septiembre de 2012 .
- ^ "Especificación formal abstracta de la API seL4 / ARMv6" (PDF) . Archivado desde el original (PDF) el 21 de mayo de 2015 . Consultado el 19 de mayo de 2015 .
- ^ Christoph Baumann, Bernhard Beckert, Holger Blasum y Thorsten Bormer ¿ Ingredientes de la corrección del sistema operativo? Lecciones aprendidas en la verificación formal de PikeOS
- ^ "Haciéndolo bien" por Jack Ganssle
- ^ Harris, Robin. "¿Sistema operativo no hackeable? CertiKOS permite la creación de núcleos de sistema seguros" . ZDNet . Consultado el 10 de junio de 2019 .
- ^ "CertiKOS: Yale desarrolla el primer sistema operativo resistente a los piratas informáticos del mundo" . International Business Times Reino Unido . 15 de noviembre de 2016 . Consultado el 10 de junio de 2019 .
- ^ Heller, Brandon. "Buscando la verdad en las redes: de la prueba a la verificación" . Redes de avance . Consultado el 12 de febrero de 2018 .
- ^ Scroxton, Alex. "Para Cisco, las redes basadas en la intención anuncian las futuras demandas tecnológicas" . Computer Weekly . Consultado el 12 de febrero de 2018 .
- ^ Lerner, Andrew. "Redes basadas en intenciones" . Gartner . Consultado el 12 de febrero de 2018 .
- ^ Kerravala, Zeus. "Cisco lleva redes basadas en intención al centro de datos" . NetworkWorld . Consultado el 12 de febrero de 2018 .
- ^ "Redes de avance: acelerar y reducir el riesgo de las operaciones de red" . Insights Success . Consultado el 12 de febrero de 2018 .
- ^ "Conectarse a tierra en redes basadas en intención" (PDF) . NetworkWorld . Consultado el 12 de febrero de 2018 .
- ^ "Sistemas Veriflow" . Bloomberg . Consultado el 12 de febrero de 2018 .