We consider ensuring the security of executed mobile code by applying runtime monitoring. Of the many approaches for code security, the runtime monitoring approach is perhaps the most general and flexible. We have formerly implemented a rule-based language for describing runtime security policies, and now we discuss the verification of those policies.

A security policy can be considered as a specification that restricts the execution of a program in some way. These restrictions can be connected to the program state and the execution history. In this paper, we introduce invariant expressions for our security monitor descriptions, and describe a methodology for proving that the monitor preserves its invariant. Our invariant expressions describe the true meaning of security monitor and relate the monitor state to the execution history and current state of the monitored program. The advantage of our approach is that we can prove specific monitors to guarantee all monitored programs to preserve such properties that cannot in general be effectively proved or disproved of all possible executions of any program.