[Soot-list] java.lang.VerifyError and byte code execution trace

John Jorgensen jorgensen.john at gmail.com
Mon Sep 16 16:03:40 EDT 2013


I don't think that the problem is that the instruction


   52: aload 5


_occurs_ before the instruction


   91: astore 5


in the bytecode array. I think the problem is that, as far as the verifier
can tell, "aload 5" can be _executed_ before "astore 5", because the
verifier doesn't do constant propagation when it performs its program
analysis, so it can't tell in what order the cases in the switch might be
executed. Back when I knew something about the verification specification,
the only dataflow analysis it performed was the check that no local
variable was read before being initialized.  Beyond that, verification just
ensured that the types---not the detailed values---were consistent on all
control paths.

If I'm correct, then even if your control flattener reordered the switch
cases so that the "astore 5" preceded "aload 5", verification would still
fail, because the verifier doesn't keep track of the fact that local_7 gets
assigned the value 6 before the loop is entered. It just says, "hmm, I can
think of execution paths that would perform "aload 5" without local_5
containing a reference to a String, and that's not good".

So you should probably start by reading the JVM specification's description
of verification<http://docs.oracle.com/javase/specs/jvms/se7/html/jvms-4.html#jvms-4.10>(along
with whatever background information you can google up), to get a
more up-to-date idea of how it works.

If my diagnosis is correct, you might be able to accommodate the verifier
by starting your generated code by initializing a set of temporary
variables, one of each type you need to assign, with dummy values of those
types.  Then have the loads and stores in your generated switch cases work
through those temporaries.  E.g., in this example, your method would start
with the bytecode equivalent of

  String stringTemp = new String("");

and then your "astore 5" block would store to stringTemp instead of
local_5, and the aload would load from stringTemp.  Then whichever order
the blocks were executed in, they would have valid values available to them.

But you really need to learn the details of what verification does, since
this is probably not the only way that obfuscation can produce unverifiable
code (after all, when you're deliberately making the control flow hard to
understand, it's not surprising that it can confuse the verifier).



On Mon, Sep 16, 2013 at 11:09 AM, Yongzhi Wang
<wang.yongzhi2009 at gmail.com>wrote:
Dear All,

Sorry for not giving you enough information. The example is as follows:

Suppose I want to transform the following program into flatten control flow:

public static String process(String s){

return s+":"+s.length();

}


The error message I get while executing the program is as follows:


wpc-10-108-5-230:sootOutput yongzhiwang$ java Test

Exception in thread "main" java.lang.VerifyError: (class: Test, method:
process signature: (Ljava/lang/String;)Ljava/lang/String;) Register 5
contains wrong type


The class file I get after transformation is as follows:


public static java.lang.String process(java.lang.String);

  Signature: (Ljava/lang/String;)Ljava/lang/String;

  Code:

   0: bipush 6

   2: istore 7

   4: iload 7

   6: tableswitch{ //0 to 7

0: 52;

1: 65;

 2: 76;

3: 85;

4: 99;

5: 113;

6: 124;

 7: 134;

default: 52 }

   52: aload 5

   54: invokevirtual #10; //Method
java/lang/StringBuilder.toString:()Ljava/lang/String;

   57: astore 6

   59: iconst_2

   60: istore 7

   62: goto 4

   65: aload_0

   66: invokestatic #31; //Method
java/lang/String.valueOf:(Ljava/lang/Object;)Ljava/lang/String;

   69: astore_2

   70: iconst_5

   71: istore 7

   73: goto 4

   76: aload 6

   78: areturn

   79: iconst_m1

   80: istore 7

   82: goto 4

   85: aload_3

   86: iload 4

   88: invokevirtual #14; //Method
java/lang/StringBuilder.append:(I)Ljava/lang/StringBuilder;

   91: astore 5

   93: iconst_0

   94: istore 7

   96: goto 4

   99: aload_1

   100: ldc #38; //String :

   102: invokevirtual #15; //Method
java/lang/StringBuilder.append:(Ljava/lang/String;)Ljava/lang/StringBuilder;

   105: astore_3

   106: bipush 7

   108: istore 7

   110: goto 4

   113: aload_1

   114: aload_2

   115: invokespecial #26; //Method
java/lang/StringBuilder."<init>":(Ljava/lang/String;)V

   118: iconst_4

   119: istore 7

   121: goto 4

   124: new #19; //class java/lang/StringBuilder

   127: astore_1

   128: iconst_1

   129: istore 7

   131: goto 4

   134: aload_0

   135: invokevirtual #44; //Method java/lang/String.length:()I

   138: istore 4

   140: iconst_3

   141: istore 7

   143: goto 4


}


