请输入您要查询的百科知识：

　

词条 Static program analysis
释义

  1. Rationale

  2. Tool types

  3. Formal methods

  4. Data-driven static analysis

  5. See also

  6. References

  7. Further reading

  8. External links

{{Software development process}}

Static program analysis is the analysis of computer software that is performed without actually executing programs, in contrast with dynamic analysis, which is analysis performed on programs while they are executing.[1] 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 automated tool, with human analysis being called program understanding, program comprehension, or code review. Software inspections and software walkthroughs are also used in the latter case.

Rationale

The sophistication of the analysis performed by tools varies from those that only consider the behaviour of individual statements and declarations, 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 tool) to formal methods that mathematically prove properties about a given program (e.g., its behaviour matches that of its specification).

Software metrics 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.[2]

A growing commercial use of static analysis is in the verification of properties of software used in safety-critical computer systems and

locating potentially vulnerable code.[3] 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:

  1. Medical software: The U.S. Food and Drug Administration (FDA) has identified the use of static analysis for medical devices.&91;4&93;
  2. Nuclear software: In the UK the Office for Nuclear Regulation (ONR) recommends the use of static analysis on reactor protection systems.&91;5&93;
  3. Aviation software (in combination with dynamic analysis)&91;6&93;

A study in 2012 by VDC Research reports that 28.7% of the embedded software engineers surveyed currently use static analysis tools and 39.7% expect to use them within 2 years.[7]

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.[8]

In the application security industry the name Static Application Security Testing (SAST) is also used. SAST is an important part of Security Development Lifecycles (SDLs) such as the SDL defined by Microsoft [9] and a common practice in software companies.[10]

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.[11]

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.[12]
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.

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.

Formal methods

{{main|Formal methods}}

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:[13]

  • 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).[14] The Frama-C value analysis plugin and Polyspace heavily rely on abstract interpretation.
  • 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) 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 or may be reduced to finite state by abstraction;
  • Symbolic execution, as used to derive mathematical expressions representing the value of mutated variables at particular points in the code.

Data-driven static analysis

Data-driven static analysis uses large amounts of code to infer coding rules.[15] For instance, one can use all Java open-source packages on GitHub to learn a good analysis strategy. The rule inference can use machine learning techniques.[16] 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.[17] It is also possible to learn from a large amount of past fixes and warnings.[15]

See also

{{Portal|Software Testing}}
  • Code audit
  • Documentation generator
  • Formal semantics of programming languages
  • Formal verification
  • List of tools for static code analysis
  • Shape analysis (software)

References

1. ^{{cite journal |archiveurl=https://web.archive.org/web/20110927010304/http://www.ida.liu.se/~TDDC90/papers/industrial95.pdf |archivedate=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 |url=http://www.ida.liu.se/~TDDC90/papers/industrial95.pdf}}
2. ^"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.
3. ^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.
4. ^{{cite web |title = Infusion Pump Software Safety Research at FDA |author = FDA |publisher = Food and Drug Administration |date = 2010-09-08 |url = http://www.fda.gov/MedicalDevices/ProductsandMedicalProcedures/GeneralHospitalDevicesandSupplies/InfusionPumps/ucm202511.htm |accessdate = 2010-09-09 |deadurl = no |archiveurl = https://web.archive.org/web/20100901084658/http://www.fda.gov/MedicalDevices/ProductsandMedicalProcedures/GeneralHospitalDevicesandSupplies/InfusionPumps/ucm202511.htm |archivedate = 2010-09-01 |df = }}
5. ^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 | dead-url=yes | archive-date=January 4, 2013 |accessdate=May 15, 2013 }}
6. ^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."
7. ^{{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/ | accessdate=2012-04-10 | deadurl=no | archiveurl=https://web.archive.org/web/20120411211422/http://alm.parasoft.com/embedded-software-vdc-report/ | archivedate=2012-04-11 | df= }}
8. ^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
9. ^M. Howard and S. Lipner. The Security Development Lifecycle: SDL: A Process for Developing Demonstrably More Secure Software. Microsoft Press, 2006. {{ISBN|978-0735622142}}
10. ^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. {{cite web |url=https://www.brucker.ch/bibliography/download/2014/brucker.ea-sast-expierences-2014.pdf |title=Archived copy |accessdate=2015-05-20 |deadurl=no |archiveurl=https://web.archive.org/web/20141021065105/http://www.brucker.ch/bibliography/download/2014/brucker.ea-sast-expierences-2014.pdf |archivedate=2014-10-21 |df= }}
11. ^{{cite web |url=http://www.omg.org/CISQ_compliant_IT_Systemsv.4-3.pdf |title=Archived copy |accessdate=2013-10-18 |deadurl=no |archiveurl=https://web.archive.org/web/20131228132152/http://www.omg.org/CISQ_compliant_IT_Systemsv.4-3.pdf |archivedate=2013-12-28 |df= }}
12. ^{{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 }}
13. ^{{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|accessdate=2015-05-11|display-authors=etal|deadurl=no|archiveurl=https://web.archive.org/web/20160304074248/http://www.kroening.com/papers/tcad-sw-2008.pdf|archivedate=2016-03-04|df=}}
14. ^{{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 |accessdate=2010-09-09 |deadurl=yes |archiveurl=https://web.archive.org/web/20110710185427/http://embeddeddsp.embedded.com/design/opensource/222700533 |archivedate=July 10, 2011 }}
15. ^1 {{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 |language=en}}
16. ^{{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}}
17. ^{{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}}

Further reading

  • Syllabus and readings for Alex Aiken’s Stanford CS295 course.
  • {{cite journal |last1 = Ayewah |first1 = Nathaniel |last2 = Hovemeyer |first2 = David |last3 = Morgenthaler |first3 = J. David |last4 = Penix |first4 = John |last5 = Pugh |first5 = William |year = 2008 |title = Using Static Analysis to Find Bugs |journal = IEEE Software |volume = 25 |issue = 5 |pages = 22–29 |doi = 10.1109/MS.2008.130 |citeseerx = 10.1.1.187.8985 }}
  • {{cite book |author = Brian Chess, Jacob West (Fortify Software) | title= Secure Programming with Static Analysis | publisher= Addison-Wesley |year = 2007 |isbn = 978-0-321-42477-8}}
  • {{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 }}
  • "Abstract interpretation and static analysis," International Winter School on Semantics and Applications 2003, by David A. Schmidt

External links

  • Code Quality Improvement - Coding standards conformance checking (DDJ)
  • [https://sv-comp.sosy-lab.org Competition on Software Verification (SV-COMP)]
  • Episode 59: Static Code Analysis Interview (Podcast) at Software Engineering Radio
  • [https://www.infoq.com/articles/governance-coding-standards Implementing Automated Governance for Coding Standards] Explains why and how to integrate static code analysis into the build process
  • Integrate static analysis into a software development process
  • [https://samate.nist.gov The SAMATE Project], a resource for Automated Static Analysis tools
{{portal|Software testing}}

5 : Program analysis|Software review|Software testing|Static program analysis|Quality assurance
随便看

　

开放百科全书收录14589846条英语、德语、日语等多语种百科知识，基本涵盖了大多数领域的百科知识，是一部内容自由、开放的电子版国际百科全书。

　

Copyright © 2023 OENC.NET All Rights Reserved
京ICP备2021023879号 更新时间：2024/11/12 10:12:55