Re: Java insecurity - long - argumentative - you are warned.

-----BEGIN PGP SIGNED MESSAGE-----

>> > While all this checking appears excruciatingly detailed, by the time
>> > the byte code verifier has done its work, the Java interpreter can
>> > proceed knowing that the code will run securely. Knowing these
>> > properties makes the Java interpreter much faster, because it doesn't
>> > have to check anything.
>
>Yikes!!  I'll leave this for someone else to address.  This sounds to me
>like a variation on virus scanning.  I think that there are far more
>reputable virus experts than I who can comment and expand on *flaws* with
>that approach.

This "checking," as any comp-sci undergrad will tell you, amounts to solving
the halting problem for the java interpreter. While this is possible for a
finite state automata like the java interpreter (made more difficult by the
fact that it can use the "net" for additional state), it is not even
remotely feasable.

If you can write a checker that works in a reasonable amount of time, I'll
write a turing machine simulator that'll do something nasty if the input
machine halts. Then we'll split the fame and fortune for solving the 5 state
Busy Beaver problem. Deal?


-----BEGIN PGP SIGNATURE-----
Version: 2.6.2

iQBgAwUBMJ8gtXIf3YegbdiBAQGqMQJXWzwuPYM2bNb96Fgfb1wGeDC83fNFOW5H
8PQHbnt8bDFsHxKv2L8kcBhtO/TWA0cugVYR9YFf2BOaGoA2UIoCBdwfABM1HAKU
hd0H
=TA2E
-----END PGP SIGNATURE-----

Dietrich Kappe | Red Planet    http://www.redweb.com
Red Planet, LLC| "Chess Space" | "MS Access Products" |  PGP Public Key
1-800-RED 0 WEB|    /chess     |       /cobre         | /goedel/key.txt
Web Publishing | Key fingerprint: 8C2983E66AB723F9 A014A0417D268B84

On Tue, 7 Nov 1995, Dietrich J. Kappe wrote:
> 
> This "checking," as any comp-sci undergrad will tell you, amounts to solving
> the halting problem for the java interpreter. While this is possible for a
[...]
> If you can write a checker that works in a reasonable amount of time, I'll
> write a turing machine simulator that'll do something nasty if the input
> machine halts. Then we'll split the fame and fortune for solving the 5 state

Yeah, but when you graduate, they let you in to the real secret- if a 
problem is NPC or Undecideable, either use some wild guesswork (oops, 
heuristic), or try solving enough of the problem to be usable. 

The java verifier not only terminates, but runs in time linear to the 
size of the program to be verified. This is because the verifier doesn't 
really calculate whether a program is safe or not; it determines whether 
it can prove that the program is safe or not. It's possible to generate 
sequences of bytecodes that do not perform unsafe accesses, yet which are 
still rejected by the verifier because they violate it's requirements.

The verifier can be considered to be an abstract interpretation over the 
depth and type-state of the operand stack. If the state is known before 
an instruction, it is always known after that instruction, and if there 
is more than one way to arrive at an instruction, each control path must 
arrive at that instruction with the same typestate.

Examples (not real JavaVM, but similar)

	load-int  <int>	== push an int onto the stack.
			before: ...
			after : ...,int

	load-float <flt>== push a float onto the tack
			before: ...
			after: ...,float
		
	add-int		== pop two ints off the stack, push sum onto stack
			before: ...,int,int
			after:  ...,int

	blt <val><add>  == pop an int off the stack, compare to val, and 
			      jump to address add if int is less than val

			before:  ...,int
			after:	 ...

	jmp <add>	== jump to adddress add
			before: ...
			after: ...

VALID
	load-int  1	; stack = (int)
	load-int  1	; stack = (int), (int)
	add-int		; stack = (int)

INVALID
	load-int 1	; stack = (int)
	load-float 1.0	; stack = (int) (float)
	add-int		; error, stack != (int), (int)

VALID
	load-int 2	;stack = (int)
	blt 1, a  	;stack = null
	load-int 3	; stack = (int)
	jmp b		; stack = (int)
    a	load-int 1	; stack = (int);
    b 	load-int 4	; stack = (int) (int)
	add-int		; stack = (int)

INVALID
	load-int 2	;stack = (int)
	blt 1, a  	;stack = null
	load-float 3	; stack = (float)
	jmp b		; stack = (float)	
    a	load-int 1	; stack = (int);	
    b 	load-int 4	; stack = ERROR (float || int)
	add-int		; stack = (int) ERROR

This last example is invlaid, even though it's possible in this case to show 
dynamically that the program will always arrive at b with an int on the 
stack; there are still two control paths that arive at b, one with an 
int, the other with a float.

I hope this makes sense

Simon