Extraction of Properties in C Implementations of Security APIs for the Verification of Java Applications

Date Added: May 2009
Format: PDF

Java applications utilize various security APIs for cryptography and access control, such as available through packages and javax.crypto. For performance reasons, these libraries internally use an implementation written in C, accessed through the Java Native Interface. The goal is to extract properties in the source code of the C library, and translate these assertions back into the Java domain. This allows these properties to be used in verification of Java code, opening up various applications that are not possible when verifying binary code.