With the wide variety of applications offered by Android, this system has been able to dominate the smartphone market. These applications provide all kinds of features and services that have become highly requested and welcomed by users. Besides, these applications represent risky vehicles for malware on Android devices. In this paper, we propose a novel formal technique to enforce the security of Android applications. We start off with an untrusted Android application and a security policy, and we end up in a new version of the application that behaves according to the policy. To ensure the correctness of results, we use formal methods in each step of the process, either in the system and the security policy specification or in the enforcement technique itself. The target application is reverse-engineered to its assembly-like code, Smali. An executable semantics called k-Smali was defined for this code using a language definitional framework, called k Framework. Security policies are specified in LTL-logic. The enforcement step consists of integrating the LTL formula in the k-Smali program using rewriting. It aims to rewrite the system specification automatically so that it satisfies the requested formula.
IOS Press, Inc.
6751 Tepper Drive
Clifton, VA 20124
Tel.: +1 703 830 6300
Fax: +1 703 830 2300 email@example.com
(Corporate matters and books only) IOS Press c/o Accucoms US, Inc.
For North America Sales and Customer Service
West Point Commons
Lansdale PA 19446
Tel.: +1 866 855 8967
Fax: +1 215 660 5042 firstname.lastname@example.org