A survey of static analysis methods for identifying security vulnerabilities in software systems <s> INFORMATION FLOW <s> This paper investigates mechanisms that guarantee secure information flow in a computer system. These mechanisms are examined within a mathematical framework suitable for formulating the requirements of secure information flow among security classes. The central component of the model is a lattice structure derived from the security classes and justified by the semantics of information flow. The lattice properties permit concise formulations of the security requirements of different existing systems and facilitate the construction of mechanisms that enforce security. The model provides a unifying view of all systems that restrict information flow, enables a classification of them according to security objectives, and suggests some new approaches. It also leads to the construction of automatic program certification mechanisms for verifying the secure flow of information through a program. <s> BIB001 </s> A survey of static analysis methods for identifying security vulnerabilities in software systems <s> 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> BIB002 </s> A survey of static analysis methods for identifying security vulnerabilities in software systems <s> INFORMATION FLOW <s> I First Concepts.- 1 Two Definitions of Lattices.- 2 How to Describe Lattices.- 3 Some Algebraic Concepts.- 4 Polynomials, Identities, and Inequalities.- 5 Free Lattices.- 6 Special Elements.- Further Topics and References.- Problems.- II Distributive Lattices.- 1 Characterization and Representation Theorems.- 2 Polynomials and Freeness.- 3 Congruence Relations.- 4 Boolean Algebras.- 5 Topological Representation.- 6 Pseudocomplementation.- Further Topics and References.- Problems.- III Congruences and Ideals.- 1 Weak Projectivity and Congruences.- 2 Distributive, Standard, and Neutral Elements.- 3 Distributive, Standard, and Neutral Ideals.- 4 Structure Theorems.- Further Topics and References.- Problems.- IV Modular and Semimodular Lattices.- 1 Modular Lattices.- 2 Semimodular Lattices.- 3 Geometric Lattices.- 4 Partition Lattices.- 5 Complemented Modular Lattices.- Further Topics and References.- Problems.- V Varieties of Lattices.- 1 Characterizations of Varieties.- 2 The Lattice of Varieties of Lattices.- 3 Finding Equational Bases.- 4 The Amalgamation Property.- Further Topics and References.- Problems.- VI Free Products.- 1 Free Products of Lattices.- 2 The Structure of Free Lattices.- 3 Reduced Free Products.- 4 Hopfian Lattices.- Further Topics and References.- Problems.- Concluding Remarks.- Table of Notation.- A Retrospective.- 1 Major Advances.- 2 Notes on Chapter I.- 3 Notes on Chapter II.- 4 Notes on Chapter III.- 5 Notes on Chapter IV.- 6 Notes on Chapter V.- 7 Notes on Chapter VI.- 8 Lattices and Universal Algebras.- B Distributive Lattices and Duality by B. Davey, II. Priestley.- 1 Introduction.- 2 Basic Duality.- 3 Distributive Lattices with Additional Operations.- 4 Distributive Lattices with V-preserving Operators, and Beyond.- 5 The Natural Perspective.- 6 Congruence Properties.- 7 Freeness, Coproducts, and Injectivity.- C Congruence Lattices by G. Gratzer, E. T. Schmidt.- 1 The Finite Case.- 2 The General Case.- 3 Complete Congruences.- D Continuous Geometry by F. Wehrung.- 1 The von Neumann Coordinatization Theorem.- 2 Continuous Geometries and Related Topics.- E Projective Lattice Geometries by M. Greferath, S. Schmidt.- 1 Background.- 2 A Unified Approach to Lattice Geometry.- 3 Residuated Maps.- F Varieties of Lattices by P. Jipsen, H. Rose.- 1 The Lattice A.- 2 Generating Sets of Varieties.- 3 Equational Bases.- 4 Amalgamation and Absolute Retracts.- 5 Congruence Varieties.- G Free Lattices by R. Frecse.- 1 Whitman's Solutions Basic Results.- 2 Classical Results.- 3 Covers in Free Lattices.- 4 Semisingular Elements and Tschantz's Theorem.- 5 Applications and Related Areas.- H Formal Concept Analysis by B. Cantor and R. Wille.- 1 Formal Contexts and Concept Lattices.- 2 Applications.- 3 Sublattices and Quotient Lattices.- 4 Subdirect Products and Tensor Products.- 5 Lattice Properties.- New Bibliography. <s> BIB003 </s> A survey of static analysis methods for identifying security vulnerabilities in software systems <s> 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> BIB004
In this section we discuss techniques that identify information-flow vulnerabilities in software systems and focus on integrity and confidentiality as the two main types of vulnerabilities. We discuss the research work to date in this area and describe in more detail some recent contributions. The data manipulated by a program can be tagged with security levels, BIB002 which naturally assume the structure of a partially ordered set. Under certain conditions, this partially ordered set is a lattice. BIB001 BIB003 In the simplest example, this lattice only contains two elements, indicated with high and low. Given a program, the principle of non-interference dictates that low-security behavior of the program not be affected by any high-security data. BIB004 Assuming that high means confidential and low means public, then verifying that no information ever flows from higher to lower security levels (unless that information has previously been declassified) is equivalent to verifying confidentiality. Conversely, if high means untrusted and low means trusted, then verifying that no information ever flows from higher to lower security levels (unless that information has previously been endorsed) is equivalent to verifying integrity. Vulnerabilities such as those caused by nonvalidated input and injection flaws constitute integrity violations. Globally, declassification and endorsement are also known as downgrading because they allow high-level security information to be used in low-level security contexts.