In computer science, program analysis is the process of automatically analyzing the behavior of computer programs regarding a property such as correctness, robustness, safety and liveness. Program analysis focuses on two major areas: program optimization and program correctness. The first focuses on improving the program’s performance while reducing the resource usage while the latter focuses on ensuring that the program does what It is supposed to do.
Static program analysis
Static analysis can discover vulnerabilities during the development phase of the program. These vulnerabilities are easier to correct than the ones found during the testing phase since static analysis leads to the root of the vulnerability. Due to static analysis being computationally undecidable, the mechanism are either too permissive or incomplete. Despite their limitations the first might reduce the number of vulnerabilities while the second can give strong assurance of the lack of vulnerabilities.
The purpose of Control-flow analysis is to obtain information about which functions can be called at various points during the execution of a program. The collected information is represented by a control flow graph (CFG) where the nodes are instructions of the program and the edges represent the flow of control. By identifying code blocks and loops CFG becomes a starting point for compiler made optimizations.
Data-flow analysis is a technique designed to gather information about the values at each point of the program and how they change over time. This technique is often used by compilers to optimize the code. One of the most known examples of the technique is Taint checking which consists on considering all variables which have user supplied data tainted (unsecured) and preventing those variables from being used until they are sanitized. This technique is often used to prevent SQL injection attacks.
Abstract interpretation allows to extract information about a possible execution of a program without actually executing the program. This information can be used by compilers to look for possible optimizations or for certifying a program against certain classes of bugs.
Type systems associate types to programs that fulfill certain requirements. Their purpose is to select a subset of programs of a language that are considered correct according to a property.
- Type checking – verify whether the program is accepted by the type system.
- Type inference – to infer the type that allows a type system to accept a program.
Type checking is used in programming to limit how a programming object is used and what can they do. This is done by the compiler or interpreter. Type checking can also help preventing vulnerabilities by ensuring that a signed value isn't attributed to an unsigned variable. Type checking can be done statically (at compile time), dynamically (at runtime) or a combination of both.
Effect systems is a formal system designed to study the effects executing a program can have. An effect comprises what is being done and with what it is being done, usually referred to as effect kind and region.
Model checking refers to the problem of finding a strict, formal and automated way to check if a given model complies with the given specification. Due to the finite state nature of the system and both the model and the system being expressed by a logic formulas, it is possible to check if the system violates the specification using efficient algorithmic methods.
Dynamic program analysis
Dynamic analysis can use runtime knowledge of the program to increase the precision of the analysis while also providing runtime protection but can only analyze a single execution of the problem and might degrade the program’s performance due to runtime checks.
Software should be tested to ensure its quality and that it performs as it is supposed to in a reliable manner, and that won’t create conflicts with other software that may function alongside it. The tests are performed by executing the program with an input and evaluating its behavior and the produced output. Even if no security requirements are specified, additional security testing should be performed to ensure that an attacker can’t tamper with the software and steal information, disrupt the software’s normal operations or use it as a pivot to attack its users.
Program monitoring records and logs different kinds of information about the program such as resource usage, events and interaction so it can be reviewed to find abnormal behavior or even pinpoint what caused the abnormal behavior. Furthermore it can be used to perform security audits. Automated monitoring of programs is sometimes referred to as Runtime verification.
For a given subset of a program’s behavior, program slicing consists of reducing the program to the minimum form that still produces the selected behavior. The reduced program is called a “slice” and is a faithful representation of the original program within the domain of the specified behavior subset. Generally, finding a slice is an unsolvable problem, but by specifying the target behavior subset by the values of a set of variables, it is possible to obtain approximate slices using a data-flow algorithm. These slices are usually used by developers during debugging to locate the source of errors.
- Hiralal Agrawal, Joseph R. Horgan, "Dynamic program slicing"
- Wang Chunlei, Zhao Gang, Dai Yiqi, "An Efficient Control Flow Security Analysis Approach for Binary Executables"
- Flemming Nielson, Hanne Riis Nielson, Chris Hankin (2005). "Principles of Program Analysis". Springer.