System and method for pre-verification of stack usage in bytecode program loops

• US 6,704,923 B1
• Filed: 02/28/2000
• Issued: 03/09/2004
• Est. Priority Date: 12/20/1994
• Status: Expired due to Fees

• Current Assignee: Sun Microsystems Incorporated (Oracle Corporation)
• Original Assignee: Sun Microsystems Incorporated (Oracle Corporation)
• Inventors: Gosling, James A.
• Primary Examiner(s): NAHAR, QAMRUN
• Application Number:
  US09/514,536
• Time in Patent Office: 1,471 Days
• Field of Search: 717/3-8
• US Class Current: 717/126
• CPC Class Codes: G06F 11/3604 Software analysis for verifying properties of programs byte-code verification G06F9/44589
• CPC Class Codes: G06F 9/44589 Program code verification, e.g. Java bytecode verification, proof-carrying code high-level semantic checks G06F8/43; testing and debugging software G06F11/36

Abstract

The present invention provides a verifier for use in conjunction with programs utilizing data type specific bytecodes for verifying the proper operation of the executable program prior to actual execution by a host processor. A verifier is provided which includes a virtual stack for temporarily storing stack information which parallels the typical stack operations required during the execution a bytecode program. The verifier also includes a stack snapshot storage structure having a snapshot directory and stack snapshot storage area for storing the state of the virtual stack at various points during program verification so as to assure proper stack manipulations by the source program. A two step source program verification process is provided for in which the source program is initially loaded into the verifier and a first pass source program evaluation is performed. During the first pass, the addresses of all source program target destinations resulting from conditional or un-conditional jumps are stored in sequential order in the stack snapshot directory. The source program is then reloaded and a verification of stack manipulations is performed using a virtual stack and the stack snapshot storage structure to verify proper stack manipulations by the source program. Upon completion, the source program may be interpreted, or compiled, or converted into another executable format as required by an individual user.

Claims

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

(A) storing a program in a memory, the program including a sequence of bytecodes, where each of a multiplicity of the bytecodes represents an operation on data of a specific data type;

each bytecode having associated data type restrictions on the data type of data to be manipulated by that bytecode;

(B) prior to execution of the program, preprocessing the program by;

(B1) determining the state of a virtual stack associated with the program before execution of each bytecode in the program, the virtual stack state storing data type values for operands that would be stored in an operand stack during execution of the program;

(B2) determining whether execution of any bytecode in the program would violate the data type restrictions for that bytecode and generating a program fault signal when execution of any bytecode in the program would violate the data type restrictions for that bytecode; and

(B3) determining whether execution of any loop in the program would result in a net addition or deletion of operands to the operand stack and generating a program fault signal when execution of any loop in the program would produce a net addition or deletion of operands to the operand stack;

(C) when the preprocessing of the program results in the generation of no program fault signals, enabling execution of the program; and

(D) when the preprocessing of the program results in the generation of a program fault, preventing execution of the program;

wherein step (B) includes determining, whenever a location in the program can be immediately preceded in execution by two or more distinct bytecodes in the program, at least one of the two or more distinct bytecodes in the program comprising a jump/branch bytecode, whether the states of the virtual stack subsequent to execution of each of the two or more distinct bytecodes in the program are compatible with each other, and generating a program fault if the virtual stack states are not compatible.

2. The method of claim 1, further including the steps of:

when execution of the program has been enabled, executing the program without performing operand stack underflow and overflow checks during execution of the program and without performing data type checks on operands stored in the operand stack during execution of the program.

3. The method of claim 1,

step B includes:

during a first pass through the program, identifying all locations in the program that are the target of conditional and/or unconditional jump/branch instructions, and storing a list of those program locations in a snapshot list, and

during a second pass through the program, processing each bytecode in the program, including processing each jump/branch bytecode in the program by;

(A) determining for each successor program location, comprising each program location in the snapshot list that contains a bytecode that is executable immediately after the jump/branch bytecode being processed, whether or not a snapshot of the virtual stack state for that program location has previously been stored, (B) if the determination is positive, comparing the virtual stack state subsequent to the execution of the jump/branch bytecode being processed with the previously stored virtual stack state snapshot for the successor program location and generating a program fault signal if the virtual stack state is not compatible with the previously stored virtual stack state snapshot for the successor program location, and (C) if the determination is negative, storing a snapshot for the successor program location, comprising a snapshot of the virtual stack state subsequent to the execution of the jump/branch bytecode being processed.

4. The method of claim 1,

step B including, processing each bytecode in the program, including processing at least a subset of the bytecodes in the program by:

(B4A) determining if a snapshot for a successor program location, comprising a program location that contains a bytecode executable immediately after the bytecode being processed, has previously been stored, (B4B) if the determination is positive, comparing the virtual stack state subsequent to the execution of the jump/branch bytecode being processed with the previously stored virtual stack state snapshot for the successor program location and generating a program fault signal if the virtual stack state is not compatible with the previously stored virtual stack state snapshot for the successor program location, and (B4C) if the determination is negative, storing a snapshot for the successor program location, comprising a snapshot of the virtual stack state subsequent to the execution of the jump/branch bytecode being processed.

5. A computer system, comprising:

memory for storing a program, the program including a sequence of bytecodes, where each of a multiplicity of the bytecodes each represents an operation on data of a specific data type;

each bytecode having associated data type restrictions on the data type of data to be manipulated by that bytecode;

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

a bytecode program verifier, stored in the memory, the bytecode program verifier including;

stack status tracking instructions for determining the state of a virtual stack associated with the program before execution of each bytecode in the program, the virtual stack state storing data type values for operands that would be stored in an operand stack during execution of the program;

