Re: verify.c

[Guy Laden <guy@math.tau.ac.il>]

> And also:  Is the code wrong, or just the comment?  Does it reject
> valid code or accept invalid code?

I now see what you mean ;-) and of-course it depends very much on the 
actual code in verify.c.

What derived assumptions did you make based on 'no-multi-level-rets'?
One potential problem I see is that this assumption could, _depending 
on the implementation_, cause unreachable code to be considered reachable 
and reachable code to be considered unreachable.

Below are simple examples of this but whether this is a real problem
really depends on the actual code with which I'm not familiar enough.


consider the example again:
	jsr L1			
	return			
L1:	astore 1		
	jsr L2			
XXX:	...			
L2:	astore 2		
	ret 1			

If XXX is considered reachable from the last ret because its only supposed
to return one level, then any number of bytecode invariants could be 
invalidated. 
For example if XXX is reachable via a goto from some other place that has 
a stack depth different from the one at the ret the verifier might reject 
the code, unjustly.

Similarly, one might accept unverified code: wrongly assuming the last 'ret'
returns to XXX could mean that the code at the 'return' statement is 
unreachable (eg: if there is a 'return' at XXX).
Any number of bytecode invariants could be invalidated at the supposedly
unreachable code, which the verifier won't catch.

Clearly these kinds of problems could lead to code-generation bugs, not 
only security problems. I noticed this in, for example, the Java to SUIF 
translator.

Once again, I'm not at all saying the above are actual problems with
verify.c. It depends on how far the assumption that rets return just 
one level 'poisoned' the code.

Guy.