Transcript slides - CS Technion

International Conference on Software Engineering – Minneapolis, MN, May 2007
When Role Models Have Flaws:
Static Validation
of Enterprise Security Policies
Marco Pistoia
IBM T. J. Watson Research Center
Hawthorne, New York
Stephen J. Fink
IBM T. J. Watson Research Center
Hawthorne, New York
[email protected]
[email protected]
Robert J. Flynn
Polytechnic University
Brooklyn, New York
Eran Yahav
IBM T. J. Watson Research Center
Hawthorne, New York
[email protected]
[email protected]
Role-Based Access Control Systems
• A role is a set of permissions that can be granted to users
and/or groups of a computer system
• Each permission represents the right to perform a securitysensitive operation; it does not directly represent the right to
access security-sensitive data or resources
• Examples of RBAC systems:
– Java, Enterprise Edition (Java EE)
– Microsoft .NET Common Language Runtime (CLR)
Permission to invoke
method setGrades
Permission to invoke
method assignHomework
Professor
User bob
User alice
2
Role Definition in Java EE
• Roles are application-specific
• They are defined in the deployment descriptors
of an application’s components
• They can be used to restrict access to enterprise
methods
<assembly-descriptor>
<security-role>
<role-name>Professor</role-name>
</security-role>
<method-permission>
<role-name>Professor</role-name>
<method>
<ejb-name>StudentBean</ejb-name>
<method-intf>Remote</method-intf>
<method-name>setGrade</method-name>
</method>
</method-permission>
</assembly-descriptor>
3
RBAC Programming and
Configuration Challenges
Redundant
Roles Granted:
Student, Assistant
User: bob
Intercomponent call
Intracomponent call
m0
Component
Role Required: Student
or Assistant
run-as: Professor
m1
Role Required: Professor m3
Subversive
m6
Role Required: Student
Role Required: Student
m2
m4
m7
Insufficient
m5
Role Required:
Professor
Insufficient
Role Required: Student
4
Contributions
• Novel theoretical foundation to model the flow of
authorization information in an RBAC system
• Enterprise Security Policy Evaluator (EPSE), an
interprocedural analysis framework for RBAC
– Analysis implementation
– Static analyzer tailored to Java, EE applications
• Identification of RBAC policies that are:
– Insufficient
– Redundant
– Subversive
5
RBAC Policies
• Given a program with sets of methods M, roles R, and users U,
role formulae B(R) are propositional logic statements over R,
where each r  R is considered as a predicate
• An RBAC policy is a tuple P = (R, U, υ, μ, π), where:
– υ : U → B(R) is the user role assignment function (conjunction of roles)
– μ : M → B(R) is the role requirement function (disjunction of roles)
– π : M z B(R) is the principal delegation partial function
υ(bob) = Student Assistant
Roles Granted:
Student, Assistant
User: bob
Intercomponent call
μ(m0) = Student
Intracomponent call
m0
Component
μ(m1) = Student  Assistant
π(m1) = π(m4) = Professor
Role Required: Student
or Assistant
run-as: Professor
μ(m3) = Professor
Role Required: Professor m3
m6
μ(m6) = Student
Role Required: Student
m1
Role Required: Student
m2
μ(m5) = Professor
m4
m7
m5
Role Required:
Professor
μ(m7) = Student
Role Required: Student
6
Concrete Semantics
• Standard concrete semantics for a program in the underlying
language
• State S = (pc, stack, heap, local_variables, global_variables)
• Instrumented program state
– Additional stack w of dynamically held roles
– Stack alphabet Σ := B(R)
• <S, w>  <S', w' > transition of instrumented concrete
semantics from configuration <S, w> to configuration <S', w' >
• Operations that affect instrumentations are only method calls
and returns
7
Concrete Instrumented Semantics <S,w>
Init – User u calls entry point m'
Call – Method m calls method m'
Return – Method m' returns to method m
S1
ε
υ(bob) = Student Assistant ⇒ μ(m0) = Student
S2
υ(bob) = Student Assistant
υ(bob) = Student Assistant ⇒ μ(m1) = Student  Assistant
S53
υ(bob) = Student Assistant
p(m1) = Professor ⇒ μ(m4)
μ(m3) = 
Professor
S64
p(m1) = Professor
υ(bob) = Student Assistant
Roles Granted:
Student, Assistant
User: bob
Intercomponent call
μ(m0) = Student
Intracomponent call
m0
Component
μ(m1) = Student  Assistant
π(m1) = π(m4) = Professor
Role Required: Student
or Assistant
run-as: Professor
μ(m3) = Professor
Role Required: Professor m3
Role Required: Student
m1
m4
8
Modified Instrumentation
Init – User u calls entry point m'
Intercomponent Call – m calls m', md(m) ≠ md(m')
Intracomponent
– m calls
m', md(m)
Return – MethodCall
m' returns
to method
m = md(m')
υ(bob) = Student Assistant
S1
ε
S2
υ(bob) = Student Assistant
S53
υ(bob) = Student Assistant
S6
υ(bob) = Student Assistant
Roles Granted:
Student, Assistant
User: bob
Intercomponent call
μ(m0) = Student
Intracomponent call
m0
Component
μ(m1) = Student  Assistant
π(m1) = π(m4) = Professor
Role Required: Student
or Assistant
run-as: Professor
μ(m3) = Professor
Role Required: Professor m3
Role Required: Student
m1
m4
9
Concrete Instrumented Semantics <S,w>
Init – User u calls entry point m'
Call – Method m calls method m'
Return – Method m' returns to method m
S1
ε
υ(bob) = Student Assistant ⇒ μ(m0) = Student
S2
υ(bob) = Student Assistant
υ(bob) = Student Assistant ⇒ μ(m1) = Student  Assistant
S53
υ(bob) = Student Assistant
p(m1) = Professor ⇒ μ(m4)
μ(m3) = 
Professor
S64
p(m1) = Professor
υ(bob) = Student Assistant
Roles Granted:
Student, Assistant
User: bob
Intercomponent call
μ(m0) = Student
Intracomponent call
m0
Component
μ(m1) = Student  Assistant
π(m1) = π(m4) = Professor
Role Required: Student
or Assistant
run-as: Professor
μ(m3) = Professor
Role Required: Professor m3
Role Required: Student
m1
m4
10
Modified Instrumentation
Init – User u calls entry point m'
Intercomponent Call – m calls m', md(m) ≠ md(m')
Intracomponent
– m calls
m', md(m)
Return – MethodCall
m' returns
to method
m = md(m')
υ(bob) = Student Assistant
S1
ε
S2
υ(bob) = Student Assistant
S53
υ(bob) = Student Assistant
S6
υ(bob) = Student Assistant
Roles Granted:
Student, Assistant
User: bob
Intercomponent call
μ(m0) = Student
Intracomponent call
m0
Component
μ(m1) = Student  Assistant
π(m1) = π(m4) = Professor
Role Required: Student
or Assistant
run-as: Professor
μ(m3) = Professor
Role Required: Professor m3
Role Required: Student
m1
m4
11
Sufficiency
• An RBAC policy P for a program p is sufficient if for any user
u and for any execution e such that υ(u) ⇒ μ(me), e does not
transition to an authorization error state; insufficient otherwise
• Insufficient policies can lead to stability problems
Roles Granted:
Student
User: bob
Intercomponent call
Intracomponent call
m0
Component
Role Required: Student
or Assistant
run-as: Professor
m1
Role Required: Professor m3
m6
Role Required: Student
Role Required: Student
m2
m4
m7
Insufficient
m5
Role Required:
Professor
Insufficient
Role Required: Student
12
Minimality
• An RBAC policy P sufficient for a program p is minimal if
there exists no sufficient RBAC policy Q for p such that Q ≺ P
• Otherwise, P is redundant
• Redundant policies violate the Principle of Least Privilege
Redundant
Roles Granted:
Student, Assistant
User: bob
Intercomponent call
Intracomponent call
m0
Component
Role Required: Student
or Assistant
run-as: Professor
m1
m3
m6
Role Required: Student
Role Required: Student
m2
m4
m5
m7
13
Subversion
• An RBAC policy P is subversive if there exists any execution
with P that transitions to an authorization error state under the
base instrumentation, but not under the modified
instrumentation
• Subversive policies violate the Principle of Least Privilege
Roles Granted:
Student
User: bob
Intercomponent call
Intracomponent call
m0
Component
Role Required: Student
or Assistant
run-as: Professor
m1
Role Required: Professor m3
Subversive
m6
Role Required: Student
Role Required: Student
m2
m4
m5
m7
14
Analysis Domain
r1  (r1  r5)
 (r2  r3)
r1
r1
(r1  r5)
 (r2  r3)
r2,r3
r2,r3
r1  r5
r1  r5
r4
r1  r5
r1  r5
r1,r5
r1,r5
r4
• μ : M → B(R) maps each
method to a disjunction of
roles
• Our analysis computes
conjunctions of disjunctions
• The analysis domain can be
the set MCNF(R): role
formulae in Monotone (no
negation) Conjunctive
Normal Form
15
Analysis Domain
f
• Theorem: (MCNF(R),∧,⇒) ≈ (P (P (R)),∪,⊇)
• Corollary: Set-based dataflow analysis formulation
is a correct representation
16
Role-Requirement Analysis
υ(bob) = Student Assistant
Subversion Analysis
Sufficiency
Minimality
•
Policy Panalysis
Iteratively
Repeat
isremove
abstractly
disregarding
onesufficient
role from
distinction
ifrole assignments
between interυ(u),
∀u∈U,
and
and
∀m∈M,
edges
and
verify
whether
the
resulting
– intra-component
υ(u)
⇒ π(m),
In(e0) ∪
Gen(n
)
0
" policy
entryTheorem:
edge
e0 = abstractly
(n, n0), " u sufficient
∈ U : υ(u) ⇒ μ(n0)
RBAC
is still
•
Soundness
–– π(n
In(e)
∪ Gen(n
= (n1, n2)
•
Completeness
Theorem
2), " run-as
If P1)is⇒abstractly
sufficient,
then it edge
is notesubversive
•
Soundness
Theorem:
– If
an RBAC
policy
P is abstractly sufficient, and $ abstractly
Potential
false
positives
–
–
User: bob
Student
sufficient
policy
Q : Q⇒
≺P
P,sufficient
then P is redundant
P abstractly
sufficient
Potential false negatives
positives
m0
Student,
Assistant
μ(m0) = Student
Professor
μ(m1) = Student  Assistant
π(m1) = π(m4) = Professor
Student
μ(m6) = Student
m6
m2
Professor
m3
Student
m1
Professor
μ(m3) = Professor
m4
μ(m5) = Professor
Student
m7
μ(m7) = Student
17
m5
Implementation
• ESPE is based on T. J. Watson Libraries for Analysis
(WALA), specifically tailored to Java, EE
applications
• WALA analyzes enterprise beans after deployment
configuration, but before deployment
– Less code  Scalability
– No analysis of container implementation  Precision
– No dependence on container vendor  Portability
• WALA models several native methods
• WALA models reflection by tracking objects to casts
• http://wala.sourceforge.net
18
Modeling Remote Method Invocations
ENTERPRISE BEAN Bean1Bean SOURCE CODE
public void m1() {
Context initial = new InitialContext();
Object objRef = initial.lookup("java:comp/env/ejb/Bean2");
Bean2Home bean2Home = (Bean2Home)
PortableRemoteObject.narrow(objref, Bean2Home.class);
Bean2 bean2Object = bean2Home.create();
bean2Object.m2();
}
Traditional Static
Analysis Engine
ESPE
ENTERPRISE BEAN DEPLOYMENT DESCRIPTOR
Bean1Bean.m1()
Bean1Bean.m1()
Bean2.m2()
Bean2.m2()
Bean2Bean.m2()
<ejb-name>Bean1Bean</ejb-name>
<home>Bean1Home</home>
<remote>Bean1</remote>
<ejb-class>Bean1Bean</ejb-class>
<session-type>Stateless</session-type>
<transaction-type>Bean1</transaction-type>
<ejb-ref>
<ejb-ref-name>ejb/Bean2</ejb-ref-name>
<ejb-ref-type>Session</ejb-ref-type>
<home>Bean2Home</home>
<remote>Bean2</remote>
<ejb-class>Bean2Bean</ejb-class>
</ejb-ref>
19
ESPE Experimental Results
20
Discussion
•
•
•
•
Closed-world analysis
Call-graph construction algorithm used: RTA
All Java SE and Java EE libraries included in the analysis scope
No false positives detected:
– Java EE applications trigger the execution of libraries, but they themselves are shallow
– Calling patterns in Java EE programs that affect RBAC analysis are predominantly
monomorphic
– Most enterprise beans map directly from the structure of an underlying relational
database, and so do not utilize inheritance or linked structures
– Applications rarely store or manipulate EJB instances with complex heap data structures
– Although the underlying container utilizes complex libraries and data structures, the
WALA analyzer truncates paths into the container, so container code does not pollute the
application-level call graph
– Interactions with Java standard libraries are usually uninteresting for role analysis, since
library methods are not restricted with roles
21
Conclusion
1. Defined theoretical foundation for RBAC
consistency and policy validations
2. Introduced and implemented static analysis
models
3. Static analyzer tailored to Java EE
applications
4. Experimental results have shown zero false
positives
22
Thank You!