REGISTER  |  SIGN IN
United States Patent6477702
Yellin , ; et al.November 5, 2002
Title
Bytecode program interpreter apparatus and method with pre-verification of data type restrictions and object initialization
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.
Inventors:Yellin; Frank (Redwood City, CA), Gosling; James A.  (Woodside, CA)
Assignee:Sun Microsystems, Inc. (Santa Clara, CA)
Appl. No.:711053
Filed:November 9, 2000
Current U.S. Class:717/126 
Field of Search:717/126
U.S. Patent Documents
3878513April 1975Werner
4521851June 1985Trubisky et al.
4524416June 1985Stanley et al.
4622013November 1986Cerchio
4742215May 1988Daughters et al.
5165465November 1992Kenet
5179734January 1993Candy et al.
5187799February 1993McAuley et al.
5220522June 1993Wilson et al.
5283864February 1994Knowlton
5307499April 1994Yin
5347632September 1994Filepp et al.
5422992June 1995Motoyama et al.
5446875August 1995Ogisu et al.
5450575September 1995Sites
5590329December 1996Goodnow, II et al.
5640503June 1997Alpert et al.
5668999September 1997Gosling
5740441April 1998Yellin et al.
5748964May 1998Gosling
5925125July 1999Alpert et al.
5978574November 1999Sharma
5999731December 1999Yellin et al.
6075940June 2000Gosling
6247171June 2001Yellin et al.
Foreign Patent Documents
0 424 056Oct., 1990EP
0 718 764Dec., 1995EP
Other References
Mili et al., A system for Classifying Program Verification . . . , 1984, IEEE, p. 499-509.
Primary Examiner: Morse; Gregory
Assistant Examiner: Chavis; John Q.
Attorney, Agent or Firm:Pennie & Edmonds LLP
Parent Case Text


This application is a continuation of patent application Ser. No. 09/454,821, filed Dec. 6, 1999, which was a continuation of patent application Ser. No. 09/046,719, filed Mar. 24, 1998, now U.S. Pat. No. 5,999,731, which was a continuation of patent application Ser. No. 08/575,291, filed Dec. 20, 1995, now U.S. Pat. No. 5,740,441, which was a continuation-in-part of patent application Ser. No. S/N 08/360,202, filed Dec. 20, 1994, now U.S. Pat. No. 5,748,964.
Claims

What is claimed is:
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.

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.
102. The computer program product of claim 23, wherein the program is platform independent.
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.
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.
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.
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.
Description


The present invention relates generally to the use of computer software on multiple computer platforms which use distinct underlying machine instruction sets, and more specifically to an program verifier and method that verify the integrity of computer software obtained from a network server or other source.

BACKGROUND OF THE INVENTION

Referring to FIG. 1, in a networked computer system 100, a first computer 102 may download a computer program 103 residing on a second computer 104. In this example, the first user node 102 will typically be a user workstation (often called a client) having a central processing unit 106, a user interface 108, memory 110 (e.g., random access memory and disk memory) for storing an operating system 112, programs, documents and other data, and a communications interface 114 for connecting to a computer network 120 such as the Internet, a local area network or a wide area network. The computers 102 and 104 are often called "nodes on the network" or "network nodes".

The second computer 104 will often be a network server, but may be a second user workstation, and typically would contain the same basic array of computer components as the first computer.

In the prior art (unlike the system shown in FIG. 1), after the first computer 102 downloads a copy of a computer program 103 from the second computer 104, there are essentially no standardized tools available to help the user of the first computer 102 to verify the integrity of the downloaded program 103. In particular, unless the first computer user studies the source code of the downloaded program, it is virtually impossible using prior art tools to determine whether the downloaded program 103 will underflow or overflow its stack, or whether the downloaded program 103 will violate files and other resources on the user's computer.

A second issue with regard to downloading computer software from one computer to another concerns transferring computer software between computer platforms which use distinct underlying machine instruction sets. There are some prior art examples of platform independent computer programs and platform independent computer programming languages. What the prior art lacks are reliable and automated software verification tools for enabling recipients of such software to verify the integrity of transferred platform independent computer software obtained from a network server or other source.

SUMMARY OF THE INVENTION

