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. Categories and Subject Descriptors D.4.6 [Operating Systems]: Securi...

• Type: Conference
• Year: 2008
• Where: CCS
• Authors: A. Prasad Sistla, V. N. Venkatakrishnan, Michelle Zhou, Hilary Branske
• Keywords: CCS 2008, Certain Desirable Security, Complete Mediation, Runtime Monitoring, Security Privacy