Software Model Checking for Confidentiality

Опубликовано 6 сентября 2016, 18:44

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