Abstract
A run-time monitor is a program that runs in parallel with an untrusted application and examines actions from the application’s instruction stream. If the sequence of program actions deviates from a specified security policy, the monitor transforms the sequence or terminates the program. We present the design and formal specification of a language for defining the policies enforced by program monitors.
Our language provides a number of facilities for composing complex policies from simpler ones. We allow policies to be parameterized by values or other policies, and we define operators for forming the conjunction and disjunction of policies. Since the computations that implement these policies modify program behavior, naive composition of computations does not necessarily produce the conjunction (or disjunction) of the policies that the computations implement separately. We use a type and effect system to ensure that computations do not interfere with one another when they are composed.
This research was supported in part by a gift from Microsoft Research, Redmond; DARPA award F30602-99-1-0519; and NSF Trusted Computing grant CCR-0208601.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bowen Alpern and Fred Schneider. Recognizing safety and liveness. Distributed Computing, 2:117–126, 1987.
Lujo Bauer, Jarred Ligatti, and David Walker. A calculus for composing security policies. Technical Report TR-655-02, Princeton University, 2002. Forthcoming.
Lujo Bauer, Jarred Ligatti, and David Walker. More enforceable security policies. InFoundations of Computer Security, Copenhagen, Denmark, July 2002.
Lujo Bauer, Jarred Ligatti, and David Walker. More enforceable security policies. Technical Report TR-649-02, Princeton University, June 2002.
David Brewer and Michael Nash. The Chinese wall security policy. In IEEE Symposium on Security and Privacy, pages 206–214, Oakland, May 1989.
P. Deutsch and C. A. Grant. A flexible measurement tool for software systems. In Information Processing, pages 320–326, 1971. Appeared in the proceedings of the IFIP Congress.
Úlfar Erlingsson and Fred B. Schneider. SASI enforcement of security policies: A retrospective. In Proceedings of the New Security Paradigms Workshop, pages 87–95, Caledon Hills, Canada, September 1999.
Úlfar Erlingsson and Fred B. Schneider. IRM enforcement of Java stack inspection. In IEEE Symposium on Security and Privacy, pages 246–255, Oakland, California, May 2000.
David Evans and Andrew Twyman. Flexible policy-directed code safety. In IEEE Security and Privacy, Oakland, CA, May 1999.
Andrew D. Gordon and Don Syme. Typing a multi-language intermediate code. In ACM Symposium on Principles of Programming Languages, London, UK, January 2001.
John Gough. Compiling for the.NET Common Language Runtime. Prentice Hall, 2001.
Robert Grimm and Brian Bershad. Separating access control policy, enforcement and functionality in extensible systems. ACM Transactions on Computer Systems, pages 36–70, February 2001.
Gregor Kiczales, Erik Hilsdale, Jim Hugunin, Mik Kersten, Jeffrey Palm, and William Griswold. An overview of AspectJ. In European Conference on Objectoriented Programming. Springer-Verlag, 2001.
Moonjoo Kim, Mahesh Viswanathan, Hanene Ben-Abdallah, Sampath Kannan, Insup Lee, and Oleg Sokolsky. Formally specified monitoring of temporal properties. In European Conference on Real-time Systems, York, UK, June 1999.
Insup Lee, Sampath Kannan, Moonjoo Kim, Oleg Sokolsky, and Mahesh Viswanathan. Run-time assurance based on formal specifications. In International Conference on Parallel and Distributed Processing Techniques and Applications, Las Vegas, June 1999.
Tim Lindholm and Frank Yellin. The Java Virtual Machine Specification. Addison-Wesley, 2nd edition, 1999.
Erik Meijer and John Gough. A technical overview of the Common Language Infrastructure. http://research.microsoft.com/~emeijer/Papers/CLR.pdf.
Eugenio Moggi. Notions of computation and monads. Information and Computation, 93:55–92, 1991.
R. Pandey and B. Hashii. Providing fine-grained access control for Java programs through binary editing. Concurrency: Practice and Experience, 12(14):1405–1430, 2000.
Xiaohu Qie, Ruoming Pang, and Larry Peterson. Defensive programming: Using an annotation toolkit to build DoS-resistant software. Technical Report TR-658-02, Princeton University, July 2002.
Anders Sandholm and Michael Schwartzbach. Distributed safety controllers for web services. In Fundamental Approaches to Software Engineering, volume 1382 of Lecture Notes in Computer Science, pages 270–284. Springer-Verlag, 1998.
Fred B. Schneider. Enforceable security policies. ACM Transactions on Information and Systems Security, 3(1):30–50, February 2000.
Mitchell Wand, Gregor Kiczales, and Christopher Dutchyn. A semantics for advice and dynamic join points in aspect-oriented programming. In Workshop on Foundations of Aspect-Oriented Languages, 2002.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bauer, L., Ligatti, J., Walker, D. (2003). Types and Effects for Non-interfering Program Monitors. In: Okada, M., Pierce, B.C., Scedrov, A., Tokuda, H., Yonezawa, A. (eds) Software Security — Theories and Systems. ISSS 2002. Lecture Notes in Computer Science, vol 2609. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36532-X_10
Download citation
DOI: https://doi.org/10.1007/3-540-36532-X_10
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-00708-1
Online ISBN: 978-3-540-36532-7
eBook Packages: Springer Book Archive