23.5 Gupta and Gligor's Theory of Penetration Analysis

Gupta and Gligor [428] developed a formal analysis technique arising from failure to perform adequate checks. This is not a vulnerabilities model, because it presupposes classification—that is, the vulnerabilities that their technique detects are asserted to be vulnerabilities arising from failure to perform adequate checks. As a scheme for classifying flaws, this obviously is not adequate. As a method for detecting previously undetected flaws of the designated class, it is very elegant. We present this model here because it is an excellent example of the use of a classification scheme.

Gupta and Gligor make two hypotheses.

Hypothesis of Penetration Patterns. "[S]ystem flaws that cause a large class of penetration patterns can be identified in system (i.e., TCB) source code as incorrect/absent condition checks or integrated flows that violate the intentions of the system designers."^[1]

^[1] See [428], p. 67.

If true, this hypothesis implies that an appropriate set of design and implementation principles would prevent vulnerabilities. This leads to the next hypothesis:

Hypothesis of Penetration-Resistant Systems. "[A] system (i.e., TCB) is largely resistant to penetration if it adheres to a specific set of design properties."^[2]

^[2] See [428], p. 67.

Gupta and Gligor select and formalize several properties, and from those properties derive checks to determine if the system correctly obeys them.

• System isolation or tamperproofness, which states that users must not be able to tamper with the system. This encompasses parameter checking at the system boundary, separation of user and system addresses, and allowing entry to the system only at well-defined gates at which parameters and privileges can be validated.

• System noncircumventability, which states that the system must check all references to objects.

• Consistency of global objects belonging to the system, with respect to both timing and storage.

• Elimination of undesirable system and user dependencies, which usually refers to prevention of denial-of-service attacks.

For modeling purposes, Gupta and Gligor focus on the consistency principle and set as their policy that accesses to system entities and functions were allowed only if the conditions for access were validated atomically.

23.5.1 The Flow-Based Model of Penetration Analysis

Gupta and Gligor's model focuses on the flow of control during the validation of parameters. Consider the system function rmdir [429]. It takes a single parameter. When invoked, it allocates space for a copy of the parameter on the stack and copies that parameter into the allocated storage. Thus, control flows through three steps: the allocation of storage, the binding of the parameter with the formal argument, and the copying of the formal argument (parameter) to the storage. The failure to check the length of the parameter is the flaw.

The model represents the system as a sequence of states and state transitions. The abstract cell set C = { c₁, …, c_n } is the set of system entities that holds information. The system function set F = { f₁, …, f_x } is the set of all system functions that the user may invoke; those involving time delays (such as sleep and pause) are also in the set Z F. The system condition set R = { r₁, …, r_m } is the set of all parameter checks. The information flow set is the set of all possible information flows between pairs of abstract cells and is represented as IF = C x C, where each (c_i, c_j) means that information flows from c_i to c_j. Similarly, the call relationship between system functions is denoted by SF = F x F, where each (f_i, f_j) means that f_i calls f_j or f_i returns to f_j. The latter two sets capture the flow of information and control throughout the system.

System-critical functions are functions that the analysts deem critical with respect to penetration; examples include functions that cause time delays (because this may allow a window during which checked parameters are changed) and functions that can cause the system to crash. These functions are represented by the set K = { k₁, …, k_s }. System entry points are the gates through which user processes invoke system functions; they are represented by the set E = { e₁, …, e_t }.

EXAMPLE: Consider the rmdir function. Figure 23-11 shows the flow of control and information. fname points to a global entity and therefore is a member of C. rmdir is a system function and thus is in F; it is also an entry point and thus is in E. The parameter fname cannot be an illegal address, and the string it points to must be smaller than the space allocated to buf. This means that the predicates islegal(fname) and length(fname) < spacefor(buf) are in R. We deem strcpy to be a system-critical function because it does not check destination bounds or source addresses, so strcpy is in K. Because information flows from fname to buf, the tuple (fname, buf) IF, and because the rmdir function calls strcpy, (rmdir, strcpy) SF. Figure 23-11. The integrated flow path for the rmdir system function in one version of the UNIX operating system. From [429], Figure 11(a), p. 178.

The alter set AC = { (c₁, R₁), … (c_n, R_n), }, where R_i R, is the set of abstract cells that can be altered and the conditions that must be validated first. The predicate Element(c_i, R_i) means that the conditions in R_i must be checked before c_i is viewed or altered. The view set VC = { (c₁, R'₁), … (c_n, R'_n), }, where R'_i R, is the set of abstract cells that can be viewed and the conditions that must be validated first. The critical function set KF = { (k₁, R''₁), … (k_s, R''_s) } and the entry point set EF = { (e₁, R'"₁), … (e_t, R'"_t) } are defined analogously.

EXAMPLE: Before strcpy views fname, it must validate the address as legal, and before strcpy alters buf, it must validate the size of fname as being small enough. Thus, (strcpy, islegal(fname) length(fname) < spacefor(buf)) KF.