The present invention verifies the integrity of computer programs written in a bytecode language, commercialized as the JAVA bytecode language, which uses a restricted set of data type specific bytecodes. All the available source code bytecodes in the language either (A) are stack data consuming bytecodes that have associated data type restrictions as to the types of data that can be processed by each such bytecode, (B) do not utilize stack data but affect the stack by either adding data of known data type to the stack or by removing data from the stack without regard to data type, or (C) neither use stack data nor add data to the stack.

The present invention provides a verifier tool and method for identifying, prior to execution of a bytecode program, any instruction sequence that attempts to process data of the wrong type for such a bytecode or if the execution of any bytecode instructions in the specified program would cause underflow or overflow of the operand stack, and to prevent the use of such a program.

The bytecode program verifier of the present invention includes a virtual operand stack for temporarily storing stack information indicative of data stored in a program operand stack during the actual execution a specified bytecode program. The verifier processes the specified program using data flow analysis, processing each bytecode instruction of the program whose stack and register input status map is affected by another instruction processed by the verifier. A stack and register input status map is generated for every analyzed bytecode instruction, and when an instruction is a successor to multiple other instructions, its status map is generated by merging the status maps created during the processing of each of the predecessor instructions. The verifier also compares the stack and register status map information with data type restrictions associated with each bytecode instruction so as to determine if the operand stack or registers during program execution would contain data inconsistent with the data type restrictions of the bytecode instruction, and also determines if any bytecode instructions in the specified program would cause underflow or overflow of the operand stack.

The merger of stack and register status maps requires special handling for the instructions associated with exception handlers and the instructions associated with subroutine calls (including "finally" instruction blocks that are executed via a subroutine call whenever a protected code block is exited).

After pre-processing of the program by the verifier, if no program faults were found, a bytecode program 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.

BRIEF DESCRIPTION OF THE DRAWINGS

The accompanying drawings, which are incorporated in and form a part of this specification, illustrate embodiments of the invention and, together with the description, serve to explain the principles of the invention, wherein:

FIG. 1 is a block diagram of a computer system incorporating a preferred embodiment of the present invention.

FIG. 2 is a block diagram of the data structure for an object in a preferred embodiment of the present invention.

FIG. 3 is a block diagram of the data structures maintained by a bytecode verifier during verification of a bytecode program in accordance with the present invention.

FIGS. 4A-4G represents flow charts of the bytecode program verification process in the preferred embodiment of the present invention.

FIG. 5 represents a flow chart of the class loader and bytecode program interpreter process in the preferred embodiment of the present invention.

DETAILED DESCRIPTION OF THE PREFERRED EMBODIMENTS

Reference will now be made in detail to the preferred embodiments of the invention, examples of which are illustrated in the accompanying drawings. While the invention will be described in conjunction with the preferred embodiments, it will be understood that they are not intended to limit the invention to those embodiments. On the contrary, the invention is intended to cover alternatives, modifications and equivalents, which may be included within the spirit and scope of the invention as defined by the appended claims.

Referring now to a distributed computer system 100 as shown in FIG. 1, there is shown a distributed computer system 100 having multiple client computers 102 and multiple server computers 104. In the preferred embodiment, each client computer 102
is connected to the servers 104 via the Internet 120, although other types of communication connections could be used. While most client computers are desktop computers, such as Sun workstations, IBM compatible computers and Macintosh computers, virtually any type of computer can be a client computer. In the preferred embodiment, each client computer includes a CPU 106, a user interface 108, memory 110, and a communications interface 114. Memory 110 stores: an operating system 112; an Internet communications manager program 116; a bytecode program verifier 120 for verifying whether or not a specified program satisfies certain predefined integrity criteria; a bytecode program interpreter 122 for executing application programs; a class loader
124, which loads object classes into a user's address space and utilizes the bytecode program verifier to verify the integrity of the methods associated with each loaded object class; at least one class repository 126, for locally storing object classes
128 in use and/or available for use by user's of the computer 102; at least one object repository 130 for storing objects 132, which are instances of objects of the object classes stored in the object repository 126.

In the preferred embodiment the operating system 112 is an object oriented multitasking operating system that supports multiple threads of execution within each defined address space.

