Enforceable security policies

ABSTRACT

A precise characterization is given for the class of security policies enforceable with mechanisms that work by monitoring system execution, and automata are introduced for specifying exactly that class of security policies. Techniques to enforce security policies specified by such automata are also discussed.

REFERENCES

• 1: ALPERN, B. AND SCHNEIDER, F. B. 1985. Defining liveness. Inf. Process. Lett. 21, 4 (Oct.), 181-185.
• 2: ALPERN, B. AND SCHNEIDER, F. B. 1987. Recognizing safety and liveness. Distrib. Comput. 2, 117-126.
• 3: Bowen Alpern , Fred B. Schneider, Verifying temporal properties without temporal logic, ACM Transactions on Programming Languages and Systems (TOPLAS), v.11 n.1, p.147-167, Jan. 1989 [doi>10.1145/59287.62028]
• 4: Edsger W. Dijkstra, Guarded commands, nondeterminacy and formal derivation of programs, Communications of the ACM, v.18 n.8, p.453-457, Aug. 1975 [doi>10.1145/360933.360975]
• 5: Guy Edjlali , Anurag Acharya , Vipin Chaudhary, History-based access control for mobile code, Proceedings of the 5th ACM conference on Computer and communications security, p.38-48, November 02-05, 1998, San Francisco, California, United States [doi>10.1145/288090.288102]
• 6: Samuel Eilenberg, Automata, Languages, and Machines, Academic Press, Inc., Orlando, FL, 1974
• 7: Úlfar Erlingsson , Fred B. Schneider, SASI enforcement of security policies: a retrospective, Proceedings of the 1999 workshop on New security paradigms, p.87-95, September 22-24, 1999, Caledon Hills, Ontario, Canada [doi>10.1145/335169.335201]
• 8: EVANS, D. AND TWYMAN, A. 1999. Policy-directed code safety. In Proceedings of the 1999 IEEE Computer Society Symposium on Research in Security and Privacy (Oakland, CA, May), IEEE Computer Society Press, Los Alamitos, CA, 32-45.
• 9: Virgil D. Gligor, A note on denial-of-service in operating systems, IEEE Transactions on Software Engineering, v.10 n.3, p.320-324, May 1984 [doi>10.1109/TSE.1984.5010241]
• 10: GLIGOR, V. D., GAVRILA, S., AND FERRAIOLO, D. 1998. On the formal definition of separationof-duty policies and their composition. In Proceedings of the 1998 IEEE Computer Society Symposium on Research in Security and Privacy (Oakland, CA, May), IEEE Computer Society Press, Los Alamitos, CA, 172-183.
• 11: GOGUEN, g. A. AND MESEGUER, g. 1982. Security policies and security models. In Proceedings of the 1982 IEEE Computer Society Symposium on Research in Security and Privacy (Oakland, CA, May), IEEE Computer Society Press, Los Alamitos, CA, 11-20.
• 12: Li Gong, Java Security: Present and Near Future, IEEE Micro, v.17 n.3, p.14-19, May 1997 [doi>10.1109/40.591650]
• 13: Robert Grimm , Brian N. Bershad, Providing policy-neutral and transparent access control in extensible systems, Secure Internet programming: security issues for mobile and distributed objects, Springer-Verlag, London, 2001
• 14: John E. Hopcroft , Jeffrey D. Ullman, Formal languages and their relation to automata, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1969
• 15: Sushil Jajodia , Pierangela Samarati , V. S. Subrahmanian, A Logical Language for Expressing Authorizations, Proceedings of the 1997 IEEE Symposium on Security and Privacy, p.31, May 04-07, 1997
• 16: Neil D. Jones , Carsten K. Gomard , Peter Sestoft, Partial evaluation and automatic program generation, Prentice-Hall, Inc., Upper Saddle River, NJ, 1993
• 17: LAMPORT, L. 1977. Proving the correctness of multiprocess programs. IEEE Trans. Softw. Eng. 3, 2 (Mar.), 125-143.
• 18: M. W. Alford , J. P. Ansart , G. Hommel , L. Lamport , B. Liskov , G. P. Mullery , F. B. Schneider, Distributed systems: methods and tools for specification. An advanced course, Springer-Verlag New York, Inc., New York, NY, 1985
• 19: LAMPSON, B. 1974. Protection. In Proceedings of the 5th Symposium on Information Sciences and Systems (Princeton, NJ, Mar.), 437-443.
• 20: Tim Lindholm , Frank Yellin, Java Virtual Machine Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1999
• 21: MARCHUKOV, M. AND SULLIVAN, K. 1999. Reconciling behavioral mismatch through component restriction. CS 99-22. Department of Computer Science, University of Virginia, Charlottesville, VA. Technical Report
• 22: John McLean, A General Theory of Composition for Trace Sets Closed under Selective Interleaving Functions, Proceedings of the 1994 IEEE Symposium on Security and Privacy, p.79, May 16-18, 1994
• 23: Greg Morrisett , David Walker , Karl Crary , Neal Glew, From system F to typed assembly language, Proceedings of the 25th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.85-97, January 19-21, 1998, San Diego, California, United States [doi>10.1145/268946.268954]
• 24: George C. Necula, Proof-carrying code, Proceedings of the 24th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.106-119, January 15-17, 1997, Paris, France [doi>10.1145/263699.263712]
• 25: George C. Necula , Peter Lee, The design and implementation of a certifying compiler, ACM SIGPLAN Notices, v.33 n.5, p.333-344, May 1998
• 26: Linda M. Null , Johnny Wong, The DIAMOND security policy for object-oriented databases, Proceedings of the 1992 ACM annual conference on Communications, p.49-56, March 03-05, 1992, Kansas City, Missouri, United States [doi>10.1145/131214.131221]
• 27: PANDEY, R. AND HASHII, B. 1998. Providing fine grained access control for mobile programs through binary editing. TR98 08. Department of Computer Science, University of California at Davis, Davis, CA.
• 28: RUSHBY, J. 1989. Kernels for safety? In Safe and Secure Computing Systems, T. Anderson, Ed. Blackwell Scientific Publications, Ltd., Oxford, UK, 210-220.
• 29: SALTZER, J. H. AND SCHROEDER, M. D. 1975. The protection of information in computer systems. Proc. IEEE 63, 9 (Sept.), 1278-1308.
• 30: SMALL, C. 1997. Misfit: A tool for constructing safe extensible C+ + systems. In Proceedings of the 3rd USENIX Conference on Object-Oriented Technologies (Portland, OR, June), USENIX Assoc., Berkeley, CA, 38-48.
• 31: STEFIK, M. 1996. Letting loose the light: Igniting commerce in electronic publication. In Internet Dreams, M. Stefik, Ed. MIT Press, Cambridge, MA.
• 32: Robert Wahbe , Steven Lucco , Thomas E. Anderson , Susan L. Graham, Efficient software-based fault isolation, Proceedings of the fourteenth ACM symposium on Operating systems principles, p.203-216, December 05-08, 1993, Asheville, North Carolina, United States
• 33: WIKA, K. G. AND KNIGHT, J. C. 1995. On the enforcement of software safety policies. In Proceedings of the lOth Annual IEEE Conference on Computer Assurance (COMPASS '95, Gaithersburg, MD, June), IEEE Computer Society Press, Los Alamitos, CA.
• 34: Authorization in Distributed Systems: A Formal Approach, Proceedings of the 1992 IEEE Symposium on Security and Privacy, p.33, May 04-06, 1992

INDEX TERMS

Primary Classification:
  K. Computing Milieux
  K.6 MANAGEMENT OF COMPUTING AND INFORMATION SYSTEMS

Additional Classification:
  D. Software
  D.2 SOFTWARE ENGINEERING
      D.2.9 Management
          Subjects: Software configuration management
  D.4 OPERATING SYSTEMS

  F. Theory of Computation
  F.1 COMPUTATION BY ABSTRACT DEVICES
      F.1.1 Models of Computation
          Subjects: Automata (e.g., finite, push-down, resource-bounded)
  F.3 LOGICS AND MEANINGS OF PROGRAMS
      F.3.1 Specifying and Verifying and Reasoning about Programs
          Subjects: Specification techniques

  K. Computing Milieux
  K.4 COMPUTERS AND SOCIETY
      K.4.4 Electronic Commerce
          Subjects: Security

General Terms:
Security

Keywords:
EM security policies, SASI, inlined reference monitors, proof carrying code, safety properties, security automata, security policies