RV4ANDROID: An End-to-End Pipeline for Runtime Verification of Cryptographic API Specifications on Contemporary Android Applications
Resumo
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.Referências
Amann, S., Nguyen, H. A., Nadi, S., Nguyen, T. N., and Mezini, M. (2019). A systematic evaluation of static api-misuse detectors. IEEE Trans. Software Eng., 45(12):1170–1188.
Brasil, Presidência da República (2018). Lei nº 13.709, de 14 de agosto de 2018 (Lei Geral de Proteção de Dados Pessoais – LGPD), art. 46. [link].
Chen, F. and Rosu, G. (2007). Mop: an efficient and generic runtime verification framework. In Gabriel, R. P., Bacon, D. F., Lopes, C. V., and Jr., G. L. S., editors, Proceedings of the 22nd Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2007, October 21-25, 2007, Montreal, Quebec, Canada, pages 569–588. ACM.
Daian, P., Falcone, Y., Meredith, P. O., Serbanuta, T., Shiraishi, S., Iwai, A., and Rosu, G. (2015). Rv-android: Efficient parametric android runtime verification, a brief tutorial. In Bartocci, E. and Majumdar, R., editors, Runtime Verification - 6th International Conference, RV 2015 Vienna, Austria, September 22-25, 2015. Proceedings, volume 9333 of Lecture Notes in Computer Science, pages 342–357. Springer.
Gu, T., Sun, C., Ma, X., Cao, C., Xu, C., Yao, Y., Zhang, Q., Lu, J., and Su, Z. (2019). Practical GUI testing of android applications via model abstraction and refinement. In Atlee, J. M., Bultan, T., and Whittle, J., editors, Proceedings of the 41st International Conference on Software Engineering, ICSE 2019, Montreal, QC, Canada, May 25-31, 2019, pages 269–280. IEEE / ACM.
Jin, D., Meredith, P. O., Lee, C., and Rosu, G. (2012). Javamop: Efficient parametric runtime monitoring framework. In Glinz, M., Murphy, G. C., and Pezzè, M., editors, 34th International Conference on Software Engineering, ICSE 2012, June 2-9, 2012, Zurich, Switzerland, pages 1427–1430. IEEE Computer Society.
Kiczales, G., Hilsdale, E., Hugunin, J., Kersten, M., Palm, J., and Griswold, W. G. (2001). An overview of aspectj. In Knudsen, J. L., editor, ECOOP 2001 - Object-Oriented Programming, 15th European Conference, Budapest, Hungary, June 18-22, 2001, Proceedings, volume 2072 of Lecture Notes in Computer Science, pages 327–353. Springer.
Krüger, S., Nadi, S., Reif, M., Ali, K., Mezini, M., Bodden, E., Göpfert, F., Günther, F., Weinert, C., Demmler, D., and Kamath, R. (2017). Cognicrypt: supporting developers in using cryptography. In Rosu, G., Penta, M. D., and Nguyen, T. N., editors, Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering, ASE 2017, Urbana, IL, USA, October 30 - November 03, 2017, pages 931–936. IEEE Computer Society.
Krüger, S., Späth, J., Ali, K., Bodden, E., and Mezini, M. (2021). Crysl: An extensible approach to validating the correct usage of cryptographic apis. IEEE Trans. Software Eng., 47(11):2382–2400.
Leucker, M. and Schallhart, C. (2009). A brief account of runtime verification. J. Log. Algebraic Methods Program., 78(5):293–303.
Li, Y., Yang, Z., Guo, Y., and Chen, X. (2017). Droidbot: a lightweight ui-guided test input generator for android. In Uchitel, S., Orso, A., and Robillard, M. P., editors, Proceedings of the 39th International Conference on Software Engineering, ICSE 2017, Buenos Aires, Argentina, May 20-28, 2017 - Companion Volume, pages 23–26. IEEE Computer Society.
Luo, Q., Zhang, Y., Lee, C., Jin, D., Meredith, P. O., Serbanuta, T., and Rosu, G. (2014). Rv-monitor: Efficient parametric runtime verification with simultaneous properties. In Bonakdarpour, B. and Smolka, S. A., editors, Runtime Verification - 5th International Conference, RV 2014, Toronto, ON, Canada, September 22-25, 2014. Proceedings, volume 8734 of Lecture Notes in Computer Science, pages 285–300. Springer.
Nadi, S., Krüger, S., Mezini, M., and Bodden, E. (2016). Jumping through hoops: why do java developers struggle with cryptography apis? In Dillon, L. K., Visser, W., and Williams, L. A., editors, Proceedings of the 38th International Conference on Software Engineering, ICSE 2016, Austin, TX, USA, May 14-22, 2016, pages 935–946. ACM.
OWASP. MASWE-0021: Improper hashing. [link].
OWASP Mobile Application Security Weakness Enumeration (MASWE), category MASVS-CRYPTO-1.
Patel, P., Srinivasan, G., Rahaman, S., and Neamtiu, I. (2018). On the effectiveness of random testing for android: or how I learned to stop worrying and love the monkey. In Bai, X., Li, J. J., and Ulrich, A., editors, Proceedings of the 13th International Workshop on Automation of Software Test, AST@ICSE 2018, Gothenburg, Sweden, May 28-29, 2018, pages 34–37. ACM.
Pecorelli, F., Catolino, G., Ferrucci, F., Lucia, A. D., and Palomba, F. (2022). Software testing and android applications: a large-scale empirical study. Empir. Softw. Eng., 27(2):31.
Rahaman, S., Xiao, Y., Afrose, S., Shaon, F., Tian, K., Frantz, M., Kantarcioglu, M., and Yao, D. D. (2019). Cryptoguard: High precision detection of cryptographic vulnerabilities in massive-sized java projects. In Cavallaro, L., Kinder, J., Wang, X., and Katz, J., editors, Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, CCS 2019, London, UK, November 11-15, 2019, pages 2455–2472. ACM.
Torres, A., Costa, P. H. T., Amaral, L. H. V., Pastro, J., Bonifácio, R., d’Amorim, M., Legunsen, O., Bodden, E., and Canedo, E. D. (2023). Runtime verification of crypto apis: An empirical study. IEEE Trans. Software Eng., 49(10):4510–4525.
Yang, S., Zhang, H., Wu, H., Wang, Y., Yan, D., and Rountev, A. (2015). Static window transition graphs for android (T). In Cohen, M. B., Grunske, L., and Whalen, M., editors, 30th IEEE/ACM International Conference on Automated Software Engineering, ASE 2015, Lincoln, NE, USA, November 9-13, 2015, pages 658–668. IEEE Computer Society.
Brasil, Presidência da República (2018). Lei nº 13.709, de 14 de agosto de 2018 (Lei Geral de Proteção de Dados Pessoais – LGPD), art. 46. [link].
Chen, F. and Rosu, G. (2007). Mop: an efficient and generic runtime verification framework. In Gabriel, R. P., Bacon, D. F., Lopes, C. V., and Jr., G. L. S., editors, Proceedings of the 22nd Annual ACM SIGPLAN Conference on Object-Oriented Programming, Systems, Languages, and Applications, OOPSLA 2007, October 21-25, 2007, Montreal, Quebec, Canada, pages 569–588. ACM.
Daian, P., Falcone, Y., Meredith, P. O., Serbanuta, T., Shiraishi, S., Iwai, A., and Rosu, G. (2015). Rv-android: Efficient parametric android runtime verification, a brief tutorial. In Bartocci, E. and Majumdar, R., editors, Runtime Verification - 6th International Conference, RV 2015 Vienna, Austria, September 22-25, 2015. Proceedings, volume 9333 of Lecture Notes in Computer Science, pages 342–357. Springer.
Gu, T., Sun, C., Ma, X., Cao, C., Xu, C., Yao, Y., Zhang, Q., Lu, J., and Su, Z. (2019). Practical GUI testing of android applications via model abstraction and refinement. In Atlee, J. M., Bultan, T., and Whittle, J., editors, Proceedings of the 41st International Conference on Software Engineering, ICSE 2019, Montreal, QC, Canada, May 25-31, 2019, pages 269–280. IEEE / ACM.
Jin, D., Meredith, P. O., Lee, C., and Rosu, G. (2012). Javamop: Efficient parametric runtime monitoring framework. In Glinz, M., Murphy, G. C., and Pezzè, M., editors, 34th International Conference on Software Engineering, ICSE 2012, June 2-9, 2012, Zurich, Switzerland, pages 1427–1430. IEEE Computer Society.
Kiczales, G., Hilsdale, E., Hugunin, J., Kersten, M., Palm, J., and Griswold, W. G. (2001). An overview of aspectj. In Knudsen, J. L., editor, ECOOP 2001 - Object-Oriented Programming, 15th European Conference, Budapest, Hungary, June 18-22, 2001, Proceedings, volume 2072 of Lecture Notes in Computer Science, pages 327–353. Springer.
Krüger, S., Nadi, S., Reif, M., Ali, K., Mezini, M., Bodden, E., Göpfert, F., Günther, F., Weinert, C., Demmler, D., and Kamath, R. (2017). Cognicrypt: supporting developers in using cryptography. In Rosu, G., Penta, M. D., and Nguyen, T. N., editors, Proceedings of the 32nd IEEE/ACM International Conference on Automated Software Engineering, ASE 2017, Urbana, IL, USA, October 30 - November 03, 2017, pages 931–936. IEEE Computer Society.
Krüger, S., Späth, J., Ali, K., Bodden, E., and Mezini, M. (2021). Crysl: An extensible approach to validating the correct usage of cryptographic apis. IEEE Trans. Software Eng., 47(11):2382–2400.
Leucker, M. and Schallhart, C. (2009). A brief account of runtime verification. J. Log. Algebraic Methods Program., 78(5):293–303.
Li, Y., Yang, Z., Guo, Y., and Chen, X. (2017). Droidbot: a lightweight ui-guided test input generator for android. In Uchitel, S., Orso, A., and Robillard, M. P., editors, Proceedings of the 39th International Conference on Software Engineering, ICSE 2017, Buenos Aires, Argentina, May 20-28, 2017 - Companion Volume, pages 23–26. IEEE Computer Society.
Luo, Q., Zhang, Y., Lee, C., Jin, D., Meredith, P. O., Serbanuta, T., and Rosu, G. (2014). Rv-monitor: Efficient parametric runtime verification with simultaneous properties. In Bonakdarpour, B. and Smolka, S. A., editors, Runtime Verification - 5th International Conference, RV 2014, Toronto, ON, Canada, September 22-25, 2014. Proceedings, volume 8734 of Lecture Notes in Computer Science, pages 285–300. Springer.
Nadi, S., Krüger, S., Mezini, M., and Bodden, E. (2016). Jumping through hoops: why do java developers struggle with cryptography apis? In Dillon, L. K., Visser, W., and Williams, L. A., editors, Proceedings of the 38th International Conference on Software Engineering, ICSE 2016, Austin, TX, USA, May 14-22, 2016, pages 935–946. ACM.
OWASP. MASWE-0021: Improper hashing. [link].
OWASP Mobile Application Security Weakness Enumeration (MASWE), category MASVS-CRYPTO-1.
Patel, P., Srinivasan, G., Rahaman, S., and Neamtiu, I. (2018). On the effectiveness of random testing for android: or how I learned to stop worrying and love the monkey. In Bai, X., Li, J. J., and Ulrich, A., editors, Proceedings of the 13th International Workshop on Automation of Software Test, AST@ICSE 2018, Gothenburg, Sweden, May 28-29, 2018, pages 34–37. ACM.
Pecorelli, F., Catolino, G., Ferrucci, F., Lucia, A. D., and Palomba, F. (2022). Software testing and android applications: a large-scale empirical study. Empir. Softw. Eng., 27(2):31.
Rahaman, S., Xiao, Y., Afrose, S., Shaon, F., Tian, K., Frantz, M., Kantarcioglu, M., and Yao, D. D. (2019). Cryptoguard: High precision detection of cryptographic vulnerabilities in massive-sized java projects. In Cavallaro, L., Kinder, J., Wang, X., and Katz, J., editors, Proceedings of the 2019 ACM SIGSAC Conference on Computer and Communications Security, CCS 2019, London, UK, November 11-15, 2019, pages 2455–2472. ACM.
Torres, A., Costa, P. H. T., Amaral, L. H. V., Pastro, J., Bonifácio, R., d’Amorim, M., Legunsen, O., Bodden, E., and Canedo, E. D. (2023). Runtime verification of crypto apis: An empirical study. IEEE Trans. Software Eng., 49(10):4510–4525.
Yang, S., Zhang, H., Wu, H., Wang, Y., Yan, D., and Rountev, A. (2015). Static window transition graphs for android (T). In Cohen, M. B., Grunske, L., and Whalen, M., editors, 30th IEEE/ACM International Conference on Automated Software Engineering, ASE 2015, Lincoln, NE, USA, November 9-13, 2015, pages 658–668. IEEE Computer Society.
Publicado
01/09/2026
Como Citar
COSTA, Pedro Henrique Teixeira; BONIFÁCIO, Rodrigo.
RV4ANDROID: An End-to-End Pipeline for Runtime Verification of Cryptographic API Specifications on Contemporary Android Applications. In: SALÃO DE FERRAMENTAS - SIMPÓSIO BRASILEIRO DE CIBERSEGURANÇA (SBSEG), 26. , 2026, Armação dos Búzios/RJ.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
2026
.
p. 196-205.
DOI: https://doi.org/10.5753/sbseg_estendido.2026.33679.