The bytecode program verifier 120 includes a snapshot array 140, a status array 142, and other data structures that will be described in more detail below.

The class loader 124 is typically invoked when a user first initiates execution of a procedure, requiring that an object of the appropriate object class be generated. The class loader 124 loads in the appropriate object class and calls the bytecode program verifier 120 to verify the integrity of all the bytecode programs in the loaded object class. If all the methods are successfully verified an object instance of the object class is generated, and the bytecode interpreter 122 is invoked to execute the user requested procedure, which is typically called a method. If the procedure requested by the user is not a bytecode program and if execution of the non-bytecode program is allowed (which is outside the scope of the present document), the program is executed by a compiled program executer (not shown).

The class loader is also invoked whenever an executing bytecode program encounters a call to an object method for an object class that has not yet been loaded into the user's address space. Once again the class loader 124 loads in the appropriate object class and calls the bytecode program verifier 120 to verify the integrity of all the bytecode programs in the loaded object class. In many situations the object class will be loaded from a remotely located computer, such as one of the servers 104 shown in FIG. 1. If all the methods in the loaded object class are successfully verified, an object instance of the object class is generated, and the bytecode interpreter 122 is invoked to execute the called object method.

FIG. 2 shows the data structure 200 in a preferred embodiment of the present invention for an object A-01 of class A. An object of object class A has an object handle 202 that includes a pointer 204 to the methods for the object and a pointer 206
to a data array 208 for the object.

The pointer 204 to the object's methods is actually an indirect pointer to the methods of the associated object class. More particularly, the method pointer 204 points to the Virtual Function Table (VFT) 210 for the object's object class. Each object class has a VFT 210 that includes (A) pointers 212 to each of the methods 214 of the object class, (B) one or more pointers 215 to methods 216 associated with superclasses of class A, and (C) a pointer 217 to a special Class Object 218.

Referring to FIGS. 1 and 2, in the preferred embodiment, the methods in an object class to be loaded are bytecode programs, which when interpreted will result in a series of executable instructions. A listing of all the source code bytecode instructions in the JAVA instruction set is provided in Table 1. The JAVA bytecode instruction set is characterized by bytecode instructions that are data type specific. Specifically, the JAVA instruction set distinguishes the same basic operation on different primitive data types by designating separate opcodes. Accordingly, a plurality of bytecodes are included within the instruction set to perform the same basic function (for example to add two numbers), with each such bytecode being used to process only data of a corresponding distinct data type. In addition, the JAVA instruction set is notable for instructions not included. For instance, there are no instructions in the JAVA bytecode language for converting numbers into object references. These restrictions on the JAVA bytecode instruction set help to ensure that any bytecode program which utilizes data in a manner consistent with the data type specific instructions in the JAVA instruction set will not violate the integrity of a users computer system.

In the preferred embodiment, the available data types are integer, long integer, single precision floating point, double precision floating point, handles (sometimes herein called objects or object references), and return addresses (pointers to virtual machine code). Additional data types are arrays of integers, arrays of long integers, arrays of single precision floating point numbers, arrays of double precision floating point numbers, arrays of handles, arrays of booleans, arrays of bytes (8-bit integers), arrays of short integers (16 bit signed integer), and arrays of unicode characters.

The "handle" data type includes a virtually unlimited number of data subtypes because each handle data type includes an object class specification as part of the data type. In addition, constants used in programs are also data typed, with the available constant data types in the preferred embodiment comprising the data types mentioned above, plus class, fieldref, methodref, string, and Asciz, all of which represent two or more bytes having a specific purpose.

The few bytecodes that are data type independent perform stack manipulation functions such as (A) duplicating one or more words on the stack and placing them at specific locations within the stack, thereby producing more stack items of known data type, or (B) clearing one or more items from the stack. A few other data type independent bytecodes do not utilize any words on the stack and leave the stack unchanged, or add words to the stack without utilizing any of the words previously on the stack. These bytecodes do not have any data type restrictions with regard to the stack contents prior to their execution, and all but a few modify the stack's contents and thus affect the program verification process.

