A survey of static analysis methods for identifying security vulnerabilities in software systems <s> Analysis techniques for RBAC systems <s> A technique is presented for global analysis of program structure in order to perform compile time optimization of object code generated for expressions. The global expression optimization presented includes constant propagation, common subexpression elimination, elimination of redundant register load operations, and live expression analysis. A general purpose program flow analysis algorithm is developed which depends upon the existence of an "optimizing function." The algorithm is defined formally using a directed graph model of program flow structure, and is shown to be correct. Several optimizing functions are defined which, when used in conjunction with the flow analysis algorithm, provide the various forms of code optimization. The flow analysis algorithm is sufficiently general that additional functions can easily be defined for other forms of global code optimization. <s> BIB001 </s> A survey of static analysis methods for identifying security vulnerabilities in software systems <s> Analysis techniques for RBAC systems <s> Modern multiuser software systems have adopted Role- Based Access Control (RBAC) for authorization management. This paper presents a formal model for RBAC policy validation and a static-analysis model for RBAC systems that can be used to (i) identify the roles required by users to execute an enterprise application, (ii) detect potential inconsistencies caused by principal-delegation policies, which are used to override a user's role assignment, (iii) report if the roles assigned to a user by a given policy are redundant or insufficient, and (iv) report vulnerabilities that can result from unchecked intra-component accesses. The algorithms described in this paper have been implemented as part of IBM's Enterprise Security Policy Evaluator (ESPE) tool. Experimental results show that the tool found numerous policy flaws, including ten previously unknown flaws from two production-level applications, with no false-positive reports. <s> BIB002
The ESPE algorithm RBAC systems present similar challenges to those facing SBAC systems. Specifically, for RBAC, it is desirable to identify an application's role requirements, evaluate an existing RBAC policy to detect if it is too permissive or too restrictive, and detect if the RBAC policy restricts access on data consistently. RBAC policies restrict access to operations (or methods) rather than data or resources. In order to invoke a particular entry point to an application, a user needs to be granted all the roles required to invoke all the methods transitively invoked starting at that entry point. The Enterprise Security Policy Evaluation (ESPE) algorithm by Pistoia et al.  BIB002 casts the problem of evaluating an RBAC policy to a data-flow problem. The execution of a Java EE application protected with a set of roles R is modeled as a call graph G ¼ (N, E) . The goal is to map each node n 2 N to v(n), a propositional logic statement in conjunctive normal form, corresponding to the roles necessary to invoke the method m represented by n at runtime. The statement v(n) can be represented as an element of P(P (R)), where the P operator maps a set to its powerset. Specifically, if m has been restricted with roles r 1 , r 2 , . . ., r k 2 R, initially v(n) :¼ ffr 1 , r 2 , . . ., r k gg, modeling the property that a user u initiating any execution traversing m has to show possession of at least one role in the set fr 1 , r 2 , . . ., r k g, which can also be stated by saying that the roles granted to u must be compatible with the logical expression r 1~r2~. . .~r k . If m has not been restricted with any role, then v(n) :¼ Ø. Subsequently, the elements of P(P (R)) associated with each node are recursively propagated backward in the call graph, performing set unions at each node, until a fixed point is reached. BIB001 At the end of this process, each node n will be mapped to a set v(n) ¼ fR 1 , R 2 , . . ., . ., h, meaning that the set of roles granted to u must evaluate to true for the proposition (r 11~r12 . . .r ESPE detects a potentially insufficient RBAC policy. For example, in Figure 4 , user bob has been granted the Employee and Developer roles, which allow bob to invoke the application's entry point m 0 , restricted with the Employee role. However, the roles granted to bob will not allow bob to execute method m 5 , which will be invoked as part of the execution initiated by m 0 . Additionally, the analysis can help detect if the user has been granted unnecessary roles. For example, the Developer role is unnecessary for user bob in the scenario of Figure 4 . RBAC systems support principal-delegation policies to override the roles granted to a user. Under a principal-delegation policy associated with a component, all the methods subsequently traversed execute with the authority as specified by the principal-delegation policy. For example, consider the Java EE run-as policy associated with the component of m 1 and m 4 in Figure 4 . This policy overrides the set of roles granted to user bob with the singleton fManagerg, which will suffice to execute method m 7 . To model principal-delegation policies, the data-flow algorithm described above must be augmented by killing, BIB001 at each component that enforces a principal-delegation policy, any element of P(P(R)) propagated backward. This augmented algorithm detects whether a principaldelegation policy is insufficient by simply comparing, at each component setting a principal-delegation policy, the roles set by the policy with the roles propagated backward in G.