Epistemic Temporal Logic for Specifying and Checking Mobile Apps

Abstract

Interactive applications that manipulate our personal information pervade the modern world. Language based security attempts to formally define and enforce security policies for applications, leading to technical and pragmatic frameworks. However, it is unclear how to apply traditional techniques to modern applications (such as Android apps). In this work, we define a framework for interactive applications that manipulate user input, communicate with observers, and read time-varying secrets. We define an epistemic temporal logic that allows us to state security policies for programs written in our formalism, and show how our logic subsumes prior logics and encodes a variety of traditional security properties (such as gradual release). Critically, our logic allows us to relate user input configurations (coming from, e.g., GUI interactions) to knowledge that is released about secret inputs. Finally, we present preliminary results in checking Android programs using symbolic execution. Our symbolic executor certifies that a Java program satisfies formulas in our logic corresponding to security properties.

Other suggested papers

See the PLDG wiki page