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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
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)