CMV: Automatic Verification of Complete Mediation for Java Virtual Machines

Runtime monitoring systems play an important role in system security, and verification efforts that ensure that these systems satisfy certain desirable security properties are growing in importance. One such security property is complete mediation, which requires that sensitive operations are performed by a piece of code only after the monitoring system authorizes these actions. In this paper, we describe a verification technique that is designed to check for the satisfaction of this property directly on code from Java standard libraries. We describe a tool CMV that implements this technique and automatically checks shrink-wrapped Java bytecode for the complete mediation property. Experimental results on running our tool over several thousands of lines of bytecode from the Java libraries suggest that our approach is scalable, and leads to a very significant reduction in human efforts required for system verification.

 @inproceedings{
  ASIACCS08:CMV,
  author        = {Sistla, A. Prasad and V.N. Venkatakrishnan and Michelle Zhou and Hilary Branske},
  crossref      = {ASIACCS08},
  title         = {{CMV}: Automatic Verification of Complete Mediation for {Java} Virtual Machines}
}
@proceedings{
  ASIACCS08,
  location      = {Tokyo, Japan},
  booktitle     = {ACM Symposium on Information, Computer and Communications Security},
  month         = mar,
  year          = {2008}
}