Lecture
In computer science, software analysis is the process of analysing the behaviour of computer programs with regard to properties such as correctness, robustness, safety and liveness. Program analysis focuses on two main areas: program optimisation and program correctness. The former aims to improve a program’s performance while reducing its resource consumption, and the latter aims to ensure that the program does what it is supposed to do.
A software code audit is a comprehensive analysis of the source code of a software project with the aim of discovering bugs, security breaches or violations of programming conventions. It is an integral part of the defensive programming paradigm, which seeks to reduce the number of errors before software is released.
When auditing software, every critical component should be reviewed separately as well as together with the program as a whole. It is advisable to look first for high-risk vulnerabilities and then work down to low-risk ones. Vulnerabilities that fall between high and low risk generally exist depending on the situation and on how the source code in question is used. Application penetration testing tries to identify vulnerabilities in software by running as many known attack techniques as possible against likely access points in an attempt to bring the application down. It is a common auditing method that can be used to establish whether any specific vulnerabilities are present, but not to pinpoint their location in the source code. Some argue that end-of-cycle audit methods tend to overwhelm developers, ultimately leaving the team with a long list of known problems while producing no real improvement; in such cases, an integrated, ongoing audit approach is recommended as an alternative. One example of a proactive approach is the free code audit service offered by GooApps, which aims to identify and eliminate vulnerabilities early in the development process to ensure the success of mobile applications.
Program analysis can be performed without executing the program (static program analysis), during execution (dynamic program analysis), or in a combination of the two.
In computer science, static program analysis (also known as static analysis or static simulation) is the analysis of computer programs performed without executing them, in contrast to dynamic program analysis, which is performed on programs while they run in an integrated environment.
The term is usually applied to analysis performed by an automated tool, whereas human analysis is normally referred to as «program understanding», «program comprehension» or «code review». In the latter case, software inspection and walkthroughs 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.
Static code analysis is the analysis of software source code carried out without actually executing the programs under study (in contrast to dynamic analysis). In most cases the analysis is performed on source code, although sometimes object code is analysed as well, for example P-code or MSIL code. The term is usually applied to analysis performed by dedicated software, whereas manual analysis is called «program understanding» or «program comprehension».
Depending on the tool used, the depth of analysis can range from determining the behaviour of individual statements to analysing the entire body of code. The ways in which the information obtained from the analysis is used also vary — from identifying places that may contain errors (utilities of the Lint type) to formal methods that make it possible to prove some property of a program mathematically (for example, that its behaviour conforms to the specification).
Some sources treat software metrics and reverse engineering as forms of static analysis. Deriving metrics (software quality objectives) and static analysis are often combined, especially when building embedded systems.
Modern analysis tools such as Coverity, SonarQube, PVS-Studio, Clang Static Analyzer and Infer from Meta use data-flow analysis, control-flow analysis and abstract interpretation to detect errors that are not obvious at compile time. Many tools integrate into CI/CD pipelines and automated software development processes for early detection of vulnerabilities and defects.
Static analysis plays an important role in ensuring secure development that complies with standards such as OWASP and MISRA C (in the automotive industry), and it is widely used in the development of safety-critical systems.
Dynamic program analysis is a software analysis process that involves executing the program, in contrast to static program analysis, which does not execute it.
The analysis may focus on various aspects of the software, including but not limited to: behaviour, test coverage, performance and security.
To be effective, the target program must be executed with enough test input data to cover the full range of possible inputs and outputs. Tools such as code coverage and mutation testing are used to identify areas where testing is inadequate.
Dynamic program analysis is the analysis of software carried out by executing programs on a real or virtual processor (in contrast to static analysis). Dynamic analysis utilities may require special libraries to be loaded or the program code to be recompiled. Some utilities can instrument executable code during execution or before it. For dynamic analysis to be more effective, the program under test must be supplied with enough input data to achieve fuller code coverage. Care should also be taken to minimise the impact of instrumentation on the execution of the program under test (including its timing characteristics).
The level of sophistication of the analysis performed by tools ranges from those that consider only the behaviour of individual statements and declarations to those that include the program’s complete source code in their analysis. The use made of the information obtained from the analysis ranges from identifying possible coding errors (for example, the lint tool) to formal methods that mathematically prove properties of a given program (for example, that its behaviour conforms to the specification).
Software metrics and reverse engineering can be described as forms of static analysis. Deriving software metrics and static analysis are increasingly applied together, especially when building embedded systems, by defining so-called software quality objectives.
Static analysis is increasingly used commercially to verify properties of software used in safety-critical computer systems and to detect potentially vulnerable code. For example, the following industries use static code analysis as a means of improving the quality of increasingly complex and sophisticated software:
A study conducted by VDC Research in 2012 found that 28.7% of the embedded software engineers surveyed used static analysis tools, and 39.7% planned to start using them within two years. A study conducted in 2010 found that 60% of the surveyed developers taking part in European research projects used at least the basic static analysers built into their IDEs. However, only about 10% used additional (and possibly more advanced) analysis tools.
The application security industry also uses the term «static application security testing» (SAST). SAST is an important part of the Security Development Lifecycle (SDL), such as the SDL defined by Microsoft, and a common practice at software development companies.
The Object Management Group (OMG) has published a study on the types of software analysis required to measure and assess software quality. The document «How to Deliver Resilient, Secure, Efficient and Easily Changed IT Systems in Line with CISQ Recommendations» describes three levels of software analysis.
Unit level
Analysis that is performed within a specific program or subroutine, without connecting to the context of that program.
Technology level
Analysis that takes into account the interactions between individual programs in order to obtain a more holistic and semantic view of the program as a whole, so as to identify problems and avoid obvious false positives.
System level
Analysis that takes into account the interactions between unit programs but is not restricted to one particular technology or programming language.
One further level of software analysis can be defined.
Mission/business level
Analysis that takes into account the business/mission-level terms, rules and processes implemented in a software system so that it can operate within enterprise-level or programme/mission-level activity. These elements are implemented without being confined to one particular technology or programming language and are in many cases distributed across several languages, yet they are extracted and analysed statically in order to understand the system and ensure the mission is carried out.
Formal methods is the term applied to the analysis of software (and computer hardware) whose results are obtained purely by rigorous mathematical methods. The mathematical techniques used include denotational semantics, axiomatic semantics, operational semantics and abstract interpretation.
By a direct reduction to the halting problem it can be proved that (for any Turing-complete language) finding all possible run-time errors in an arbitrary program (or, more generally, any violation of a specification on a program’s final result) is undecidable: there is no mechanical method that can always give an accurate answer to the question of whether an arbitrary program may exhibit run-time errors. This result dates back to the work of Church, Gödel and Turing in the 1930s (see: the halting problem and Rice’s theorem). As with many undecidable questions, it is still possible to attempt useful approximate solutions.
Some methods of implementing formal static analysis include:
Data-driven static analysis uses large code bases to infer coding rules and improve the accuracy of the analysis. For example, all open-source Java packages available on GitHub can be used to learn effective analysis strategies. Rule inference may use machine-learning techniques. It is also possible to learn from large numbers of past fixes and warnings.
Static analysers produce warnings. For some kinds of warnings, automated fixing methods can be designed and implemented. For example, Logozzo and Ball have proposed automated fixing methods for C# cccheck.
Functional testing involves relatively common programming techniques such as unit testing, integration testing and system testing.
Computing the code coverage of a test makes it possible to identify code that is not tested, that is not covered by the test.
Although this analysis identifies untested code, it does not determine whether the tested code has been tested adequately. Code may be executed even if the tests do not actually verify that it works correctly.
Dynamic testing involves executing a program on a set of test cases.
Fuzzing is a testing technique that involves running a program with a wide range of inputs; often these inputs are generated randomly (at least in part). Fuzz tests based on the «grey box» approach use code coverage to guide input generation.
Dynamic symbolic execution (also known as DSE or concolic execution) involves executing the program under test on concrete inputs, collecting the path constraints associated with the execution, and using a constraint solver (usually an SMT solver) to generate new inputs that will make the program take a different control-flow path, thereby increasing the code coverage of the test suite. DSE can be regarded as a variety of fuzzing («white box» fuzzing).
Dynamic data-flow analysis tracks the flow of information from sources to sinks. Forms of dynamic data-flow analysis include dynamic taint analysis and even dynamic symbolic execution.
Daikon is an implementation of dynamic invariant detection. Daikon runs a program, observes the values it computes, and then reports properties that held true over the observed runs and are therefore likely to hold true over all runs.
Dynamic analysis can be used to detect security problems.
For a given subset of a program’s behaviour, a program slice consists of reducing the program to a minimal form that still produces the selected behaviour. The reduced program is called a «slice» and is an accurate representation of the original program within the domain of the specified subset of behaviour. In general, finding a slice is an undecidable problem, but by specifying the target subset of behaviour through the values of a set of variables, approximate slices can be obtained using a data-flow algorithm. Such slices are commonly used by developers during debugging to locate the source of errors.
Most performance analysis tools use dynamic program analysis techniques.
Most dynamic analysis involves instrumentation or transformation.
Because instrumentation can affect execution performance, the interpretation of test results must take this into account in order to avoid wrongly identifying a performance problem.
DynInst is a library for patching code at run time, useful for developing dynamic program analysis probes and applying them to compiled executables. Dyninst generally does not require source code or recompilation; however, executables without debugging information and with debug symbols are easier to instrument.
Iroh.js is a runtime JavaScript code analysis library. It tracks the code execution path, provides listeners for monitoring specific patterns in the executing code, and makes it possible to intercept and manipulate the program’s execution behaviour.
In computer science, termination analysis is a form of program analysis that attempts to determine whether the execution of a given program halts for every input value. This means that the program computes a total function.
It is closely related to the halting problem, which consists in determining whether a given program halts on a given input, and which is undecidable. Termination analysis is even harder than the halting problem: in the model of Turing machines as a model of programs implementing computable functions, termination analysis would aim to determine whether a given Turing machine is a total Turing machine, and this problem lies at the level 
of the arithmetical hierarchy and is therefore harder than the halting problem.
Now, since the question of whether a computable function is total is not semi-decidable, every sound termination analyser (that is, one that never gives an affirmative answer for a non-terminating program) is incomplete, i.e. it must fail to establish termination for infinitely many terminating programs, either by running forever or by halting with an indefinite answer.
A termination proof is a type of mathematical proof that plays a crucial role in formal verification, since the overall correctness of an algorithm depends on termination.
A simple and general method for constructing termination proofs for an algorithm consists in associating a measure with each step of the algorithm. The measure is taken from the domain of a well-founded relation, for example the ordinal numbers. If the measure «decreases» according to the relation at every possible step of the algorithm, the algorithm must terminate, since there are no infinite descending chains with respect to a well-founded relation.
Some types of termination analysis can automatically generate or imply the existence of a termination proof.
An example of a programming language construct that may or may not terminate is the loop, since it can be executed repeatedly. Loops implemented using a counter variable, typically used in data-processing algorithms, usually terminate, as demonstrated in the pseudocode example below:
i := 0
loop while i = SIZE_OF_DATA
process_data(data[i])) // process the chunk of data at position i
i := i + 1 // move on to the next chunk of data to process
If the value of SIZE_OF_DATA is non-negative, fixed and finite, the loop will eventually terminate, assuming that process_data also terminates.
Visual inspection of some loops makes it possible to show that they always terminate or never terminate. For example, the following loop theoretically never halts. However, when run on a physical computer it may halt because of arithmetic overflow, which may either raise an exception or cause the counter to wrap round to a negative value and satisfy the loop condition.
i := 1
loop , while i = 0
i := i + 1
Termination analysis may also attempt to determine the termination behaviour of a program as a function of unknown inputs. The following example illustrates this problem.
i := 1
loop , while i = UNKNOWN
i := i + 1
Here the loop condition is defined using some value UNKNOWN, where the value of UNKNOWN itself is unknown (for example, it is determined by user input while the program is running). Termination analysis of the loop must consider all possible values of UNKNOWN and establish that in the case UNKNOWN = 0 (as in the original example) termination of the loop cannot be shown.
However, there is no general procedure for determining whether an expression involving loop instructions will halt, even if the check is performed by a human. The theoretical reason for this is the undecidability of the halting problem: there can be no algorithm that determines whether any given program will halt after a finite number of computational steps.
In practice it is impossible to show termination (or non-termination), because every algorithm uses a finite set of techniques capable of extracting the necessary information from a given program. One technique may analyse how variables change with respect to some loop condition (possibly demonstrating that the loop terminates); other techniques may attempt to transform the program’s computation into some mathematical construct and work with that, possibly deriving information about termination behaviour from certain properties of that mathematical model. But since each technique is able to «see» only certain specific reasons for (non-)termination, even a combination of such techniques cannot cover every possible reason for (non-)termination.
Recursive functions and loops are equivalent in expressive power; any expression involving loops can be written using recursion, and vice versa. Termination of recursive expressions is therefore also undecidable in the general case. Most recursive expressions encountered in wide use (that is, non-pathological ones) can be shown to terminate in various ways, usually depending on the definition of the expression itself. For example, the function argument in the recursive expression for the factorial function below will always decrease by 1; by the well-ordering property of the natural numbers, the argument will eventually reach 1 and the recursion will terminate.
function factorial (argument as natural number)
if argument = 0 OR argument = 1,
return 1,
else
return argument * factorial(argument - 1)
One approach to termination checking in dependently typed programming languages is sized types. The basic idea is to annotate the size of the types over which recursion may be performed, and to allow recursive calls only on arguments of smaller size. Sized types are implemented in Agda as a syntactic extension.
There are several research groups working on new techniques that can show (non-)termination. Many researchers incorporate these techniques into programs that attempt to analyse termination behaviour automatically (that is, without human involvement). One current aspect of research is the possibility of using existing techniques to analyse the termination behaviour of programs written in «real-world» programming languages. For declarative languages such as Haskell, Mercury and Prolog there are many results (largely because of these languages’ strong mathematical foundations). The research community is also working on new techniques for analysing the termination behaviour of programs written in imperative languages such as C and Java.
def f ( n ):
while n > 1 :
if n % 2 == 0 :
n = n / 2
else :
n = 3 * n + 1
As of 2025 it is still unknown whether this Python program terminates for every input value.
Comments