I guess the java verifier give the error because it see the instruction


   52: aload 5

before

   91: astore 5


Please let me know your opinion. Thanks!


Best regards,

Yongzhi


On Mon, Sep 16, 2013 at 11:09 AM, Yongzhi Wang
<wang.yongzhi2009 at gmail.com>wrote:

> Dear All,
>
> Sorry for not giving you enough information. The example is as follows:
>
> Suppose I want to transform the following program into flatten control
> flow:
>
> public static String process(String s){
>
> return s+":"+s.length();
>
> }
>
>
> The error message I get while executing the program is as follows:
>
>
> wpc-10-108-5-230:sootOutput yongzhiwang$ java Test
>
> Exception in thread "main" java.lang.VerifyError: (class: Test, method:
> process signature: (Ljava/lang/String;)Ljava/lang/String;) Register 5
> contains wrong type
>
>
> The class file I get after transformation is as follows:
>
>
> public static java.lang.String process(java.lang.String);
>
>   Signature: (Ljava/lang/String;)Ljava/lang/String;
>
>   Code:
>
>    0: bipush 6
>
>    2: istore 7
>
>    4: iload 7
>
>    6: tableswitch{ //0 to 7
>
> 0: 52;
>
> 1: 65;
>
>  2: 76;
>
> 3: 85;
>
> 4: 99;
>
> 5: 113;
>
> 6: 124;
>
>  7: 134;
>
> default: 52 }
>
>    52: aload 5
>
>    54: invokevirtual #10; //Method
> java/lang/StringBuilder.toString:()Ljava/lang/String;
>
>    57: astore 6
>
>    59: iconst_2
>
>    60: istore 7
>
>    62: goto 4
>
>    65: aload_0
>
>    66: invokestatic #31; //Method
> java/lang/String.valueOf:(Ljava/lang/Object;)Ljava/lang/String;
>
>    69: astore_2
>
>    70: iconst_5
>
>    71: istore 7
>
>    73: goto 4
>
>    76: aload 6
>
>    78: areturn
>
>    79: iconst_m1
>
>    80: istore 7
>
>    82: goto 4
>
>    85: aload_3
>
>    86: iload 4
>
>    88: invokevirtual #14; //Method
> java/lang/StringBuilder.append:(I)Ljava/lang/StringBuilder;
>
>    91: astore 5
>
>    93: iconst_0
>
>    94: istore 7
>
>    96: goto 4
>
>    99: aload_1
>
>    100: ldc #38; //String :
>
>    102: invokevirtual #15; //Method
> java/lang/StringBuilder.append:(Ljava/lang/String;)Ljava/lang/StringBuilder;
>
>    105: astore_3
>
>    106: bipush 7
>
>    108: istore 7
>
>    110: goto 4
>
>    113: aload_1
>
>    114: aload_2
>
>    115: invokespecial #26; //Method
> java/lang/StringBuilder."<init>":(Ljava/lang/String;)V
>
>    118: iconst_4
>
>    119: istore 7
>
>    121: goto 4
>
>    124: new #19; //class java/lang/StringBuilder
>
>    127: astore_1
>
>    128: iconst_1
>
>    129: istore 7
>
>    131: goto 4
>
>    134: aload_0
>
>    135: invokevirtual #44; //Method java/lang/String.length:()I
>
>    138: istore 4
>
>    140: iconst_3
>
>    141: istore 7
>
>    143: goto 4
>
>
> }
>
>
> I guess the java verifier give the error because it see the instruction
>
>
>    52: aload 5
>
> before
>
>    91: astore 5
>
>
> Please let me know your opinion. Thanks!
>
>
> Best regards,
>
> Yongzhi
>
>
>
> On Mon, Sep 16, 2013 at 8:48 AM, Bodden, Eric <
> eric.bodden at sit.fraunhofer.de> wrote:
>
>> Dear Yongzhi,
>>
>> without knowing more about the code you generate it's hard to help you.
>> The error suggests that you are causing a control flow that loads into
>> register 3 a value of some type that is then later-on used as a value of
>> another type. In other words, you generate incorrect code and should fix
>> your transformation. -noverify should not be an option.
>>
>> Cheers,
>> Eric
>>
>>
>>
>> On 14.09.2013, at 05:44, Yongzhi Wang <wang.yongzhi2009 at gmail.com> wrote:
>>
>> > Dear All,
>> >
>> > Thanks for your suggestion. I am transforming class files into other
>> form at the jimple level. However, the transfromation is about control flow
>> and it is a little unusual. I am trying to "flattening" the control flow: I
>> chop each original function into multiple blocks and makes them accessible
>> to a big switch. The control flow is preserved by the variable of big
>> switch. The idea is explained in the following webpage and the example is
>> as follows:
>> >
>> >
>> http://reverseengineering.stackexchange.com/questions/2221/what-is-a-control-flow-flattening-obfuscation-technique
>> >
>> > Suppose I have original function as follows:
>> >
>> > int a = 1;
>> > int b = 2;
>> > int c = a+b;
>> > return;
>> >
>> > The transformation result is as follows:
>> >
>> > int l = 0;
>> > while (true){
>> > switch(l){
>> >  case 0: goto L1;break;
>> >  case 1: goto L2; break;
>> >  case 2: goto L3; break;
>> >  case 3: goto L4; break;
>> > }
>> >
>> > L1: int a = 1; l = 1;
>> > L2: int b = 2; l = 2;
>> > L3: int c = a+b;l = 3;
>> > L4: return;
>> > }
>> >
>> > I guess the  "Register 3 contains wrong type" error is because that my
>> transformed class file has instruction aload_3 appears before astore_3. If
>> that's the case, do we have some tricks to pass the verifier.
>> >
>> > When I run the program with "-noverify" option, The program give me the
>> following JVM crash error message:
>> >
>> > #
>> > # A fatal error has been detected by the Java Runtime Environment:
>> > #
>> > #  Internal Error
>> (/BUILD_AREA/jdk6_25/hotspot/src/share/vm/gc_interface/collectedHeap.inline.hpp:256),
>> pid=28705, tid=1904704400
>> > #  assert(!Universe::heap()->is_gc_active()) failed: Allocation during
>> gc not allowed
>> > #
>> > # JRE version: 6.0_25-b03
>> > # Java VM: Java HotSpot(TM) Client VM (20.0-b10-fastdebug interpreted
>> mode linux-x86 )
>> > # If you would like to submit a bug report, please visit:
>> > #   http://java.sun.com/webapps/bugreport/crash.jsp
>> > #
>> >
>> > I observe that the bytecode "newarray byte" is executed. I assume this
>> will allocate memory, while the gc is performed. But I have no clue why
>> does this happen. The original program will also execute "newarray byte".
>> But no such error happens.
>> >
>> > Best regards,
>> > Yongzhi
>> >
>> >
>> > On Fri, Sep 13, 2013 at 1:33 AM, John Jorgensen <
>> jorgensen.john at gmail.com> wrote:
>> >
>> > My knowledge of this topic is stale, but ten years ago when I modified
>> Soot's exceptional control flow analysis, I ran into circumstances where
>> improving the precision of exception analysis could lead Soot to generate
>> unverifiable code by basing its optimizations on more precise analyses than
>> those available to the bytecode verifier.
>> >
>> > In that case, the unverifiable code resulted because the bytecode
>> verifier assumed that every instruction within the scope of an exception
>> handler might have that handler as its successor, even if the instruction
>> could not possibly throw an exception that the handler would catch.  That
>> meant that if Soot made optimizations based on knowing that some
>> instructions could not throw particular exceptions, it was possible that
>> the verifier could judge the resulting code unsafe, because it would think
>> the code might lead the exception handler to be executed with the VM in an
>> improper state (for example that some instruction in the handler might be
>> executed when "Register 3 contains wrong type").  See sections 2.6 and 3.4
>> of the Sable Technical Report 2003-3 for more detail.
>> >
>> > So in your example, it is conceivable that the verifier is not smart
>> enough to determine that astore_3 is always executed before aload_3, even
>> though you can see that it is.  Or maybe there is dead code that wants to
>> read a different type from register 3, but the verifier can't tell it is
>> dead.
>> >
>> > But as I said before, my knowledge of this subject is outdated (as I
>> just confirmed by  glancing at the current JVM spec's description of
>> verification: I don't remember it including any Prolog in the old days).
>> >
>> >
>> >
>> >
>> > On Thu, Sep 12, 2013 at 11:29 PM, John Jorgensen <
>> jorgensen.john at gmail.com> wrote:
>> > My knowledge of this topic is stale, but ten years ago when I modified
>> Soot's exceptional control flow analysis, I ran into circumstances where
>> improving the precision of exception analysis could lead Soot to generate
>> unverifiable code by basing its optimizations on more precise analyses than
>> those available to the bytecode verifier.
>> >
>> > In that case, the unverifiable code resulted because the bytecode
>> verifier assumed that every instruction within the scope of an exception
>> handler might have that handler as its successor, even if the instruction
>> could not possibly throw an exception that the handler would catch.  That
>> meant that if Soot made optimizations based on knowing that some
>> instructions could not throw particular exceptions, it was possible that
>> the verifier could judge the resulting code unsafe, because it would think
>> the code might lead the exception handler to be executed with the VM in an
>> improper state (for example that some instruction in the handler might be
>> executed when "Register 3 contains wrong type").  See sections 2.6 and 3.4
>> of the Sable Technical Report 2003-3 for more detail.
>> >
>> > So in your example, it is conceivable that the verifier is not smart
>> enough to determine that astore_3 is always executed before aload_3, even
>> though you can see that it is.  Or maybe there is dead code that wants to
>> read a different type from register 3, but the verifier can't tell it is
>> dead.
>> >
>> > But as I said before, my knowledge of this subject is outdated (as I
>> just confirmed by  glancing at the current JVM spec's description of
>> verification: I don't remember it including any Prolog in the old days).
>> >
>> >
>> >
>> > On Thu, Sep 12, 2013 at 7:27 PM, Yongzhi Wang <
>> wang.yongzhi2009 at gmail.com> wrote:
>> > Dear All,
>> >
>> > I am stucked by the byte code that I generate with soot. I am using
>> soot to transform the control flow of java class. The transformed program
>> should behave same as the original program. However, my generated class
>> file cannot be executed  without the "-noverify" option.
>> >
>> > If I run the class file in java without "-noverify" option, I got the
>> following error message:
>> > java.lang.VerifyError: (class: Test, method: main signature:
>> ([Ljava/lang/String;)V) Register 3 contains wrong type
>> >
>> > If I run the class file in java with "-noverify" option, some test
>> program will run correctly. But some test programs will be pending. I
>> suspect the program is in a dead loop given my transformed control flow.
>> >
>> > My question is:
>> >
>> > 1. What is the usual reason of "Register contains wrong type" error? I
>> can observe that my transformed class file has instruction aload_3 appears
>> before astore_3, even though I use goto instruction to control the control
>> flow to make sure astore_3 is executed before aloud_3. Is that the reason?
>> If so, what's the trick to fix this problem?
>> >
>> > 2. I suspect the test program is in a dead loop. How can I trace the
>> bytecode instruction execution sequence from JVM? Is there any tool or JVM
>> option I can use?
>> >
>> > Thanks!
>> > Best regards,
>> > Yongzhi
>> >
>> > _______________________________________________
>> > Soot-list mailing list
>> > Soot-list at sable.mcgill.ca
>> > http://mailman.cs.mcgill.ca/mailman/listinfo/soot-list
>> >
>> >
>> >
>> >
>> > _______________________________________________
>> > Soot-list mailing list
>> > Soot-list at sable.mcgill.ca
>> > http://mailman.cs.mcgill.ca/mailman/listinfo/soot-list
>>
>> --
>> Prof. Eric Bodden, Ph.D., http://sse.ec-spride.de/ http://bodden.de/
>> Head of Secure Software Engineering  at Fraunhofer SIT, TU Darmstadt and
>> EC SPRIDE
>> Tel: +49 6151 16-75422    Fax: +49 6151 16-72051
>> Room 3.2.14, Mornewegstr. 30, 64293 Darmstadt
>>
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://mailman.cs.mcgill.ca/pipermail/soot-list/attachments/20130916/72ad3820/attachment-0001.html 


More information about the Soot-list mailing list