We are on the cusp of a major opportunity: software tools that take advantage of Big Code. Specifically, Big Code will enable novel tools in areas such as security enhancers, bug finders, and code synthesizers. What do researchers need from Big Code to make progress on their tools? Our answer is an infrastructure that consists of 100,000 executable Java programs together with a set of working tools and an environment for building new tools.
The current security mechanisms for Android apps, both static and dynamic analysis approaches, are insufficient for detection and prevention of the increasingly dynamic and sophisticated security attacks.
Permission-induced attacks, i.e., security breaches enabled by permission misuse, are among the most critical and frequent issues threatening the security of Android devices. By ignoring the temporal aspects of an attack during the analysis and enforcement, the state-of-the-art approaches aimed at protecting the users against such attacks are prone to have low-coverage in detection and high-disruption in prevention of permission-induced attacks. To address the aforementioned shortcomings, we present Terminator, a temporal permission analysis and enforcement framework for Android.
Recent introduction of a dynamic permission model in Android, allowing the users to grant and revoke permissions a at the installation of an app, has made it much harder to properly test apps. Since an app's behavior may change depending on the granted permissions, it needs to be tested under a wide range of granted permission combinations.
We present a comprehensive review of the existing approaches for Android security analysis. The review is carried out to achieve the following objectives:
The Alloy specification language, and the corresponding Alloy Analyzer, have received much attention in the last two decades with applications in many areas of software engineering. Increasingly, formal analyses enabled by Alloy are desired for use in an on-line mode, where the specifications are automatically kept in sync with the running, possibly changing, software system. However, given Alloy Analyzer's reliance on computationally expensive SAT solvers, an important challenge is the time it takes for such analyses to execute at runtime.
COVERT is a tool for compositional verification of Android inter-application vulnerabilities. It automatically identifies vulnerabilities that occur due to the interaction of apps comprising a system. Subsequently, it determines whether it is safe for a bundle of apps, requiring certain permissions and potentially interacting with each other, to be installed together.
ISR
