Hispanopedia Wiki
Articulo de referencia

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 especificación o pro...

Hispanopedia WikiContenido en espanolLectura gratuita

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 especificación o propiedad formal determinada, utilizando métodos formales de matemáticas . [ 1 ] La verificación formal es un incentivo clave para la especificación formal de sistemas y constituye 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 alcanzar el Nivel de Garantía de Evaluación ( EAL7 ) más alto en el marco de los criterios comunes para la certificación de seguridad informática . [ 2 ]

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 . Ejemplos destacados de sistemas de software verificados incluyen el compilador C verificado por 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. [ 3 ] 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 vectorial , autómatas temporizados , autómatas híbridos , álgebra de procesos , semántica formal de lenguajes de programación como la semántica operacional , la semántica denotacional , la semántica axiomática y la lógica de Hoare . [ 4 ]

Aproches

Verificación de modelos

La verificación de modelos implica una exploración sistemática y exhaustiva del modelo matemático. Dicha exploración es posible para modelos finitos , pero también para algunos modelos infinitos, donde conjuntos infinitos de estados pueden representarse de manera finita mediante abstracción o aprovechando la simetría. Por lo general, esto consiste en explorar todos los estados y transiciones en el modelo, utilizando 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. Las propiedades que se van 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 aserciones de SystemVerilog (SVA) [ 5 ] o la 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 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.

verificación deductiva

Otro enfoque es la verificación deductiva. [ 6 ] [ 7 ] Consiste en generar a partir del sistema y sus especificaciones (y posiblemente otras anotaciones) una colección de obligaciones de prueba matemática , cuya veracidad 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 , Rocq (anteriormente conocido como Coq ) o PVS ), o demostradores de teoremas automáticos , incluyendo en particular solucionadores de satisfacibilidad módulo teorías (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, precondiciones, postcondiciones) de componentes del sistema (por ejemplo, funciones o procedimientos) y quizás subcomponentes (como bucles o estructuras de datos).

Aplicación al 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 la verificación formal incluyen la verificación deductiva (véase más arriba), la interpretación abstracta , la demostración automática de teoremas , los sistemas de tipos y los métodos formales ligeros . Un enfoque prometedor de verificación basado en tipos es la programación con tipos dependientes , en la que los tipos de las funciones incluyen (al menos en parte) las especificaciones de dichas funciones, y la comprobación de tipos del código establece su corrección con respecto a esas especificaciones. Los lenguajes con tipos dependientes completos admiten la verificación deductiva como un caso especial.

Otro enfoque complementario es la derivación de programas , en la que se genera 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 puede considerarse otra forma de síntesis de programas .

Estas técnicas pueden ser sólidas , lo que significa que las propiedades verificadas pueden deducirse 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 enteros hasta cierto número, y proporciona un resultado "suficientemente bueno". Las técnicas también pueden ser decidibles , lo que significa que sus implementaciones algorítmicas tienen la garantía de terminar con una respuesta, o indecidibles, lo que significa que pueden no terminar nunca. Al limitar el alcance de las posibilidades, se podrían construir técnicas no sólidas que sean decidibles cuando no se disponga de técnicas sólidas decidibles.

Verificación y validación

La verificación es un aspecto de la evaluación de la idoneidad de un producto para su propósito. La validación es el aspecto complementario. A menudo, el proceso general de verificación se denomina V&V.

  • Validación : "¿Estamos intentando hacer lo correcto?", es decir, ¿el producto se ajusta a las necesidades reales del usuario?
  • Verificación : "¿Hemos logrado lo que nos propusimos?", es decir, ¿el producto cumple con 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 ejecutar pruebas con casos específicos (dinámico). La validación generalmente 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 de programas

La reparación de programas se realiza con respecto a un oráculo que abarca la funcionalidad deseada del programa y que se utiliza para validar la correcció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, principalmente el uso de solucionadores de satisfacibilidad módulo teorías (SMT) y programación genética [ 8 ] , que utiliza computación evolutiva para generar y evaluar posibles candidatos para correcciones. El primer método es determinista, mientras que el segundo es aleatorio. Por ejemplo, la herramienta Nopol codifica la reparación de sentencias condicionales con errores como una instancia SMT para generar parches de forma determinista para condiciones if y precondiciones faltantes [ 9 ] .

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, los cuales pueden ser abordados por los módulos de síntesis. Los sistemas de reparación suelen centrarse en una pequeña clase predefinida de errores para reducir el espacio de búsqueda. Su uso industrial es limitado debido al coste computacional de las técnicas existentes.

