A1 Refereed original research article in a scientific journal

Rule-Based Monitors and Policy Invariants for Guaranteeing Mobile Code Security




AuthorsSanna Mäkelä, Sami Mäkelä, Ville Leppänen

Publication year2015

JournalInternational Journal on Information Technologies and Security

Volume7

Issue2

First page 17

Last page36

Number of pages20

ISSN1313-8251


Abstract

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.

 



Downloadable publication

This is an electronic reprint of the original article.
This reprint may differ from the original in pagination and typographic detail. Please cite the original version.





Last updated on 2024-26-11 at 22:04