Abstract
Today, the majority of security errors in software systems are due to implementation errors, as opposed to flaws in fundamental algorithms (e.g., cryptography). Type-safe languages, such as Java, help rule out a class of these errors, such as code-injection through buffer overruns. But attackers simply shift to implementation flaws above the level of the primitive operations of the language (e.g., SQL-injection attacks). Thus, next-generation languages need type systems that can express and enforce application-specific security policies.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
PLT Scheme, http://www.plt-scheme.org/
Leavens, G.T., et al.: Preliminary design of JML: a behavioral interface specification language for Java. SIGSOFT Softw. Eng. Notes 31(3), 1–38 (2006)
The Coq Proof Assistant, http://coq.inria.fr/
Leroy, X.: Formal verification of a realistic compiler. Comm. of the ACM. 52(7), 107–115 (2009)
ACL2, http://userweb.cs.utexas.edu/~moore/acl2/acl2-doc.html
Epigram, http://www.e-pig.org/
Nanevski, A., et al.: Polymorphism and separation in Hoare Type Theory. In: 11th ACM Intl. Conf. on Functional Prog, pp. 62–73. ACM Press, New York (2006)
Malecha, G., et al.: Towards a verified relational database management system. In: 37th ACM Symp. on Principles of Prog, pp. 237–248. ACM Press, New York (2010)
Chlipala, A., et al.: Effective interactive proofs for higher-order imperative programs. In: 14th ACM Intl. Conf. on Functional Prog, pp. 79–90. ACM Press, New York (2009)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2010 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Morrisett, G. (2010). Integrating Types and Specifications for Secure Software Development. In: Kotenko, I., Skormin, V. (eds) Computer Network Security. MMM-ACNS 2010. Lecture Notes in Computer Science, vol 6258. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-14706-7_3
Download citation
DOI: https://doi.org/10.1007/978-3-642-14706-7_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-14705-0
Online ISBN: 978-3-642-14706-7
eBook Packages: Computer ScienceComputer Science (R0)