Certification of programs for secure information flow

ABSTRACT

ertification mechanism for verifying the secure flow of information through a program. Because it exploits the properties of a lattice structure among security classes, the procedure is sufficiently simple that it can easily be included in the analysis phase of most existing compilers. Appropriate semantics are presented and proved correct. An important application is the confinement problem: The mechanism can prove that a program cannot cause supposedly nonconfidential results to depend on confidential input data.

REFERENCES

• 1: Frances E. Allen, Control flow analysis, Proceedings of a symposium on Compiler optimization, p.1-19, July 27-28, 1970, Urbana-Champaign, Illinois
• 2: Gregory Richard Andrews, Cops--a protection mechanism for computer systems., 1974
• 3: Bell, D.E., and LaPadula, L.J. Secure Computer Systems: Mathematical Foundations, Vol. 1-III. ESD-TR-73-278, The MITRE Corp., Bedford, Mass.
• 4: Birkhoff, G. Lattice Theory. Amer. Math. Soc. Col. Pub. XXV, Amer. Math. Soc., Providence, R.I., 3rd ed., 1967.
• 5: Denning, D.E., Denning, P.J., and Graham, G.S. Selectively confined subsystems. Proc. Int. Workshop on Protection in Operating Systems, IRIA-Laboria, France, Aug. 1974, pp. 55-61.
• 6: Dorothy Elizabeth Robling Denning, Secure information flow in computer systems., 1975
• 7: 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]
• 8: Denning, D.E. On the derivation of lattice structured information flow policies. Tech. Rep. TR-179, Dep. of Comptr. Sci., Purdue U., W. Lafayette, Ind., March 1976.
• 9: Fenton, J.S. Information protection systems. Ph.D. Diss., Comptr. Lab., U. of Cambridge, England, 1973.
• 10: Fenton, J.S. Memoryless subsystems. Comptr. J. 17, 2 (May 1974), 143-147.
• 11: Fenton, J.S. An abstract computer model demonstrating directional information flow. U. of Cambridge, Cambridge, England, 1974.
• 12: John B. Goodenough, Exception handling: issues and a proposed notation, Communications of the ACM, v.18 n.12, p.683-696, Dec. 1975 [doi>10.1145/361227.361230]
• 13: Gat, I., and Saal, H.J. Memoryless execution: A programmer's viewpoint. IBM Tech. Rep. 025, IBM Israeli Scientific Ctr., Haifa, March 1975.
• 14: Graham, G.S., and Denning, P.J. Protection-principles and practice. Proc. AFIPS 1972 SJCC, Vol. 40, AFIPS Press, Montvale, N.J., pp. 417-429.
• 15: David Gries, Compiler Construction for Digital Computers, John Wiley & Sons, Inc., New York, NY, 1971
• 16: Michael A. Harrison , Walter L. Ruzzo , Jeffrey D. Ullman, On protection in operating systems, Proceedings of the fifth ACM symposium on Operating systems principles, p.14-24, November 19-21, 1975, Austin, Texas, United States
• 17: IBM. System/360 PL/I (F) Language Reference Manual. Rep. No. GC28-8201-3, IBM Systems Reference Library, 1971.
• 18: Anita Katherine Jones, Protection in programmed systems., 1973
• 19: 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
• 20: 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]
• 21: 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
• 22: Edward S. Lowry , C. W. Medlock, Object code optimization, Communications of the ACM, v.12 n.1, p.13-22, Jan. 1969 [doi>10.1145/362835.362838]
• 23: 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]
• 24: Marvin Lee Minsky, Computation: Finite and Infinite Machines, Prentice-Hall, Inc., Upper Saddle River, NJ, 1967
• 25: Charles G. Moore, III, Potential Capabilities in Algol-Like Programs, Cornell University, Ithaca, NY, 1974
• 26: Rotenberg, L.J. Making computers keep secrets. Ph.D. Th., MAC-TR-115, Project Mac, M.I.T., Cambridge, Mass., Feb. 1974.
• 27: M. D. Schroeder, COOPERATION OF MUTUALLY SUSPICIOUS SUBSYSTEMS IN A COMPUTER UTILITY, Massachusetts Institute of Technology, Cambridge, MA, 1972
• 28: Stone, K.S. Discrete Mathematical Structures and Their Applications. Science Research Associates, Chicago, 1973.
• 29: K. G. Walter , S. I. Schaen , W. F. Ogden , W. C. Rounds , D. G. Shumway , D. D. Schaeffer , K. J. Biba , F. T. Bradshaw , S. R. Ames , J. M. Gilligan, Structured specification of a Security Kernel, Proceedings of the international conference on Reliable software, p.285-293, April 21-23, 1975, Los Angeles, California
• 30: Weissman, C. Security controls in the ADEPT-50 time-sharing system. Proc. AFIPS 1969 FJCC, Vol. 35, AFIPS Press, Montvale, N.J., pp. 119-133.
• 31: Wirth, N. The programming language Pascal. Acta Informatica 1, 1 (1971), 35-63.

INDEX TERMS

Keywords:
confinement, information flow, lattice, program certification, protection, security, security classes