US 5,987,252 A · Method and apparatus for statically analyzing a computer program for data dependencies

Abstract

A method and an apparatus analyze a computer program for dependencies of the program output on the program input. To analyze the program, the program is transformed by a function into a Boolean expression called a verification condition. An example of this function is the weakest liberal precondition. The verification condition characterizes a condition between the input and the output of the program that must be satisfied for the output to be independent of the input. A theorem prover evaluates the verification condition to determine whether the output would depend on the input if the program was executed. If the verification condition evaluates to true, then the output is independent of the input; false, then the output depends on the input.

Claims22

Dependent claims

A computerized method for providing secure information flow in a computer system by analyzing a computer program for data dependencies, comprising the steps of:

generating a representation of the computer program by applying a function for transforming the computer program, the representation including a verification condition indicating a relationship between input data including private data to the computer program and an output of the computer program;
and
evaluating the verification condition using a theorem prover to determine whether the output would depend on the private data if the program were executed;
and
preventing execution of the program when the evaluation produces a predefined failure result.

2 more elements

A computer program product for analyzing a computer program for data dependencies to preserve secure information flow, the 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 verification condition generator that generates a representation of the computer program by applying a function for transforming the computer program, the representation including a verification condition indicating a relationship between input data including private data to the computer program and an output of the computer program;
a theorem prover receiving the verification condition from the verification condition generator and evaluating the verification condition to determine whether the output would depend on the private data if the program were executed;
and
instructions for preventing evaluation of the program when the theorem prover produces a failure result.

1 more element

Dependencies are inferred from the claim text.

Method and apparatus for statically analyzing a computer program for data dependencies

Life of this patent

Method and apparatus for statically analyzing a computer program for data dependencies

Life of this patent

Abstract

Claims22