Dorothy E. Denning
Peter J. Denning
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.
- 1 Allen, F.E. Control flow analysis. Proc. Symp. Compiler Optimization, SIGPLAN Notices (ACM) 5, 7 (July 1970), 1-19. Google Scholar
Digital Library
- 2 Andrews, G.R. COPS-A protection mechanism for computer systems. Ph.D. Diss., U. of Wash., Seattle, Wash., July 1974. Google ScholarDigital Library
- 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.Google Scholar
- 4 Birkhoff, G. Lattice Theory. Amer. Math. Soc. Col. Pub. XXV, Amer. Math. Soc., Providence, R.I., 3rd ed., 1967.Google Scholar
- 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.Google Scholar
- 6 Denning, D.E. Secure information flow in computer systems. Ph.D. Th., Comptr. Sci. Dep., Purdue U., W. Lafayette, Ind., May 1975. Google ScholarDigital Library
- 7 Denning, D.E. A lattice model of secure information flow. Comm. ACM 19, 5 (May 1976), 236-243. Google ScholarDigital Library
- 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.Google Scholar
- 9 Fenton, J.S. Information protection systems. Ph.D. Diss., Comptr. Lab., U. of Cambridge, England, 1973.Google Scholar
- 10 Fenton, J.S. Memoryless subsystems. Comptr. J. 17, 2 (May 1974), 143-147.Google ScholarCross Ref
- 11 Fenton, J.S. An abstract computer model demonstrating directional information flow. U. of Cambridge, Cambridge, England, 1974.Google Scholar
- 12 Goodenough, J.B. Exception handling: Issues and a proposed notation. Comm. ACM 18, 12 (Dec. 1975), 683-696. Google ScholarDigital Library
- 13 Gat, I., and Saal, H.J. Memoryless execution: A programmer's viewpoint. IBM Tech. Rep. 025, IBM Israeli Scientific Ctr., Haifa, March 1975.Google Scholar
- 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.Google Scholar
- 15 Gries, D. Compiler Construction for Digital Computers, Wiley, New York, 1971. Google ScholarDigital Library
- 16 Harrison, M.A., Ruzzo, W.L., and Ullman, J.D. On protection in operating systems. Proc. Fifth Symp. on Operating Systems Principles, Operating Syst. Rev. (ACM SIGOPS Newsletter) 9, 5 (Nov. 1975), 14-24. Google ScholarDigital Library
- 17 IBM. System/360 PL/I (F) Language Reference Manual. Rep. No. GC28-8201-3, IBM Systems Reference Library, 1971.Google Scholar
- 18 Jones, A.K. Protection in programmed systems. Ph.D. Th., Carnegie-Mellon U., Pittsburgh, Pa., June 1973. Google ScholarDigital Library
- 19 Jones, A.K., and Lipton, R.J. The enforcement of security policies for computation. Proc. Fifth Symp. on Operating Systems Principles, Operating Syst. Rev. (ACM SIGOPS Newsletter) 9, 5 (Nov. 1975), 197-206. Google ScholarDigital Library
- 20 Lampson, B.W. A note on the confinement problem. Comm. ACM 16, 10 (Oct. 1973), 613-615. Google ScholarDigital Library
- 21 Lipner, S.B. A comment on the confinement problem. Proc. Fifth Symp. on Operating Systems Principles, Operating Syst. Rev. (ACM SIGOPS Newsletter) 9, 5 (Nov. 1975), 192-196. Google ScholarDigital Library
- 22 Lowry, E.S., and Medlock, C.W. Object code optimization. Comm. ACM 12, 1 (Jan. 1969), 13-22. Google ScholarDigital Library
- 23 Millen, J.K. Security Kernel Validation in Practice. Comm. ACM 19, 5 (May 1976), 243-250. Google ScholarDigital Library
- 24 Minsky, M.L. Computation: Finite and Infinite Machines, Prentice-Hall, Englewood Cliffs, N.J., 1967. Google ScholarDigital Library
- 25 Moore, C.G. III. Potential capabilities in ALGOL-like programs. TR 74-211, Dep. Comptr. Sci., Cornell U., Ithaca, N.Y., Sept. 1974. Google ScholarDigital Library
- 26 Rotenberg, L.J. Making computers keep secrets. Ph.D. Th., MAC-TR-115, Project Mac, M.I.T., Cambridge, Mass., Feb. 1974.Google Scholar
- 27 Schroeder, M.D. Cooperation ofmutually suspicious subsystems in a computer utility. Ph.D. Th., MAC-TR-104, Project MAC, Sept. 1972. Google ScholarDigital Library
- 28 Stone, K.S. Discrete Mathematical Structures and Their Applications. Science Research Associates, Chicago, 1973.Google Scholar
- 29 Walter, K.G., et al. Structured specification of a security kernel. Proc. Int. Conf. on Reliable Software, SIGPLAN Notices (ACM) 10, 6 (June 1975), 285-293. Google ScholarDigital Library
- 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.Google Scholar
- 31 Wirth, N. The programming language Pascal. Acta Informatica 1, 1 (1971), 35-63.Google ScholarDigital Library
Recommendations
A lattice model of secure information flow
This paper investigates mechanisms that guarantee secure information flow in a computer system. These mechanisms are examined within a mathematical framework suitable for formulating the requirements of secure information flow among security classes. ...
An Application of the (max, +) Algebra to Information Flow Security
ICN '08: Proceedings of the Seventh International Conference on NetworkingConfidentiality is one of the most important topics in computer security research. In order to check and ensure confidentiality information flow models are widely used. These models support the specification of valid flows of information. Furthermore, ...
Information Flow Certification Using an Intermediate Code Program Representation
This paper describes a compile-time information flow control (IFC) mechanism that certifies secure information flow within the collection of objects accessed by a program. The IFC mechanism is based on the lattice model and certification mechanism of ...
Comments