Bytecode program interpreter apparatus and method with pre-verification of data type restrictions and object initialization

• US 6,477,702 B1
• Filed: 11/09/2000
• Issued: 11/05/2002
• Est. Priority Date: 12/20/1994
• Status: Expired due to Term

• Current Assignee: Sun Microsystems Incorporated (Oracle Corporation)
• Original Assignee: Sun Microsystems Incorporated (Oracle Corporation)
• Inventors: Yellin, Frank, Gosling, James A.
• Primary Examiner(s): Morse, Gregory
• Assistant Examiner(s): Chavis, John Q.
• Application Number:
  US09/711,053
• Time in Patent Office: 726 Days
• Field of Search: 717/126
• US Class Current: 717/126
• CPC Class Codes: G06F 11/3612 by runtime analysis performance monitoring G06F11/3466
• CPC Class Codes: G06F 21/51 at application loading time, e.g. accepting, rejecting, starting or inhibiting executable software based on integrity or source reliability
• CPC Class Codes: G06F 21/52 during program execution, e.g. stack integrity ; Preventing unwanted data erasure; Buffer overflow
• CPC Class Codes: G06F 21/566 Dynamic detection, i.e. detection performed at run-time, e.g. emulation, suspicious activities
• CPC Class Codes: G06F 9/44589 Program code verification, e.g. Java bytecode verification, proof-carrying code high-level semantic checks G06F8/43; testing and debugging software G06F11/36
• CPC Class Codes: G06F 9/45508 Runtime interpretation or emulation, e g. emulator loops, bytecode interpretation

Abstract

A program interpreter for computer programs written in a bytecode language, which uses a restricted set of data type specific bytecodes. The interpreter, prior to executing any bytecode program, executes a bytecode program verifier procedure that verifies the integrity of a specified program by identifying any bytecode instruction that would process data of the wrong type for such a bytecode and any bytecode instruction sequences in the specified program that would cause underflow or overflow of the operand stack. If the program verifier finds any instructions that violate predefined stack usage and data type usage restrictions, execution of the program by the interpreter is prevented. After pre-processing of the program by the verifier, if no program faults were found, the interpreter executes the program without performing operand stack overflow and underflow checks and without performing data type checks on operands stored in operand stack. As a result, program execution speed is greatly improved.

Claims

1. A method, comprising:

selectively connecting a computer system via a network to a sending computer to receive from the sending computer a program formed of low-level, stack-oriented, program code;

verifying prior to execution that when an instruction of the program is executed that can be executed along more than one execution path, a number of operands on a stack when arriving at that instruction during execution is identical regardless of the execution path taken to arrive at the instruction, and a type state of the stack when arriving at the instruction during execution of a first execution path that includes the instruction is compatible with a type state of the stack when arriving at the instruction during execution of all other execution paths that include the instruction; and

executing the verified program.

2. The method of claim 1, wherein the verifying includes confirming prior to execution of the program that the number of operands on the stack when arriving at the instruction that can be executed along more than one execution path is identical for all execution paths that include the instruction, even when the stack is not empty prior to execution of the instruction.

3. The method of claim 1, wherein the verifying includes confirming prior to execution of the program that execution of any loop in the program will not result in a net addition or deletion of operands on the stack.

4. The method of claim 1, wherein when the program is executed no check is made for overflow and underflow of the stack.

5. The method of claim 1, wherein t he verifying includes verifying prior to execution that when a loop of the program is executed, immediately before and after each iteration of the loop, a number of operands an the s tack is identical, even when the stack is not empty, and a type state of the stack remains compatible with an initial type state of the stack regardless of how many times the loop is executed.

6. The method of claim 1, wherein the executing includes executing the program without performing a check during execution of the program that corresponds to a check performed by the verifying.

7. The method of claim 1, wherein each instruction of the program comprises one or more bytecodes, and wherein the verifying includes determining whether execution of any bytecoded instruction in the program would violate predetermined data type restrictions for that instruction.

8. The method of claim 1, wherein at least one instruction of the program comprises one or more bytecodes that represent an operation on a specific data type and is selected from the group consisting of:

aaload, aastore, aconst_null, aload, areturn, arraylength, astore, astore_<

n>

, athrow, bipush, breakpoint, catchsetup, catchteardown, checkcast, df2, d2i, d2l, dadd, daload, dastore, dcmpg, dcmpl, dconst_<

d>

, ddiv, dload, dload_<

d>

, dmod, dmul, dneg, dreturn, dstore, dstore_<

n>

, dsub, dup, dup2, dup2_x1, dup2_x2, dup_x1, dup_x2, f2d, f2i, f2l, fadd, faload, fastore, fempg, fempl, fconst_<

f>

, fdiv, fload, fload_<

n>

, fmod, fmul, fneg, freturn, fstore, fstore_<

n>

, fsub, gatfield, getstatic, goto, i2d, i2f, i2l, iadd, iaload, iand, iastore, iconst_<

n>

, iconst_m1, idiv, if_acmpeq, if_acmpne, if_icmpeq, if_icmpge, if_icmpgt, if_icmple, if_icmplt, if_icmpne, ifeq, ifge, ifgt, ifle, iflt, ifne;

iinc, iload, iload_<

n>

, imod, imul, ineg, instanceof, int2byte, int2char, invokeinterface, invokemethod, invokesuper, ior, ireturn, ishl, Ishr, istore, istore_<

n>

, isub, iushr, ixor, jsr, 12d, 12f, 12i, ladd, laload, land, lastore, lcmp, lconst_<

l>

, ldc1, ldc2, ldc2w, ldiv, lload, lload_<

n>

, lmod, lmul, lneg, lookupswitch, lor, lreturn, lshl, lshr, lstore, lstore_n>

, lsub, lushr, lxor, monitorenter, monitorexit, new, newarray, newfromname, nop, pop, pop2, putfield, putstatic, ret, return, saload, sastore, siaload, siastore, sipush, tableswitch, and verifystack.

9. The method of claim 1, wherein the verifying includes certifying that the program complies with a stack non-overflow constraint and a stack non-underflow constraint.

10. The method of claim 1, wherein the verifying includes using a virtual stack to track the type state of the stack.

11. The method of claim 1, wherein the verifying includes using an array of virtual local variables to track a type state of local variables used by the program.

12. A computer system, comprising:

means for selectively connecting the computer system via a network to a sending computer to receive from the sending computer a program formed of low-level, stack-oriented, program code;

memory for storing the program;

a data processing unit for executing programs stored in the memory;

a program verifier, stored in the memory and executed by the data processing unit, the program verifier including instructions for verifying prior to execution that when an instruction of the program is executed that can be executed along more than one execution path, a number of operands on a stack when arriving at that instruction during execution is identical regardless of the execution path taken to arrive at the instruction, and a type state of the stack when arriving at the instruction during execution of a first execution path that includes the instruction is compatible with a type state of the stack when arriving at the instruction during execution of all other execution paths that include the instruction; and

a program execution module for executing the verified program.

13. The computer system of claim 12, wherein the verifying instructions include instructions for confirming prior to execution of the program that the number of operands on the stack when arriving at the instruction that can be executed along more than one execution path is identical for all execution paths that include the instruction, even when the stack is not empty prior to execution of the instruction.

14. The computer system of claim 12, wherein the verifying instructions include instructions for confirming prior to execution of the program that execution of any loop in the program will not result in a net addition or deletion of operands on the stack.

15. The computer system of claim 12, wherein the program execution module does not check for overflow and underflow of the stack when executing the verified program.

16. The computer system of claim 12, wherein the verifying instructions include instructions for verifying prior to execution that when a loop of the program is executed, immediately before and after each iteration of the loop, a number of operands on the stack is identical, even when the stack is not empty, and a type state of the stack remains compatible with an initial type state of the stack regardless of how many times the loop is executed.

17. The computer system of claim 12, wherein the program execution module includes instructions for executing the program with out performing a check during execution of the pro gram that corresponds to a check performed by the program verifier.

18. The computer system of claim 12, wherein each instruction of the program comprises one or more bytecodes, and wherein the program verifier includes instructions for determining whether execution of any bytecoded instruction in the program would violate predetermined data type restrictions for that instruction.

19. The computer system of claim 12, wherein at least one instruction of the program comprises one or more bytecodes that represent an operation on a specific data type and is selected from the group consisting of:

aaload, aastore, aconst_null, aload, areturn, arraylength, astore, astore_<

n>

, athrow, bipush, breakpoint, catchsetup, catchteardown, checkcast, df2, d2i, d2l, dadd, daload, dastore, dcmpg, dcmpl, dconst_<

d>

, ddiv, dload, dload_<

d>

, dmod, dmul, dneg, dreturn, dstore, dstore_<

n>

, dsub, dup, dup2, dup2_x1, dup2_x2, dup_x1, dup_—

x2, f2d, f2i, f2l, fadd, faload, fastore, fempg, fempl, fconst_<

f>

, fdiv, fload, fload_<

n>

