Method and apparatus for statically analyzing a computer program

Details Method and apparatus for statically analyzing a computer program Method and apparatus for statically analyzing a computer program

1997-09-19

1999-11-16

Hafiz, Tariq R.

G06F 945

Patent

active

059872527

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.

REFERENCES:
patent: 4814978 (1989-03-01), Dennis
patent: 5329626 (1994-07-01), Klein et al.
patent: 5513350 (1996-04-01), Griffin et al.
patent: 5680552 (1997-10-01), Netravali et al.
patent: 5754861 (1998-05-01), Kumar
patent: 5787287 (1998-06-01), Bharadwaj
Banatre et al., "Compile-time detection of information flow in sequential programs," 3.sup. rd European Symposium on Research in Computer Security (ESORICS), Brighton, UK, Nov. 1994.
Denning et al., "Certification of Programs for Secure Information Flow," ACM Jul. 1977, vol. 20, No. 7, Operating Systems, R. S. Gaines Editor, pp. 504-513.
Dijkstra, E.W., "States and Their Characterization," A Discipline of Programming, Prentice-Hall 1976, Chapter 2, pp. 10-37.
Harel, D., "First-Order Dynamic Logic," Lecture Notes in Computer Science, Editor: Goos et al, Springer-Verlag, 1979, pp. 7-2.3.
Hoare, C.A.R., "An Axiomatic Basis for Computer Programming," Communications of the ACM, vol. 12, No. 10, Oct. 1969.
Hoare, C.A.R., "Proof of correctness of data representations," Acta Informatica, 1(4), 271-81, Springer-Verlag GmbH 1972.
Hoare, C.A.R., "An axiomatic basis for computer programming," Comm. ACM 12(10), 576-80, 583, Oct. 1969.
Kozen et al., "Logics of Programs," Handbook of Theoretical Computer Science, Editor: J. van Leeuwen, Elsevier Science Publishers B.V., 1990.
Lampson, B.W., "A Note on the Confinement Problem," Comm. Of the ACM Oct. 1971, vol. 16, No. 10, Operating Systems, Editor: C. Weissman, 1973.
Volpano et al., "A Type-Based Approach to Program Security," Proceedings of TAPSOFT '97, Colloquium on Formal Approaches in Software Engineering, Lille France, Apr. 14-18, 1997.
The article "Communicating Sequential Processes" by C.A. Hoare in ACM, Aug. 1978.
The article "An Axiomatic Basis for Computer Programming" by C.A.R. Hoare, in ACM, Oct. 1969.

Affiliated with

Also associated with

Rating

Method and apparatus for statically analyzing a computer program does not yet have a rating. At this time, there are no reviews or comments for this patent.

If you have personal experience with Method and apparatus for statically analyzing a computer program, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and Method and apparatus for statically analyzing a computer program will most certainly appreciate the feedback.

Rate now

Comments { 0 }

Profile ID: LFUS-PAI-O-1335549