|Title||Automated Verification of Security Policies in Mobile Code.|
|Publication Type||Conference Paper|
|Year of Publication||2007|
|Authors||Braghin, C., Sharygina Natasha, and Barone Adesi Katerina|
|Conference Name||Integrated Formal Methods (IFM)|
|Publisher||Springer, Volume 4591|
This paper describes an approach for the automated verification of mobile programs. Mobile systems are characterized by the explicit notion of locations (e.g., sites where they run) and the ability to execute at different locations, yielding a number of security issues. We give formal semantics to mobile systems as Labeled Kripke Structures, which encapsulate the notion of the location net. The location net summarizes the hierarchical nesting of threads constituting a mobile program and enables specifying security policies. We formalize a language for specifying security policies and show how mobile programs can be exhaustively analyzed against any given security policy by using model checking techniques.