Correctness in access control

ABSTRACT

A number of approaches have been developed to modularize parts of multiuser computer systems so that access to each part can be controlled. The devices of rings and capabilities are two examples. However, today's systems are notably incomplete and subject to defeat by determined and clever users. A point of view is presented here which allows proving that a logical design of an access control system is correct relative to a designer-specified set of criteria. Implementation questions are also discussed.

REFERENCES

• 1: R. W. Conway , W. L. Maxwell , H. L. Morgan, On the implementation of security measures in information systems, Communications of the ACM, v.15 n.4, p.211-220, April 1972 [doi>10.1145/361284.361287]
• 2: Bernard Elspas , Karl N. Levitt , Richard J. Waldinger , Abraham Waksman, An Assessment of Techniques for Proving Program Correctness, ACM Computing Surveys (CSUR), v.4 n.2, p.97-147, June 1972 [doi>10.1145/356599.356602]
• 3: Friedman, T., "The Authorization Problem in Shared Files," IBM Systems Journal 9, 4 (1970), pp. 258-280.
• 4: Graham, G. S., and P. J. Denning "Protection—Principles and Practice," AFIPS Conf. Proc. 40 (SJCC 1972), pp. 417-429.
• 5: Robert M. Graham, Protection in an information processing utility, Communications of the ACM, v.11 n.5, p.365-369, May 1968 [doi>10.1145/363095.363146]
• 6: Lance J. Hoffman, Computers and Privacy: A Survey, ACM Computing Surveys (CSUR), v.1 n.2, p.85-103, June 1969 [doi>10.1145/356546.356548]
• 7: Hoffman, L. F., "The Formulary Model for Flexible Privacy and Access Controls," AFIPS Conf. Proc. 39 (FJCC 1971), pp. 587-601.
• 8: Lampson, B. W., "Dynamic Protection Structures," AFIPS Conf. Proc. 35 (FJCC 1969), pp. 27-38.
• 9: Lampson, B. W., "Protection," Proc. 5th Princeton Conf. on Information Sciences and Systems (March 1971), pp. 437-443.
• 10: Schell, R. (Head of Computer Security Branch, USAF/ESD), private communication, July 1972.
• 11: Computer Security Technology Planning Study, ESD-TR-73-51, USAF Hanscom Field, October 1972.

INDEX TERMS

Primary Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.4 Software/Program Verification
          Subjects: Correctness proofs

Additional Classification:
  D. Software
  D.4 OPERATING SYSTEMS
      D.4.6 Security and Protection
          Subjects: Access controls

  H. Information Systems
  H.2 DATABASE MANAGEMENT
      H.2.1 Logical Design

General Terms:
Design, Languages, Management, Performance, Verification

Keywords:
Access control, Correctness, Data base, Logical design, Security, Time-sharing