The open Android application development platform allows anyone to create and upload applications to the Android Market for distribution. The main problem with this open design is that many programmers do not pay the necessary attention to the robustness and security of their applications. The result is that many applications on the market today contains defects and vulnerabilities. These applications can be exploited by attackers or can severely influence the performance of the mobile device on which they run.
Users can not verify if mobile applications are secure and error free. They can not determine if an application requesting Internet permission and read permission to your personal information, sends this information over the Internet or if an application behaves badly in terms of battery usage, data usage or responsiveness. Even developers can not always anticipate some errors and vulnerabilities.
This project will extend Java Path Finder, a software model checker engine for the Java programming language, to allow the verification of Android applications. The extension will be used to detect risks and defects in Android applications.My contact details: firstname.lastname@example.org