Abstract
The DroidSafe project developed effective program analysis techniques and tools to uncover malicious code in Android mobile applications. The core of the system is a static information flow analysis that reports the context under which sensitive information is used. For example, “Application A has the potential to send location information to network address 128.6.21.6 on ‘Button B’ press”. The DroidSafe project invested significant time developing a comprehensive semantic model of Android run-time behaviors alongside the analysis to achieve acceptable precision, accuracy, and scalability for real-world Android applications. The combined system has been demonstrated to be the most precise and accurate information flow analysis for Android applications. The analysis results can be used to automatically check applications for security policy violations, and the results can help a human analyst inspect sensitive behaviors of an app, increasing accuracy and throughput of application vetting. For each of the last six APAC engagements to date, the DroidSafe team has been unsurpassed in malware diagnosis accuracy and human-analysis diagnosis throughput. To address subtle functional correctness bugs and vulnerabilities, we have produced a formal model of (part of) the Android system capable of supporting proofs of functional correctness of simple but non-trivial Android apps. We also explored how to move precise static analysis and verification techniques from specialized research tools to an approach that can feasibly be adopted by programmers in the real world. The critical issue in doing so is the lack of precision that such analyses inevitably encounter when analyzing programs that occur in practice. Our hypothesis is that, in existing programs, only a small percentage of the code (the code’s dark corners) is responsible for this lack of precision. We found that in many cases relatively straightforward code modifications can yield code that is analyzable and still practical.