RV4ANDROID: An End-to-End Pipeline for Runtime Verification of Cryptographic API Specifications on Contemporary Android Applications

Abstract

The Java Cryptography Architecture (JCA), the standard cryptographic API for Java and Android, is notoriously difficult to use correctly, making cryptographic API misuse a major source of software vulnerabilities. Runtime verification (RV) can detect such misuses during execution, providing concrete evidence of reachable vulnerabilities, but its effectiveness depends on exercising the monitored code. Existing Android RV tooling is also outdated and unable to instrument many contemporary applications. Here we present RV4ANDROID, an end-to-end runtime verification framework for contemporary Android applications. RV4ANDROID modernizes the instrumentation pipeline, compiles JCA specifications into runtime monitors, injects them into APKs, and automates execution with Android test-generation tools while measuring execution coverage. We evaluated RV4ANDROID on 33 official gov.br apps using an Android test case generation tool (APE) under a one-hour execution budget. We found that 90.9% of the apps (30 of 33) triggered at least one JCA violation at runtime, with weak cryptographic hashing (SHA-1 or MD5) as the strongest security signal. Moreover, 96% of all distinct violations were detected within the first ten minutes of execution, indicating that RV4ANDROID can uncover most runtime cryptographic misuses quickly while remaining applicable to contemporary Android applications.