En informàtica, l'anàlisi estàtica de programes (també coneguda com a anàlisi estàtica o simulació estàtica) és l'anàlisi de programes informàtics realitzada sense executar-los, a diferència de l'anàlisi dinàmica de programes, que es realitza sobre programes durant la seva execució en l'entorn integrat.
El terme s'aplica normalment a l'anàlisi realitzada per una eina automatitzada, i l'anàlisi humana s'anomena normalment "comprensió del programa", comprensió del programa o revisió de codi. En l'últim d'aquests, també s'utilitza la inspecció de programari i les revisions de programari. En la majoria dels casos, l'anàlisi es realitza sobre alguna versió del codi font d'un programa i, en altres casos, sobre alguna forma del seu codi objecte.
Dos enfocaments destacats per a la certificació de recursos són l'anàlisi estàtica (SA) i la complexitat computacional implícita (ICC). L'SA és de naturalesa algorísmica: se centra en un llenguatge de programació determinat i pretén determinar, mitjançant mètodes sintàctics, si certs programes escrits en aquest llenguatge són viables. En canvi, l'ICC intenta crear des del principi llenguatges de programació o mètodes especialitzats que delimiten una classe de complexitat. Així doncs, l'SA se centra en la fase de compilació i no imposa requisits al programador, mentre que l'ICC és una disciplina de disseny de llenguatges.
— D. Leivant (2020)
La disciplina de l'anàlisi estàtica no s'ha de confondre amb el linting, que és el procés de comprovació d'errors d'estil de codificació.
Raonament La sofisticació de l'anàlisi realitzada per les eines varia des de les que només consideren el comportament de les sentències i declaracions individuals, fins a les que inclouen el codi font complet d'un programa en la seva anàlisi. Els usos de la informació obtinguda de l'anàlisi varien des de destacar possibles errors de codificació (per exemple, l'eina lint) fins a mètodes formals que demostren matemàticament propietats sobre un programa determinat (per exemple, que el seu comportament coincideixi amb el de la seva especificació).
Les mètriques de programari i l'enginyeria inversa es poden descriure com a formes d'anàlisi estàtica. La derivació de mètriques de programari i l'anàlisi estàtica s'implementen cada cop més conjuntament, especialment en la creació de sistemes integrats, mitjançant la definició dels anomenats objectius de qualitat de programari."Software Quality Objectives for Source Code" (PDF). Proceedings: Embedded Real Time Software and Systems 2010 Conference, ERTS2010.org, Toulouse, France: Patrick Briand, Martin Brochet, Thierry Cambois, Emmanuel Coutenceau, Olivier Guetta, Daniel Mainberte, Frederic Mondot, Patrick Munier, Loic Noury, Philippe Spozio, Frederic Retailleau.
Un ús comercial creixent de l'anàlisi estàtica és en la verificació de les propietats del programari utilitzat en sistemes informàtics crítics per a la seguretat i la localització de codi potencialment vulnerable.Improving Software Security with Precise Static and Runtime Analysis (PDF), Benjamin Livshits, section 7.3 "Static Techniques for Security". Stanford doctoral thesis, 2006. Per exemple, les següents indústries han identificat l'ús de l'anàlisi estàtica de codi com un mitjà per millorar la qualitat d'un programari cada cop més sofisticat i complex:
Insereix un paràgraf
Programari mèdic: L'Administració d'Aliments i Medicaments dels EUA (FDA) ha identificat l'ús de l'anàlisi estàtica per a dispositius mèdics. Programari nuclear: Al Regne Unit, l'Oficina de Regulació Nuclear (ONR) recomana l'ús d'anàlisi estàtica en sistemes de protecció de reactors. Programari d'aviació (en combinació amb anàlisi dinàmica). Automoció i màquines (les característiques de seguretat funcional formen part integral de cada fase de desenvolupament de productes d'automoció, ISO 26262, secció 8).
Un estudi del 2012 de VDC Research va informar que el 28,7% dels enginyers de programari integrat enquestats utilitzen eines d'anàlisi estàtica i el 39,7% espera utilitzar-les en els propers 2 anys. Un estudi del 2010 va trobar que el 60% dels desenvolupadors entrevistats en projectes de recerca europeus feien ús, com a mínim, dels analitzadors estàtics integrats al seu IDE bàsic. No obstant això, només al voltant del 10% va emprar una altra eina d'anàlisi addicional (i potser més avançada).Prause, Christian R., René Reiners, and Silviya Dencheva. "Empirical study of tool support in highly distributed research projects." Global Software Engineering (ICGSE), 2010 5th IEEE International Conference on. IEEE, 2010 https://ieeexplore.ieee.org/Xplore/login.jsp?url=%2Fielx5%2F5581168%2F5581493%2F05581551.pdf&authDecision=-203
En la indústria de la seguretat d'aplicacions també s'utilitza el nom de proves de seguretat d'aplicacions estàtiques (SAST). SAST és una part important dels cicles de vida del desenvolupament de seguretat (SDL), com ara l'SDL definit per Microsoft,M. Howard and S. Lipner. The Security Development Lifecycle: SDL: A Process for Developing Demonstrably More Secure Software. Microsoft Press, 2006. i una pràctica habitual a les empreses de programari.Achim D. Brucker and Uwe Sodan. Deploying Static Application Security Testing on a Large Scale . In GI Sicherheit 2014. Lecture Notes in Informatics, 228, pages 91-101, GI, 2014.
Tipus d'eines L'OMG (Object Management Group) va publicar un estudi sobre els tipus d'anàlisi de programari necessaris per a la mesura i l'avaluació de la qualitat del programari. Aquest document sobre "Com oferir sistemes informàtics resilients, segurs, eficients i fàcilment modificables d'acord amb les recomanacions del CISQ" descriu tres nivells d'anàlisi de programari.
Insereix un paràgraf
Nivell d'unitat Anàlisi que té lloc dins d'un programa o subrutina específic, sense connectar-se al context d'aquest programa. Nivell tecnològic Anàlisi que té en compte les interaccions entre els programes unitaris per obtenir una visió més holística i semàntica del programa en general per tal de trobar problemes i evitar falsos positius evidents. Nivell de sistema Anàlisi que té en compte les interaccions entre programes unitaris, però sense limitar-se a una tecnologia o llenguatge de programació específic.
Es pot definir un nivell addicional d'anàlisi de programari.
Missió/Nivell empresarial Anàlisi que té en compte els termes, les regles i els processos de la capa de negoci/missió que s'implementen dins del sistema de programari per al seu funcionament com a part de les activitats de l'empresa o de la capa de programa/missió. Aquests elements s'implementen sense estar limitats a una tecnologia o llenguatge de programació específic i, en molts casos, es distribueixen en múltiples llenguatges, però s'extreuen i s'analitzen estàticament per a la comprensió del sistema per assegurar la missió.
Moltes eines d'anàlisi estàtica utilitzen representacions intermèdies de programes per examinar l'estructura del codi font sense executar el programa. Per a aquest propòsit, s'utilitzen habitualment arbres de sintaxi abstracta (AST), ja que proporcionen una representació estructurada dels elements sintàctics d'un programa.
Mètodes formals Mètodes formals és el terme que s'aplica a l'anàlisi de programari (i maquinari informàtic) els resultats del qual s'obtenen únicament mitjançant l'ús de mètodes matemàtics rigorosos. Les tècniques matemàtiques utilitzades inclouen la semàntica denotacional, la semàntica axiomàtica, la semàntica operacional i la interpretació abstracta.
Mitjançant una reducció directa al problema de l'aturada, és possible demostrar que (per a qualsevol llenguatge de Turing complet ), trobar tots els possibles errors d'execució en un programa arbitrari (o més generalment qualsevol tipus de violació d'una especificació sobre el resultat final d'un programa) és indecidible : no hi ha cap mètode mecànic que pugui respondre sempre amb veracitat si un programa arbitrari pot o no presentar errors d'execució. Aquest resultat data dels treballs de Church, Gödel i Turing a la dècada del 1930 (vegeu: Problema de la parada i teorema de Rice). Com passa amb moltes preguntes indecidibles, encara es poden intentar donar solucions aproximades útils.
Algunes de les tècniques d'implementació de l'anàlisi estàtica formal inclouen:
Insereix un paràgraf
Interpretació abstracta, per modelar l'efecte que cada sentència té sobre l'estat d'una màquina abstracta (és a dir, "executa" el programari basant-se en les propietats matemàtiques de cada sentència i declaració). Aquesta màquina abstracta sobreaproxima els comportaments del sistema: així, el sistema abstracte es fa més senzill d'analitzar, a costa de la incompletesa (no totes les propietats certes del sistema original són certes del sistema abstracte). Si es fa correctament, però, la interpretació abstracta és sòlida (cada propietat certa del sistema abstracte es pot assignar a una propietat certa del sistema original). Anàlisi de flux de dades, una tècnica basada en xarxes per recopilar informació sobre el possible conjunt de valors; Lògica de Hoare, un sistema formal amb un conjunt de regles lògiques per raonar rigorosament sobre la correcció dels programes informàtics. Hi ha suport d'eines per a alguns llenguatges de programació (per exemple, el llenguatge de programació SPARK (un subconjunt d'Ada) i el llenguatge de modelatge Java —JML— utilitzant ESC/Java i ESC/Java2, el complement Frama-C WP (precondició més feble) per al llenguatge C ampliat amb ACSL (llenguatge d'especificació C ANSI/ISO)). La comprovació de models considera sistemes que tenen un estat finit o que es poden reduir a un estat finit per abstracció; Execució simbòlica, tal com s'utilitza per derivar expressions matemàtiques que representen el valor de variables mutades en punts particulars del codi. Anàlisi de referència nullable
Anàlisi estàtica basada en dades L'anàlisi estàtica basada en dades aprofita bases de codi extenses per inferir regles de codificació i millorar la precisió de l'anàlisi. Per exemple, es poden utilitzar tots els paquets de codi obert de Java disponibles a GitHub per aprendre bones estratègies d'anàlisi. La inferència de regles pot utilitzar tècniques d'aprenentatge automàtic. També és possible aprendre d'una gran quantitat de correccions i avisos anteriors.
Remediació Els analitzadors estàtics generen avisos. Per a certs tipus d'avisos, és possible dissenyar i implementar tècniques de remediació automatitzades. Per exemple, Logozzo i Ball han proposat solucions automatitzades per a C# cccheck.
Referències
Categoria:Programari Categoria:Llenguatges de programació