Análisis estático de software

Análisis estático de software es un tipo de análisis de software que se realiza sin ejecutar el programa (el análisis realizado sobre los programas en ejecución se conoce como análisis dinámico de software).^[1] En la mayoría de los casos, el análisis se realiza en alguna versión del código fuente y en otros casos se realiza en el código objeto. El término se aplica generalmente a los análisis realizados por una herramienta automática, el análisis realizado por un humano es llamado comprensión de programas (o entendimiento de programas) como también revisión de código.

Motivación

La sofisticación de los análisis realizados por las herramientas varía de aquellos que sólo tienen en cuenta el comportamiento de instrucciones y declaraciones individuales, a los que se incluye el código fuente completo de un programa en su análisis. Los usos de la información obtenida de un análisis varían desde indicar posibles errores de codificación hasta demostrar matemáticamente con métodos formales ciertas propiedades acerca de un programa dado (por ejemplo, que su comportamiento coincide con el de su especificación) dependiendo de que programa se utilice para el análisis.

Las métricas del software y la ingeniería inversa pueden ser descritas como forma de análisis estático de software. El análisis estático y las métricas del software se han comenzado a desarrollar a la par, sobre todo en sistemas embebidos donde se definen lo que se llama objetivos del software de calidad.^[2]

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

Software médico: La Administración de Alimentos y Medicamentos (FDA) de Estados Unidos ha identificado al análisis estático como un servicio médico.^[4]
Software nuclear: En el Reino Unido el Ejecutivo de Salud y Seguridad recomendó el uso de análisis estático para los sistemas de protección de reactores.^[5]

En 2012, un estudio de VDC Research informó que el 28,7% de los ingenieros de software de sistemas embebidos encuestados utilizaban herramientas de análisis estático y que un 39,7% esperaban utilizarlas próximamente.^[6]

Herramientas

Artículo principal: Anexo:Herramientas para el análisis estático de software

Métodos formales

Los métodos formales es un análisis de software (y hardware), cuyos resultados se obtienen exclusivamente mediante el uso de métodos matemáticos rigurosos. Las técnicas matemáticas utilizadas incluyen semántica formal, semántica axiomática, semántica operacional e interpretación abstracta.

Por una simplificación del problema de la parada es posible probar que (para cualquier lenguaje turing completo) encontrar todos los posibles errores en tiempo de ejecución de un programa arbitrario (o más generalmente, cualquier tipo de violación de especificación en el programa final) es indecidible: no existe un método mecánico que siempre pueda contestar con la verdad si un determinado programa puede o no tener errores de ejecución. Este resultado se remonta a los trabajos de Alonzo Church, Kurt Gödel y Alan Turing de 1930 (Problema de la parada y teorema de Rice). Al igual que con muchas cuestiones indecidibles, todavía se puede intentar dar soluciones útiles aproximados.

Algunas de las técnicas de análisis estático formal incluyen:

Model checking
Interpretación abstracta
Uso de aserciones en el código del programa, fue sugerido por la lógica de Hoare

Tipos de análisis estáticos

Véase también

Referencias

