Análisis de programa estático

En informática, el análisis estático de programas (o análisis estático) es el análisis de programas informáticos realizado sin ejecutarlos, en contraste con el análisis dinámico de programas, que se realiza sobre los programas durante su ejecución.

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

Fundamento

La sofisticación del análisis que realizan las herramientas varía desde aquellas que solo consideran el comportamiento de sentencias y declaraciones individuales, 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 (p. ej., la herramienta lint) hasta métodos formales que prueban matemáticamente las propiedades de un programa determinado (p. ej., su comportamiento coincide con el de su especificación).

Las métricas de software y la ingeniería inversa se pueden describir como formas de análisis estático. La derivación de métricas de software y el análisis estático se implementan cada vez más juntos, especialmente en la creación de sistemas integrados, mediante la definición de los llamados objetivos de calidad del software.

Un uso comercial cada vez mayor 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 localizar código potencialmente vulnerable. Por ejemplo, las siguientes industrias han identificado el uso del análisis de código estático como un medio para mejorar la calidad del 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.
2. Software nuclear: En el Reino Unido la Oficina de Regulación Nuclear (ONR) recomienda el uso de análisis estáticos sobre sistemas de protección de reactores.
3. Software de aviación (en combinación con análisis dinámico)
4. Máquinas automotrices (Las características de seguridad funcional forman parte integral de cada fase de desarrollo del producto automotriz, ISO 26262, Sec 8.)

Un estudio realizado en 2012 por VDC Research informó que el 28,7 % de los ingenieros de software integrado encuestados actualmente usa herramientas de análisis estático y el 39,7 % espera usarlas dentro de 2 años. Un estudio de 2010 encontró que el 60% de los desarrolladores entrevistados en proyectos de investigación europeos hicieron al menos uso de sus analizadores estáticos integrados IDE básicos. Sin embargo, solo alrededor del 10% empleó otra herramienta de análisis adicional (y quizás más avanzada).

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

Tipos de herramientas

El OMG (Object Management Group) publicó un estudio sobre los tipos de análisis de software necesarios para medir y evaluar la calidad del software. Este documento sobre "Cómo ofrecer sistemas de TI resistentes, seguros, eficientes y fáciles de cambiar de acuerdo con las recomendaciones de CISQ" describe tres niveles de análisis de software.

Nivel de unidad

Análisis que tiene lugar dentro de un programa específico o subrutina, sin conectarse al contexto de ese programa.

Nivel de tecnología

Análisis que tiene en cuenta las interacciones entre los programas de unidad para obtener una visión más holística y semántica del programa general con el fin de encontrar problemas y evitar falsos positivos obvios. Por ejemplo, es posible analizar estaticamente la pila de tecnología Android para encontrar errores de permiso.

Nivel de sistema

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

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

Nivel de la Misión y el Personal

Análisis que tiene en cuenta los términos, reglas y procesos de las capas de negocio/misión que se implementan dentro del sistema de software para su funcionamiento como parte de las actividades empresariales o de las capas de programa/misión. Estos elementos se implementan sin limitarse a un lenguaje específico de la tecnología o la programación y en muchos casos se distribuyen en varios idiomas, pero se extraen y analizan estadísticamente para la comprensión del sistema para la seguridad de la misión.

Métodos formales

Métodos formales es el término que se aplica al análisis de software (y hardware de computadora) cuyos resultados se obtienen puramente mediante el uso de métodos matemáticos rigurosos. Las técnicas matemáticas utilizadas incluyen semántica denotacional, semántica axiomática, semántica operativa e interpretación abstracta.

Mediante una reducción directa al problema de la detención, es posible demostrar que (para cualquier lenguaje completo de Turing), encontrar todos los posibles errores en tiempo de ejecución en un programa arbitrario (o, de manera más general, cualquier tipo de violación de una especificación en el resultado final de un programa) es indecidible: no existe un método mecánico que siempre pueda responder con veracidad si un programa arbitrario puede o no presentar errores de tiempo de ejecución. Este resultado data de los trabajos de Church, Gödel y Turing en la década de 1930 (ver: problema de detención y teorema de Rice). Al igual que con muchas preguntas indecidibles, todavía se puede intentar dar soluciones aproximadas útiles.

Algunas de las técnicas de implementación del análisis estático formal incluyen:

• Interpretación abstracta, para modelar el efecto que cada declaración tiene en el estado de una máquina abstracta (es decir, "exactúa" el software basado en las propiedades matemáticas de cada declaración y declaración). Esta máquina abstracta supera los comportamientos del sistema: el sistema abstracto se hace más simple de analizar, a expensas de incompleta (no toda propiedad verdadera del sistema original es verdadera del sistema abstracto). Si se hace correctamente, sin embargo, la interpretación abstracta es sonido (toda propiedad verdadera del sistema abstracto se puede mapear a una verdadera propiedad del sistema original).
• Análisis de flujo de datos, una técnica basada en la celosía para reunir información sobre el posible conjunto de valores;
• La lógica Hoare, un sistema formal con un conjunto de reglas lógicas para razonar rigurosamente sobre la corrección de los programas informáticos. Hay soporte de herramientas para algunos lenguajes de programación (por ejemplo, el lenguaje de programación SPARK (un subconjunto de Ada) y el lenguaje de modelado Java—JML—usando ESC/Java y ESC/Java2, Frama-C WP (precondición más débil) plugin para el lenguaje C extendido con ACSL (ANSI/ISO C Lenguaje de especificación)).
• Verificación de modelos, considera sistemas que tienen estado finito o pueden ser reducidos al estado finito por abstracción;
• Ejecución simbólica, como se utiliza para derivar expresiones matemáticas que representan el valor de variables mutadas en puntos particulares del código.

Análisis estático basado en datos

El análisis estático basado en datos utiliza grandes cantidades de código para inferir reglas de codificación. Por ejemplo, uno puede usar todos los paquetes de código abierto de Java en GitHub para aprender una buena estrategia de análisis. La inferencia de reglas puede utilizar técnicas de aprendizaje automático. Por ejemplo, se ha demostrado que cuando uno se desvía demasiado en la forma en que usa una API orientada a objetos, es probable que se trate de un error. También es posible aprender de una gran cantidad de correcciones y advertencias anteriores.

Remediación

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 han propuesto soluciones automatizadas para C# cccheck y Etemadi y sus colegas utilizan la transformación del programa para corregir automáticamente las advertencias de SonarQube.