Kevin W. Hamlen
Greg Morrisett
Fred B. Schneider
Skip Abstract Section
Abstract
A precise characterization of those security policies enforceable by program rewriting is given. This also exposes and rectifies problems in prior work, yielding a better characterization of those security policies enforceable by execution monitors as well as a taxonomy of enforceable security policies. Some but not all classes can be identified with known classes from computational complexity theory.
- Anderson, J. 1972. Computer security technology planning study vols. I and III. Tech. Rep. ESD-TR-73-51, HQ Electronic Systems Division: Hanscom AFB, MA, Fort Washington, Pennsylvania. October.]]Google Scholar
- Deutsch, P. and Grant, C. 1971. A flexible measurement tool for software systems. In Information Processing (Proceedings of the IFIP Congress). 320--326.]]Google Scholar
- Erlingsson, Ú. and Schneider, F. B. 2000a. IRM enforcement of Java stack inspection. In IEEE Symposium on Security and Privacy. Oakland, California, 246--255.]] Google Scholar
- Erlingsson, Ú. and Schneider, F. B. 2000b. SASI enforcement of security policies: A retrospective. In WNSP: New Security Paradigms Workshop. ACM Press.]] Google Scholar
- Evans, D. and Twynman, A. 1999. Flexible policy-directed code safety. In IEEE Symposium on Security and Privacy. Oakland, California, 32--45.]]Google Scholar
- Fong, P. W. L. 2004. Access control by tracking shallow execution history. In Proceedings of the 2004 IEEE Symposium on Security and Privacy. Berkeley, California, 43--55.]]Google Scholar
- Gödel, K. 1931. Über formal unentscheidbare sätze der Principia Mathematica und verwandter Systeme. Monatshefte für Mathematik und Physik 38, 173--198.]]Google Scholar
- Harrison, M. A., Ruzzo, W. L., and Ullman, J. D. 1976. Protection in operating systems. Comm. ACM 19, 8 (Aug.), 461--471.]] Google Scholar
- Hopcroft, J. E. and Ullman, J. D. 1979. Introduction to Automata Theory, Languages, and Computation. Addison-Wesley.]] Google Scholar
- Kiczales, G., Lamping, J., Medhdhekar, A., Maeda, C., Lopes, C., Loingtier, J.-M., and Irwin, J. 1997. Aspect-oriented programming. In European Conference on Object-Oriented Programming, M. Akşit and S. Matsuoka, Eds. Vol. 1241. Springer-Verlag, Berlin, Heidelberg, and New York, 220--242.]]Google Scholar
- Kim, M., Kannon, S., Lee., I., and Sokolsky, O. 2001. Java-MaC: A run-time assurance tool for Java. In First International Workshop on Run-time Verification. Paris, France.]]Google Scholar
- Lamport, L. 1977. Proving the correctness of multiprocess programs. IEEE Trans. Soft. Eng. SE-3 2, 125--143.]]Google Scholar
- Lampson, B. 1971. Protection. In Proceedings of the 5th Symposium on Information Sciences and Systems. Princeton, New Jersey, 437--443.]]Google Scholar
- Ligatti, J., Bauer, L., and Walker, D. 2003. Edit automata: Enforcement mechanisms for run-time security policies. Tech. Rep. TR-681-03, Princeton University, Princeton, New Jersey. May.]]Google Scholar
- Ligatti, J., Bauer, L., and Walker, D. 2005. Enforcing non-safety security policies with program monitors. Tech. Rep. TR-720-05, Princeton University, Princeton, New Jersey. January.]]Google Scholar
- Lindholm, T. and Yellin, F. 1999. The Java#8482; Virtual Machine Specification, second ed. Addison-Wesley.]] Google Scholar
- Marcus, L. Fall 1989. The search for a unifying framework for computer security. IEEE Cipher, 55--63. Invited Panel Discussion Position Paper, Second Franconia Workshop on Foundations of Computer Security, June 11--14, 1989.]]Google Scholar
- Morrisett, G., Crary, K., and Glew, N. 1999. From System F to Typed Assembly Language. ACM Trans. Prog. Lang. Syst. 21, 3 (May), 527--568.]] Google Scholar
- Myers, A. C. 1999. Practical mostly-static information flow control. In Proceedings of the 26th ACM Symposium on Principles of Programming Languages. San Antonio, Texas, 228--241.]] Google Scholar
- Nachenberg, C. 1997. Computer virus--antivirus coevolution. Comm. ACM 40, 1 (Jan.), 46--51.]] Google Scholar
- Necula, G. 1997. Proof-Carrying Code. In 24th ACM Symposium on Principles of Programming Languages. Paris, France, 106--119.]] Google Scholar
- Necula, G. C. and Lee, P. 1996. Safe kernel extensions without run-time checking. In Second Symposium on Operating Systems Design and Implementation (OSDI '96). USENIX, Berkeley, CA, USA, 229--243.]] Google Scholar
- Necula, G. C. and Lee, P. 1998. The design and implementation of a certifying compiler. In Proceedings of the 1998 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI). 333--344.]] Google Scholar
- Papadimitriou, C. H. 1995. Computational Complexity. Addison-Wesley.]]Google Scholar
- Rees, J. and Clinger, W. 1991. Revised 4 report on the algorithmic language Scheme. Lisp Pointers 4, 3 (July--Sept.), 1--55.]] Google Scholar
- Robben, W., Vanhaute, B., Joosen, W., and Verbaeten, P. 1999. Non-functional policies. Lecture Notes in Computer Science 1616, 74--92.]] Google Scholar
- Schneider, F. B. 2000. Enforceable security policies. ACM Trans. Inform. Syst. Secur. 3, 1 (Feb.), 30--50.]] Google Scholar
- Small, C. 1997. MiSFIT: A tool for constructing safe extensible C++ systems. In Proceedings of the Third USENIX Conference on Object-Oriented Technologies. Portland, Oregon.]] Google Scholar
- Turing, A. M. 1936. On computable numbers with an application to the Entscheidungs-problem. In Proceedings of the London Mathematical Society. vol. 2. 42, 230--265.]]Google Scholar
- Viswanathan, M. 2000. Foundations for the run-time analysis of software systems. Ph.D. thesis, University of Pennsylvania.]] Google Scholar
- Wahbe, R., Lucco, S., Anderson, T. E., and Graham, S. L. 1993. Efficient software-based fault isolation. In Proceedings of the 14th ACM Symposium on Operating Systems Principles. 203--216.]] Google Scholar
- Ware, W. 1979. Security controls for computer systems. Tech. Rep. R-609-1, Rand Corp. October.]]Google Scholar
Index Terms
- Computability classes for enforcement mechanisms
Recommendations
Run-Time Enforcement of Nonsafety Policies
A common mechanism for ensuring that software behaves securely is to monitor programs at run time and check that they dynamically adhere to constraints specified by a security policy. Whenever a program monitor detects that untrusted software is ...
Certified In-lined Reference Monitoring on .NET
PLAS '06: Proceedings of the 2006 workshop on Programming languages and analysis for securityMOBILE is an extension of the .NET Common Intermediate Language that supports certified In-Lined Reference Monitoring. Mobile programs have the useful property that if they are well-typed with respect to a declared security policy, then they are ...
Execution monitoring enforcement for limited-memory systems
PST '06: Proceedings of the 2006 International Conference on Privacy, Security and Trust: Bridge the Gap Between PST Technologies and Business ServicesRecently, attention has been given to formally characterize security policies that are enforceable by different kinds of security mechanisms. Since execution monitoring (EM) is a ubiquitous technique for enforcing security policies, this class of ...
Comments