Jif-Based Verification of Information Flow Policies for Android Apps

Jif-Based Verification of Information Flow Policies for Android Apps

Lina M. Jimenez (Systems and Computing Engineering Department, Universidad de los Andes, Bogotá, Colombia), Martin Ochoa (Singapore University of Technology and Design, Singapore) and Sandra J. Rueda (Systems and Computing Engineering Department, Universidad de los Andes, Bogotá, Colombia)
Copyright: © 2017 |Pages: 15
DOI: 10.4018/IJSSE.2017010102


Android stores and users need mechanisms to evaluate whether their applications are secure or not. Although various previous works use data and control flow techniques to evaluate security features of Android applications, this paper extends those works by using Jif to verify compliance of information flow policies. To do so, the authors addressed some challenges that emerge in Android environments, like automatizing generation of Jif labels for Android applications, and defining translations for Java instructions that are not currently supported by the Jif compiler. Results show that a Jif-based analysis is faster and has a better recall than other available mechanisms, but it also has a slightly lower precision. Jif also provides an open source compiler, generates executable code for an application only if such application meets a defined policy, and checks implicit flows which may be relevant for highly sensitive applications.
Article Preview

1. Introduction

Controlling access and use of users’ data on Android platforms is key. First, Android is the most used platform in a market that keeps growing. Android had 78% of the market in 2013, and grew up to 80% in 2014 (Gartner Inc. 2015a). Furthermore, analysts project the number of mobile devices to grow to 2062 millions of units for 2017 (Gartner Inc. 2015b). Second, security in this platform worries experts as different evaluations have found multiple mobile applications that leak user’s data; while malware do it on purpose (Jiang and Zhou 2012), some applications do it by mistake (BBC 2012), (GSMA 2015). Finally, analysts warn about security in this context, as more people are using mobile devices for various tasks, ranging from management of personal data like family pictures and bank transactions, to management of data from their organizations, like official documents and e-mails (Symantec 2014), (Symantec 2015).

This work focuses on tools to support honest developers. While official stores can evaluate applications and remove those that do not meet expected behavior, it would be better for honest developers, that do not make errors on purpose, to have tools to check their applications before publishing them in stores and having them available to users. Errors in code may appear for several reasons, one of them being that developers cannot detect and fix errors on time because they do not normally use tools for security analysis as part of their development environments.

Traditional approaches to analyze program behavior use static and dynamic analyses. Tools based on static analysis use source code to build an abstract representation of a program’s behavior, and use that representation to evaluate particular properties, like reachability. Possible representations include control flow graphs, data flow graphs, and call dependency graphs (Bhosale 2014), (Fritz 2013), (Reps, Horwitz and Sagiv 1995). Tools based on dynamic analysis monitor a program behavior during execution, by using mechanisms like instrumentation, sandboxing, system calls traces, and dynamic taint marking (Clause, Li and Orso 2007), (Ernst, Static and dynamic analysis: synergy and duality 2003); if the tool detects a dangerous operation, it generates a warning and may even stop the operation if it has the required privileges. For both approaches programmers must first completely develop their applications, and only later they may use tools that are not part of their development environment to evaluate security of such applications. Adjusting applications after finishing them, if an evaluation finds errors, is also more expensive than evaluating and fixing them while they are under development.

This work proposes using Jif, a security-typed language, to build secure Android applications from early development phases, applications that would meet information flow security policies and avoid data leaks. Using a security typed language instead of the mentioned traditional approaches has several advantages: (1) security types enable developers to define various policies, according to particular requirements, (2) a security-typed language supports policy definition from the beginning of the development process, and (3) Jif only generates code that may be executed if the source code meets a defined policy. A developer may use this procedure to offer users a security guarantee; if the source code is available, an app store and even users, could verify policy compliance. Additionally, information flow policies (IFP) guarantee noninterference, that is high level input does not affect low level outputs, unless programmers explicitly use mechanisms to securely modify levels assigned to data (i.e. downgraders and endorsers).

Complete Article List

Search this Journal:
Open Access Articles: Forthcoming
Volume 8: 4 Issues (2017)
Volume 7: 4 Issues (2016)
Volume 6: 4 Issues (2015)
Volume 5: 4 Issues (2014)
Volume 4: 4 Issues (2013)
Volume 3: 4 Issues (2012)
Volume 2: 4 Issues (2011)
Volume 1: 4 Issues (2010)
View Complete Journal Contents Listing