Verificação Formal de Software para Internet das Coisas com Validação de Aplicações em Kotlin/Java: Mapeamento Sistemático Preliminar
Resumo
Esse projeto destina-se à utilização de técnicas de verificação formal em bytecodes Kotlin/Java para identificação de deadlocks, memory leak, arithmetic overflow e data race em aplicações IoT. Para isso, será utilizada a ferramenta de verificação ESBMC-Jimple em uma aplicação Android para detectar possíveis vulnerabilidades e tratá-las visando à segurança e melhoria do software.Referências
Biere, A., Cimatti, A., Clarke, E. M., Strichman, O., and Zhu, Y. (2009). Bounded model checking. Handbook of satisfiability, 185(99):457–481.
Cordeiro, L., Kesseli, P., Kroening, D., Schrammel, P., and Trtik, M. (2018). Jbmc: A bounded model checking tool for verifying java bytecode. In International Conference on Computer Aided Verification, pages 183–190. Springer.
Kahsai, T., Rümmer, P., and Schäf, M. (2019). Jayhorn: A java model checker: (competition contribution). In Tools and Algorithms for the Construction and Analysis of Systems: 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April 6–11, 2019, Proceedings, Part III 25, pages 214–218. Springer.
Menezes, R., Moura, D., Cavalcante, H., de Freitas, R., and Cordeiro, L. C. (2022). Esbmc-jimple: verifying kotlin programs via jimple intermediate representation. In Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis, pages 777–780.
Monteiro, F. R., Gadelha, M. R., and Cordeiro, L. C. (2022). Model checking c++ programs. Software Testing, Verification and Reliability, 32(1):e1793.
Moraes, A. d. and Hayashi, V. (2021). Segurança em IoT: Entendendo os Riscos e Ameaças em IoT. Alta Books. Editora Alta Books.
Petersen, K., Feldt, R., Mujtaba, S., and Mattsson, M. (2008). Systematic mapping studies in software engineering. In 12th International Conference on Evaluation and Assessment in Software Engineering (EASE) 12, pages 1–10.
Rowland, C., Goodman, E., Charlier, M., Light, A., and Lui, A. (2015). Designing connected products: UX for the consumer Internet of Things. ”O’Reilly Media, Inc.”.
SILVA, V. J., CORDEIRO, L. C., and JÚNIOR, V. F. D. L. (2013). Verificação de aplicações ami usando java pathfinder.
Cordeiro, L., Kesseli, P., Kroening, D., Schrammel, P., and Trtik, M. (2018). Jbmc: A bounded model checking tool for verifying java bytecode. In International Conference on Computer Aided Verification, pages 183–190. Springer.
Kahsai, T., Rümmer, P., and Schäf, M. (2019). Jayhorn: A java model checker: (competition contribution). In Tools and Algorithms for the Construction and Analysis of Systems: 25 Years of TACAS: TOOLympics, Held as Part of ETAPS 2019, Prague, Czech Republic, April 6–11, 2019, Proceedings, Part III 25, pages 214–218. Springer.
Menezes, R., Moura, D., Cavalcante, H., de Freitas, R., and Cordeiro, L. C. (2022). Esbmc-jimple: verifying kotlin programs via jimple intermediate representation. In Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis, pages 777–780.
Monteiro, F. R., Gadelha, M. R., and Cordeiro, L. C. (2022). Model checking c++ programs. Software Testing, Verification and Reliability, 32(1):e1793.
Moraes, A. d. and Hayashi, V. (2021). Segurança em IoT: Entendendo os Riscos e Ameaças em IoT. Alta Books. Editora Alta Books.
Petersen, K., Feldt, R., Mujtaba, S., and Mattsson, M. (2008). Systematic mapping studies in software engineering. In 12th International Conference on Evaluation and Assessment in Software Engineering (EASE) 12, pages 1–10.
Rowland, C., Goodman, E., Charlier, M., Light, A., and Lui, A. (2015). Designing connected products: UX for the consumer Internet of Things. ”O’Reilly Media, Inc.”.
SILVA, V. J., CORDEIRO, L. C., and JÚNIOR, V. F. D. L. (2013). Verificação de aplicações ami usando java pathfinder.
Publicado
20/02/2024
Como Citar
ROCHA, Evelim B.; SILVA, Vandermi J. da; RODRIGUES, Andrey.
Verificação Formal de Software para Internet das Coisas com Validação de Aplicações em Kotlin/Java: Mapeamento Sistemático Preliminar. In: CONFERÊNCIA CONNECT TECH, 1. , 2024, Itacoatiara/AM.
Anais [...].
Porto Alegre: Sociedade Brasileira de Computação,
2024
.
p. 62-66.
DOI: https://doi.org/10.5753/connect.2024.238553.