The second computer node 104, assumed here to be configured as a file or other information server, includes a central processing unit 150, a user interface 156, memory 154, and a other communication interface 158 that connects the second computer node to the computer communication network 120. Memory 154 stores programs 103, 164, 166 for execution by the processor 150 and/or distribution to other computer nodes.

The first and second computer nodes 102 and 104 may utilize different computer platforms and operating systems 112, 160 such that object code programs executed on either one of the two computer nodes cannot be executed on the other. For instance, the server node 104 might be a Sun Microsystems computer using a Unix operating system while the user workstation node 102 may be an IBM compatible computer using an 80486 microprocessor and a Microsoft DOS operating system. Furthermore, other user workstations coupled to the same network and utilizing the same server 104 might use a variety of different computer platforms and a variety of operating systems.

In the past, a server 104 used for distributing software on a network having computers of many types would store distinct libraries of software for each of the distinct computer platform types (e.g., Unix, Windows, DOS, Macintosh, etc.). Thus, different versions of the same computer program might be stored in each of the libraries. However, using the present invention, many computer programs could be distributed by such a server using just a single, bytecode version of the program.

The bytecode verifier 120 is an executable program which verifies operand data type compatibility and proper stack manipulations in a specified bytecode (source) program 214 prior to the execution of the bytecode program by the processor 106
under the control of the bytecode interpreter 122. Each bytecode program has an associated verification status value that is True if the program's integrity is verified by the bytecode verifier 120, and it otherwise set to False.

During normal execution of programs using languages other than the Java bytecode language, the interpreter must continually monitor the operand stack for overflows (i.e., adding more data to the stack than the stack can store) and underflows (i.e., attempting to pop data off the stack when the stack is empty). Such stack monitoring must normally be performed for all instructions that change the stack's status (which includes most all instructions). For many programs, stack monitoring instructions executed by the interpreter account for approximately 80% of the execution time of an interpreted computed program.

For many purposes, particularly the integrity of downloaded computer programs, the Internet is a "hostile environment." A downloaded bytecode program may contain errors involving the data types of operands not matching the data type restrictions of the instructions using those operands, which may cause the program to be fail during execution. Even worse, a bytecode program might attempt to create object references (e.g., by loading a computed number into the operand stack and then attempting to use the computed number as an object handle) and to thereby breach the security and/or integrity of the user's computer.

Use of the bytecode verifier 120 in accordance with the present invention enables verification of a bytecode program's integrity and allows the use of an interpreter 122 which does not execute the usual stack monitoring instructions during program execution, thereby greatly accelerating the program interpretation process.

The Bytecode Program Verifier

Referring now to FIG. 3, the bytecode program verifier 120 (often called the "verifier") uses a few temporary data structures to store information it needs while verifying a specified bytecode program 300. In particular, the verifier 120 uses a set of data structures 142 for representing current stack and register status information, and a snapshot data structure 140 for representing the status of the virtual stack and registers just prior to the execution of each instruction in the program being verified. The current status data structures 142 include: a stack size indicator, herein called the stack counter 301, a virtual stack 302 that indicates the data types of all items in the virtual operand stack, a virtual register array 304 that indicates the data types of all items in the virtual registers, and a "jsr" bit vector array 306 that stores zero or more bit vectors associated with the zero or more subroutine calls required to reach the instruction currently being processed.

The stack counter 301, which indicates the number of stack elements that are currently in use (i.e., at the point in the method associated with the instruction currently being analyzed), is updated by the verifier 120 as it keeps track of the virtual stack manipulations so as to reflect the current number of virtual stack entries.

The virtual stack 302 stores data type information regarding each datum that will be stored by the bytecode program 300 in the virtual operand stack during actual execution of the program. In the preferred embodiment, the virtual stack 302 is used in the same way as a regular stack, except that instead of storing actual data and constants, the virtual stack 302 stores a data type indicator value for each datum that will be stored in the operand stack during actual execution of the program. Thus, for instance, if during actual execution the stack were to store three values: HandleToObjectA 5 1

the corresponding virtual stack entries will be R;Class A;initialized I I

