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.
If you cannot see the document below, the PDF document is most likely not freely accessible. In this case, please try to access the document via this link.
% BibTex
@inproceedings{Reynolds10,
author = {Mark C. Reynolds},
editor = {Marc Frappier and
Uwe Gl{\"{a}}sser and
Sarfraz Khurshid and
R{\'{e}}gine Laleau and
Steve Reeves},
title = {Lightweight Modeling of Java Virtual Machine Security Constraints},
booktitle = {Abstract State Machines, Alloy, {B} and Z, Second International Conference,
{ABZ} 2010, Orford, QC, Canada, February 22-25, 2010. Proceedings},
series = {Lecture Notes in Computer Science},
volume = {5977},
pages = {146--159},
publisher = {Springer},
year = {2010},
url = {https://doi.org/10.1007/978-3-642-11811-1\_12},
doi = {10.1007/978-3-642-11811-1\_12},
timestamp = {Tue, 14 May 2019 10:00:50 +0200},
biburl = {https://dblp.org/rec/conf/asm/Reynolds10.bib},
bibsource = {dblp computer science bibliography, https://dblp.org}
}