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

Analysis that takes into account the interactions between unit programs, but without being limited to one specific technology or programming language.

A further level of software analysis can be defined.

Mission/Business Level

Analysis that takes into account the business/mission layer terms, rules and processes that are implemented within the software system for its operation as part of enterprise or program/mission layer activities. These elements are implemented without being limited to one specific technology or programming language and in many cases are distributed across multiple languages, but are statically extracted and analyzed for system understanding for mission assurance.

Many static analysis tools use intermediate representations of programs to examine the structure of source code without executing the program. For this purpose, abstract syntax trees (ASTs) are commonly used, since they provide a structured representation of a program's syntactic elements.

Formal methods is the term applied to the analysis of software (and computer hardware) whose results are obtained purely through the use of rigorous mathematical methods. The mathematical techniques used include denotational semantics, axiomatic semantics, operational semantics, and abstract interpretation.

By a straightforward reduction to the halting problem, it is possible to prove that (for any Turing complete language), finding all possible run-time errors in an arbitrary program (or more generally any kind of violation of a specification on the final result of a program) is undecidable: there is no mechanical method that can always answer truthfully whether an arbitrary program may or may not exhibit runtime errors. This result dates from the works of Church, Gödel and Turing in the 1930s (see: Halting problem and Rice's theorem). As with many undecidable questions, one can still attempt to give useful approximate solutions.

Some of the implementation techniques of formal static analysis include:^[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). "Using Static Analysis to Find Bugs". 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). Secure Programming with Static Analysis. Addison-Wesley. ISBN 978-0-321-42477-8.
• Flemming Nielson; Hanne R. Nielson; Chris Hankin (2004-12-10). Principles of Program Analysis (1999 (corrected 2004) ed.). Springer. ISBN 978-3-540-65410-0.
• "Abstract interpretation and static analysis," International Winter School on Semantics and Applications 2003, by David A. Schmidt