Monitoring Android Applications for SecLTL formulas 


Android has a huge number of diverse applications. And most of these
applications exchange and share data with other applications, moreover most
of them are intended to function on users' personal or confidential data like
user contacts, bank account details, credit card details, and user details. Hence,
the guarantee that the program does its intended purpose and handles users'
personal or confidential data with care becomes very significant.

The goal of this work is to present a way of monitoring Android applica-
tions for SecLTL formulas. SecLTL, a recently proposed temporal logic, is an
extension of LTL with a new Hide operator which can specify information ow
properties. Information ow properties in security are properties that ensure
that the program will not leak any confidential information to the observer or
attacker. It is essential that in reactive systems, the secrecy requirements of
confidential information may be changed over time depending on the environ-
ment it interacts with. In some cases, it might be required to reveal confidential
information in order to correctly fulfill other functions. SecLTL also can specify
when and under which conditions private information must not leak to public
output.

In this work we present the framework for monitoring Android applications
for SecLTL formula and its algorithm for implementation. The core idea is to
dynamically execute the application, and trace its execution. And while tracing
its execution at run-time we monitor SecLTL formula. Monitoring SecLTL for-
mula is based on constructing its alternating automaton, and traverse automata
using an on-the-y technique.