, fmod, fmul, fneg, freturn, fstore, fstore_<

n>

, fsub, gatfield, getstatic, goto, i2d, i2f, i2l, iadd, iaload, iand, iastore, iconst_<

n>

, iconst_m1, idiv, if_acmpeq, if_acmpne, if_icmpeq, if_icmpge, if_icmpgt, if_icmple, if_icmplt, if_icmpne, ifeq, ifge, ifgt, ifle, iflt, ifne, iinc, iload, iload_<

n>

, imod, imul, ineg, instanceof, int2byte, int2char, invokeinterface, invokemethod, invokesuper, ior, ireturn, ishl, Ishr, istore, istore_<

n>

, isub, iushr, ixor, jsr, 12d, 12f, 12i, ladd, laload, land, lastore, lcmp, lconst_<

1>

, lda1, ldc2, ldc2w, ldiv, lload, lload_<

n>

, lmod, lmul, lneg, lookupswitch, lor, lreturn, lshl, lshr, lstore, Istore_<

n>

, lsub, lushr, lxor, monitorenter, monitorexit, new, newarray, newfromname, nop, pop, pop2, putfield, putstatic, ret, return, saload, sastore, siaload, siastore, sipush, tableswitch, and verifystack.

20. The computer system of claim 12, wherein the program verifier includes instructions for certifying that the program complies with a stack non-overflow constraint and a stack non-underflow constraint.

21. The computer system of claim 12, wherein the program verifier includes instructions using a virtual stack to track the type state of the stack.

22. The computer system of claim 12, wherein the program verifier includes instructions using an array of virtual local variables to track a type state of local variables used by the program.

23. A computer program product for use in conjunction with a computer system, the computer program product comprising a computer readable storage medium and a computer program mechanism embedded therein, the computer program mechanism comprising:

a program verifier, for analyzing a program formed of low-level, stack-oriented, program code;

the program verifier including instructions for verifying prior to execution of the program that when an instruction of the program is executed that can be executed along more than one execution path, a number of operands on a stack when arriving at that instruction during execution is identical regardless of the execution path taken to arrive at the instruction, and a type state of the stack when arriving at the instruction during execution of a first execution path that includes the instruction is compatible with a type state of the stack when arriving at the instruction during execution of all other execution paths that include the instruction; and

a program execution module for executing the verified program.

24. The computer program product of claim 23, wherein the verifying instructions include instructions for confirming prior to execution of the program that the number of operands on the stack when arriving at the instruction that can be executed along more than one execution path is identical for all execution paths that include the instruction, even when the stack is not empty prior to execution of the instruction.

25. The computer program product of claim 23, wherein the verifying instructions include instructions for confirming prior to execution of the program that execution of any loop in the program will not result in a net addition or deletion of operands on the stack.

26. The computer program product of claim 23, wherein the program execution module does not check for overflow and underflow of the stack when executing the verified program.

27. The computer program product of claim 23, wherein the verifying instructions include instructions for verifying prior to execution that when a loop of the program is executed, immediately before and after each iteration of the loop, a number of operands on the stack is identical, even when the stack is not empty, and a type associated with each of the operands on the stack is compatible regardless of how many times the loop is executed.

28. The computer program product of claim 23, wherein the program execution module includes instructions for executing the program without performing a check during execution of the program that corresponds to a check performed by the program verifier.

29. The computer program product of claim 23, wherein each instruction of the program comprises one or more bytecodes, and wherein the program verifier includes instructions for determining whether execution of any bytecoded instruction in the program would violate predetermined data type restrictions for that instruction.

30. The computer program product of claim 23, wherein at least one instruction of the program comprises one or more bytecodes that represent an operation on a specific data type and is selected from the group consisting of:

aaload, aastore, aconst_null, aload, areturn, arraylength, astore, astore_<

n>

, athrow, bipush, breakpoint, catchsetup, catchteardown, checkcast, df2, d2i, d2l, dadd, daload, dastore, dcmpg, dcmpl, dconst_<

d>

, ddiv, dload, dload_<

d>

, dmod, dmul, dneg, dreturn, dstore, dstore_<

n>

, dsub, dup, dup2, dup2_x1, dup2_x2, dup_x1, dup_—

x2, f2d, f2i, f2l, fadd, faload, fastore, fempg, fempl, fconst_<

f>

, fdiv, fload, fload_<

n>

, fmod, fmul, fneg, freturn, fstore, fstore_<

n>

, fsub, gatfield, getstatic, goto, i2d, i2f, i2l, iadd, iaload, iand, iastore, iconst_<

n>

, iconst_m1, idiv, if_acmpeq, if_acmpne, if_icmpeq, if_icmpge, if_icmpgt, if_icmple, if_icmplt, if_icmpne, ifeq, ifge, ifgt, ifle, iflt, ifne, iinc, iload, iload_<

n>

, imod, imul, ineg, instanceof, int2byte, int2char, invokeinterface, invokemethod, invokesuper, ior, ireturn, ishl, Ishr, istore, istore_<

n>

, isub, iushr, ixor, jsr, 12d, 12f, 12i, ladd, laload, land, lastore, lcmp, lconst_<

1>

, ldc1, ldc2, ldc2w, ldiv, lload, lload_<

n>

, lmod, lmul, lneg, lookupswitch, lor, lreturn, lshl, lshr, lstore, lstore_<

n>

, lsub, lushr, lxor, monitorenter, monitorexit, new, newarray, newfromname, nop, pop, pop2, putfield, putstatic, ret, return, saload, sastore, siaload, siastore, sipush, tableswitch, and verifystack.

31. The computer program product of claim 23, wherein the program verifier includes instructions for certifying that the program complies with a stack non-overflow constraint and a stack non-underflow constraint.

32. The computer program product of claim 23, wherein the program verifier includes instructions using a virtual stack to track the type state of the stack.

33. The computer program product of claim 23, wherein the program verifier includes instructions using an array of virtual local variables to track a type state of local variables used by the program.

102. The computer program product of claim 23, wherein the program is platform independent.

34. A method comprising:

providing a program formed of low-level, stack-oriented, program code; and

making the program available to a computer system via a network;

wherein after the computer system accesses the program, the computer system verifies prior to execution of the program that when an instruction of the program is executed that can be executed along more than one execution path, a number of operands on a stack when arriving at that instruction during execution is identical regardless of the execution path taken to arrive at the instruction, and a type state of the stack when arriving at the instruction during execution of a first execution path that includes the instruction is compatible with a type state of the stack when arriving at the instruction during execution of all other execution paths that include the instruction.

35. The method of claim 34, wherein the computer system confirms prior to execution of the program that the number of operands on the stack when arriving at the instruction that can be executed along more than one execution path is identical for all execution paths that include the instruction, even when the stack is not empty prior to execution of the instruction.

36. The method of claim 34, wherein the computer system confirms prior to execution of the program that execution of any loop in the program will not result in a net addition or deletion of operands on the stack.

37. The method of claim 34, wherein the computer system confirms prior to execution of the program that when a loop of the program is executed, immediately before and after each iteration of the loop, a number of operands on the stack is identical, even when the stack is not empty, and a type associated with each of the operands on the stack is compatible regardless of how many times the loop is executed.

38. The method of claim 34, including executing the program without performing a check during execution of the program that corresponds to a check performed by the computer system prior to execution of the program.

39. The method of claim 34, wherein each instruction of the program comprises one or more bytecodes, and wherein the computer system determines prior to execution of the program whether execution of any bytecoded instruction in the program would violate predetermined data type restrictions for that instruction.

40. The method of claim 34, wherein at least one instruction of the program comprises one or more bytecodes that represent an operation on a specific data type and is selected from the group consisting of:

aaload, aastore, aconst-null, aload, areturn, arraylength, astore, astore_<

n>

, athrow, bipush, breakpoint, catchsetup, catchteardown, checkcast, df2, d2i, d2l, dadd, daload, dastore, dcmpg, dcmpl, dconst_<

d>

, ddiv, dload, dload_<

d>

, dmod, dmul, dneg, dreturn, dstore, dstore_<

n>

, dsub, dup, dup2, dup2_x1, dup2_x2, dup_x1, dup_—

x2, f2d, f2i, f2l, fadd, faload, fastore, fempg, fempl, fconst_<

f>

, fdiv, fload, fload_<

n>

, fmod, fmul, fneg, freturn, fstore, fstore_<

n>

, fsub, gatfield, getstatic, goto, i2d, i2f, i2l, iadd, iaload, iand, iastore, iconst_<

n>

, iconst_m1, idiv, if_acmpeq, if_acmpne, if_icmpeq, if_icmpge, if_icmpgt, if_icmple, if_icmplt, if_icmpne, ifeq, ifge, ifgt, ifle, iflt, ifne, iinc, iload, iload_<

n>

, imod, imul, ineg, instanceof, int2byte, int2char, invokeinterface, invokemethod, invokesuper, ior, ireturn, ishl, Ishr, istore, istore_<

n>

