Security Checking Experiments with Mobile Services

In this paper, we continue to investigate the problem of software security. The problem is to check if software under test has some vulnerabilities such as exceeding of admissible values of input/output parameters or internal variables or can reach states where the software (service) behavior is not defined. We illustrate by experiments that the well-known verifier Java Path Finder (JPF) can be utilized for this purpose. We apply JPF-mobile to Android applications and results of security checking experiments are presented.