Uso industrial

El aumento de la complejidad de los diseños incrementa la importancia de las técnicas de verificación formal en la industria del hardware . [ 10 ] [ 11 ] Actualmente, la verificación formal es utilizada por la mayoría o la totalidad de las empresas líderes de hardware, [ 12 ] pero su uso en la industria del software aún está rezagado. Esto podría atribuirse a la mayor necesidad en la industria del hardware, donde los errores tienen mayor relevancia comercial. Debido a las posibles interacciones sutiles entre componentes, resulta cada vez más difícil evaluar 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 facilita la introducción de la verificación formal y la hace más productiva. [ 13 ]

A partir de 2011Se han verificado formalmente varios sistemas operativos: el microkernel Secure Embedded L4 de NICTA , vendido comercialmente como seL4 por OK Labs; [ 14 ] el sistema operativo en tiempo real ORIENTAIS basado en OSEK/VDX de la Universidad Normal del Este de China ; el sistema operativo Integrity de Green Hills Software ; y PikeOS de SYSGO . [ 15 ] [ 16 ] En 2016, un equipo liderado por Zhong Shao en Yale desarrolló un kernel de sistema operativo verificado formalmente llamado CertiKOS. [ 17 ] [ 18 ]

Desde 2017, la verificación formal se ha aplicado al diseño de grandes redes informáticas mediante un modelo matemático de la red, [ 19 ] y como parte de una nueva categoría de tecnología de red, la red basada en intenciones . [ 20 ] Entre los proveedores de software de red que ofrecen soluciones de verificación formal se incluyen Cisco [ 21 ] Forward Networks [ 22 ] [ 23 ] y Veriflow Systems. [ 24 ]

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 .

El compilador CompCert C es un compilador C formalmente verificado que implementa la mayor parte de ISO C. [ 25 ] [ 26 ]

Véase también