, isub, iushr, ixor, jsr, 12d, 12f, 12i, ladd, laload, land, lastore, lcmp, lconst_<

1>

, ldc1, ldc2, ldc2w, ldiv, lload, lload_<

n>

, lmod, lmul, lneg, lookupswitch, lor, lreturn, lshl, lshr, lstore, lstore_<

n>

, lsub, lushr, lxor, monitorenter, monitorexit, new, newarray, newfromname, nop, pop, pop2, putfield, putstatic, ret, return, saload, sastore, siaload, siastore, sipush, tableswitch, and verifystack.

41. The method of claim 34, wherein the computer system, prior to execution of the program, verifies that the program complies with a stack non-overflow constraint and a stack non-underflow constraint.

42. The method of claim 34, wherein the computer system, prior to execution of the program, uses a virtual stack to track the type state of the stack during execution of the program.

43. The method of claim 34, wherein the computer system, prior to execution of the program, uses an array of virtual local variables to track a type state of local variables used during execution of the program.

44. A computer system, comprising:

memory for storing a program formed of low-level, stack-oriented, program code;

a data processing unit for executing programs stored in the memory;

a program verifier, stored in the memory and executed by the data processing unit, the program verifier including instructions for verifying, prior to execution, that when an instruction of the program is executed that can be executed along more than one execution path, a number of operands on a stack when arriving at that instruction during execution is identical regardless of the execution path taken to arrive at the instruction, and a type state of the stack when arriving at the instruction during execution of a first execution path that includes the instruction is compatible with a type state of the stack when arriving at the instruction during execution of all other execution paths that include the instruction.

45. The computer system of claim 44, wherein the verifying instructions include instructions for confirming prior to execution of the program that the number of operands on the stack when arriving at the instruction that can be executed along more than one execution path is identical for all execution paths that include the instruction, even when the stack is not empty prior to execution of the instruction.

46. The computer system of claim 44, wherein the verifying instructions include instructions for confirming prior to execution of the program that execution of any loop in the program will not result in a net addition or deletion of operands on the stack.

47. The computer system of claim 44, wherein the verifying instructions include instructions for verifying prior to execution that when a loop of the program is executed, immediately before and after each iteration of the loop, a number of operands on the stack is identical, even when the stack is not empty, and a type associated with each of the operands on the stack is compatible regardless of how many times the loop is executed.

48. The computer system of claim 44, including a program execution module having instructions for executing the program without performing a check during execution of the program that corresponds to a check performed by the program verifier.

49. The computer system of claim 44, wherein each instruction of the program comprises one or more bytecodes, and wherein the program verifier includes instructions for determining whether execution of any bytecoded instruction in the program would violate predetermined data type restrictions for that instruction.

50. The computer system of claim 44, wherein at least one instruction of the program comprises one or more bytecodes that represent an operation on a specific data type and is selected from the group consisting of:

aaload, aastore, aconst_null, aload, areturn, arraylength, astore, astore_<

n>

, athrow, bipush, breakpoint, catchsetup, catchteardown, checkcast, df2, d2i, d2l, dadd, daload, dastore, dcmpg, dcmpl, dconst_<

d>

, ddiv, dload, dload_<

d>

, dmod, dmul, dneg, dreturn, dstore, dstore_<

n>

, dsub, dup, dup2, dup2_x1, dup2_x2, dup_x1, dup_—

x2, f2d, f2i, f2l, fadd, faload, fastore, fempg, fempl, fconst_<

f>

, fdiv, fload, fload_<

n>

, fmod, fmul, fneg, freturn, fstore, fstore_<

n>

, fsub, gatfield, getstatic, goto, i2d, i2f, i2l, iadd, iaload, iand, iastore, iconst_<

n>

, iconst_m1, idiv, if_acmpeq, if_acmpne, if_icmpeq, if_icmpge, if_icmpgt, if_icmple, if_icmplt, if_icmpne, ifeq, ifge, ifgt, ifle, iflt, ifne, iinc, iload, iload_<

n>

, imod, imul, ineg, instanceof, int2byte, int2char, invokeinterface, invokemethod, invokesuper, ior, ireturn, ishl, Ishr, istore, istore_<

n>

, isub, iushr, ixor, jsr, 12d, 12f, 12i, ladd, laload, land, lastore, lcmp, lconst_<

1>

, ldc1, ldc2, ldc2w, ldiv, lload, lload_<

n>

, lmod, lmul, lneg, lookupswitch, lor, lreturn, lshl, lshr, lstore, lstore_<

n>

, lsub, lushr, lxor, monitorenter, monitorexit, new, newarray, newfromname, nop, pop, pop2, putfield, putstatic, ret, return, saload, sastore, siaload, siastore, sipush, tableswitch, and verifystack.

51. The computer system of claim 44, wherein the program verifier includes instructions for certifying that the program complies with a stack non-overflow constraint and a stack non-underflow constraint.

52. The computer system of claim 44, wherein the program verifier includes instructions using a virtual stack to track the type state of the stack.

53. The computer system of claim 44, wherein the program verifier includes instructions using an array of virtual local variables to track a type state of local variables used by the program.

54. A computer program product for use in conjunction with a computer system, the computer program product comprising a computer readable storage medium and a computer program mechanism embedded therein, the computer program mechanism comprising:

a program verifier for analyzing a program formed of low-level, stack-oriented, program code, the program verifier including instructions for verifying at run time, prior to execution, that when an instruction of the program is executed that can be executed along more than one execution path, a number of operands on a stack when arriving at that instruction during execution is identical regardless of the execution path taken to arrive at the instruction, and a type state of the stack when arriving at the instruction during execution of a first execution path that includes the instruction is compatible with a type state of the stack when arriving at the instruction during execution of all other execution paths that include the instruction.

55. The computer program product of claim 54, wherein the verifying instructions include instructions for confirming prior to execution of the program that a number of operands on the stack when arriving at the instruction that can be executed along more than one execution path is identical for all execution paths that include the instruction, even when the stack is not empty prior to execution of the instruction.

56. The computer program product of claim 54, wherein the verifying instructions include instructions for confirming prior to execution of the program that execution of any loop in the program will not result in a net addition or deletion of operands on the stack.

57. The computer program product of claim 54, wherein the verifying instructions include instructions for verifying prior to execution that when a loop of the program is executed, immediately before and after each iteration of the loop, a number of operands on the stack is identical, even when the stack is not empty, and a type associated with each of the operands on the stack is compatible regardless of how many times the loop is executed.

58. The computer program product of claim 54, further including a program execution module having instructions for executing the program without performing a check during execution of the program that corresponds to a check performed by the program verifier.

59. The computer program product of claim 54, wherein each instruction of the program comprises one or more bytecodes, and wherein the program verifier includes instructions for determining whether execution of any bytecoded instruction in the program would violate predetermined data type restrictions for that instruction.

60. The computer program product of claim 54, wherein at least one instruction of the program comprises one or more bytecodes that represent an operation on a specific data type and is selected from the group consisting of:

aaload, aastore, aconst_null, aload, areturn, arraylength, astore, astore_<

n>

, athrow, bipush, breakpoint, catchsetup, catchteardown, checkcast, df2, d2i, d2l, dadd, daload, dastore, dcmpg, dcmpl, dconst_<

d>

, ddiv, dload, dload_<

d>

, dmod, dmul, dneg, dreturn, dstore, dstore_<

n>

, dsub, dup, dup2, dup2_x1, dup2_x2, dup_x1, dup_—

x2, f2d, f2i, f2l, fadd, faload, fastore, fempg, fempl, fconst_<

f>

, fdiv, fload, fload_<

n>

, fmod, fmul, fneg, freturn, fstore, fstore_<

n>

, fsub, gatfield, getstatic, goto, i2d, i2f, i2l, iadd, iaload, iand, iastore, iconst_<

n>

, iconst_m1, idiv, if_acmpeq, if_acmpne, if_icmpeq, if_icmpge, if_icmpgt, if_icmple, if_icmplt, if_icmpne, ifeq, ifge, ifgt, ifle, iflt, ifne, iinc, iload, iload_<

n>

, imod, imul, ineg, instanceof, int2byte, int2char, invokeinterface, invokemethod, invokesuper, ior, ireturn, ishl, Ishr, istore, istore_<

n>

, isub, iushr, ixor, jsr, 12d, 12f, 12i, ladd, laload, land, lastore, lcmp, lconst_<

1>

, ldc1, ldc2, ldc2w, ldiv, lload, lload_<

n>

, lmod, lmul, lneg, lookupswitch, lor, lreturn, lshl, lshr, lstore, lstore_<

n>

, lsub, lushr, lxor, monitorenter, monitorexit, new, newarray, newfromname, nop, pop, pop2, putfield, putstatic, ret, return, saload, sastore, siaload, siastore, sipush, tableswitch, and verifystack.

61. The computer program product of claim 54, wherein the program verifier includes instructions for certifying that the program complies with a stack non-overflow constraint and a stack non-underflow constraint.

