Digital Commons Network^™

A Formal Specification In Jml Of The Java Security Package, Poonam Agarwal, Carlos E. Rubio-Medrano, Yoonsik Cheon, Patricia J. Teller

Departmental Technical Reports (CS)

The Java security package allows a programmer to add security features to Java applications. Although the package provides a complex application programming interface (API), its informal description, e.g., Javadoc comments, is often ambiguous or imprecise. Nonetheless, the security of an application can be compromised if the package is used without a concrete understanding of the precise behavior of the API classes and interfaces, which can be attained via formal specification. In this paper, we present our experiences in formally specifying the Java security package in JML, a formal behavior interface specification language for Java. We illustrate portions of our JML …