Análisis estático de programas

En informática , el análisis estático de programas (también conocido como análisis estático o simulación estática ) es el análisis de programas informáticos realizado sin ejecutarlos, a diferencia del análisis dinámico de programas , que se realiza sobre los programas durante su ejecución en el entorno integrado. ^{[ 1 ] [ 2 ]}

El término se aplica generalmente al análisis realizado por una herramienta automatizada, mientras que el análisis humano se suele denominar "comprensión del programa", " comprensión del programa " o "revisión de código" . En este último caso, también se utilizan los términos inspección de software y recorrido del software . En la mayoría de los casos, el análisis se realiza sobre alguna versión del código fuente de un programa y, en otros casos, sobre alguna forma de su código objeto .

Dos de los enfoques principales para la certificación de recursos han sido el Análisis Estático (AE) y la Complejidad Computacional Implícita (CCI). El AE es de naturaleza algorítmica: se centra en un lenguaje de programación amplio y busca determinar, mediante métodos sintácticos, si determinados programas en ese lenguaje son factibles. En cambio, la CCI intenta crear desde el principio lenguajes o métodos de programación especializados que definan una clase de complejidad. Por lo tanto, el AE se centra en el tiempo de compilación, sin exigir nada al programador; mientras que la CCI es una disciplina de diseño de lenguajes.

La disciplina del análisis estático no debe confundirse con el análisis estático , que es el proceso de comprobar si hay errores de estilo en la codificación .

La sofisticación del análisis realizado por las herramientas varía desde aquellas que solo consideran el comportamiento de instrucciones y declaraciones individuales ^{[ 4 ]} hasta aquellas que incluyen el código fuente completo de un programa en su análisis. Los usos de la información obtenida del análisis varían desde resaltar posibles errores de codificación (por ejemplo, la herramienta lint ) hasta métodos formales que demuestran matemáticamente propiedades sobre un programa dado (por ejemplo, que su comportamiento coincide con el de su especificación).

Las métricas de software y la ingeniería inversa pueden describirse como formas de análisis estático. La obtención de métricas de software y el análisis estático se utilizan cada vez más de forma conjunta, especialmente en la creación de sistemas embebidos, mediante la definición de los denominados objetivos de calidad del software . ^{[ 5 ]}

Un uso comercial cada vez más extendido del análisis estático es la verificación de las propiedades del software utilizado en sistemas informáticos críticos para la seguridad y la localización de código potencialmente vulnerable . ^{[ 6 ]} Por ejemplo, las siguientes industrias han identificado el uso del análisis estático de código como un medio para mejorar la calidad de un software cada vez más sofisticado y complejo:

1. Software médico : La Administración de Alimentos y Medicamentos de los Estados Unidos (FDA) ha identificado el uso de análisis estático para dispositivos médicos. ^{[ 7 ]}
2. Software nuclear: En el Reino Unido, la Oficina de Regulación Nuclear (ONR) recomienda el uso de análisis estático en los sistemas de protección de reactores . ^{[ 8 ]}
3. Software de aviación (en combinación con análisis dinámico ). ^{[ 9 ]}
4. Automoción y maquinaria (las características de seguridad funcional forman parte integral de cada fase de desarrollo de productos automotrices, ISO 26262 , sección 8).

Un estudio de 2012 realizado por VDC Research informó que el 28,7 % de los ingenieros de software embebido encuestados utilizaban herramientas de análisis estático y el 39,7 % esperaba utilizarlas en los próximos dos años. ^{[ 10 ]} Un estudio de 2010 reveló que el 60 % de los desarrolladores entrevistados en proyectos de investigación europeos utilizaban al menos los analizadores estáticos integrados en su IDE básico. Sin embargo, solo alrededor del 10 % empleaba una herramienta de análisis adicional (y quizás más avanzada). ^{[ 11 ]}

En la industria de la seguridad de aplicaciones, también se utiliza el nombre de pruebas estáticas de seguridad de aplicaciones (SAST). SAST es una parte importante de los ciclos de vida de desarrollo seguro (SDL), como el SDL definido por Microsoft ^{[ 12 ]} , y una práctica común en las empresas de software ^{[ 13 ] .}

El OMG ( Object Management Group ) publicó un estudio sobre los tipos de análisis de software necesarios para la medición y evaluación de la calidad del software . Este documento, titulado "Cómo ofrecer sistemas de TI resilientes, seguros, eficientes y fácilmente modificables de acuerdo con las recomendaciones de CISQ", describe tres niveles de análisis de software. ^{[ 14 ]}

Nivel de unidad

Análisis que se realiza dentro de un programa o subrutina específicos, sin estar conectado al contexto de ese programa.

Nivel tecnológico

Análisis que tiene en cuenta las interacciones entre los programas de las unidades para obtener una visión más holística y semántica del programa en su conjunto, con el fin de detectar problemas y evitar falsos positivos obvios .

Nivel del sistema

Análisis que tiene en cuenta las interacciones entre programas unitarios, pero sin limitarse a una tecnología o lenguaje de programación específico.