62. The computer program product of claim 54, wherein the program verifier includes instructions using a virtual stack to track the type state of the stack.

63. The computer program product of claim 54, wherein the program verifier includes instructions using an array of virtual local variables to track a type state of local variables used by the program.

64. A method of operating a computer system, comprising:

receiving from a source computer a program formed of low-level, stack-oriented, program code;

verifying at run time, prior to execution, that when an instruction of the program is executed that can be executed along more than one execution path, a number of operands on a stack when arriving at that instruction during execution is identical for all execution paths that include the instruction, and a type state of the stack when arriving at the instruction during execution of a first execution path that includes the instruction is compatible with a type state of the stack when arriving at the instruction during execution of all other execution paths that include the instruction; and

executing the verified program.

65. The method of claim 64, wherein the verifying comprises confirming prior to execution of the program that a number of operands on the stack when arriving at the instruction that can be executed along more than one execution path is identical for all execution paths that include the instruction, even when the stack is not empty prior to execution of the instruction.

66. The method of claim 64, wherein the verifying includes confirming prior to execution of the program that execution of any loop in the program will not result in a net addition or deletion of operands on the stack.

67. The method of claim 64, wherein the verifying includes confirming prior to execution of the program that execution of any loop in the program will not result in a net addition or deletion of operands on the stack.

68. The method of claim 64, wherein the verifying includes verifying prior to execution that when a loop of the program is executed that, immediately before and after each iteration of the loop, a number of operands on the stack is identical, even when the stack is not empty, and a type state of the stack remains compatible with an initial type state of the stack regardless of how many times the loop is executed.

69. The method of claim 64, wherein the executing includes executing the program without performing a check during execution of the program that corresponds to a check performed by the verifying.

70. The method of claim 64, wherein each instruction of the program comprises one or more bytecodes, and wherein the verifying includes determining whether execution of any bytecoded instruction in the program would violate predetermined data type restrictions for that instruction.

71. The method of claim 64, wherein at least one instruction of the program comprises one or more bytecodes that represent an operation on a specific data type and is selected from the group consisting of:

aaload, aastore, aconst_null, aload, areturn, arraylength, astore, astore_<

n>

, athrow, bipush, breakpoint, catchsetup, catchteardown, checkcast, df2, d2i, d2l, dadd, daload, dastore, dcmpg, dcmpl, dconst_<

d>

, ddiv, dload, dload_<

d>

, dmod, dmul, dneg, dreturn, dstore, dstore_<

n>

, dsub, dup, dup2, dup2_x1, dup2_x2, dup_x1, dup_—

x2, f2d, f2i, f2l, fadd, faload, fastore, fempg, fempl, fconst_<

f>

, fdiv, fload, fload_<

n>

, fmod, fmul, fneg, freturn, fstore, fstore_<

n>

, fsub, gatfield, getstatic, goto, i2d, i2f, i2l, iadd, iaload, iand, iastore, iconst_<

n>

, iconst_m1, idiv, if_acmpeq, if_acmpne, if_icmpeq, if_icmpge, if_icmpgt, if_icmple, if_icmplt, if_icmpne, ifeq, ifge, ifgt, ifle, iflt, ifne, iinc, iload, iload_<

n>

, imod, imul, ineg, instanceof, int2byte, int2char, invokeinterface, invokemethod, invokesuper, ior, ireturn, ishl, Ishr, istore, istore_<

n>

, isub, iushr, ixor, jsr, 12d, 12f, 12i, ladd, laload, land, lastore, lcmp, lconst_<

l>

, ldc1, ldc2, ldc2w, ldiv, lload, lload_<

n>

, lmod, lmul, lneg, lookupswitch, lor, lreturn, lshl, lshr, lstore, lstore_<

n>

, lsub, lushr, lxor, monitorenter, monitorexit, new, newarray, newfromname, nop, pop, pop2, putfield, putstatic, ret, return, saload, sastore, siaload, siastore, sipush, tableswitch, and verifystack.

72. The method of claim 64, wherein the verifying includes certifying that the program complies with a stack non-overflow constraint and a stack non-underflow constraint.

73. The method of claim 64, wherein the verifying includes using a virtual stack to track the type state of the stack.

74. The method of claim 64, wherein the verifying includes using an array of virtual local variables to track a type state of local variables used by the program.

75. A computer system, comprising:

an interface for receiving a program formed of low-level, stack-oriented, program code;

memory for storing the program;

a data processing unit for executing programs stored in the memory;

a program verifier, stored in the memory and executed by the data processing unit, the program verifier including instructions for verifying prior to execution that when an instruction of the program is executed that can be executed along more than one execution path, a number of operands on a stack when arriving at that instruction during execution is identical regardless of the execution path taken to arrive at the instruction, and a type state of the stack when arriving at the instruction during execution of a first execution path that includes the instruction is compatible with a type state of the stack when arriving at the instruction during execution of all other execution paths that include the instruction; and

a program execution module for executing the verified program.

76. The computer system of claim 75, wherein the verifying instructions include instructions for confirming prior to execution of the program that the number of operands on the stack when arriving at the instruction that can be executed along more than one execution path is identical for all execution paths that include the instruction, even when the stack is not empty prior to execution of the instruction.

77. The computer system of claim 75, wherein the verifying instructions include instructions for confirming prior to execution of the program that execution of any loop in the program will not result in a net addition or deletion of operands on the stack.

78. The computer system of claim 75, wherein the program execution module does not check for overflow and underflow of the stack when executing the verified program.

79. The computer system of claim 75, wherein the verifying instructions include instructions for verifying prior to execution that when a loop of the program is executed, immediately before and after each iteration of the loop, a number of operands on the stack is identical, even when the stack is not empty, and a type state of the stack remains compatible with an initial type state of the stack regardless of how many times the loop is executed.

80. The computer system of claim 75, wherein the program execution module includes instructions for executing the program without performing a check during execution of the program that corresponds to a check performed by the program verifier.

81. The computer system of claim 75, wherein each instruction of the program comprises one or more bytecodes, and wherein the program verifier includes instructions for determining whether execution of any bytecoded instruction in the program would violate predetermined data type restrictions for that instruction.

82. The computer system of claim 75, wherein at least one instruction of the program comprises one or more bytecodes that represent an operation on a specific data type and is selected from the group consisting of:

aaload, aastore, aconst_null, aload, areturn, arraylength, astore, astore_<

n>

, athrow, bipush, breakpoint, catchsetup, catchteardown, checkcast, df2, d2i, d2l, dadd, daload, dastore, dcmpg, dcmpl, dconst_<

d>

, ddiv, dload, dload_<

d>

, dmod, dmul, dneg, dreturn, dstore, dstore_<

n>

, dsub, dup, dup2, dup2_x1, dup2_x2, dup_x1, dup_—

x2, f2d, f2i, f2l, fadd, faload, fastore, fempg, fempl, fconst_<

f>

, fdiv, fload, fload_<

n>

, fmod, fmul, fneg, freturn, fstore, fstore_<

n>

, fsub, gatfield, getstatic, goto, i2d, i2f, i2l, iadd, iaload, iand, iastore, iconst_<

n>

, iconst_m1, idiv, if_acmpeq, if_acmpne, if_icmpeq, if_icmpge, if_icmpgt, if_icmple, if_icmplt, if_icmpne, ifeq, ifge, ifgt, ifle, iflt, ifne, iinc, iload, iload_<

n>

, imod, imul, ineg, instanceof, int2byte, int2char, invokeinterface, invokemethod, invokesuper, ior, ireturn, ishl, Ishr, istore, istore_<

n>

, isub, iushr, ixor, jsr, 12d, 12f, 12i, ladd, laload, land, lastore, lcmp, lconst_<

l>

, ldc1, ldc2, ldc2w, ldiv, lload, lload_<

n>

, lmod, lmul, lneg, lookupswitch, lor, lreturn, lshl, lshr, lstore, lstore_<

n>

, lsub, lushr, lxor, monitorenter, monitorexit, new, newarray, newfromname, nop, pop, pop2, putfield, putstatic, ret, return, saload, sastore, siaload, siastore, sipush, tableswitch, and verifystack.

83. The computer system of claim 75, wherein the program verifier includes instructions for certifying that the program complies with a stack non-overflow constraint and a stack non-underflow constraint.

84. The computer system of claim 75, wherein the program verifier includes instructions using a virtual stack to track the type state of the stack.

85. The computer system of claim 75, wherein the program verifier includes instructions using an array of virtual local variables to track a type state of local variables used by the program.

86. The computer system of claim 75, wherein the program is platform independent, and wherein the interface is configured to receive the program from a remote device.

87. The computer system of claim 75, wherein the interface is configured to receive the program from a remote device.

88. A method of operating a computer system, comprising:

providing a program formed of low-level, stack-oriented, program code;

