Multi-session Security Monitoring for Mobile Code

There is increasing demand for running multiple times a number of interacting applications in a secure and controllable way on mobile devices. Such demand is not supported by the Java/.NET security models based on trust domains nor by current security monitors or language-based security approaches. Trust domains don’t allow for interactions while language-based security doesn’t support enough customizable policies. A careful analysis of the security requirements in the booming domain of mobile games reveals that most practical security requirements can be represented with an enhanced notion of pure past temporal Logic augmented with the intuitive notion of session. We propose an approach that allows security policies that are i) expressive enough to capture multiple sessions and interacting applications, ii) suitable for efficient monitoring, iii) convenient for a developer to specify them. Since getting all three at once is impossible, we advocate a logical language, 2D-LTL a bi-dimensional temporal logic fit for multiple sessions and for which efficient monitoring algorithms can be given, and a graphical language based on standard UML sequence diagrams with a tight correspondence between the two. In this paper we show a refined formal model for capturing the notion of session and the correctness and completeness of the monitoring algorithm for security policies expressed in 2D-LTL.