An Axiomatic Approach to Information Flow in Programs

ABSTRACT

A new approach to information flow in sequential and parallel programs is presented. Flow proof rules that capture the information flow semantics of a variety of statements are given and used to construct program flow proofs. The method is illustrated by examples. The applications of flow proofs to certifying information flow policies and to solving the confinement problem are considered. It is also shown that flow rules and correctness rules can be combined to form an even more powerful proof system.

REFERENCES

• 1: BRINCH HANSEN, P. The programming language Concurrent Pascal. IEEE Trans. Sofiw. Eng. SE-1, 2 (June 1975), 199-207.
• 2: Ellis Choen, Information transmission in computational systems, Proceedings of the sixth ACM symposium on Operating systems principles, p.133-139, November 16-18, 1977, West Lafayette, Indiana, United States
• 3: Dorothy E. Denning, A lattice model of secure information flow, Communications of the ACM, v.19 n.5, p.236-243, May 1976 [doi>10.1145/360051.360056]
• 4: 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]
• 5: DIZKSTRA, E.W. Cooperating sequential processes. In Programming Languages (F. Genuys, Ed.), Academic Press, New York, 1968.
• 6: FENTON, J.S. Memoryless subsystems. Comput. J. 17, 2 (May 1974), 143-147.
• 7: GAT, I. Security aspects of computer systems. Ph.D. Thesis, Technion--Israel inst. of Technology, June 1976.
• 8: C. A. R. Hoare, An axiomatic basis for computer programming, Communications of the ACM, v.12 n.10, p.576-580, Oct. 1969 [doi>10.1145/363235.363259]
• 9: C. A. R. Hoare, Monitors: an operating system structuring concept, Communications of the ACM, v.17 n.10, p.549-557, Oct. 1974 [doi>10.1145/355620.361161]
• 10: Anita K. Jones , Richard J. Lipton, The enforcement of security policies for computation, Proceedings of the fifth ACM symposium on Operating systems principles, p.197-206, November 19-21, 1975, Austin, Texas, United States
• 11: Butler W. Lampson, A note on the confinement problem, Communications of the ACM, v.16 n.10, p.613-615, Oct. 1973 [doi>10.1145/362375.362389]
• 12: Steven B. Lipner, A comment on the confinement problem, Proceedings of the fifth ACM symposium on Operating systems principles, p.192-196, November 19-21, 1975, Austin, Texas, United States
• 13: Thomas Bennet London, The semantics of information flow., 1977
• 14: MCGRAW, J.R., ANO ANOREWS, G.R. Access control in parallel programs. IEEE Trans. Softw. Eng. SE-5, 1 (Jan. 1979), 1-9.
• 15: Jonathan K. Millen, Security Kernel validation in practice, Communications of the ACM, v.19 n.5, p.243-250, May 1976 [doi>10.1145/360051.360059]
• 16: Charles G. Moore, III, Potential Capabilities in Algol-Like Programs, Cornell University, Ithaca, NY, 1974
• 17: NF-UMANN, P.G., ET AL. A provably secure operating system: The system, its applications, and proofs. Final Rep., SRi Proj. 4332, SRI International, Menlo Park, Calif., Feb. 1977.
• 18: OWICKI, S., AND GRIES, D. An axiomatic proof technique for parallel programs. Acta Inf. 6 (1976), 319-340.
• 19: Gerald J. Popek , David A. Farber, A model for verification of data security in operating systems, Communications of the ACM, v.21 n.9, p.737-749, Sept. 1978 [doi>10.1145/359588.359597]
• 20: David P. Reed , Rajendra K. Kanodia, Synchronization with eventcounts and sequencers, Communications of the ACM, v.22 n.2, p.115-123, Feb. 1979 [doi>10.1145/359060.359076]
• 21: Richard Philip Reitman, Information flow in parallel programs: an axiomatic approach., 1978
• 22: Richard P. Reitman , Gregory R. Andrews, Certifying information flow properties of programs: an axiomatic approach, Proceedings of the 6th ACM SIGACT-SIGPLAN symposium on Principles of programming languages, p.283-290, January 29-31, 1979, San Antonio, Texas [doi>10.1145/567752.567779]
• 23: WEISSMAN, C. Security controls in the Adept-50 time-sharing system. AFIPS 1969 FJCC, Vol. 35, AFIPS Press, Arlington, Va., pp. 119-133.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING

General Terms:
Design, Languages, Performance, Theory