Software Model Checking for Confidentiality

Protecting confidentiality of data manipulated by programs is a growing concern in various application domains. In particular, for extensible software platforms that allow users to install third party plugins, there is a need for an automated method that can verify that programs do not leak confidential information. Software model checking has emerged as an effective technique for checking programs with respect to correctness requirements. However, existing methods and tools are not applicable for specifying and verifying confidentiality properties. In this talk, I will describe a specification framework for confidentiality, decision procedures for finite state systems, an abstraction-based program analysis technique, and a prototype tool for analyzing bytecode of a set of methods of J2ME midlets for mobile devices.

Joint work with Pavol Cerny

Speaker Details

Rajeev Alur is Zisman Family Professor and Graduate Group Chair in the Department of Computer and Information Science at University of Pennsylvania. He obtained his bachelor’s degree in computer science from Indian Institute of Technology at Kanpur in 1987, and PhD in computer science from Stanford University in 1991. Before joining Penn in 1997, he was with Computing Science Research Center in Bell Laboratories. His areas of research include formal modeling and analysis of reactive systems, hybrid systems, model checking, software verification, logics and automata, and design automation for embedded software. His awards include The CAV Award (2008), President of India’s Gold Medal for academic excellence (1987), US National Science Foundation’s CAREER (1997) and ITR (2001) awards, Alfred P. Sloan Faculty Fellowship (1999), ACM Fellow (2007), IEEE Fellow (2007), and designation as a highly cited scientist by the Institute for Scientific Information (2005). Prof. Alur has (co)chaired scientific meetings such as CAV (Intl Conf on Computer-Aided Verification), EMSOFT (ACM Symp on Embedded Software), HSCC (Intl Conf on Hybrid Systems: Computation and Control), and LICS (IEEE Symp on Logic in Computer Science), and served as the chair of ACM SIGBED (Special Interest Group on Embedded Systems).

Date:
Speakers:
Rajeev Alur