verifying, at run time, that when an instruction of the program is executed that can be executed along more than one execution path, a number of operands on a stack when arriving at that instruction during execution is identical for all execution paths that include the instruction, even when the stack is not empty, and a type state of the stack when arriving at the instruction during execution of a first execution path that includes the instruction is compatible with a type state of the stack when arriving at the instruction during execution of all other execution paths that include the instruction; and

executing the verified program.

89. The method of claim 88, wherein the verifying includes confirming prior to execution of the program that the number of operands on the stack when arriving at the instruction that can be executed along more than one execution path is identical for all execution paths that include the instruction, even when the stack is not empty prior to execution of the instruction.

90. The method of claim 88, wherein the verifying includes confirming prior to execution of the program that execution of any loop in the program will not result in a net addition or deletion of operands on the stack.

91. The method of claim 88, wherein when the program is executed no check is made for overflow and underflow of the stack.

92. The method of claim 88, wherein the verifying includes verifying prior to execution that when a loop of the program is executed, immediately before and after each iteration of the loop, a number of operands on the stack is identical, even when the stack is not empty, and a type state of the stack remains compatible with an initial type state of the stack regardless of how many times the loop is executed.

93. The method of claim 88, wherein the executing includes, when the program has been verified, executing the program without performing a check during execution of the program that corresponds to a check performed during the verifying.

94. The method of claim 88, wherein each instruction of the program comprises one or more bytecodes, and wherein the verifying includes determining whether execution of any bytecoded instruction in the program would violate predetermined data type restrictions for that instruction.

95. The method of claim 88, wherein at least one instruction of the program comprises one or more bytecodes that represent an operation on a specific data type and is selected from the group consisting of:

aaload, aastore, aconst_null, aload, areturn, arraylength, astore, astore_<

n>

, athrow, bipush, breakpoint, catchsetup, catchteardown, checkcast, df2, d2i, d2l, dadd, daload, dastore, dcmpg, dcmpl, dconst_<

d>

, ddiv, dload, dload_<

d>

, dmod, dmul, dneg, dreturn, dstore, dstore_<

n>

, dsub, dup, dup2, dup2_x1, dup2_x2, dup_x1, dup_—

x2, f2d, f2i, f2l, fadd, faload, fastore, fempg, fempl, fconst_<

f>

, fdiv, fload, fload_<

n>

, fmod, fmul, fneg, freturn, fstore, fstore_<

n>

, fsub, gatfield, getstatic, goto, i2d, i2f, i2l, iadd, iaload, iand, iastore, iconst_<

n>

, iconst_m1, idiv, if_acmpeq, if_acmpne, if_icmpeq, if_icmpge, if_icmpgt, if_icmple, if_icmplt, if_icmpne, ifeq, ifge, ifgt, ifle, iflt, ifne, iinc, iload, iload_<

n>

, imod, imul, ineg, instanceof, int2byte, int2char, invokeinterface, invokemethod, invokesuper, ior, ireturn, ishl, Ishr, istore, istore_<

n>

, isub, iushr, ixor, jsr, 12d, 12f, 12i, ladd, laload, land, lastore, lcmp, lconst_<

l>

, ldc1, ldc2, ldc2w, ldiv, lload, lload_<

n>

, lmod, lmul, lneg, lookupswitch, lor, lreturn, lshl, lshr, lstore, lstore_<

n>

, lsub, lushr, lxor, monitorenter, monitorexit, new, newarray, newfromname, nop, pop, pop2, putfield, putstatic, ret, return, saload, sastore, siaload, siastore, sipush, tableswitch, and verifystack.

96. The method of claim 88, wherein the verifying includes certifying that the program complies with a stack non-overflow constraint and a stack non-underflow constraint.

97. The method of claim 88, wherein the verifying is performed using a virtual stack to track the type state of the stack.

98. The method of claim 88, wherein the verifying is performed using an array of virtual local variables to track a type state of local variables used by the program.

99. The method of claim 88, wherein the program is platform independent, and wherein the providing includes receiving the program from a remote device.

100. The method of claim 88, wherein the providing includes receiving the program from a remote device.

101. The method of claim 88, wherein the verifying occurs at a point in time prior to execution of the program by the computer system.

103. A method of operating a computer system, comprising:

receiving a program formed of low-level, stack-oriented, program code from a server over a network;

determining whether the program successfully completed a verification process, wherein the verification process verifies, prior to execution of the program, that when an instruction of the program is executed that can be executed along more than one execution path, a number of operands on a stack when arriving at that instruction during execution is identical for all execution paths that include the instruction regardless of the execution path taken to arrive at the instruction, and a type state of the stack when arriving at the instruction during execution of a first execution path that includes the instruction is compatible with a type state of the stack when arriving at the instruction during execution of all other execution paths that include the instruction; and

executing or aborting execution of the program based on a result of the determination.

104. The method of claim 103, wherein when the program is executed no check is made to verify that when an instruction of the program is executed that can be executed along more than one execution path, a number of operands on a stack when arriving at that instruction is identical regardless of the execution path taken to arrive at the instruction, and no check is made during execution of the program that a type state of the stack when arriving at the instruction during execution of the first execution path is compatible with a type state of the stack when arriving at the instruction during execution of all other execution paths that include the instruction.

105. The method of claim 103, wherein when the program is executed no check is made for overflow and underflow of the stack.

106. The method of claim 103, wherein the executing includes executing the program without performing a check during execution of the program that corresponds to a check performed during the verification process.

107. The method of claim 103, wherein each instruction of the program comprises one or more bytecodes, and wherein the verification process determines whether execution of any bytecoded instruction in the program would violate predetermined data type restrictions for that instruction.

108. The method of claim 103, wherein at least one instruction of the program comprises one or more bytecodes that represent an operation on a specific data type and is selected from the group consisting of:

aaload, aastore, aconst_null, aload, areturn, arraylength, astore, astore_<

n>

, athrow, bipush, breakpoint, catchsetup, catchteardown, checkcast, df2, d2i, d2l, dadd, daload, dastore, dcmpg, dcmpl, dconst_<

d>

, ddiv, dload, dload_<

d>

, dmod, dmul, dneg, dreturn, dstore, dstore_<

n>

, dsub, dup, dup2, dup2_x1, dup2_x2, dup_x1, dup_—

x2, f2d, f2i, f2l, fadd, faload, fastore, fempg, fempl, fconst_<

f>

, fdiv, fload, fload_<

n>

, fmod, fmul, fneg, freturn, fstore, fstore_<

n>

, fsub, gatfield, getstatic, goto, i2d, i2f, i2l, iadd, iaload, iand, iastore, iconst_<

n>

, iconst_m1, idiv, if_acmpeq, if_acmpne, if_icmpeq, if_icmpge, if_icmpgt, if_icmple, if_icmplt, if_icmpne, ifeq, ifge, ifgt, ifle, iflt, ifne, iinc, iload, iload_<

n>

, imod, imul, ineg, instanceof, int2byte, int2char, invokeinterface, invokemethod, invokesuper, ior, ireturn, ishl, Ishr, istore, istore_<

n>

, isub, iushr, ixor, jsr, 12d, 12f, 12i, ladd, laload, land, lastore, lcmp, lconst_<

l>

, ldc1 ldc2, ldc2w, ldiv, lload, lload_<

n>

, lmod, lmul, lneg, lookupswitch, lor, Ireturn, lshl, lshr, lstore, lstore_<

n>

, lsub, lushr, lxor, monitorenter, monitorexit, new, newarray, newfromname, nop, pop, pop2, putfield, putstatic, ret, return, saload, sastore, siaload, siastore, sipush, tableswitch, and verifystack.

109. A computer system, comprising:

an interface for receiving a program formed of low-level, stack-oriented, program code;

memory for storing the program;

a data processing unit for executing programs stored in the memory;

a first module for determining whether the program successfully completed a verification process, wherein the verification process verifies, prior to execution of the program, that when an instruction of the program is executed that can be executed along more than one execution path, a number of operands on a stack when arriving at that instruction during execution is identical for all execution paths that include the instruction regardless of the execution path taken to arrive at the instruction, and a type state of the stack when arriving at the instruction during execution of a first execution path that includes the instruction is compatible with a type state of the stack when arriving at the instruction during execution of all other execution paths that include the instruction; and

a program execution module for executing or aborting based on a result generated by the first module.

110. The computer system of claim 109, wherein the verification process verifies that the number of operands on the stack when arriving at the instruction that can be executed along more than one execution path is identical for all execution paths that include the instruction, even when the stack is not empty prior to execution of the instruction.

111. The computer system of claim 109, wherein the verification process verifies that execution of any loop in the program will not result in a net addition or deletion of operands on the stack.

112. The computer system of claim 109, wherein the program execution module does not check for overflow and underflow of the stack when executing the verified program.

113. The computer system of claim 109, wherein the verification process verifies that when a loop of the program is executed, immediately before and after each iteration of the loop, a number of operands on the stack is identical, even when the stack is not empty, and a type state of the stack remains compatible with an initial type state of the stack regardless of how many times the loop is executed.