Se puede definir un nivel adicional de análisis de software.

Nivel de misión/negocio

Análisis que considera los términos, reglas y procesos de la capa de negocio/misión implementados en el sistema de software para su funcionamiento como parte de las actividades de la capa empresarial o de programa/misión. Estos elementos se implementan sin limitarse a una tecnología o lenguaje de programación específico y, en muchos casos, se distribuyen en varios lenguajes, pero se extraen y analizan estáticamente para la comprensión del sistema y la garantía de la misión.

Muchas herramientas de análisis estático utilizan representaciones intermedias de los programas para examinar la estructura del código fuente sin ejecutar el programa. Para ello, se suelen utilizar árboles de sintaxis abstracta (AST), ya que proporcionan una representación estructurada de los elementos sintácticos de un programa.

El término «métodos formales» se aplica al análisis de software (y hardware informático ) cuyos resultados se obtienen exclusivamente mediante el uso de métodos matemáticos rigurosos. Las técnicas matemáticas empleadas incluyen la semántica denotacional , la semántica axiomática , la semántica operacional y la interpretación abstracta .

Mediante una reducción directa al problema de la parada , es posible demostrar que (para cualquier lenguaje Turing completo ), encontrar todos los posibles errores de ejecución en un programa arbitrario (o, más generalmente, cualquier tipo de violación de una especificación sobre el resultado final de un programa) es indecidible : no existe un método mecánico que pueda responder siempre con veracidad si un programa arbitrario puede o no presentar errores de ejecución. Este resultado data de los trabajos de Church , Gödel y Turing en la década de 1930 (véase: Problema de la parada y teorema de Rice ). Como ocurre con muchas cuestiones indecidibles, aún se pueden intentar proporcionar soluciones aproximadas útiles.

Algunas de las técnicas de implementación del análisis estático formal incluyen: ^{[ 15 ]}

• La interpretación abstracta modela el efecto que cada enunciado tiene sobre el estado de una máquina abstracta (es decir, "ejecuta" el software basándose en las propiedades matemáticas de cada enunciado y declaración). Esta máquina abstracta sobreestima el comportamiento del sistema: el sistema abstracto se simplifica así para su análisis, a costa de la incompletitud (no todas las propiedades verdaderas del sistema original son verdaderas del sistema abstracto). Sin embargo, si se realiza correctamente, la interpretación abstracta es sólida (toda propiedad verdadera del sistema abstracto puede mapearse a una propiedad verdadera del sistema original). ^{[ 16 ]}
• Análisis de flujo de datos , una técnica basada en retículas para recopilar información sobre el conjunto posible de valores;
• La lógica de Hoare es un sistema formal con un conjunto de reglas lógicas para razonar rigurosamente sobre la corrección de los programas informáticos . Existe soporte de herramientas para algunos lenguajes de programación (por ejemplo, el lenguaje de programación SPARK (un subconjunto de Ada ) y el Java Modeling Language —JML— usando ESC/Java y ESC/Java2 , el complemento Frama-C WP ( precondición más débil ) para el lenguaje C extendido con ACSL ( ANSI/ISO C Specification Language )).
• La verificación de modelos considera sistemas que tienen un estado finito o que pueden reducirse a un estado finito mediante abstracción ;
• La ejecución simbólica se utiliza para derivar expresiones matemáticas que representan el valor de las variables modificadas en puntos específicos del código.
• Análisis de referencia anulable

El análisis estático basado en datos aprovecha extensas bases de código para inferir reglas de codificación y mejorar la precisión del análisis. ^{[ 17 ] [ 18 ]} Por ejemplo, se pueden usar todos los paquetes de código abierto de Java disponibles en GitHub para aprender buenas estrategias de análisis. La inferencia de reglas puede usar técnicas de aprendizaje automático. ^{[ 19 ]} También es posible aprender de una gran cantidad de correcciones y advertencias anteriores. ^{[ 17 ]}

Los analizadores estáticos generan advertencias. Para ciertos tipos de advertencias, es posible diseñar e implementar técnicas de remediación automatizadas . Por ejemplo, Logozzo y Ball propusieron remediaciones automatizadas para C# cccheck . ^{[ 20 ]}

• Ayewah, Nathaniel; Hovemeyer, David; Morgenthaler, J. David; Penix, John; Pugh, William (2008). "Uso del análisis estático para encontrar errores". IEEE Software . 25 (5): 22– 29. CiteSeerX 10.1.1.187.8985 . doi : 10.1109/MS.2008.130 . S2CID 20646690 .  
• Brian Chess, Jacob West (Fortify Software) (2007). Programación segura con análisis estático . Addison-Wesley. ISBN 978-0-321-42477-8.
• Flemming Nielson; Hanne R. Nielson; Chris Hankin (10 de diciembre de 2004). Principios del análisis de programas (edición de 1999 (corregida en 2004)  ). Springer. ISBN 978-3-540-65410-0.
• "Interpretación abstracta y análisis estático", Escuela Internacional de Invierno sobre Semántica y Aplicaciones 2003, por David A. Schmidt