Transcript PPT - University of Virginia, Department of Computer Science

cs205: engineering software
university of virginia
fall 2006
Byte Code
Verification
cs205: engineering software
1
Java Byte Code Instructions
• 0: nop
• 1-20: putting constants on the stack
• 96-119: arithmetic on ints, longs,
floats, doubles
• What other kinds of instructions do
we need?
cs205: engineering software
2
Other Instructions
• Loading and Storing Variables (65
instructions)
• Control Flow (~20 instructions)
– if, goto, return
• Method Calls (4 instructions)
• Creating objects (1 instruction)
• Using object fields (4 instructions)
• Arrays (3 instructions)
• checkcast, instanceof
cs205: engineering software
3
Referencing Memory
• iload <varnum>
– Pushes the int in local variable
<varnum> (1 byte) on the stack
• istore <varnum>
– Pops the int on the top of the stack and
stores it in local variable <varnum>
What if you have more than
256 local variables?
cs205: engineering software
4
Referencing
Example
Method void main(java.lang.String[])
0
1
2
3
4
5
6
7
8
11
14
15
18
iconst_2
public class Locals1 {
istore_1
static public void main (String args[]) {
iconst_3
int a = 2;
istore_2
int b = 3;
iload_1
int c = a + b;
iload_2
iadd
System.err.println ("c: " + c); } }
istore_3
getstatic #2 <Field java.io.PrintStream err>
new #3 <Class java.lang.StringBuffer>
dup
invokespecial #4 <Method java.lang.StringBuffer()>
ldc #5 <String "c: ">
20 invokevirtual #6 <Method java.lang.StringBuffer append(java.lang.String)>
23
24
27
30
33
iload_3
invokevirtual #7 <Method java.lang.StringBuffer append(int)>
invokevirtual #8 <Method java.lang.String toString()>
invokevirtual #9 <Method void println(java.lang.String)>
return
cs205: engineering software
5
Control Flow
• ifeq <label>
Pop an int off the stack. If it is zero,
jump to the label. Otherwise, continue
normally.
• if_icmple <label>
Pop two ints off the stack. If the second
one is <= the first one, jump to the
label. Otherwise, continue normally.
cs205: engineering software
6
Method Calls
• invokevirtual <method>
– Invokes the method <method> on the
parameters and object on the top of the
stack.
– Finds the appropriate method at runtime based on the actual type of the this
object.
invokevirtual <Method void println(java.lang.String)>
cs205: engineering software
7
Method Calls
• invokestatic <method>
– Invokes a static (class) method
<method> on the parameters on the
top of the stack.
– Finds the appropriate method at runtime based on the actual type of the this
object.
cs205: engineering software
8
Example
public class Sample1 {
static public void main (String args[]) {
System.err.println ("Hello!");
System.exit (1);
}
}
cs205: engineering software
9
> javap -c Sample1
public class Sample1 {
static public void main (String args[]) {
System.err.println ("Hello!");
System.exit (1); } }
Compiled from Sample1.java
public class Sample1 extends java.lang.Object {
public Sample1();
public static void main(java.lang.String[]);
}
Method Sample1()
0 aload_0
1 invokespecial #1 <Method java.lang.Object()>
4 return
Method void main(java.lang.String[])
0 getstatic #2 <Field java.io.PrintStream err>
3 ldc #3 <String "Hello!">
5 invokevirtual #4 <Method void println(java.lang.String)>
8 iconst_1
9 invokestatic #5 <Method void exit(int)>
12 return
cs205: engineering software
10
The Worst Instruction
http://java.sun.com/docs/books/vmspec/2nd-edition/html/Instructions2.doc7.html
jsr [branchbyte1] [branchbyte2]
Operand Stack
...  ..., address
Description
The address of the opcode of the instruction immediately following this
jsr instruction is pushed onto the operand stack as a value of type
returnAddress. The unsigned branchbyte1 and branchbyte2 are used to
construct a signed 16-bit offset, where the offset is (branchbyte1 << 8)
| branchbyte2. Execution proceeds at that offset from the address of
this jsr instruction. The target address must be that of an opcode of an
instruction within the method that contains this jsr instruction.
Notes
The jsr instruction is used with the ret instruction in the implementation
of the finally clauses of the Java programming language. Note that jsr
pushes the address onto the operand stack and ret gets it out of a local
variable. This asymmetry is intentional.
cs205: engineering software
11
Try-Catch-Finally
public class JSR {
static public void main (String args[]) {
try {
System.out.println("hello");
} catch (Exception e) {
System.out.println ("There was an exception!");
} finally {
System.out.println ("I am finally here!");
}
}
}
cs205: engineering software
12
public class JSR {
Method void main(java.lang.String[])
static public void main (String args[]) {
0 getstatic #2 <Field java.io.PrintStream out>
try {
3 ldc #3 <String "hello">
System.out.println("hello");
} catch (Exception e) {
5 invokevirtual #4 <Method void println(java.lang.String)>
System.out.println (“... exception!");
8 jsr 35
} finally {
11 goto 46
System.out.println ("I am finally");
14 astore_1
}
15 getstatic #2 <Field java.io.PrintStream out>
}
18 ldc #6 <String "There was an exception!">
}
20 invokevirtual #4 <Method void println(java.lang.String)>
23 jsr 35
26 goto 46
29 astore_2
30 jsr 35
Exception table:
33 aload_2
from to target type
34 athrow
0
8 14 <Class java.lang.Exception>
35 astore_3
36 getstatic #2 <Field java.io.PrintStream
0 11 out>
29 any
39 ldc #7 <String "I am finally here!">
14 26 29 any
41 invokevirtual #4 <Method void
29println(java.lang.String)>
33 29 any
44 ret 3
46 return
cs205: engineering software
13
Java
malcode.java
javac
Compiler
malcode.class
JVML
Trusted Computing Base
Java Bytecode Verifier
Invalid
“Okay”
STOP
JavaVM
Joe User
cs205: engineering software
14
Running Mistyped Code
.method public static main([Ljava/lang/String;)V
…
iconst_2
istore_0
> java Simple
aload_0
Exception in thread "main" java.lang.VerifyError:
iconst_2
(class: Simple, method: main signature:
iconst_3
([Ljava/lang/String;)V)
iadd
Register 0 contains wrong type
…
> java –noverify Simple
return
.end method result: 5
cs205: engineering software
15
Running Mistyped Code
.method public static main([Ljava/lang/String;)V
…
> java –noverify Simple
Unexpected Signal : EXCEPTION_ACCESS_VIOLATION
ldc 205
(0xc0000005) occurred at PC=0x809DCEB
istore_0
Function=JVM_FindSignal+0x1105F
Library=C:\j2sdk1.4.2\jre\bin\client\jvm.dll
aload_0
iconst_2 Current Java thread:
iconst_3 at Simple.main(Simple.java:7)
…
iadd
#
…
# HotSpot Virtual Machine Error : EXCEPTION_ACCESS_VIOLATION
.end method # Error ID : 4F530E43505002EF
# Please report this error at
# http://java.sun.com/cgi-bin/bugreport.cgi
#
# Java VM: Java HotSpot(TM) Client VM (1.4.2-b28 mixed mode)
cs205: engineering software
16
Bytecode Verifier
• Checks class file is formatted
correctly
– Magic number: class file starts with
0xCAFEBABE
– String table, code, methods, etc.
• Checks JVML code satisfies safety
properties
– Simulates program execution to know
types are correct, but doesn’t need to
examine any instruction more than
once
cs205: engineering software
17
Verifying Safety Properties
• Type safe
– Stack and variable slots must store and load as
same type
• Memory safe
– Must not attempt to pop more values from
stack than are on it
– Doesn’t access private fields and methods
outside class implementation
• Control flow safe
– Jumps must be to valid addresses within
function, or call/return
cs205: engineering software
18
Simulating All Paths
• The bytecode verifier verifies type
safety for all possible executions of
the program
• Since there are infinitely many paths
through the program, how is this
possible?
cs205: engineering software
19
Verifier (should be) Conservative
JVML programs
Safe programs
Verifiable programs
(Slide from Nate
Paul’s ACSAC talk)
cs205: engineering software
20
Complexity Increases Risk
JVML programs
Safe programs
Verifiable programs
Bug
cs205: engineering software
(Slide from Nate
Paul’s ACSAC talk)
21
Vulnerabilities in JavaVM
Vulnerabilities Reported
45
40
35
30
25
20
15
10
5
0
0
July 1996
1
cs205: engineering software
2
3
4
5
6
Years Since First Release
7
8
9
July 2005
22
Where are They?
Verification
12
API bugs
Class loading
Other or unknown
10
8
2
3
4
5
Missing policy checks
Configuration
DoS attacks (crash, consumption)
several of these were because of jsr complexity
cs205: engineering software
23
Summary:
Low-level vs. Policy Security
• Low-level Code Safety:
– Type safety, memory safety, control flow
safety
– Needed to prevent malcode from
circumventing any policy mechanism
• Policy Security:
– Control access and use of resources
(files, network, display, etc.)
– Enforced by Java class
– Hard part is deciding on a good policy
cs205: engineering software
24
Charge
• Monday:
– Quiz 4: will cover through Friday’s
lecture on the Java bytecode verifier
– Using CVS (Dan)
• Friday: project design documents
due
cs205: engineering software
25