114. The computer system of claim 109, wherein the program execution module includes instructions for executing the program without performing a check during execution of the program that corresponds to a check performed by the program verifier.

115. The computer system of claim 109, wherein each instruction of the program comprises one or more bytecodes, and wherein the verification process determines whether execution of any bytecoded instruction in the program would violate predetermined data type restrictions for that instruction.

116. The computer system of claim 109, wherein at least one instruction of the program comprises one or more bytecodes that represent an operation on a specific data type and is selected from the group consisting of:

aaload, aastore, aconst_null, aload, areturn, arraylength, astore, astore_<

n>

, athrow, bipush, breakpoint, catchsetup, catchteardown, checkcast, df2, d2i, d2l, dadd, daload, dastore, dcmpg, dcmpl, dconst_<

d>

, ddiv, dload, dload_<

d>

, dmod, dmul, dneg, dreturn, dstore, dstore_<

n>

, dsub, dup, dup2, dup2_x1, dup2_x2, dup_x1, dup_—

x2, f2d, f2i, f2l, fadd, faload, fastore, fempg, fempl, fconst_<

f>

, fdiv, fload, fload_<

n>

, fmod, fmul, fneg, freturn, fstore, fstore_<

n>

, fsub, gatfield, getstatic, goto, i2d, i2f, i2l, iadd, iaload, iand, iastore, iconst_<

n>

, iconst_m1, idiv, if_acmpeq, if_acmpne, if_icmpeq, if_icmpge, if_icmpgt, if_icmple, if_icmplt, if_icmpne, ifeq, ifge, ifgt, ifle, iflt, ifne, iinc, iload, iload_<

n>

, imod, imul, ineg, instanceof, int2byte, int2char, invokeinterface, invokemethod, invokesuper, ior, ireturn, ishl, Ishr, istore, istore_<

n>

, isub, iushr, ixor, jsr, 12d, 12f, 12i, ladd, laload, land, lastore, lcmp, lconst_<

l>

, ldc1, ldc2, ldc2w, ldiv, lload, lload_<

n>

, lmod, lmul, lneg, lookupswitch, lor, lreturn, lshl, lshr, lstore, lstore_<

n>

, lsub, lushr, lxor, monitorenter, monitorexit, new, newarray, newfromname, nop, pop, pop2, putfield, putstatic, ret, return, saload, sastore, siaload, siastore, sipush, tableswitch, and verifystack.

117. The computer system of claim 109, wherein the verification process verifies that the program complies with a stack non-overflow constraint and a stack non-underflow constraint.

118. A computer program product for use in conjunction with a computer system, the computer program product comprising a computer readable storage medium and a computer program mechanism embedded therein, the computer program mechanism comprising:

a first module for determining whether the program successfully completed a verification process, wherein the verification process verifies, prior to execution of the program, that when an instruction of the program is executed that can be executed along more than one execution path, a number of operands on a stack when arriving at that instruction during execution is identical for all execution paths that include the instruction regardless of the execution path taken to arrive at the instruction, and a type state of the stack when arriving at the instruction during execution of a first execution path that includes the instruction is compatible with a type state of the stack when arriving at the instruction during execution of all other execution paths that include the instruction; and

a program execution module for executing or aborting based on a result generated by the first module.

119. The computer program product of claim 118, wherein the verification process verifies that the number of operands on the stack when arriving at the instruction that can be executed along more than one execution path is identical for all execution paths that include the instruction, even when the stack is not empty prior to execution of the instruction.

120. The computer program product of claim 118, wherein the verification process verifies that execution of any loop in the program will not result in a net addition or deletion of operands on the stack.

121. The computer program product of claim 118, wherein the program execution module does not check for overflow and underflow of the stack when executing the verified program.

122. The computer program product of claim 118, wherein the verification process verifies that when a loop of the program is executed, immediately before and after each iteration of the loop, a number of operands on the stack is identical, even when the stack is not empty, and a type state of the stack remains compatible with an initial type state of the stack regardless of how many times the loop is executed.

123. The computer program product of claim 118, wherein the program execution module includes instructions for executing the program without performing a check during execution of the program that corresponds to a check performed by the program verifier.

124. The computer program product of claim 118, wherein each instruction of the program comprises one or more bytecodes, and wherein the verification process determines whether execution of any bytecoded instruction in the program would violate predetermined data type restrictions for that instruction.

125. The computer program product of claim 118, wherein at least one instruction of the program comprises one or more bytecodes that represent an operation on a specific data type and is selected from the group consisting of:

aaload, aastore, aconst_null, aload, areturn, arraylength, astore, astore_<

n>

, athrow, bipush, breakpoint, catchsetup, catchteardown, checkcast, df2, d2i, d2l, dadd, daload, dastore, dcmpg, dcmpl, dconst_<

d>

, ddiv, dload, dload_<

d>

, dmod, dmul, dneg, dreturn, dstore, dstore_<

n>

, dsub, dup, dup2, dup2_x1, dup2_x2, dup_x1, dup_—

x2, f2d, f2i, f2l, fadd, faload, fastore, fempg, fempl, fconst_<

f>

, fdiv, fload, fload_<

n>

, fmod, fmul, fneg, freturn, fstore, fstore_<

n>

, fsub, gatfield, getstatic, goto, i2d, i2f, i2l, iadd, iaload, iand, iastore, iconst_<

n>

, iconst_m1, idiv, if_acmpeq, if_acmpne, if_icmpeq, if_icmpge, if_icmpgt, if_icmple, if_icmplt, if_icmpne, ifeq, ifge, ifgt, ifle, iflt, ifne, iinc, iload, iload_<

n>

, imod, imul, ineg, instanceof, int2byte, int2char, invokeinterface, invokemethod, invokesuper, ior, ireturn, ishl, Ishr, istore, istore_<

n>

, isub, iushr, ixor, jsr, 12d, 12f, 12i, ladd, laload, land, lastore, lcmp, lconst_<

l>

, ldc1, ldc2, ldc2w, ldiv, lload, lload_<

n>

, lmod, lmul, lneg, lookupswitch, lor, lreturn, lshl, lshr, lstore, lstore_<

n>

, lsub, lushr, lxor, monitorenter, monitorexit, new, newarray, newfromname, nop, pop, pop2, putfield, putstatic, ret, return, saload, sastore, siaload, siastore, sipush, tableswitch, and verifystack.

126. The computer program product of claim 118, wherein the verification process verifies that the program complies with a stack non-overflow constraint and a stack non-underflow constraint.

127. A method of operating a computer system, comprising the steps of:

providing a program formed of low-level, stack-oriented, program code;

verifying at run time, prior to execution, that when a loop of the program is executed that, immediately before and after each iteration of the loop, a number of operands on a stack is identical, even when the stack is not empty, and a type state of the stack before a first iteration of the loop is compatible with a type state of the stack after the each iteration of the loop regardless of how many times the loop is executed; and

executing the verified program.

128. The method of claim 127, wherein the executing includes, when the program has been verified, executing the program without performing a check during execution of the program that corresponds to a check performed during the verifying.

129. The method of claim 127, wherein each instruction of the program comprises one or more bytecodes, and wherein the verifying includes determining whether execution of any bytecoded instruction in the program would violate predetermined data type restrictions for that instruction.

130. The method of claim 127, wherein at least one instruction of the program comprises one or more bytecodes that represent an operation on a specific data type and is selected from the group consisting of:

aaload, aastore, aconst_null, aload, areturn, arraylength, astore, astore_<

n>

, athrow, bipush, breakpoint, catchsetup, catchteardown, checkcast, df2, d2i, d2l, dadd, daload, dastore, dcmpg, dcmpl, dconst_<

d>

, ddiv, dload, dload_<

d>

, dmod, dmul, dneg, dreturn, dstore, dstore_<

n>

, dsub, dup, dup2, dup2_x1, dup2_x2, dup_x1, dup_—

x2, f2d, f2i, f2l, fadd, faload, fastore, fempg, fempl, fconst_<

f>

, fdiv, fload, fload_<

n>

, fmod, fmul, fneg, freturn, fstore, fstore_<

n>

, fsub, gatfield, getstatic, goto, i2d, i2f, i2l, iadd, iaload, iand, iastore, iconst_<

n>

, iconst_m1, idiv, if_acmpeq, if_acmpne, if_icmpeq, if_icmpge, if_icmpgt, if_icmple, if_icmplt, if_icmpne, ifeq, ifge, ifgt, ifle, iflt, ifne, iinc, iload, iload_<

n>

, imod, imul, ineg, instanceof, int2byte, int2char, invokeinterface, invokemethod, invokesuper, ior, ireturn, ishl, Ishr, istore, istore_<

n>

, isub, iushr, ixor, jsr, 12d, 12f, 12i, ladd, laload, land, lastore, lcmp, lconst_<

l>

, ldc1, ldc2, ldc2w, ldiv, lload, lload_<

n>

, lmod, lmul, lneg, lookupswitch, lor, lreturn, lshl, lshr, lstore, lstore_<

n>

