View article

Software model checking has emerged as an effective technique for checking programs with respect to correctness requirements. Existing tools analyze individual program executions, and are not applicable to checking confidentiality properties that require reasoning about equivalence among executions. In this paper, we develop an automated analysis technique for such properties. A motivating application is verification of J2ME midlets for mobile devices, where a central correctness requirement concerns confidentiality of data that the user wants to keep secret. For programs for which an upper bound on the number of iterations can be computed statically for each loop, our method produces a logical formula that precisely characterizes the confidentiality requirement, and we identify syntactic restrictions under which its validity can be decided by existing decision procedures. For general while-programs, our method uses invariants for over-approximations, coupled with underapproximations via loop unrolling. We demonstrate feasibility of our approach by analyzing a number of illustrative Java methods.