The model defines three functions for capturing the history of transitions. Each triple in the altered cells set ACS = { (c₁, e₁, pathcond₁), …, } means that c_i has been altered by invoking entry point e_i, and pathcond_i IF SF R is the sequence (ordered set) of information flows, function flows, and conditions along the path. The viewed cells set VCS = { (c₁, e₁ , pathcond'₁), …, } and the critical functions invoked set KFS = { (k₁, e₁, pathcond"₁), …, } are defined analogously. The triplet (ACS, VCS, KFS) makes up the state of the system.

A state is said to be penetration-resistant if it meets the following three requirements.

These requirements define a state invariant SI. Intuitively, SI says that if the system function checks all conditions on the global variables and parameters to be altered (requirement 1) or viewed (requirement 2), and all conditions on the system-critical functions (requirement 3), then the system cannot be penetrated using a technique that exploits a failure to check the conditions. Part (a) of each requirement requires checking of conditions on entry. Part (b) requires checking of conditions on the memory locations or system-critical functions. Part (c) requires checking of changes in previously checked parameters as a result of a time delay caused by a function.

State transition rules control the updating of information as the system changes. If t is a state transition function and S = (ACS, VCS, KFS) is the current state, then t(S) = S' = (ACS', VCS', KFS'). In this model, t is alter_cell, view_cell, or invoke_crit_func.

The function alter_cell(c, e, p) checks that c C, e E, and p IF SF R and that requirement 1 holds. If so, ACS' = ACS { (c, e, p) }, VCS' = VCS, and KFS' = KFS. If not, the function has attempted to move the system into a state that is not penetration-resistant.

The function view_cell(c, e, p) checks that c C, e E, and p IF SF R, and that requirement 2 holds. If so, ACS' = ACS, VCS' = VCS { (c, e, p) }, and KFS' = KFS. If not, the function has attempted to move the system into a state that is not penetration-resistant.

Finally, the function invoke_crit_func(k, e, p) checks that k K, e E, and p IF SF R and that requirement 3 holds. If so, ACS' = ACS, VCS' = VCS, and KFS' = KFS { (f, e, p) }. If not, the function has attempted to move the system into a state that is not penetration-resistant.

Theorem 23–1. Let the system be in a state V that satisfies the state invariant SI. Then, if a state transition function is applied to V, the resulting state V' will also satisfy SI.

EXAMPLE: Consider the rmdir function, and assume that the system is in a penetration-resistant state. The call to strcpy is a state transition in which a system-critical function is invoked, so the tuple is (strcpy, rmdir, p), where p is the sequence of conditions, information flows, and function invocations so far. The invoke_crit_func function tells us that requirement 3 must hold. Because there is no condition associated with the entry point rmdir, 3a holds. However, requirement 3b does not hold: the conditions for strcpy, { islegal(fname) length(fname) < spacefor(buf) } p because they have not been checked within the TCB. After the rmdir system call, the system is no longer in a penetration-resistant state. The specific attack on this system call is to give it an argument sufficiently long to overflow buf and alter the stack, much as the fingerd bug in Section 23.3.1 did.

23.5.2 The Automated Penetration Analysis Tool

Gupta and Gligor designed and implemented an automated penetration analysis (APA) tool that performed this testing. The primitive flow generator reduces C statements to Prolog facts recording data and control flow information, condition statements, and sequencing information. Two other modules, the information flow integrator and the function flow integrator, integrate execution paths derived from the primitive flow statements to show pertinent flows of information, flows of control among functions, and how the conditions affect the execution paths. The condition set consistency prover analyzes conditions along an execution path and reports inconsistencies. Finally, the flaw detection module applies the Hypothesis of Penetration Patterns by determining whether the conditions for each entry point conform to penetration-resistant specifications.

23.5.3 Discussion

The Gupta-Gligor theory presents a formalization of one of the classes of vulnerabilities—specifically, inconsistent and incomplete parameter validation (possibly combined with improper change). The formalization builds preconditions for executing system functions; the APA tool verifies that these preconditions hold (or determines that they do not).

Whether or not this technique can be generalized to other classes of flaws is an open question. In particular, the technique is extremely sensitive to the level of detail at which the system is analyzed and to the quality of the specifications describing the policy. This work is best seen as a foundation on which future automation of penetration analysis may build and a reinforcement of the idea that automated tools can aid an analyst in uncovering system vulnerabilities.

Could the theory be generalized to classify vulnerabilities? The model assumes an existing classification scheme (specifically, improper or inadequate checks) and describes a technique and a tool for detecting vulnerabilities of this class. Were the purpose of the model to classify vulnerabilities (rather than to detect them), basing classification on the nature of the tools that detect them is tautological and a single vulnerability could fall into several classes depending on how the tool was crafted. Hence, such an (inverted) application of the Gupta-Gligor approach would suffer from the same flaws that plague the other classification schemes. However, the purpose of the model is to detect, not to classify, vulnerabilities of one specific type.