Static program analysis: Difference between revisions

Content deleted Content added
Whoops.
GreenC bot (talk | contribs)
 
(24 intermediate revisions by 18 users not shown)
Line 1:
{{Short description|Establishing propertiesAnalysis of computer programs without executing them}}
{{Software development process}}
In [[computer science]], '''static program analysis''' (oralso known as '''static analysis''' or '''static simulation''') is the [[program analysis|analysis]] of computer programs performed without executing them, in contrast with [[dynamic program analysis]], which is performed on programs during their execution in the integrated environment.<ref>{{cite journal |archive-url=https://web.archive.org/web/20110927010304/http://www.ida.liu.se/~TDDC90/papers/industrial95.pdf |archive-date=2011-09-27 | title=Industrial Perspective on Static Analysis. |journal=Software Engineering Journal |date=Mar 1995 |pages=69–75 |last1=Wichmann |first1=B. A. |first2=A. A. |last2=Canning |first3=D. L. |last3=Clutterbuck |first4=L. A. |last4=Winsbarrow |first5=N. J. |last5=Ward |first6=D. W. R. |last6=Marsh |volume=10 |issue=2 |doi=10.1049/sej.1995.0010 |url=http://www.ida.liu.se/~TDDC90/papers/industrial95.pdf}}</ref><ref>{{Cite journal|last1=Egele|first1=Manuel|last2=Scholte|first2=Theodoor|last3=Kirda|first3=Engin|last4=Kruegel|first4=Christopher|date=2008-03-05|title=A survey on automated dynamic malware-analysis techniques and tools|url=https://doi.org/10.1145/2089125.2089126|journal=ACM Computing Surveys|volume=44|issue=2|pages=6:1–6:42|doi=10.1145/2089125.2089126| s2cid=1863333 |issn=0360-0300|url-access=subscription}}</ref>
 
The term is usually applied to analysis performed by an automated tool, with human analysis typically being called "program understanding", [[program comprehension]], or [[code review]]. In the last of these, [[software inspection]] and [[software walkthrough]]s are also used. In most cases the analysis is performed on some version of a program's [[source code]], and, in other cases, on some form of its [[object code]].
 
== Rationale ==
The sophistication of the analysis performed by tools varies from those that only consider the behaviorbehaviour of individual statements and declarations,<ref>{{Cite journal|last1=Khatiwada|first1=Saket|last2=Tushev|first2=Miroslav|last3=Mahmoud|first3=Anas|date=2018-01-01|title=Just enough semantics: An information theoretic approach for IR-based software bug localization|url=https://linkinghub.elsevier.com/retrieve/pii/S0950584916302269|journal=Information and Software Technology|language=en|volume=93|pages=45–57|doi=10.1016/j.infsof.2017.08.012|url-access=subscription}}</ref> to those that include the complete [[source code]] of a program in their analysis. The uses of the information obtained from the analysis vary from highlighting possible coding errors (e.g., the [[lint programming tool|lint]] tool) to [[formal methods]] that mathematically prove properties about a given program (e.g., its behaviorbehaviour matches that of its specification).
 
[[Software metric]]s and [[reverse engineering]] can be described as forms of static analysis. Deriving software metrics and static analysis are increasingly deployed together, especially in creation of embedded systems, by defining so-called ''software quality objectives''.<ref>[http://web1.see.asso.fr/erts2010/Site/0ANDGY78/Fichier/PAPIERS%20ERTS%202010/ERTS2010_0035_final.pdf "Software Quality Objectives for Source Code"] {{webarchive|url=https://web.archive.org/web/20150604203133/http://web1.see.asso.fr/erts2010/Site/0ANDGY78/Fichier/PAPIERS%20ERTS%202010/ERTS2010_0035_final.pdf |date=2015-06-04 }} (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.</ref>
Line 13:
locating potentially [[Vulnerability (computing)|vulnerable]] code.<ref>[http://research.microsoft.com/en-us/um/people/livshits/papers/pdf/thesis.pdf ''Improving Software Security with Precise Static and Runtime Analysis''] {{webarchive|url=https://web.archive.org/web/20110605125310/http://research.microsoft.com/en-us/um/people/livshits/papers/pdf/thesis.pdf |date=2011-06-05 }} (PDF), Benjamin Livshits, section 7.3 "Static Techniques for Security". Stanford doctoral thesis, 2006.</ref> For example, the following industries have identified the use of static code analysis as a means of improving the quality of increasingly sophisticated and complex software:
 
# [[Medical software]]: The US [[Food and Drug Administration]] (FDA) has identified the use of static analysis for medical devices.<ref>{{cite web |title = Infusion Pump Software Safety Research at FDA |author = FDA |publisher = Food and Drug Administration |date = 2010-09-08 |url = https://www.fda.gov/MedicalDevices/ProductsandMedicalProcedures/GeneralHospitalDevicesandSupplies/InfusionPumps/ucm202511.htm |access-date = 2010-09-09 |url-status = livedead |archive-url = https://web.archive.org/web/20100901084658/https://www.fda.gov/MedicalDevices/ProductsandMedicalProcedures/GeneralHospitalDevicesandSupplies/InfusionPumps/ucm202511.htm |archive-date = 2010-09-01 }}</ref>
# Nuclear software: In the UK the Office for Nuclear Regulation (ONR) recommends the use of static analysis on [[reactor protection system]]s.<ref>Computer based safety systems - technical guidance for assessing software aspects of digital computer based protection systems, {{cite web | title = Computer based safety systems | url=http://www.hse.gov.uk/nuclear/operational/tech_asst_guides/tast046.pdf | archive-url=http://webarchive.nationalarchives.gov.uk/20130104193206/http://www.hse.gov.uk/nuclear/operational/tech_asst_guides/tast046.pdf | url-status=dead | archive-date=January 4, 2013 |access-date=May 15, 2013 }}</ref>
# Aviation software (in combination with [[Dynamic program analysis|dynamic analysis]]).<ref>[http://www.faa.gov/aircraft/air_cert/design_approvals/air_software/cast/cast_papers/media/cast-9.pdf Position Paper CAST-9. Considerations for Evaluating Safety Engineering Approaches to Software Assurance] {{webarchive|url=https://web.archive.org/web/20131006134233/http://www.faa.gov/aircraft/air_cert/design_approvals/air_software/cast/cast_papers/media/cast-9.pdf |date=2013-10-06 }} // FAA, Certification Authorities Software Team (CAST), January, 2002: "Verification. A combination of both static and dynamic analyses should be specified by the applicant/developer and applied to the software."</ref>
# Automotive & Machines (Functionalfunctional safety features form an integral part of each automotive product development phase, [[ISO 26262]], Secsection 8.).
 
A study in 2012 by VDC Research reported that 28.7% of the embedded software engineers surveyed currently use static analysis tools and 39.7% expect to use them within 2 years.<ref>
{{cite web | title=Automated Defect Prevention for Embedded Software Quality | last=VDC Research | publisher=VDC Research | date=2012-02-01 | url=http://alm.parasoft.com/embedded-software-vdc-report/ | access-date=2012-04-10 | url-status=live | archive-url=https://web.archive.org/web/20120411211422/http://alm.parasoft.com/embedded-software-vdc-report/ | archive-date=2012-04-11 }}</ref>
A study from 2010 found that 60% of the interviewed developers in European research projects made at least use of their basic IDE built-in static analyzers. However, only about 10% employed an additional other (and perhaps more advanced) analysis tool.<ref>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 httphttps://ieeexplore.ieee.org/ielx5Xplore/5581168/5581493/05581551login.jsp?url=%2Fielx5%2F5581168%2F5581493%2F05581551.pdf&authDecision=-203</ref>
 
In the application security industry the name [[Staticstatic application security testing]] (SAST) is also used. SAST is an important part of [[Security Development LifecyclesLifecycle]]s (SDLs) such as the SDL defined by Microsoft<ref>M. Howard and S. Lipner. The Security Development Lifecycle: SDL: A Process for Developing Demonstrably More Secure Software. Microsoft Press, 2006. {{ISBN|978-0735622142}}</ref> and a common practice in software companies.<ref>Achim D. Brucker and Uwe Sodan. [https://www.brucker.ch/bibliography/download/2014/brucker.ea-sast-expierences-2014.pdf Deploying Static Application Security Testing on a Large Scale] {{webarchive|url=https://web.archive.org/web/20141021065105/http://www.brucker.ch/bibliography/download/2014/brucker.ea-sast-expierences-2014.pdf |date=2014-10-21 }}. In GI Sicherheit 2014. Lecture Notes in Informatics, 228, pages 91-101, GI, 2014. </ref>
 
== Tool types==
Line 29:
 
; Unit Level: Analysis that takes place within a specific program or subroutine, without connecting to the context of that program.
; Technology Level: Analysis that takes into account interactions between unit programs to get a more holistic and semantic view of the overall program in order to find issues and avoid obvious false positives. For instance, it is possible to statically analyze the Android technology stack to find permission errors.<ref>{{cite journal |last1=Bartel |first1=Alexandre |last2=Klein |first2=Jacques |last3=Monperrus |first3=Martin |last4=Le Traon |first4=Yves |title=Static Analysis for Extracting Permission Checks of a Large Scale Framework: The Challenges and Solutions for Analyzing Android |journal=IEEE Transactions on Software Engineering |date=1 June 2014 |volume=40 |issue=6 |pages=617–632 |doi=10.1109/tse.2014.2322867 |url=https://hal.archives-ouvertes.fr/hal-01055656/document|arxiv=1408.3976 |s2cid=6563188 }}</ref>
; System Level: 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.
Line 44:
 
Some of the implementation techniques of formal static analysis include:<ref>{{cite web|title=A Survey of Automated Techniques for Formal Software Verification|author=Vijay D’Silva|publisher=Transactions On CAD|date=2008|url=http://www.kroening.com/papers/tcad-sw-2008.pdf|access-date=2015-05-11|display-authors=etal|url-status=live|archive-url=https://web.archive.org/web/20160304074248/http://www.kroening.com/papers/tcad-sw-2008.pdf|archive-date=2016-03-04}}</ref>
* [[Abstract interpretation]], to model the effect that every statement has on the state of an abstract machine (i.e., it 'executes' the software based on the mathematical properties of each statement and declaration). This abstract machine over-approximates the behaviorsbehaviours of the system: the abstract system is thus made simpler to analyze, at the expense of ''incompleteness'' (not every property true of the original system is true of the abstract system). If properly done, though, abstract interpretation is ''sound'' (every property true of the abstract system can be mapped to a true property of the original system).<ref>{{cite web | title=A Formal Methods-based verification approach to medical device software analysis |last=Jones |first=Paul |publisher=Embedded Systems Design |date=2010-02-09 |url=http://embeddeddsp.embedded.com/design/opensource/222700533 |access-date=2010-09-09 |url-status=dead |archive-url=https://web.archive.org/web/20110710185427/http://embeddeddsp.embedded.com/design/opensource/222700533 |archive-date=July 10, 2011 }}</ref>
* [[Data flow analysis|Data-flow analysis]], a lattice-based technique for gathering information about the possible set of values;
* [[Hoare logic]], a [[formal system]] with a set of logical rules for reasoning rigorously about the [[correctness of computer programs]]. There is tool support for some programming languages (e.g., the [[SPARK programming language]] (a subset of [[Ada (programming language)|Ada]]) and the [[Java Modeling Language]]—JML—using [[ESC/Java]] and [[ESC/Java2]], Frama-C WP ([[weakest precondition]]) plugin for the C language extended with ACSL ([[ANSI/ISO C Specification Language]]) ).
* [[Model checking]], considers systems that have [[finite-state machine|finite state]] or may be reduced to finite state by [[abstraction (computer science)|abstraction]];
* [[Symbolic execution]], as used to derive mathematical expressions representing the value of mutated variables at particular points in the code.
* [[Nullable]] reference analysis
 
== Data-driven static analysis ==
 
Data-driven static analysis usesleverages largeextensive amounts of codecodebases to infer coding rules and improve the accuracy of the analysis.<ref name="dewes">{{cite web |title=Learning from other's mistakes: Data-driven code analysis. |url=https://www.slideshare.net/japh44/talk-handout-46938511 |website=www.slideshare.net |date=13 April 2015 |language=en}}</ref><ref>{{BetterCite sourcebook |last1=Söderberg |first1=Emma |last2=Church |first2=Luke |last3=Höst |first3=Martin |chapter=Open Data-driven Usability Improvements of Static Code Analysis and its Challenges needed|date=September2021-06-21 2020|title=Evaluation and Assessment in Software Engineering |chapter-url=https://doi.org/10.1145/3463274.3463808 |series=EASE '21 |___location=New York, NY, USA |publisher=Association for Computing Machinery |pages=272–277 |doi=10.1145/3463274.3463808 |isbn=978-1-4503-9053-8}}</ref> For instance, one can use all Java open-source packages available on [[GitHub]] to learn a good analysis strategystrategies. The rule inference can use machine learning techniques.<ref name="OhYang2015">{{cite book|last1=Oh|first1=Hakjoo|title=Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications - OOPSLA 2015|last2=Yang|first2=Hongseok|last3=Yi|first3=Kwangkeun|chapter=Learning a strategy for adapting a program analysis via bayesian optimisation|year=2015|pages=572–588|doi=10.1145/2814270.2814309|isbn=9781450336895|s2cid=13940725|url=https://ora.ox.ac.uk/objects/uuid:f656bcfd-ec1b-477c-9185-ff2c7490a207}}</ref> For instance, it has been shown that when one deviates too much in the way one uses an object-oriented API, it is likely to be a bug.<ref name="MonperrusMezini2013">{{cite journal|last1=Monperrus|first1=Martin|last2=Mezini|first2=Mira|title=Detecting missing method calls as violations of the majority rule|journal=ACM Transactions on Software Engineering and Methodology|volume=22|issue=1|year=2013|pages=1–25|url=https://hal.archives-ouvertes.fr/hal-00702196/document|doi=10.1145/2430536.2430541|arxiv=1306.0762|s2cid=1212778}}</ref> It is also possible to learn from a large amount of past fixes and warnings.<ref name="dewes"/>{{Better source needed|date=September 2020}}
 
== Remediation ==
 
Static analyzers produce warnings. For certain types of warnings, it is possible to design and implement [[Automatic bug fixing|automated remediation]] techniques. For example, Logozzo and Ball have proposed automated remediations for C# ''cccheck''.<ref>{{Cite journal |lastlast1=Logozzo |firstfirst1=Francesco |last2=Ball |first2=Thomas |date=2012-11-15 |title=Modular and verified automatic program repair |url=http://dx.doi.org/10.1145/2398857.2384626 |journal=ACM SIGPLAN Notices |volume=47 |issue=10 |pages=133–146 |doi=10.1145/2398857.2384626 |issn=0362-1340}}</ref> and Etemadi and colleagues use program transformation to automatically fix [[SonarQube]]'s warnings.<ref>{{Cite journal |last=Etemadi Someoliayi |first=Khashayar |last2=Harrand |first2=Nicolas Yves Maurice |last3=Larsen |first3=Simon |last4=Adzemovic |first4=Haris |last5=Luong Phu |first5=Henry |last6=Verma |first6=Ashutosh |last7=Madeiral |first7=Fernanda |last8=Wikstrom |first8=Douglas |last9=Monperrus |first9=Martin |date=2022 |title=Sorald: Automatic Patch Suggestions for SonarQube Static Analysis Violations |url-access=https://ieeexplore.ieee.org/document/9756950/subscription |journal=IEEE Transactions on Dependable and Secure Computing |pages=1–1 |doi=10.1109/TDSC.2022.3167316 |issn=1545-5971}}</ref>
 
 
== See also ==
Line 70:
* [[Lint (software)]]
* [[List of tools for static code analysis]]
* [[Shape analysis (softwareprogram analysis)|Shape analysis]]
* [[Software quality]]
* [[Software quality assurance]]
* [[SonarQube]]
}}
 
Line 83 ⟶ 84:
* {{cite book |author1=Flemming Nielson |author2=Hanne R. Nielson |author3=Chris Hankin |edition = 1999 (corrected 2004) |title = Principles of Program Analysis |publisher= Springer |isbn = 978-3-540-65410-0|date=2004-12-10 }}
* [http://santos.cis.ksu.edu/schmidt/Escuela03/home.html "Abstract interpretation and static analysis,"] International Winter School on Semantics and Applications 2003, by [http://people.cis.ksu.edu/~schmidt/ David A. Schmidt]
{{Program analysis}}
 
[[Category:Static program analysis| ]]
[[Category:Program analysis]]
[[Category:Software engineering]]