Transcript Lightweight Modeling of the Java Virtual Machine`s Security

Lightweight Modeling of Java
Virtual Machine Security
Constraints using Alloy
Mark Reynolds
BU CS511 Final Report
May 7, 2008
Outline
• Brief Recap of Model Status at Midterm
• New Constraints
• New Results
• Summary
JVM Bytecode Verifier
• Operates on binary class files
– “JVM assembly language”
• Performs a superset of the set of checks performed by
the Java compiler
• Uses a constraint based approach
–
–
–
–
–
–
Local variable constraint
Stack depth invariance constraint
Stack guard constraint
Opcode constraint
Method argument constraint
Many others
• Ideal for an Alloy model
Midterm Status
• Model template created
– “Instruction” sig models instruction properties
– “State” sig models instruction execution within a method
– Complete Alloy model except for initialization
• Class2Alloy converter written and tested
– Takes class files, converts them to Alloy relation initializers
– Class2Alloy output + model template = complete Alloy model
• Local Variable Constraint checked successfully
– “All local variables must be written before being read”
– Normal bytecodes pass
– Deliberately erroneous bytecodes fail
New Constraints
• Stack depth invariance constraint
– The stack depth at any program point is the
same for any path leading to that point
• Stack guard constraint
– The depth of the stack is never negative
– JVM is not like the Intel architecture, method
arguments are passed and returned in local
variables, not on the stack
Stack Depth Invariance
No matter how you get there, the stack depth must be the same
Stack Guard Constraint
0
Time
Stack depth on method entry = 0
Stack depth on method exit = 0
Stack depth >= 0 always
Stack Constraint Checking
• Added “smod” relation to “Instruction” sig in
order to capture stack modifications carried out
by individual instructions
• Added “Depth” as a relation within “State” sig as
a way of modeling stack depth as a function of
execution state
• Modified “nextState” predicate to update stack
depth from smod relation value
pred nextState[s, s': State] {
nextInstruction[s.prog, s'.prog] &&
nextReader[s.prog, s.readers, s'.readers] &&
nextWriter[s.prog, s.writers, s'.writers] &&
(s'.depth = add[s.depth, s.prog.smod]) }
Instruction Relations - Example
map
len
startup
-1
1
iload_1
0
1
r
w
term
ubt
cbt
0,1
smod
0
1
1
bipush
10
1
2
icmpge
13
3
3
iload_1
6
1
iconst_5
7
1
1
imul
8
1
-1
istore_2
9
1
10
3
iload_1
13
1
istore_2
14
1
iload_2
15
1
ireturn
16
1
goto
15
1
13
1
-2
1
2
-1
15
1
0
1
2
-1
2
1
1
-1
Stack Constraint Assertions
assert checkit1 {
all s, s' : State | (s.prog.map =
s'.prog.map) => (s.depth = s'.depth)
}
assert checkit2 {
all s : State | gte[s.depth, 0]
}
Results
• Normal bytecodes pass both new
constraints as well as the original LV
constraint!
• Deliberately aberrant bytecodes fail at
least one of the constraints
Summary
• Alloy is very well suited to modeling JVM
execution
• Three security constraints modeled so far
– Many more left to be done
• Exception handling proved to be difficult
– More than one exception handler in a single
method was especially tricky
– Same for the JVM itself
• http://cs-people.bu.edu/markreyn