↑ Industrial Perspective on Static Analysis. Software Engineering Journal Mar. 1995: 69-75Wichmann, B. A., A. A. Canning, D. L. Clutterbuck, L. A. Winsbarrow, N. J. Ward, and D. W. R. Marsh. https://web.archive.org/web/20110927010304/http://www.ida.liu.se/~TDDC90/papers/industrial95.pdf
↑ Software Quality Objectives for Source Code. Proceedings Embedded Real Time Software and Systems 2010 Conference, ERTS2, Toulouse, France: Patrick Briand, Martin Brochet, Thierry Cambois, Emmanuel Coutenceau, Olivier Guetta, Daniel Mainberte, Frederic Mondot, Patrick Munier, Loic Noury, Philippe Spozio, Frederic Retailleau http://www.erts2010.org/Site/0ANDGY78/Fichier/PAPIERS%20ERTS%202010/ERTS2010_0035_final.pdf Archivado el 12 de marzo de 2012 en Wayback Machine.
↑ Improving Software Security with Precise Static and Runtime Analysis, Benjamin Livshits, section 7.3 "Static Techniques for Security," Stanford doctoral thesis, 2006. http://research.microsoft.com/en-us/um/people/livshits/papers/pdf/thesis.pdf
↑ FDA (8 de septiembre de 2010). «Infusion Pump Software Safety Research at FDA». Food and Drug Administration. Consultado el 9 de septiembre de 2010.
↑ Computer based safety systems - technical guidance for assessing software aspects of digital computer based protection systems, http://webarchive.nationalarchives.gov.uk/20080731135436/http://www.hse.gov.uk/foi/internalops/nsd/tech_asst_guides/tast046app1.htm
↑ VDC Research (1 de febrero de 2012). «Automated Defect Prevention for Embedded Software Quality». VDC Research. Consultado el 10 de abril de 2012.

Bibliografía

Syllabus and readings for Alex Aiken’s Stanford CS295 course.
Nathaniel Ayewah, David Hovemeyer, J. David Morgenthaler, John Penix, William Pugh, "Using Static Analysis to Find Bugs," IEEE Software, vol. 25, no. 5, pp. 22–29, Sep./Oct. 2008, doi 10.1109/MS.2008.130
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 (1999, corrected 2004). Principles of Program Analysis. Springer. ISBN 978-3-540-65410-0.
"Abstract interpretation and static analysis," International Winter School on Semantics and Applications 2003, by David A. Schmidt

Enlaces externos

The SAMATE Project
Integrate static analysis into a software development process (enlace roto disponible en Internet Archive; véase el historial, la primera versión y la última).
Code Quality Improvement - Coding standards conformance checking (DDJ)
Episode 59: Static Code Analysis entrevista (Podcast) en Software Engineering Radio
Implementing Automated Governance for Coding Standards
.NET Static Analysis (InfoQ)

Datos: Q1329550

[1] Industrial Perspective on Static Analysis. Software Engineering Journal Mar. 1995: 69-75Wichmann, B. A., A. A. Canning, D. L. Clutterbuck, L. A. Winsbarrow, N. J. Ward, and D. W. R. Marsh. https://web.archive.org/web/20110927010304/http://www.ida.liu.se/~TDDC90/papers/industrial95.pdf

[2] Software Quality Objectives for Source Code. Proceedings Embedded Real Time Software and Systems 2010 Conference, ERTS2, Toulouse, France: Patrick Briand, Martin Brochet, Thierry Cambois, Emmanuel Coutenceau, Olivier Guetta, Daniel Mainberte, Frederic Mondot, Patrick Munier, Loic Noury, Philippe Spozio, Frederic Retailleau http://www.erts2010.org/Site/0ANDGY78/Fichier/PAPIERS%20ERTS%202010/ERTS2010_0035_final.pdf Archivado el 12 de marzo de 2012 en Wayback Machine.

[3] Improving Software Security with Precise Static and Runtime Analysis, Benjamin Livshits, section 7.3 "Static Techniques for Security," Stanford doctoral thesis, 2006. http://research.microsoft.com/en-us/um/people/livshits/papers/pdf/thesis.pdf

[4] FDA (8 de septiembre de 2010). «Infusion Pump Software Safety Research at FDA». Food and Drug Administration. Consultado el 9 de septiembre de 2010.

[5] Computer based safety systems - technical guidance for assessing software aspects of digital computer based protection systems, http://webarchive.nationalarchives.gov.uk/20080731135436/http://www.hse.gov.uk/foi/internalops/nsd/tech_asst_guides/tast046app1.htm

[6] VDC Research (1 de febrero de 2012). «Automated Defect Prevention for Embedded Software Quality». VDC Research. Consultado el 10 de abril de 2012.

[1]

[2]

[3]

[4]

[5]

[6]