A survey of static analysis methods for identifying security vulnerabilities in software systems <s> Figure 4 <s> Current implementations of Java make security decisions by searching the runtime call stack. These systems have attractive security properties, but they have been criticized as being dependent on specific artifacts of the Java implementation. The paper models the stack inspection algorithm in terms of a well understood logic for access control and demonstrates how stack inspection is a useful tool for expressing and managing complex trust relationships. We show that an access control decision based on stack inspection corresponds to the construction of a proof in the logic, and we present an efficient decision procedure for generating these proofs. By examining the decision procedure, we demonstrate that many statements in the logic are equivalent and can thus be expressed in a simpler form. We show that there are a finite number of such statements, allowing us to represent the security state of the system as a pushdown automaton. We also show that this automaton may be embedded in Java by rewriting all Java classes to pass an additional argument when a procedure is invoked. We call this security passing style and describe its benefits over previous stack inspection systems. Finally, we show how the logic allows us to describe a straightforward design for extending stack inspection across remote procedure calls. <s> BIB001 </s> A survey of static analysis methods for identifying security vulnerabilities in software systems <s> Figure 4 <s> 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). <s> BIB002 </s> A survey of static analysis methods for identifying security vulnerabilities in software systems <s> Figure 4 <s> 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. <s> BIB003 </s> A survey of static analysis methods for identifying security vulnerabilities in software systems <s> Figure 4 <s> 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. <s> BIB004
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.