Post date: Oct 30, 2008 8:12:12 PM
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 Bytecode Verifier used by the Java Virtual Machine. The Bytecode Verifier is not only responsible for statically verifying that class files to be loaded have the correct structure, it also uses a synthetic execution technique to attempt to verify that the security requirements of the bytecodes are met.
This talk describes a method for representing the static aspects of the JVM security model in the form of constraints. The lightweight modeling Alloy modeling can then be used to search for counterexamples to those constraints; this is done by providing a translation between the byte codes and a set of relation initializers in Alloy. Any counterexamples found by the Alloy analyzer correspond directly to insecure code. The work to date is illustrated by analyzing a simplified version of a real-world type confusion attack.
Future extensions of the work are discussed, with emphasis on other VM instruction sets to which the analysis might be applied, e.g. the Microsoft CLR that underlies C# and .NET.
Date: November 5, 2008
Speaker: Mark Reynolds
Slides: attached.