Show simple item record

dc.contributor.authorReynolds, Mark C.en_US
dc.date.accessioned2011-10-20T04:51:50Z
dc.date.available2011-10-20T04:51:50Z
dc.date.issued2008-12-30
dc.identifier.citationReynolds, Mark C. . "Lightweight Modeling of Java Virtual Machine Security Constraints using Alloy", Technical Report BUCS-TR-2008-031, Computer Science Department, Boston University, December 30, 2008. [Available from: http://hdl.handle.net/2144/1723]
dc.identifier.urihttps://hdl.handle.net/2144/1723
dc.description.abstractThe 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.en_US
dc.language.isoen_US
dc.publisherBoston University Computer Science Departmenten_US
dc.relation.ispartofseriesBUCS Technical Reports;BUCS-TR-2008-031
dc.titleLightweight Modeling of Java Virtual Machine Security Constraints using Alloyen_US
dc.typeTechnical Reporten_US


This item appears in the following Collection(s)

Show simple item record