data type testing instructions for determining whether execution of any bytecode in the program would violate the data type restrictions for that bytecode and generating a program fault signal when execution of any bytecode in the program would violate the data type restrictions for that bytecode; and

stack overflow/underflow testing instructions for determining (A) whether execution of the program would result in an operand stack underflow or overflow, and (B) whether execution of any loop in the program would result in a net addition or deletion of operands to the operand stack and generating a program fault signal when execution of any loop in the program would produce a net addition or deletion of operands to the operand stack; and

program execution enabling instructions that enables execution of the program only after processing the program by the bytecode program verifier generates no program fault signals;

wherein the data type testing instructions determine, whenever a location in the program can be immediately preceded in execution by two or more distinct bytecodes in the program, at least one of the two or more distinct bytecodes in the program comprising a jump/branch bytecode, whether the states of the virtual stack subsequent to execution of each of the two or more distinct bytecodes in the program are compatible with each other, and generating a program fault if the virtual stack states are not compatible.

6. The system of claim 5, wherein

the data type and stack overflow/underflow testing instructions include instructions for:

during a first pass through the program, identifying all locations in the program that are the target of conditional and/or unconditional jump/branch instructions, and storing a list of those program locations in a snapshot list, and

during a second pass through the program, processing each bytecode in the program, including processing each jump/branch bytecode in the program by;

(A) determining for each successor program location, comprising each program location in the snapshot list that contains a bytecode that is executable immediately after the jump/branch bytecode being processed, whether or not a snapshot of the virtual stack state for that program location has previously been stored, (B) it the determination is positive, comparing the virtual stack state subsequent to the execution of the jump/branch bytecode being processed with the previously stored virtual stack state snapshot for the successor program location and generating a program fault signal if the virtual stack state is not compatible with the previously stored virtual stack state snapshot for the successor program location, and (C) if the determination is negative, storing a snapshot for the successor program location, comprising a snapshot of the virtual stack state subsequent to the execution of the jump/branch bytecode being processed.

7. The system of claim 5, wherein

the data type and stack overflow/underflow testing instructions include instructions for processing each bytecode in the program, including processing at least a subset of the bytecodes in the program by:

(A) determining if a snapshot for a successor program location, comprising a program location that contains a bytecode executable immediately after the bytecode being processed, has previously been stored, (B) if the determination is positive, comparing the virtual stack state subsequent to the execution of the jump/branch bytecode being processed with the previously stored virtual stack state snapshot for the successor program location and generating a program fault signal if the virtual stack state is not compatible with the previously stored virtual stack state snapshot for the successor program location, and (C) if the determination is negative, storing a snapshot for the successor program location, comprising a snapshot of the virtual stack state subsequent to the execution of the jump/branch bytecode being processed.

8. A computer storage media for storing data and programs executable by a computer system, the computer storage media comprising:

a bytecode program verifier, stored in the computer storage media, the bytecode program verifier including;

stack status tracking instructions for determining the state of a virtual stack associated with the program before execution of each bytecode in the program, the virtual stack state storing data type values for operands that would be stored in an operand stack during execution of the program;

data type testing instructions for determining whether execution of any bytecode in the program would violate the data type restrictions for that bytecode and generating a program fault signal when execution of any bytecode in the program would violate the data type restrictions for that bytecode; and

stack overflow/underflow testing instructions for determining (A) whether execution of the program would result in an operand stack underflow or overflow, and (B) whether execution of any loop in the program would result in a net addition or deletion of operands to the operand stack and generating a program fault signal when execution of any loop in the program would produce a net addition or deletion of operands to the operand stack; and

program execution enabling instructions that enables execution of the program only after processing the program by the bytecode program verifier generates no program fault signals;

wherein the data type testing instructions determine, whenever a location in the program can be immediately preceded in execution by two or more distinct bytecodes in the program, at least one of the two or more distinct bytecodes in the program comprising a jump/branch bytecode, whether the states of the virtual stack subsequent to execution of each of the two or more distinct bytecodes in the program are compatible with each other, and generating a program fault if the virtual stack states are not compatible.

9. The computer storage media of claim 8, wherein

the data type and stack overflow/underflow testing instructions include instructions for:

during a first pass through the program, identifying all locations in the program that are the target of conditional and/or unconditional jump/branch instructions, and storing a list of those program locations in a snapshot list, and

during a second pass through the program, processing each bytecode in the program, including processing each jump/branch bytecode in the program by;

(A) determining for each successor program location, comprising each program location in the snapshot list that contains a bytecode that is executable immediately after the jump/branch bytecode being processed, whether or not a snapshot of the virtual stack state for that program location has previously been stored, (B) if the determination is positive, comparing the virtual stack state subsequent to the execution of the jump/branch bytecode being processed with the previously stored virtual stack state snapshot for the successor program location and generating a program fault signal if the virtual stack state is not compatible with the previously stored virtual stack state snapshot for the successor program location, and (C) if the determination is negative, storing a snapshot for the successor program location, comprising a snapshot of the virtual stack state subsequent to the execution of the jump/branch bytecode being processed.

10. The computer storage media of claim 8, wherein

the data type and stack overflow/underflow testing instructions include instructions for processing each bytecode in the program, including processing at least a subset of the bytecodes in the program by:

(A) determining if a snapshot for a successor program location, comprising a program location that contains a bytecode executable immediately after the bytecode being processed, has previously been stored, (B) if the determination is positive, comparing the virtual stack state subsequent to the execution of the jump/branch bytecode being processed with the previously stored virtual stack state snapshot for the successor program location and generating a program fault signal if the virtual stack state is not compatible with the previously stored virtual stack state snapshot for the successor program location, and (C) if the determination is negative, storing a snapshot for the successor program location, comprising a snapshot of the virtual stack state subsequent to the execution of the jump/branch bytecode being processed.