Abstract
Language-based security leverages program analysis and program rewriting to enforce security policies. The approach promises efficient enforcement of fine-grained access control policies and depends on a trusted computing base of only modest size. This paper surveys progress and prospects for the area, giving overviews of in-lined reference monitors, certifying compilers, and advances in type theory.
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.
Similar content being viewed by others
References
B. Alpern and F.B. Schneider. Defining liveness. Information Processing Letters 21(4):181–185, Oct. 1985.
B. Bershad, S. Savage, P. Pardyak, E. Sirer, M. Fiuczynski, D. Becker, C. Chambers, and S. Eggers. Extensibility, safety and performance in the SPIN operating system. In Proc. 15th ACM Symp. on Operating System Principles (SOSP), pages 267–284, Copper Mountain, Dec. 1995.
R. L. Constable et al. Implementing Mathematics with the NuPRL Proof Development System. Prentice-Hall, 1986.
D. Engler, M. Kaashoek, and J. O’Toole. Exokernel: An operating system architecture for application-level resource management. In Proc. 15th ACM Symp. on Operating System Principles (SOSP), Copper Mountain, 1995.
U. Erlingsson and F. B. Schneider. SASI enforcement of security policies: A retrospective. In Proceedings of the New Security Paradigms Workshop, Ontario, Canada, Sept. 1999.
U. Erlingsson and F. B. Schneider. IRM enforcement of java stack inspection. In IEEE Symposium on Security and Privacy, Oakland, California, May 2000.
R. Harper, F. Honsell, and G. Plotkin. A fram ework for defining logics. Journal of the ACM, 40(1):143–184, Jan. 1993.
L. Lamport. Proving the correctness ofm ultiprocess programs. IEEE Transactions on Software Engineering, SE-3(2):125–143, March 1977.
L. Lamport. Logical Foundation. In Distributed Systems-Methods and Tools for Specification, pages 119–130, Lecture Notes in Computer Science, Vol 190. M. Paul and H.J. Siegert, editors. Springer-Verlag, 1985, New York.
J. McLean. A general theory ofc omposition for trace sets closed under selective interleaving functions. In Proc. 1994 IEEE Computer Society Symposium on Research in Security and Privacy, pages 79–93, Oakland, Calif., May 1994.
G. Morrisett, D. Walker, K. Crary, and N. Glew. From System F to typed assembly language. In Proc. 25th ACM Symp. on Principles of Programming Languages (POPL), pages 85–97, San Diego California, USA, January 1998.
G. Morrisett, D. Walker, K. Crary, and N. Glew. From System F to typed assembly language. ACM Transactions on Programming Languages and Systems, 21(3):528–569, May 1999.
G. C. Necula and P. Lee. Safe kernel extensions without run-time checking. In Proceedings of Operating System Design and Implementation, pages 229–243, Seattle, Oct. 1996.
G. C. Necula. Proof-carrying code. In Proc. 24th ACM Symp. on Principles of Programming Languages (POPL), pages 106–119, Jan. 1997.
J. Saltzer and M. Schroeder. The protection ofi nformation in computer systems. Proceedings of the IEEE, 9(63), Sept. 1975.
F. B. Schneider, editor. Trust in Cyberspace. National Academy Press, Washington, D.C., 1999.
F. B. Schneider. Enforceable security policies. ACM Transactions on Information and System Security, 2(4), Mar. 2000.
M. Seltzer, Y. Endo, C. Small, and K. Smith. Dealing with disaster: Surviving misbehaved kernel extensions. In Proc. USENIX Symp. on Operating Systems Design and Implementation (OSDI), pages 213–227, Seattle, Washington, Oct. 1996.
D. Tarditi, G. Morrisett, P. Cheng, C. Stone, R. Harper, and P. Lee. TIL: A typedirected optimizing compiler for ML. In ACM Conf. on Programming Language Design and Implementation, pages 181–192, Philadelphia, May 1996.
R. Wahbe, S. Lucco, T. Anderson, and S. Graham. Efficient software-based fault isolation. In Proc. 14th ACM Symp. on Operating System Principles (SOSP), pages 203–216, Asheville, Dec. 1993.
H. Xi and F. Pfenning. Eliminating array bound checking through dependent types. In Proc. ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 249–257, Montreal Canada, June 1998.
E. Yasuhiro, J. Gwertzman, M. Seltzer, C. Small, K.A. Smith, and D. Tang. VINO: The 1994 fall harvest. Technical Report TR-34-94, Harvard Computer Center for Research in Computing Technology, 1994.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Schneider, F.B., Morrisett, G., Harper, R. (2001). A Language-Based Approach to Security. In: Wilhelm, R. (eds) Informatics. Lecture Notes in Computer Science, vol 2000. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44577-3_6
Download citation
DOI: https://doi.org/10.1007/3-540-44577-3_6
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-41635-7
Online ISBN: 978-3-540-44577-7
eBook Packages: Springer Book Archive