A Model Checking-based Approach for Security Policy Veriﬁcation of Mobile Systems

Publication Type:

Journal Article

Authors:

Braghin, C.; Sharygina, N.; Barone-Adesi, K.

Source:

Formal Aspects of Computing Journal, Springer (2010)

Abstract:

This article describes an approach for the automated veriﬁcation of mobile systems. Mobile systems are characterized by the explicit notion of location (e.g., sites where they run) and the ability to execute at diﬀerent locations, yielding a number of security issues. To this aim, we formalize mobile systems as Labeled Kripke Structures, encapsulating the notion of location net that describes the hierarchical nesting of the threads constituting the system. Then, we formalize a generic security-policy speciﬁcation language that includes rules for expressing and manipulating the code location. In contrast to many other approaches, our technique supports both access control and information ﬂow speciﬁcation.

We developed a prototype framework for model checking of mobile systems. It works directly on the program code (in contrast to most traditional process-algebraic approaches that can model only limited details of mobile systems) and uses abstraction-reﬁnement techniques, based also on location abstractions, to manage the program state space. We experimented with a number of mobile code benchmarks by verifying various security policies. The experimental results demonstrate the validity of the proposed mobile system modeling and policy speciﬁcation formalisms and highlight the advantages of the model checking-based approach, which combines the validation of security properties with other checks, such as the validation of buﬀer overﬂows.

Notes:

to appear

BibTex

@article { BSB10,
	title = {A Model Checking-based Approach  for Security Policy Veriﬁcation  of Mobile Systems},
	journal = {Formal Aspects of Computing Journal},
	year = {2010},
	note = {to appear},
	publisher = {Springer},
	author = {Chiara Braghin and  Natasha Sharygina and  Katerina Barone-Adesi}
}

Attachment	Size
bsb_facj2010.pdf	543.78 KB