Article Preview
Top1. 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).