You are presented with multiple paper abstracts, alongside the associated literature review and chapter titles. Given the provided information, you are going to do a literature review. Please generate a coherent literature review that synthesizes the content, draws connections between different works, highlights major findings, and identifies any gaps in the existing research.

Literature Review Title: A survey of static analysis methods for identifying security vulnerabilities in software systems 
Chapter Title:  Figure 4 
1. Abstract of Cited Paper (BIB001):  A fundamental problem in software based security is whether local security checks inserted into the code are sufficient to implement a global security property. We introduce a formalism based on a two-level linear time temporal logic for specifying global security properties pertaining to the control flow of the program, and illustrate its expressive power with a number of existing properties. We define a minimalistic, security dedicated program model that only contains procedure call and run time security checks and propose an automatic method for verifying that an implementation using local security checks satisfies a global security property. For a given formula in the temporal logic, we prove that there exists a bound on the size of the states that have to be considered in order to assure the validity of the formula: this reduces the problem to finite state model checking. Finally, we instantiate the framework to the security architecture proposed for Java (JDK 1.2). 
2. Abstract of Cited Paper (BIB002):  Two implementations are given for Java's stack inspection access-control policy. Each implementation is obtained by generating an inlined reference monitor (IRM) for a different formulation of the policy. Performance of the implementations is evaluated, and one is found to be competitive with Java's less flexible, JVM-resident implementation. The exercise illustrates the power of the IRM approach for enforcing security policies. 
3. Abstract of Cited Paper (BIB003):  Abstract We propose two control flow analyses for the Java bytecode. They safely approximate the set of permissions granted/denied to code at run-time. This static information helps optimizing the implementation of the stack inspection algorithm.

Literature Review:
A role-based access control scenario BIB001 Each method is modified so that it passes a security token as part of each invocation. The token represents an encoding of the security state at each stack frame, as well as the result of any authorization test encountered. By running the application and encoding the security state, the SPS explores subgraphs of the comparable invocation graph and discovers the associated security states and authorizations. The goal of this work is to optimize authorization performance. Rather than maintaining the security and codeexecution subsystems separately, with distinct semantics and different implementations of pushdown stacks, the key intuition behind the SPS calculus is to add the security context as an additional, implicit argument to every method. With SPS, SBAC for a program is achieved by rewriting the program's bytecode before it is loaded, without any need for changing the Java virtual machine or bytecode semantics. Pottier, Skalka, and Smith 19 extend and formalize the SPS calculus via type theory using a k-calculus, called k sec . Jensen et al. BIB002 focus on proving that code is secure with respect to a global security policy. Their model uses operational semantics to prove the properties, using a two-level temporal logic, and shows how to detect redundant authorization tests. Bartoletti et al. are interested in optimizing the performance of runtime authorization testing by eliminating redundant tests and relocating others as needed. BIB004 The reported results apply operational semantics to model the runtime stack. Similarly, Banerjee and Naumann 22 apply denotational semantics to show the equivalence of eager and lazy semantics for stack inspection, provide a static analysis of safety (the absence of security errors), and identify transformations that can remove unnecessary authorization tests. A limitation of this approach is that the analyses are restricted to a single thread and require the whole program; incomplete-program analyses are not supported. Rather than analyzing security policies as embodied by existing code, Erlingsson and Schneider BIB003 describe a system that inlines reference monitors into the code to enforce specific security policies. The objective is to define a security policy and then inject authorization points into the code. This approach can reduce or eliminate redundant authorization tests. The aforementioned works are specifically designed for Java SE authorization problems and assume that call-graph-construction algorithms are available to translate the theoretical approach into a practical implementation. However, many of the well-known call-graph-construction and data-flow algorithms  do not correctly model Java 2, Enterprise Edition (Java EE) cross-component calls and are too conservative to correctly identify authorization requirements. Both the the Java and .NET CLR platforms support subject-based authentication and authorization. Java Authentication and Authorization Service (JAAS) was introduced as an extension to the Java 2 platform in 1999  and became an integral part of the core language starting with Version 1.4. There is little work on static analysis of subject-based authorization, particularly with regard to subjectgranted rights analysis.