stringtranslate.com

Verificación formal

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]

Aproches

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).

Software

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.

Verificación y validación

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 ?").

Reparación automatizada de programas

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.

Uso industrial

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 , 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]

Véase también

Referencias

  1. ^ Sanghavi, Alok (21 de mayo de 2010). "¿Qué es la verificación formal?". EE Times Asia .
  2. ^ Sanjit A. Seshia; Natasha Sharygina; Stavros Tripakis (2018). "Capítulo 3: Modelado para verificación". En Clarke, Edmund M.; Henzinger, Thomas A.; Veith, Helmut; Bloem, Roderick (eds.). Manual de verificación de modelos. Springer. págs. 75–105. doi :10.1007/978-3-319-10575-8. ISBN . 978-3-319-10574-1.
  3. ^ Introducción a la verificación formal, Berkeley University of California, consultado el 6 de noviembre de 2013
  4. ^ Cohen, Ben; Venkataramanan, Srinivasan; Kumari, Ajeetha; Piper, Lisa (2015). Manual de afirmaciones de SystemVerilog (4.ª edición). Plataforma de publicación independiente CreateSpace. ISBN 978-1518681448.
  5. ^ 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". IEEE Transactions on Software Engineering . 38 (1): 54–72. doi :10.1109/TSE.2011.104. S2CID  4111307.
  6. ^ Harrison, J. (2003). "Verificación formal en Intel". 18.º Simposio anual IEEE sobre lógica en informática, 2003. Actas . pp. 45–54. doi :10.1109/LICS.2003.1210044. ISBN . 978-0-7695-1884-8.S2CID 44585546  .
  7. ^ Verificación formal de un diseño de hardware en tiempo real. Portal.acm.org (27 de junio de 1983). Recuperado el 30 de abril de 2011.
  8. ^ "Verificación formal: una herramienta esencial para el diseño VLSI moderno por Erik Seligman, Tom Schubert y MV Achutha Kirankumar". 2015.
  9. ^ "Verificación formal en la industria" (PDF) . Consultado el 20 de septiembre de 2012 .
  10. ^ "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 .
  11. ^ Christoph Baumann, Bernhard Beckert, Holger Blasum y Thorsten Bormer ¿Cuáles son los ingredientes de la corrección de un sistema operativo? Lecciones aprendidas en la verificación formal de PikeOS Archivado el 19 de julio de 2011 en Wayback Machine
  12. ^ "Cómo hacerlo bien" de Jack Ganssle
  13. ^ Harris, Robin. "¿Un sistema operativo inhackeable? CertiKOS permite la creación de núcleos de sistemas seguros". ZDNet . Consultado el 10 de junio de 2019 .
  14. ^ "CertiKOS: Yale desarrolla el primer sistema operativo resistente a los hackers del mundo". International Business Times UK . 15 de noviembre de 2016. Consultado el 10 de junio de 2019 .
  15. ^ Scroxton, Alex. "Para Cisco, las redes basadas en intenciones presagian las demandas tecnológicas futuras". Computer Weekly . Consultado el 12 de febrero de 2018 .
  16. ^ Lerner, Andrew. "Intent-based networking". Gartner . Consultado el 12 de febrero de 2018 .
  17. ^ Kerravala, Zeus. "Cisco lleva las redes basadas en intenciones al centro de datos". NetworkWorld. Archivado desde el original el 11 de diciembre de 2023. Consultado el 12 de febrero de 2018 .
  18. ^ "Redes avanzadas: aceleración y reducción de riesgos en las operaciones de red". Insights Success. 16 de enero de 2018. Consultado el 12 de febrero de 2018 .
  19. ^ "Conociendo las redes basadas en intenciones" (PDF) . NetworkWorld . Consultado el 12 de febrero de 2018 .
  20. ^ "Veriflow Systems". Bloomberg . Consultado el 12 de febrero de 2018 .
  21. ^ "CompCert - El compilador C de CompCert". compcert.org . Consultado el 22 de febrero de 2023 .
  22. ^ Barrière, Aurèle; Blazy, Sandrine ; Pichardie, David (9 de enero de 2023). "Generación de código nativo verificado formalmente en un JIT eficaz: convertir el backend CompCert en un compilador JIT verificado formalmente". Actas de la ACM sobre lenguajes de programación . 7 (POPL): 249–277. arXiv : 2212.03129 . doi : 10.1145/3571202 . ISSN  2475-1421. S2CID  253736486.