Abstract
The Java programming language has been widely described as secure by design. Nevertheless, a number of serious security vulnerabilities have been discovered in Java, particularly in the component known as the Bytecode Verifier. This paper describes a method for representing Java security constraints using the Alloy modeling language. It further describes a system for performing a security analysis on any block of Java bytecodes by converting the bytes into relation initializers in Alloy. Any counterexamples found by the Alloy analyzer correspond directly to insecure code. Analysis of a real world malicious applet is given to demonstrate the efficacy of the approach. This type of analysis represents a significant departure from standard malware detection methods based on signatures or anomaly detection.
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
Alloy website, http://alloy.mit.edu
Jackson, D.: Software Abstractions: Logic, Language and Analysis. MIT Press, Cambridge (2006)
McGraw, G., Felten, E.: Securing Java: Getting Down to Business with Mobile Code, 2nd edn. Wiley, New York (1999)
Common Vulnerabilities and Exposures, http://cve.mitre.org
BlackBox Security Advisory, http://www.ca.com/us/securityadvisor/virusinfo/virus.aspx?ID=36725
Java and Java Virtual Machine security vulnerabilities and their exploitation techniques, http://www.blackhat.com/presentations/bh-asia-02/LSD/bh-asia-02-lsd.pdf
Lindholm, T., Yellin, F.: The Java Virtual Machine Specification Second Edition. Addison Wesley, Boston (2003)
Xu, H.: Java Security Model and Bytecode Verification, http://www.cis.umassd.edu/~hxu/Papers/UIC/JavaSecurity.PDF
Posegga, J., Vogt, H.: Java bytecode verification using model checking, http://eprints.kfupm.edu.sa/47269
Leroy, X.: Java Bytecode Verification: An Overview. In: Berry, G., Comon, H., Finkel, A. (eds.) CAV 2001. LNCS, vol. 2102, pp. 265–285. Springer, Heidelberg (2001)
Jakarta BCEL, http://jakarta.apache.org/bcel
DJ disassembler, http://members.fortunecity.com/neshkov/dj.html
Jasmin assembler, http://jasmin.sourceforge.net
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
Reynolds, M.C. (2010). Lightweight Modeling of Java Virtual Machine Security Constraints. In: Frappier, M., Glässer, U., Khurshid, S., Laleau, R., Reeves, S. (eds) Abstract State Machines, Alloy, B and Z. ABZ 2010. Lecture Notes in Computer Science, vol 5977. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-11811-1_12
Download citation
DOI: https://doi.org/10.1007/978-3-642-11811-1_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-11810-4
Online ISBN: 978-3-642-11811-1
eBook Packages: Computer ScienceComputer Science (R0)