where "R" in the virtual stack indicates an object reference, "Class A"indicates that class or type of the referenced object is "A", "initialized" indicates that the referenced object is an initialized object, and each "I" in the virtual stack indicates an integer. Furthermore, the stack counter 301 in this example would store a value of 3, corresponding to three values being stored in the virtual stack 302.

Data of each possible data type is assigned a corresponding virtual stack marker value, for instance: integer (I), long integer (L), single precision floating point number (F), double precision floating point number (D), byte (B), short (S), and object reference (R). The marker value for an object reference includes a value (e.g., "Class A") indicating the object type and a flag indicating if the object has been initialized. If this is an object that has been created by the current method, but has not yet been initialized, the marker value for the object reference also indicates the program location of the instruction that created the object instance being referenced.

The virtual register array 304 serves the same basic function as the virtual stack 302. That is, it is used to store data type information for registers used by the specified bytecode program. Since data is often transferred by programs between registers and the operand stack, the bytecode instructions performing such data transfers and otherwise using registers can be checked to ensure that the data values in the registers accessed by each bytecode instruction are consistent with the data type usage restrictions on those bytecode instructions.

The structure and use of the jsr bit vector array 306 will be described below in the discussion of the handling of subroutine jumps and returns.

While processing the specified bytecode program, for each datum that would be popped off the stack for processing by a bytecode instruction, the verifier pops off the same number of data type values off the virtual stack 302 and compares the data type values with the data type requirements of the bytecode. For each datum that would be pushed onto the stack by a bytecode instruction, the verifier pushes onto the virtual stack a corresponding data type value.

One aspect of program verification in accordance with present invention is verification that the number of the operands in the virtual stack 302 is identical every time a particular instruction is executed, and that the data types of operands in the virtual stack are compatible. If a particular bytecode instruction can be immediately preceded in execution by two or more different instructions, then the status of the virtual stack immediately after processing of each of those different predecessor instructions must be compared. Usually, at least one of the different preceding instructions will be a conditional or unconditional jump or branch instruction. A corollary of the above "stack consistency" requirement is that each program loop must not result in a net addition or reduction in the number of operands stored in the operand stack.

The stack snapshot array 140 is used to store "snapshots" of the stack counter 301, virtual stack 302, virtual register array 304 and jsr bit vector array 306. A separate snapshot 310 is stored for every instruction in the bytecode program. Each stored stack snapshot includes a "changed" flag 320, a stack counter 321, a stack status array 322, a register status array 324 and a variable length jsr bit vector array 326. The jsr bit vector array 326 is empty except for instructions that can only be reached via one or more jsr instructions.

The changed flag 320 is used to determine which instructions require further processing by the verifier, as will be explained below. The stack counter 321, stack status array 322, register status array 324, and jsr bit vector array 326 are based on the values stored in the data structures 301, 302, 304 and 306 at corresponding points in the verification process.

The snapshot storage structure 140 furthermore stores instruction addresses 328 (e.g., the absolute or relative address of each target instruction). Instruction addresses 328 are used by the verifier to make sure that no jump or branch instruction has a target that falls in the middle of a bytecode instruction.

As was described previously, the bytecode program 300 includes a plurality of data type specific instructions, each of which is evaluated by the verifier 120 of the present invention.

Referring now to FIGS. 4A-4F, and Table 2, the execution of the bytecode verifier program 120 will be described in detail. Table 2 lists a pseudocode representation of the verifier program. The pseudocode used in Table 2 utilizes universal computer language conventions. While the pseudocode employed here has been invented solely for the purposes of this description, it is designed to be easily understandable by any computer programmer skilled in the art.

As shown in FIG. 4A, a selected class file containing one or more bytecode methods is loaded (350) into the bytecode verifier 120 for processing. The verifier first performs a number of "non-bytecode" based tests (352) on the loaded class, including verifying: the class file's format; that the class is not a subclass of a "final" class; that no method in the class overrides a "final" method in a superclass; that each class, other than "Object," has a superclass; and that each class reference, field reference and method reference in the constant pool has a legal name, class and type signature

If any of these initial verification tests fail, an appropriate error message is displayed or printed, and the verification procedure exits with an abort return code (354).

