A survey of static analysis methods for identifying security vulnerabilities in software systems <s> Analysis techniques for information flow <s> ertification mechanism for verifying the secure flow of information through a program. Because it exploits the properties of a lattice structure among security classes, the procedure is sufficiently simple that it can easily be included in the analysis phase of most existing compilers. Appropriate semantics are presented and proved correct. An important application is the confinement problem: The mechanism can prove that a program cannot cause supposedly nonconfidential results to depend on confidential input data. <s> BIB001 </s> A survey of static analysis methods for identifying security vulnerabilities in software systems <s> Analysis techniques for information flow <s> We assune that the reader is familiar with the ubiquity of information in the modern world and is sympathetic with the need for restricting rights to read, add, modify, or delete information in specific contexts. This need is particularly acute for systems having computers as significant components. <s> BIB002 </s> A survey of static analysis methods for identifying security vulnerabilities in software systems <s> Analysis techniques for information flow <s> Ensuring secure information flow within programs in the context of multiple sensitivity levels has been widely studied. Especially noteworthy is Denning’s work in secure flow analysis and the lattice model [6][7]. Until now, however, the soundness of Denning’s analysis has not been established satisfactorily. We formulate Denning’s approach as a type system and present a notion of soundness for the system that can be viewed as a form of noninterference. Soundness is established by proving, with respect to a standard programming language semantics, that all well-typed programs have this noninterference property. <s> BIB003 </s> A survey of static analysis methods for identifying security vulnerabilities in software systems <s> Analysis techniques for information flow <s> We present a new system for automatically detecting format string security vulnerabilities in C programs using a constraint-based type-inference engine. We describe new techniques for presenting the results of such an analysis to the user in a form that makes bugs easier to find and to fix. The system has been implemented and tested on several real-world software packages. Our tests show that the system is very effective, detecting several bugs previously unknown to the authors and exhibiting a low rate of false positives in almost all cases. Many of our techniques are applicable to additional classes of security vulnerabilities, as well as other type- and constraint-based systems. <s> BIB004
While the accurate detection of information flow is undecidable,  static analysis can be used to overapproximate information flows in a program in order to ensure information-flow security. In this section, we present a survey of algorithms for checking information-flow security. The basic idea behind using static analysis for detecting information flow is to statically check that flow of information between variables in a program is consistent with the security labeling of variables. Each variable is labeled with a certain security level. If a variable x is used to derive, or influence, the value of another variable y, there is potential information flow from x to y. The flow is permissible under a security policy only if the policy allows the security level of x to flow to the security level of y. Formally, let (S, ) be a lattice of security levels. For security levels a and b, a b means that it is allowed for information of level a to flow into level b. If the lattice is modeling confidentiality, then a is no more secret than b; if the lattice is modeling integrity, then a is at least as trusted as b. We denote the security level of a variable x by dom(x). There exists an explicit flow from x to y if the value of x is assigned to y in the program, as in y :¼ x. There is an implicit flow from x to y if the value of x is used to evaluate the outcome of a conditional, which then controls an assignment to y, as in if (x . 0) then y :¼ 1 else y :¼ 0 endif. We denote an explicit or implicit flow from x to y as x ) y. Denning and Denning's certification of programs for secure information flow BIB001 uses the following proposition: A program respects the security policy implied by the lattice (S, ) when, for any flow x ) y, it must be the case that dom(x) dom(y). To enforce a program's information-flow security, this property, which defines a sufficient but not necessary condition, must be verified for each flow in the program. Goguen and Meseguer BIB002 have given a more general notion of information-flow security based on noninterference. Informally, the non-interference principle says that an observer must not be able to see variation in ''low-security'' outputs that is derived from variation in ''high-security'' inputs (so the observer cannot make any inference on highsecurity information). Suppose a computation undergoes the following transition between input and output states: (H 1 , L 1 ) ! (H 2 , L 2 ), where H 1 and H 2 are high-security components and L 1 and L 2 are low-security components of the states. For this computation to be secure, it must be the case that for any other value of high-security component, the low-security output does not change: ðH Remember that the interpretation of the terms ''high security'' and ''low security'' depends on the problem being solved: for confidentiality, higher and lower security mean more and less secret; for integrity, they mean less and more trusted, respectively. For example, let h be a secret variable and l be a public variable. Then the program input h; if (h . 0) then l :¼ 1 else l :¼ 0 endif; output l violates non-interference, because different initial values of high input h can result in different final values of the low output l. Formally, let w S 3 S be an interference relation on security levels. If a w b, the security level a is allowed to interfere with the security level b, in the sense that it can impact observable values in level b. Generally, we are interested in the complement of this relation, a 6 w b; which prohibits a from interfering with b. Note that w must be reflexive, but in general it need not be transitive. While Goguen and Meseguer presented non-interference in a more abstract setting of ''actions,'' our presentation here is limited to program statements. We label each input or output statement x by its security level dom(x) (generalizing dom to apply to statements). The security level of an input statement is the security level of the input value being provided to the computation. The security level of an output statement is the security level of the variable being made visible external to the computation. Let run be the state update function State 3 Statement ! State. Let purge be a function that, given a trace of statements a, removes from it all such statements x whose security level must not interfere with a given security level t; it is defined as follows: purge(x Á a, t) :¼ x Á purge(a, t) if dom(x) w t, and purge(x Á a, t) :¼ purge(a, t) otherwise. Let s 0 be the initial state of the program. Then, the security criterion can be stated as follows: A program respects the security policy implied by a non-interference relation 6 w if for any sequence of statements a in an execution ending in a statement z: outputðrunðs 0 ; aÞ; zÞ ¼ outputðrunðs 0 ; purgeða; domðzÞÞÞ; zÞ That is, the output produced at statement z must be identical even if all such previous statements have been purged whose security level must not interfere with the security level of z. In the previous example, on any run in which input h is purged (and the default value of h, assumed 0, is in effect), the output is 0 for l; whereas a nonpurged run with input value of 1 or higher would produce the output of 1 for l. For sake of contrast, consider a slightly modified example: input h; if (h . 0) then l :¼ 1 else l :¼ 0 endif; l :¼ 2; output l. In this example, even if the statement input h is purged from any run, the output for l is 2, which is the same as for any nonpurged run, and so the conditions for noninterference are satisfied. Non-interference is a more general criterion than our first criterion of secure information flow, in that it only constrains the projection of outputs produced from actual statement sequences; it does not constrain implicit or explicit flow at each statement. Note that Denning and Denning's criterion would have rejected the modified example above because an implicit flow violating the security-lattice rule does exist. Volpano, et al. BIB003 have shown a type-based algorithm that certifies implicit and explicit flows similarly to the first criterion and also ensures non-interference. Non-interference is traditionally the technical criterion used for proving correctness of security analysis algorithms or type systems. However, it is also harder to check non-interference directly. Secure In Java and CLR, information flow issues are particularly relevant with privilege-asserting code. Privilege-asserting code has historic roots in the 1970s. The Digital Equipment Corporation (DEC) Virtual Address eXtension/Virtual Memory System (VAX/VMS) operating system had a feature similar to the doPrivileged method in Java 2 and the Assert method in CLR. The VAX/VMS feature was called privileged images. Privileged images were similar to UNIX setuid programs,  except that privileged images ran in the same process as all the user's other unprivileged programs. Thus, they were considerably easier to attack than UNIX setuid programs because they lacked the usual separate process and separate address-space protections. One example of an attack on privileged images is demonstrated in a paper by Koegel, Koegel, Li, and Miruke.  The notion of tainted variables as vehicles for integrity violations became known with the Perl language. In Perl, using the ÀT option allows detecting tainted variables.  Shankar, Talwar, Foster, and Wagner present a tainted-variable analysis for CQual using constraint graphs. BIB004 To find format string bugs, CQual uses a type-qualifier system with two qualifiers: tainted and untainted.