Abstract: In this talk I will describe an approach for the automate d verification of mobile programs. Mobile systems are characterized by th e explicit notion of locations (e.g., sites where they run) and the abilit y 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 program s can be exhaustively analyzed against any given security policy by using model checking techniques.

We developed and experimented with a prototype framework for analysi s of mobile code, using the SATABS model checker. Our approach relies on SATABS's support for unbounded thread creation and enhances it with location net abstractions, which are essential for verifying large mobile programs. Our experimental results on various benchmarks are encouraging and demonstrate advantages of the model checking-based approach, which combines the validation of security properties with other checks, such as for buffer overflows.

Natasha Sharygina is a professor at the Department of Informatics of the University of Lugano, Switzerland. She received her Ph.D. from the University of Texas at Austin, USA in 2002. Her professional experience includes consulting at Bell Labs, Lucent Technologies at the Computing Sciences Research in 2000 - 2001 and a research fellow position at Carnegie Mellon University, Software Engineering Institute in 2002 - 2005. Prof. Sharygina collaborates closely with members of the CMU School of Computer Science where she is an adjunct assistant professor. Appointments: dcm@cs.cmu.edu