, lsub, lushr, lxor, monitorenter, monitorexit, new, newarray, newfromname, nop, pop, pop2, putfield, putstatic, ret, return, saload, sastore, siaload, siastore, sipush, tableswitch, and verifystack.

131. The method of claim 127, wherein the verifying includes certifying that the program complies with a stack non-overflow constraint and a stack non-underflow constraint.

132. The method of claim 127, wherein the verifying is performed using a virtual stack to track the type state of the stack.

133. The method of claim 127, wherein the verifying is performed using an array of virtual local variables to track a type state of local variables used by the program.

134. The method of claim 127, wherein the program is platform independent, and wherein the providing includes receiving the program from a remote device.

135. The method of claim 127, wherein the providing includes receiving the program from a remote device.

157. The method of claim 127, wherein the program is platform independent, and wherein the providing includes receiving the program from a remote device.

158. The method of claim 127, wherein the providing includes receiving the program from a remote device.

136. A computer system, comprising:

memory for storing a program formed of low-level, stack-oriented, program code;

a data processing unit for executing programs stored in the memory;

a program verifier, stored in the memory and executed by the data processing unit, the program verifier including instructions for verifying prior to execution that when a loop of the program is executed that, immediately before and after each iteration of the loop, a number of operands on a stack is identical, even when the stack is not empty, and a type state of the stack before a first iteration of the loop is compatible with a type state of the stack after the each iteration of the loop regardless of how many times the loop is executed; and

a program execution module for executing the verified program.

137. The computer system of claim 136, including a program execution module for executing the program, when the program has been verified by the program verifier, without performing a check during execution of the program that corresponds to a check performed by the program verifier.

138. The computer system of claim 136, wherein each instruction of the program comprises one or more bytecodes, and wherein the program verifier includes instructions for determining whether execution of any bytecoded instruction in the program would violate predetermined data type restrictions for that instruction.

139. The computer system of claim 136, wherein at least one instruction of the program comprises one or more bytecodes that represent an operation on a specific data type and is selected from the group consisting of:

aaload, aastore, aconst_null, aload, areturn, arraylength, astore, astore_<

n>

, athrow, bipush, breakpoint, catchsetup, catchteardown, checkcast, df2, d2i, d2l, dadd, daload, dastore, dcmpg, dcmpl, dconst_<

d>

, ddiv, dload, dload_<

d>

, dmod, dmul, dneg, dreturn, dstore, dstore_<

n>

, dsub, dup, dup2, dup2_x1, dup2_x2, dup_x1, dup_—

x2, f2d, f2i, f2l, fadd, faload, fastore, fempg, fempl, fconst_<

f>

, fdiv, fload, fload_<

n>

, fmod, fmul, fneg, freturn, fstore, fstore_<

n>

, fsub, gatfield, getstatic, goto, i2d, i2f, i2l, iadd, iaload, iand, iastore, iconst_<

n>

, iconst_m1, idiv, if_acmpeq, if_acmpne, if_icmpeq, if_icmpge, if_icmpgt, if_icmple, if_icmplt, if_icmpne, ifeq, ifge, ifgt, ifle, iflt, ifne, iinc, iload, iload_<

n>

, imod, imul, ineg, instanceof, int2byte, int2char, invokeinterface, invokemethod, invokesuper, ior, ireturn, ishl, Ishr, istore, istore_<

n>

, isub, iushr, ixor, jsr, 12d, 12f, 12i, ladd, laload, land, lastore, lcmp, lconst_<

l>

, ldc1, ldc2, ldc2w, ldiv, lload, lload_<

n>

, lmod, lmul, lneg, lookupswitch, lor, lreturn, lshl, lshr, lstore, lstore_<

n>

, lsub, lushr, lxor, monitorenter, monitorexit, new, newarray, newfromname, nop, pop, pop2, putfield, putstatic, ret, return, saload, sastore, siaload, siastore, sipush, tableswitch, and verifystack.

140. The computer system of claim 136, wherein the program verifier includes instructions for certifying that the program complies with a stack non-overflow constraint and a stack non-underflow constraint.

141. The computer system of claim 136, wherein the program verifier includes instructions using a virtual stack to track the type state of the stack.

142. The computer system of claim 136, wherein the program verifier includes instructions using an array of virtual local variables to track a type state of local variables used by the program.

143. A computer program product for use in conjunction with a computer system, the computer program product comprising a computer readable storage medium and a computer program mechanism embedded therein, the computer program mechanism comprising:

a program verifier, for analyzing a program formed of low-level, stack-oriented, program code;

the program verifier including instructions for verifying prior to execution of the program that when a loop of the program is executed that, immediately before and after each iteration of the loop, a number of operands on a stack is identical, even when the stack is not empty, and a type state of the stack before a first iteration of the loop is compatible with a type state of the stack after the each iteration of the loop regardless of how many times the loop is executed; and

a program execution module for executing the verified program.

144. The computer program product of claim 143, including a program execution module for executing the program, when the program has been verified by the program verifier, without performing a check during execution of the program that corresponds to a check performed by the program verifier.

145. The computer program product of claim 143, wherein each instruction of the program comprises one or more bytecodes, and wherein the program verifier includes instructions for determining whether execution of any bytecoded instruction in the program would violate predetermined data type restrictions for that instruction.

146. The computer program product of claim 143, wherein at least one instruction of the program comprises one or more bytecodes that represent an operation on a specific data type and is selected from the group consisting of:

aaload, aastore, aconst_null, aload, areturn, arraylength, astore, astore_<

n>

, athrow, bipush, breakpoint, catchsetup, catchteardown, checkcast, df2, d2i, d2l, dadd, daload, dastore, dcmpg, dcmpl, dconst_<

d>

, ddiv, dload, dload_<

d>

, dmod, dmul, dneg, dreturn, dstore, dstore_<

n>

, dsub, dup, dup2, dup2_x1, dup2_x2, dup_x1, dup_—

x2, f2d, f2i, f2l, fadd, faload, fastore, fempg, fempl, fconst <

f>

, fdiv, fload, fload_<

n>

, fmod, fmul, fneg, freturn, fstore, fstore_<

n>

, fsub, gatfield, getstatic, goto, i2d, i2f, i2l, iadd, iaload, iand, iastore, iconst_<

n>

, iconst_m1, idiv, if_acmpeq, if_acmpne, if_icmpeq, if_icmpge, if_icmpgt, if_icmple, if_icmplt, if_icmpne, ifeq, ifge, ifgt, ifle, iflt, ifne, iinc, iload, iload_<

n>

, imod, imul, ineg, instanceof, int2byte, int2char, invokeinterface, invokemethod, invokesuper, ior, ireturn, ishl, Ishr, istore, istore_<

n>

, isub, iushr, ixor, jsr, 12d, 12f, 12i, ladd, laload, land, lastore, lcmp, lconst_<

l>

, ldc1, ldc2, ldc2w, ldiv, lload, lload_<

n>

, lmod, lmul, lneg, lookupswitch, lor, lreturn, lshl, lshr, lstore, lstore_<

n>

, lsub, lushr, lxor, monitorenter, monitorexit, new, newarray, newfromname, nop, pop, pop2, putfield, putstatic, ret, return, saload, sastore, siaload, siastore, sipush, tableswitch, and verifystack.

147. The computer program product of claim 143, wherein the program verifier includes instructions for certifying that the program complies with a stack non-overflow constraint and a stack non-underflow constraint.

148. The computer program product of claim 143, wherein the program verifier includes instructions using a virtual stack to track the type state of the stack.

149. The computer program product of claim 143, wherein the program verifier includes instructions using an array of virtual local variables to track a type state of local variables used by the program.

150. A method of operating a computer system, comprising:

receiving a program formed of low-level, stack-oriented, program code from a server over a network;

determining whether the program successfully completed a verification process, wherein the verification process verifies, prior to execution of the program, that when a loop of the program is executed that, immediately before and after each iteration of the loop, a number of operands on a stack is identical and a type state of the stack before a first iteration of the loop is compatible with a type state of the stack after the each iteration of the loop regardless of how many times the loop is executed; and

executing or aborting execution of the program based on a result of the determination.

151. The method of claim 150, wherein when the program is executed no check is made to verify that when a loop of the program is executed that, immediately before and after each iteration of the loop, a number of operands on the stack is identical and no check is made to verify that a type state of the stack before a first iteration of the loop is compatible with a type state of the stack after the each iteration of the loop regardless of how many times the loop is executed.

152. The method of claim 150, wherein each instruction of the program comprises one or more bytecodes, and wherein the verification process determines whether execution of any bytecoded instruction in the program would violate predetermined data type restrictions for that instruction.

153. The method of claim 150, wherein at least one instruction of the program comprises one or more bytecodes that represent an operation on a specific data type and is selected from the group consisting of:

aaload, aastore, aconst_null, aload, areturn, arraylength, astore, astore_<

n>

, athrow, bipush, breakpoint, catchsetup, catchteardown, checkcast, df2, d2i, d2l, dadd, daload, dastore, dcmpg, dcmpl, dconst_<

