Information-flow and data-flow analysis of while-programs

ABSTRACT

Until recently, information-flow analysis has been used primarily to verify that information transmission between program variables cannot violate security requirements. Here, the notion of information flow is explored as an aid to program development and validation. Information-flow relations are presented for while-programs, which identify those program statements whose execution may cause information to be transmitted from or to particular input, internal, or output values. It is shown with examples how these flow relations can be helpful in writing, testing, and updating programs; they also usefully extend the class of errors which can be detected automatically in the “static analysis” of a program.

REFERENCES

• 1: Alfred V. Aho , John E. Hopcroft, The Design and Analysis of Computer Algorithms, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1974
• 2: Alfred V. Aho , Jeffrey D. Ullman, Theory of Parsing, Translation and Compiling, Prentice Hall Professional Technical Reference, 1973
• 3: F. E. Allen , J. Cocke, A program data flow analysis procedure, Communications of the ACM, v.19 n.3, p.137, March 1976 [doi>10.1145/360018.360025]
• 4: Gregory R. Andrews , Richard P. Reitman, An Axiomatic Approach to Information Flow in Programs, ACM Transactions on Programming Languages and Systems (TOPLAS), v.2 n.1, p.56-76, Jan. 1980 [doi>10.1145/357084.357088]
• 5: CARRIe, B.A. Graphs and Networks. Oxford University Press, New York, 1979.
• 6: COHEN, E. Information transmission in sequential programs. In Foundations of Secure Computation, R. A. Demillo et al., Ed. Academic Press, New York, 1978, pp. 297-335.
• 7: Dorothy E. Denning , Peter J. Denning, Certification of programs for secure information flow, Communications of the ACM, v.20 n.7, p.504-513, July 1977 [doi>10.1145/359636.359712]
• 8: FARROW, R., KENNEDY, K., AND ZUCCONI, L. Graph grammars and global program flow analysis. In Proceedings of the 17th Annual IEEE Symposium on Foundations of Computer Science (Houston, Tex., Nov.). IEEE, New York, 1975, pp. 42-56.
• 9: FOSDICK L.D., AND OSTERWEIL, L.J. Validation and global optimization of programs. In Proceedings of the 4th Texas Conference on Computing Systems (Austin, Tex.). 1975. Sponsored by the IEEE Computer Society.
• 10: Lloyd D. Fosdick , Leon J. Osterweil, Data Flow Analysis in Software Reliability, ACM Computing Surveys (CSUR), v.8 n.3, p.305-330, Sept. 1976 [doi>10.1145/356674.356676]
• 11: Susan L. Graham , Mark Wegman, A Fast and Usually Linear Algorithm for Global Flow Analysis, Journal of the ACM (JACM), v.23 n.1, p.172-202, Jan. 1976 [doi>10.1145/321921.321939]
• 12: Matthew S. Hecht, Flow Analysis of Computer Programs, Elsevier Science Inc., New York, NY, 1977
• 13: HUANG, J.C. Detection of data flow anomaly through program instrumentation. IEEE Trans. So{tw. Eng. SE-5, 3 (May 1979), 226-236.
• 14: Kathleen Jensen , Niklaus Wirth, Pascal-User Manual and Report, Springer-Verlag New York, Inc., Secaucus, NJ, 1975
• 15: KENNEDY, K. A survey of data flow analysis techniques. In Program Flow Analysis: Theory and Applications, S. S. Muchnick and N. D. Jones, Eds. Prentice-Hall, Englewood Cliffs, N.J., 1981, pp. 5-54.
• 16: Gary A. Kildall, A unified approach to global program optimization, Proceedings of the 1st annual ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.194-206, October 01-03, 1973, Boston, Massachusetts [doi>10.1145/512927.512945]
• 17: MUNRO, I. Efficient determination of the transitive closure of a directed graph. Inf. Process. Lett. I (1971), 56-58.
• 18: OSTERWEIL, L.J. Using data flow tools in software engineering. In Program Flow Analysis: Theory and Applications, S. S. Muchnick and N. D. Jones, Eds. Prentice-Hall, Englewood Cliffs, N.J., 1981, pp. 237-263.
• 19: G. J. Popek , J. J. Horning , B. W. Lampson , J. G. Mitchell , R. L. London, Notes on the design of Euclid, Proceedings of an ACM conference on Language design for reliable software, p.11-18, March 28-30, 1977, Raleigh, North Carolina
• 20: Barry K. Rosen, High-level data flow analysis, Communications of the ACM, v.20 n.10, p.712-724, Oct. 1977 [doi>10.1145/359842.359849]
• 21: STRASSEN, V. Gaussian elimination is not optimal. Numer. Math. 13 (1969).
• 22: Stephen Warshall, A Theorem on Boolean Matrices, Journal of the ACM (JACM), v.9 n.1, p.11-12, Jan. 1962 [doi>10.1145/321105.321107]
• 23: Mark Weiser, Programmers use slices when debugging, Communications of the ACM, v.25 n.7, p.446-452, July 1982 [doi>10.1145/358557.358577]
• 24: WITTEN, I.H. Algorithms for adaptive linear prediction. Comput. J. 23, i (Feb. 1980), 78-84.

INDEX TERMS

Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Assertion checkers

General Terms:
Documentation, Languages, Verification