Static analysis - sagr4019/ResearchProject GitHub Wiki
Static analysis
Static code analysis is a software based test procedure during compile time. It performes formal tests on source code to detect errors before the software is executed. The goal is to disclose errors, not to emend errors. Static code analysis tools are rare and they cover a relatively small percentage of security errors. They are struggling with many false positives and some false negatives.
Methods
Generally there exists no option to find all possible run-time errors in a program. However there are methods which attempt to give useful approximate solutions.
- Abstract interpretation: Using soundness, trying to check that every statement has a state.
- Data-flow analysis: Technique to collect information about the possible set of values at certain points in the program.
- Hoare logic: Using a set of logical rules to show the correctness of programs.
- Model checking: A fully automatic (no user interaction needed) method to verify if a model meets a specification. The model could be a program, a finite state machine or a transition system. The specification is a formal property of the system. As soon as the model meets the specification, the algorithm stops and outputs a certificate of correctness.
- Symbolic execution: Trying to find which inputs cause a part of a program to execute
- Taint analysis: Trying to find variables that are "tainted" with user inputs and traces those variables to find possible vulnerable functions.
Problems that has been solved (more or less)
The lists below contain different tasks that has been solved (more or less) by some static analysis tools.