Referencias

  1. ↑ Sanghavi, Alok (21 de mayo de 2010). "¿Qué es la verificación formal?". EE Times Asia .
  2. ↑ "Criterios comunes para la evaluación de la seguridad de las tecnologías de la información, parte 5: paquetes predefinidos de requisitos de seguridad" (PDF) . Consultado el 15 de abril de 2025 .
  3. ↑ Sanjit A. Seshia; Natasha Sharygina; Stavros Tripakis (2018). «Capítulo 3: Modelado para la verificación». En Clarke, Edmund M.; Henzinger, Thomas A.; Veith, Helmut; Bloem, Roderick (eds.). Manual de verificación de modelos . Springer. pp. 75–105 . doi : 10.1007/978-3-319-10575-8 . ISBN  978-3-319-10574-1.
  4. ↑ Introducción a la verificación formal , Universidad de California en Berkeley, consultado el 6 de noviembre de 2013.
  5. ↑ Cohen, Ben; Venkataramanan, Srinivasan; Kumari, Ajeetha; Piper, Lisa (2015). Manual de aserciones de SystemVerilog (4.ª ed.). CreateSpace Independent Publishing Platform. ISBN  978-1518681448.
  6. ↑ Ahrendt, Wolgang; Beckert, Bernhard; Bubel, Richard; Hähnle, Reiner; Schmitt, Peter H., eds. (2016). Deductive Software Verification - The KeY Book: From Theory to Practice (1.ª ed. 2016). Cham: Springer International Publishing : Imprint: Springer. ISBN   978-3-319-49812-6.
  7. ↑ Pretschner, Alexander; Müller, Peter; Stöckle, Patrick, eds. (2019). «Building Deductive Program Verifiers - Lecture Notes». Engineering secure and dependable software systems . Ámsterdam, Países Bajos: IOS Press. ISBN 978-1-61499-976-8.
  8. ↑ 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 . 
  9. ↑ DeMarco, Favio; Xuan, Jifeng; Le Berre, Daniel; Monperrus, Martin (2014). "Reparación automática de condiciones if con errores y precondiciones faltantes con SMT" . ICSE '14: 36.ª Conferencia Internacional sobre Ingeniería de Software : 30–39 . arXiv : 1404.3186 . doi : 10.1145/2593735.2593740 . Recuperado el 8 de junio de 2026 .
  10. ↑ Harrison, J. (2003). "Verificación formal en Intel". 18.º Simposio Anual IEEE de Lógica en Ciencias de la Computación, 2003. Actas . págs. 45–54 . doi : 10.1109/LICS.2003.1210044 . ISBN  978-0-7695-1884-8. S2CID 44585546 . 
  11. ↑ 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.
  12. ↑ "Verificación formal: una herramienta esencial para el diseño VLSI moderno" por Erik Seligman, Tom Schubert y MV Achutha Kirankumar . 2015.
  13. ↑ "Verificación formal en la industria" (PDF) . Consultado el 20 de septiembre de 2012 .
  14. ↑ "Especificación formal abstracta de la API seL4/ARMv6" (PDF) . Archivado del original (PDF) el 21 de mayo de 2015. Recuperado el 19 de mayo de 2015 .
  15. ↑ Christoph Baumann, Bernhard Beckert, Holger Blasum y Thorsten Bormer. 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 .
  16. ↑ "Cómo hacerlo bien" de Jack Ganssle
  17. ↑ Harris, Robin. "¿Sistema operativo inexpugnable? CertiKOS permite la creación de núcleos de sistema seguros" . ZDNet . Consultado el 10 de junio de 2019 .
  18. ↑ "CertiKOS: Yale desarrolla el primer sistema operativo del mundo resistente a los hackers" . International Business Times UK . 15 de noviembre de 2016. Consultado el 10 de junio de 2019 .
  19. ↑ Scroxton, Alex. "Para Cisco, las redes basadas en intenciones anuncian las futuras demandas tecnológicas" . Computer Weekly . Consultado el 12 de febrero de 2018 .
  20. ↑ Lerner, Andrew. "Redes basadas en intenciones" . Gartner . Consultado el 12 de febrero de 2018 .
  21. ↑ Kerravala, Zeus. "Cisco lleva las redes basadas en intenciones al centro de datos" . NetworkWorld. Archivado del original el 11 de diciembre de 2023. Consultado el 12 de febrero de 2018 .
  22. ↑ "Redes de reenvío: Aceleración y reducción de riesgos en las operaciones de red" . Insightssuccess Media and Technology Pvt. Ltd. Insights Success. 16 de enero de 2018. Consultado el 12 de febrero de 2018 .
  23. ↑ "Fundamentos de las redes basadas en intenciones" (PDF) . NetworkWorld . Consultado el 12 de febrero de 2018 .
  24. ↑ "Veriflow Systems" . Bloomberg . Consultado el 12 de febrero de 2018 .
  25. ↑ "CompCert - El compilador C de CompCert" . compcert.org . Consultado el 22 de febrero de 2023 .
  26. ↑ Barrière, Aurèle; Blazy, Sandrine ; Pichardie, David (9 de enero de 2023). "Generación de código nativo formalmente verificado en un JIT efectivo: convertir el backend de CompCert en un compilador JIT formalmente verificado" . 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 .  
Lecturas relacionadas
6 articulos
Hardware de computadoraHardware de computadoraPlaca de CPU PDP-11 El hardware de una computadora incluye las partes físicas de una computadora , como la unidad central de procesamiento (CPU), l...SoftwareSoftwareEl software consiste en programas informáticos que dan instrucciones sobre la ejecución de una computadora . [1] El software puede definirse de man...Prueba matemáticaPrueba matemáticaP. Oxy. 29 , uno de los fragmentos más antiguos que se conservan de los Elementos de Euclides , un libro de texto utilizado durante milenios para e...Corrección (informática)Corrección (informática)En informática teórica , un algoritmo es correcto con respecto a una especificación si se comporta como se especifica. Lo mejor es explorar la corr...Especificación formalEn informática , las especificaciones formales son técnicas basadas en matemáticas cuyo propósito es ayudar con la implementación de sistemas y sof...[icono]Métodos formalesEn informática , los métodos formales son técnicas matemáticamente rigurosas para la especificación , desarrollo, análisis y verificación de sistem...