Name
Abstract | ||
|---|---|---|
This article describes an approach for the automated verification 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 different 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 specification 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 flow specification. 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-refinement 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 specification 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 buffer overflows. |
Year | DOI | Venue |
|---|---|---|
2011 | 10.1007/s00165-010-0159-y | Formal Asp. Comput. |
Keywords | Field | DocType |
security policy verification,security policies,different location,proposed mobile system modeling,mobile systems,information flow,mobile system,location abstraction,access control,generic security-policy specification language,model checking,code location,model checking-based approach,software verification,program security and safety,mobile code benchmarks,information flow specification | Specification language,Model checking,Computer science,Theoretical computer science,Systems modeling,Access control,Security policy,State space,Software verification,Buffer overflow | Journal |
Volume | Issue | ISSN |
23 | 5 | 1433-299X |
Citations | PageRank | References |
12 | 0.64 | 33 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Chiara Braghin | 1 | 105 | 8.86 |
| Natasha Sharygina | 2 | 1068 | 68.33 |
| Katerina Barone-Adesi | 3 | 15 | 1.03 |