d>

, ddiv, dload, dload_<

d>

, dmod, dmul, dneg, dreturn, dstore, dstore_<

n>

, dsub, dup, dup2, dup2_x1, dup2_x2, dup_x1, dup_—

x2, f2d, f2i, f2l, fadd, faload, fastore, fempg, fempl, fconst_<

f>

, fdiv, fload, fload_<

n>

, fmod, fmul, fneg, freturn, fstore, fstore_<

n>

, fsub, gatfield, getstatic, goto, i2d, i2f, i2l, iadd, iaload, iand, iastore, iconst_<

n>

, iconst_m1, idiv, if_acmpeq, if_acmpne, if_icmpeq, if_icmpge, if_icmpgt, if_icmple, if_icmplt, if_icmpne, ifeq, ifge, ifgt, ifle, iflt, ifne, iinc, iload, iload_<

n>

, imod, imul, ineg, instanceof, int2byte, int2char, invokeinterface, invokemethod, invokesuper, ior, ireturn, ishl, Ishr, istore, istore_<

n>

, isub, iushr, ixor, jsr, 12d, 12f, 12i, ladd, laload, land, lastore, lcmp, lconst_<

l>

, ldc1, ldc2, ldc2w, ldiv, lload, lload_<

n>

, lmod, lmul, lneg, lookupswitch, lor, lreturn, lshl, lshr, lstore, lstore_<

n>

, lsub, lushr, lxor, monitorenter, monitorexit, new, newarray, newfromname, nop, pop, pop2, putfield, putstatic, ret, return, saload, sastore, siaload, siastore, sipush, tableswitch, and verifystack.

154. The method of claim 150, wherein the verification process certifies that the program complies with a stack non-overflow constraint and a stack non-underflow constraint.

155. The method of claim 150, wherein the verification process uses a virtual stack to track the type state of the stack.

156. The method of claim 150, wherein the verification process uses an array of virtual local variables to track a type state of local variables used by the program.

159. A computer system, comprising:

an interface for receiving a program formed of low-level, stack-oriented, program code;

memory for storing the program;

a data processing unit for executing programs stored in the memory;

a first module for determining whether the program successfully completed a verification process, wherein the verification process verifies, prior to execution of the program, that when a loop of the program is executed that, immediately before and after each iteration of the loop, a number of operands on a stack is identical, even when the stack is not empty, and a type state of the stack before a first iteration of the loop is compatible with a type state of the stack after the each iteration of the loop regardless of how many times the loop is executed; and

a program execution module for executing or aborting execution of the program based on a result of the determination.

160. The computer system of claim 159, wherein the program execution module is configured to execute the program without checking to verify that when a loop of the program is executed that, immediately before and after each iteration of the loop, a number of operands on the stack is identical and without checking to verify that a type state of the stack before a first iteration of the loop is compatible with a type state of the stack after the each iteration of the loop regardless of how many times the loop is executed.

161. The computer system of claim 159, wherein each instruction of the program comprises one or more bytecodes, and wherein the verification process determines whether execution of any bytecoded instruction in the program would violate predetermined data type restrictions for that instruction.

162. The computer system of claim 159, wherein at least one instruction of the program comprises one or more bytecodes that represent an operation on a specific data type and is selected from the group consisting of:

aaload, aastore, aconst_null, aload, areturn, arraylength, astore, astore_<

n>

, athrow, bipush, breakpoint, catchsetup, catchteardown, checkcast, df2, d2i, d2l, dadd, daload, dastore, dcmpg, dcmpl, dconst_<

d>

, ddiv, dload, dload_<

d>

, dmod, dmul, dneg, dreturn, dstore, dstore_<

n>

, dsub, dup, dup2, dup2_x1, dup2_x2, dup_x1, dup_—

x2, f2d, f2i, f2l, fadd, faload, fastore, fempg, fempl, fconst_<

f>

, fdiv, fload, fload_<

n>

, fmod, fmul, fneg, freturn, fstore, fstore_<

n>

, fsub, gatfield, getstatic, goto, i2d, i2f, i2l, iadd, iaload, iand, iastore, iconst_<

n>

, iconst_m1, idiv, if_acmpeq, if_acmpne, if_icmpeq, if_icmpge, if_icmpgt, if_icmple, if_icmplt, if_icmpne, ifeq, ifge, ifgt, ifle, iflt, ifne, iinc, iload, iload_<

n>

, imod, imul, ineg, instanceof, int2byte, int2char, invokeinterface, invokemethod, invokesuper, ior, ireturn, ishl, Ishr, istore, istore_<

n>

, isub, iushr, ixor, jsr, 12d, 12f, 12i, ladd, laload, land, lastore, lcmp, lconst_<

1>

, ldc1, ldc2, ldc2w, ldiv, lload, lload_<

n>

, lmod, lmul, lneg, lookupswitch, lor, lreturn, lshl, lshr, lstore, lstore_<

n>

, lsub, lushr, lxor, monitorenter, monitorexit, new, newarray, newfromname, nop, pop, pop2, putfield, putstatic, ret, return, saload, sastore, siaload, siastore, sipush, tableswitch, and verifystack.

163. The computer system of claim 159, wherein the verification process certifies that the program complies with a stack non-overflow constraint and a stack non-underflow constraint.

164. The computer system of claim 159, wherein the verification process uses a virtual stack to track the type state of the stack.

165. The computer system of claim 159, wherein the verification process uses an array of virtual local variables to track a type state of local variables used by the program.

166. A computer program product for use in conjunction with a computer system, the computer program product comprising a computer readable storage medium and a computer program mechanism embedded therein, the computer program mechanism comprising:

a first module for determining whether the program successfully completed a verification process, wherein the verification process verifies, prior to execution of the program, that when a loop of the program is executed that, immediately before and after each iteration of the loop, a number of operands on a stack is identical, even when the stack is not empty, and a type state of the stack before a first iteration of the loop is compatible with a type state of the stack after the each iteration of the loop regardless of how many times the loop is executed; and

a program execution module for executing or aborting execution of the program based on a result of the determination.

167. The computer program product of claim 166, wherein the program execution module is configured to execute the program without checking to verify that when a loop of the program is executed that, immediately before and after each iteration of the loop, a number of operands on the stack is identical and without checking to verify that a type state of the stack before a first iteration of the loop is compatible with a type state of the stack after the each iteration of the loop regardless of how many times the loop is executed.

168. The computer program product of claim 166, wherein each instruction of the program comprises one or more bytecodes, and wherein the verification process determines whether execution of any bytecoded instruction in the program would violate predetermined data type restrictions for that instruction.

169. The computer program product of claim 166, wherein at least one instruction of the program comprises one or more bytecodes that represent an operation on a specific data type and is selected from the group consisting of:

aaload, aastore, aconst_null, aload, areturn, arraylength, astore, astore_<

n>

, athrow, bipush, breakpoint, catchsetup, catchteardown, checkcast, df2, d2i, d2l, dadd, daload, dastore, dcmpg, dcmpl, dconst_<

d>

, ddiv, dload, dload_<

d>

, dmod, dmul, dneg, dreturn, dstore, dstore_<

n>

, dsub, dup, dup2, dup2_x1, dup2_x2, dup_x1, dup_—

x2, f2d, f2i, f2l, fadd, faload, fastore, fempg, fempl, fconst_<

f>

, fdiv, fload, fload_<

n>

, fmod, fmul, fneg, freturn, fstore, fstore_<

n>

, fsub, gatfield, getstatic, goto, i2d, i2f, i2l, iadd, iaload, iand, iastore, iconst_<

n>

, iconst_m1, idiv, if_acmpeq, if_acmpne, if_icmpeq, if_icmpge, if_icmpgt, if_icmple, if_icmplt, if_icmpne, ifeq, ifge, ifgt, ifle, iflt, ifne, iinc, iload, iload_<

n>

, imod, imul, ineg, instanceof, int2byte, int2char, invokeinterface, invokemethod, invokesuper, ior, ireturn, ishl, Ishr, istore, istore_<

n>

, isub, iushr, ixor, jsr, 12d, 12f, 12i, ladd, laload, land, lastore, lcmp, lconst_<

l>

, ldc1, ldc2, ldc2w, ldiv, lload, lload_<

n>

, lmod, lmul, lneg, lookupswitch, lor, lreturn, lshl, lshr, lstore, lstore_<

n>

, lsub, lushr, lxor, monitorenter, monitorexit, new, newarray, newfromname, nop, pop, pop2, putfield, putstatic, ret, return, saload, sastore, siaload, siastore, sipush, tableswitch, and verifystack.

170. The computer program product of claim 166, wherein the verification process certifies that the program complies with a stack non-overflow constraint and a stack non-underflow constraint.

171. The computer program product of claim 166, wherein the verification process uses a virtual stack to track the type state of the stack.

172. The computer program product of claim 166, wherein the verification process uses an array of virtual local variables to track a type state of local variables used by the program.