Next, the verification procedure checks to see if all bytecode methods have been verified (356). If so, the procedure exits with a success return code (358). Otherwise, it selects a next bytecode method in the loaded object class file that requires verification (360).

The code for each method includes the following information: the maximum stack space needed by the method; the maximum number of registers used by the method; the actual bytecodes for executing the method; a table of exception handlers.

Each entry in the exception handlers tables gives a start and end offset into the bytecodes, an exception type, and the offset of a handler for the exception. The entry indicates that if an exception of the indicated type occurs within the code indicated by the starting and ending offsets, a handler for the exception will be found at the given handler offset.

After selecting a method to verify, the verifier initializes a number of data structures (362), including the stack counter 301, virtual stack 302, virtual register array 304, jsr bit vector array 306, and the snapshot array 140. The snapshot array is initialized as follows. The snapshot for the first instruction of the method is initialized to indicate that the stack is empty and the registers are empty except for data types indicated by the method's type signature, which indicates the initial contents of the registers. The snapshots for all other instructions are initialized to indicate that the instruction has not yet been visited.

In addition, the "changed" bit for the first instruction of the program is set, and a flag called VerificationSuccess is set to True (364). If the VerificationSuccess flag is still set to True when the verification procedure is finished (368), that indicates that the integrity of the method has been verified. If the VerificationSuccess flag is set to False when the verification procedure is finished, the method's integrity has not been verified, and therefore an error message is displayed or printed, and the verification procedure exits with an abort return code (354).

After these initial steps, a data flow analysis is performed on the selected method (366). The details of the data flow analysis, which forms the main part of the verification procedure, is discussed below with reference to FIG. 4B.

In summary, the verification procedure processes each method of the loaded class file until either all the bytecode methods are successfully verified, or the verification of any one of the methods fails.

Data Flow Analysis of Method

Referring to FIG. 4B and the corresponding portion of Table 2, the data flow analysis of the selected method is completed (382) when there are no instructions whose changed bit is set (380). Detection of any stack or register usage error during the analysis causes the VerificationSuccess flag to set to False and for the analysis to be stopped (382).

If there is at least one instruction whose changed bit is set (380), the procedure selects a next instruction whose changed bit is set (384). Any instruction whose changed bit is set can be selected.

The analysis of the selected instruction begins with the pre-existing snapshot for the selected instruction being loaded into the stack counter, virtual stack and the virtual register array, and jsr bit vector array, respectively (386). In addition, the changed bit for the selected instruction is turned off (386).

Next, the effect of the selected instruction on the stack and registers is emulated (388). More particularly, four types of "actions" performed by bytecode instructions are emulated and checked for integrity: stack pops, stack pushes, reading data from registers and writing data to registers. The detailed steps of this emulation process are described next with reference to FIGS. 4C-4G.

Referring to FIG. 4C, if the selected instruction pops data from the stack (450), the stack counter 301 is inspected (452) to determine whether there is sufficient data in the stack to satisfy the data pop requirements of the instruction. If the operand stack has insufficient data (452) for the current instruction, that is called a stack underflow, in which case an error signal or message is generated (454) identifying the place in the program that the stack underflow was detected. In addition, the verifier will then set a VerificationSuccess flag to False and abort (456) the verification process.

If no stack underflow condition is detected, the verifier will compare (458) the data type code information previously stored in the virtual stack with the data type requirements (if any) of the currently selected instruction. For example, if the opcode of the instruction being analyzed calls for an integer add of a value popped from the stack, the verifier will compare the operand information of the item in the virtual stack which is being popped to make sure that is of the proper data type, namely integer. If the comparison results in a match, then the verifier deletes (460) the information from the virtual stack associated with the entry being popped and updates the stack counter 301 to reflect the number of entries popped from the virtual stack 302.

If a mismatch is detected (458) between the stored operand information in the popped entry of the virtual stack 302 and the data type requirements of the currently selected instruction, then a message is generated (462) identifying the place in the bytecode program where the mismatch occurred. The verifier will then set the VerificationSuccess flag to False and abort (456) the verification process. This completes the stack pop verification process.

Referring to FIG. 4D, if the currently selected instruction pushes data onto the stack (470), the stack counter is inspected (472) to determine whether there is sufficient room in the stack to store t