Static program analysis: Difference between revisions

Revision as of 21:05, 13 October 2020

Revision as of 05:03, 11 December 2020

Line 1:

{{Software development process}}

'''Static program analysis''' is the [[program analysis (computer science)|analysis of computer software]] that is performed without actually executing programs, in contrast with [[dynamic program analysis|dynamic analysis]], which is analysis performed on programs while they are executing.<ref>{{cite journal |archiveurlarchive-url=https://web.archive.org/web/20110927010304/http://www.ida.liu.se/~TDDC90/papers/industrial95.pdf |archivedatearchive-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|last=Egele|first=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|issn=0360-0300}}</ref> In most cases the analysis is performed on some version of the [[source code]], and in the other cases, some form of the [[object code]].

The term is usually applied to the analysis performed by an [[List of tools for static code analysis|automated tool]], with human analysis being called program understanding, [[program comprehension]], or [[code review]]. [[Software inspection]]s and [[software walkthrough]]s are also used in the latter case.

Line 12:

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 = live |archive-url = https://web.archive.org/web/20100901084658/https://www.fda.gov/MedicalDevices/ProductsandMedicalProcedures/GeneralHospitalDevicesandSupplies/InfusionPumps/ucm202511.htm |archive-date = 2010-09-01 |df = }}</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>

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 | df= }}</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 http://ieeexplore.ieee.org/ielx5/5581168/5581493/05581551.pdf</ref>

Line 24:

== Tool types==

The OMG ([[Object Management Group]]) published a study regarding the types of software analysis required for [[software quality]] measurement and assessment. This document on "How to Deliver Resilient, Secure, Efficient, and Easily Changed IT Systems in Line with CISQ Recommendations" describes three levels of software analysis.<ref>{{cite web |url=http://www.omg.org/CISQ_compliant_IT_Systemsv.4-3.pdf |title=Archived copy |access-date=2013-10-18 |url-status=live |archive-url=https://web.archive.org/web/20131228132152/http://www.omg.org/CISQ_compliant_IT_Systemsv.4-3.pdf |archive-date=2013-12-28 |df= }}</ref>

; Unit Level: Analysis that takes place within a specific program or subroutine, without connecting to the context of that program.

Line 41:

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 [[decision problem|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 [[Alonzo Church|Church]], [[Kurt Gödel|Gödel]] and [[Alan Turing|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:<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|df=}}</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 behaviours 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> The [[Frama-C]] value analysis plugin and [[Polyspace]] heavily rely on abstract interpretation.

* [[Data flow analysis|Data-flow analysis]], a lattice-based technique for gathering information about the possible set of values;