BEGIN:VCALENDAR
VERSION:2.0
PRODID:-//Memento EPFL//
BEGIN:VEVENT
SUMMARY:Automated Verification of Security Policies in Mobile Code
DTSTART:20090112T161500
DTSTAMP:20260503T095407Z
UID:bf71555f5231e6db4316b462e2f173e4ef6714b3c036f9ce169da66e
CATEGORIES:Conferences - Seminars
DESCRIPTION:Prof. Natasha Sharygina\, Universita della Svizzera Italiana (
 USI) and Carnegie Mellon University (CMU)\nIn this talk I will describe an
  approach for the automated verification of mobile programs. Mobile system
 s are characterized by the explicit notion of locations (e.g.\, sites wher
 e 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 n
 et. The location net summarizes the hierarchical nesting of threads consti
 tuting a mobile program and enables specifying security policies. We forma
 lize a language for specifying security policies and show how mobile progr
 ams can be exhaustively analyzed against any given security policy by usin
 g model checking techniques.\n\nWe developed and experimented with a proto
 type framework for analysis of mobile code\, using our model checker\, SAT
 ABS. Our approach employs SATABS's support for unbounded thread creation a
 nd enhances it with location net abstractions\, which are essential for ve
 rifying large mobile programs. Our experimental results for various benchm
 arks are encouraging and demonstrate advantages of the model checking-base
 d approach\, which combines the validation of security properties with oth
 er checks\, such as validation for buffer overflows.\n\nThis is joint work
  with my USI students\, Chiara Braghin and Katerina Barone-Adesi.\n\nN. Sh
 arygina's homepage
LOCATION:BC 410 https://plan.epfl.ch/?room==BC%20410
STATUS:CONFIRMED
END:VEVENT
END:VCALENDAR