RV4ANDROID: An End-to-End Pipeline for Runtime Verification of Cryptographic API Specifications on Contemporary Android Applications
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 reachab...