I am a lecturer at Computing Science Department (InCo) at the Engineering School of the Universidad de la República, Montevideo, Uruguay
DBLP: Carlos Luna – Google Scholar Citations
Photo (2018) – photo: InCo 2008 -- photo: InCo 2017 [1][2]
Email: cluna@fing.edu.uy
Phone: work +598 (2) 7114244-47/ Int. 12121
Fax: work +598 27110469
Room: 121
I'm working for the following courses of the program Computing Engineering
Programación 2 (curso de grado - undergraduate course)
Taller de Producción de Programas sin Fallas (curso de grado - undergraduate course)
Construcción Formal de Programas en Teoría de Tipos (curso de posgrado - graduate course)
Iniciación a la Producción Audiovisual y Mutimedia (curso de grado - undergraduate course)
I am
a member of the Laboratory of Computing Science - Information
Security Group
My
areas of interest are: formal methods, computer security,
verification tools, constructive type theory, critical systems, and
education
Security: Formal analysis of security models for mobile devices, virtualization platforms, blockchain, and cryptocurrencies
Formal specification and verification of critical systems
Model-driven depelopment and formal methods
Computer science education
Herramientas conceptuales y tecnológicas para ciberseguridad adaptativa y certificada. Proyecto CSIC-Udelar Grupos de Investigación, Uruguay (2023-2027).
La orientación y sus impactos en el desempeño de estudiantes de la Facultad de Ingeniería. Proyecto PMICEU CSE-CSIC-Udelar, Uruguay (2020-2023).
Automatización de derivación de conocimiento para el aseguramiento de sistemas informáticos. Proyecto ANII-FMV, Uruguay (2018-2021).
Fondo de Fomento de las Ingenierías. Proyecto ANII, Uruguay (2018-2021).
Mecanismos autónomos de seguridad certificados para sistemas computacionales móviles. Proyecto ANII-FCE, Uruguay (2015-2018)
All publications, including previous ones, are available at: CVUy
M. Cristiá, G. De Luca, C. Luna, C. “An Automatically Verified Prototype of the Android Permissions System”. Journal of Automated Reasoning 67, 17 (2023). https://doi.org/10.1007/s10817-023-09666-2
F. Molina. G. Betarte, C. Luna, A. Silveira, D. Zanarini, “A Blockchain based and GDPR-compliant design of a system for digital education certificates”, CLEI Electronic Journal, Volume 26, Number 1, Paper 3, May 2023. https://doi.org/10.19153/cleiej.26.1.3
A. Silveira, G. Betarte, M. Cristiá, y C. Luna. “Un Análisis Basado en Modelos de las Propiedades de Seguridad de Mimblewimble y las Implementaciones del Protocolo”, Memoria Investigaciones en Ingeniería, n.º 24, pp. 192-142, jun. 2023. https://doi.org/10.36561/ING.24.10
M. Cristiá, G. De Luca, C. Luna. “An Automatically Verified Prototype of the Android Permissions System”. CoRR abs/2209.10278 (2022)
C. Luna. “Introducción a la planificación estratégica al comienzo de una carrera”. LACLO 2022, Colombia, 2022
A. Silveira, G. Betarte, M. Cristiá, C. Luna. “A Formal Analysis of the Mimblewimble Cryptocurrency Protocol”. Sensors 2021, 21, 5951. https://doi.org/10.3390/s21175951
G. Betarte, M. Cristiá, C. Luna, A. Silveira, D. Zanarini, "Set-Based Models for Cryptocurrency Software". CLEI Electron. J. 24(3) (2021).
F. Molina, G. Betarte, C. Luna, "Design principles for constructing GDPR-compliant blockchain solutions". In 2021 IEEE/ACM 4th International Workshop on Emerging Trends in Software Engineering for Blockchain (WETSEB), 2021, pp. 1-8, doi: 10.1109/WETSEB52558.2021.00008.
G. De Luca, C. Luna, "Towards a certified reference monitor of the Android 10 permission system". In 26th International conference on types for proofs and programs, TYPES postproceedings (2021).
A. Gonzalez, M. Cristiá, C. Luna, "Error Finding in Real-Time Systems using Mutants of Temporal Properties". In 2021 40th International Conference of the Chilean Computer Science Society (SCCC), 2021, pp. 1-8, doi: 10.1109/SCCC54552.2021.9650361.
F. Molina, G. Betarte and C. Luna, "Privacy Aware Blockchain Solutions: Design and Threat Analysis", XXIV Iberoamerican Conference on Software Engineering (CIBSE), San José, Costa Rica, Curran Associates, 2021.
A. Silveira, G. Betarte, M. Cristiá, C. Luna, “A Range Proof Scheme Analysis for the Mimblewimble Cryptocurrency Protocol”, In 2021 IEEE URUCON, 2021, pp. 329-333, doi: 10.1109/URUCON53396.2021.9647414.
F. Molina, G. Betarte and C. Luna, "On the Compliance of Blockchain Technology With Data Protection Regulations”. In 2021 IEEE URUCON, 2021, pp. 556-560, doi: 10.1109/URUCON53396.2021.9647141.
A. Silveira, G. Betarte, M. Cristiá, C. Luna, "A Formal Analysis of the MimbleWimble Cryptocurrency Protocol". CoRR abs/2104.00822 (2021).
Clara Raimondi y Carlos Luna. “Innovaciones educativas sobre una biblioteca digital de cursos filmados de la Facultad de Ingeniería”. II Jornadas Regionales de Investigación en Educación Superior, Uruguay, 2021.
Carlos Luna, Ana Carlozzi, Victoria Garcia y Pablo Babino. “Orientación al ingreso en tiempos de pandemia: Un taller de planificación estratégica en ingeniería”. II Jornadas Regionales de Investigación en Educación Superior, Uruguay, 2021.
G. Barthe, G. Betarte, J. D. Campo, C. Luna, D. Pichardie. "System-Level Non-interference of Constant-Time Cryptography. Part II: Verified Static Analysis and Stealth Memory". Journal of Automated Reasoning (2020). https://doi.org/10.1007/s10817-020-09548-x
G. Betarte, M. Cristiá, C. Luna, A. Siveira, D. Zanarini, "Towards a formally verified implementation of the MimbleWimble cryptocurrency protocol". In Zhou J. et al. (eds) Applied Cryptography and Network Security Workshops. ACNS 2020. Lecture Notes in Computer Science, vol 12418. Springer, Cham. https://doi.org/10.1007/978-3-030-61638-0_1, 2020.
F. Molina, G. Betarte, C. Luna, "A Blockchain based and GDPR-compliant design of a system for digital education certificates". CoRR abs/2010.12980 (2020)
G. Barthe, G. Betarte, J. D. Campo, C. Luna, "System-level non-interference of constant-time cryptography. Part I: model". Journal of Automated Reasoning (2019) 63:1. https://doi.org/10.1007/s10817-017-9441-5
C. Luna, A. Carlozzi, V. Garcia, L. Chiavone, P. Babino, "A workshop on initiation to strategic planning for new students of engineering careers". In InterCambios Vol. 6:1, 54-69, 2019.
A. Gonzalez, M. Cristiá, and C. Luna, "Mutants for Metric Temporal Logic Formulas". In 22nd Iberoamerican Conference on Software Engineering (CIbSE 2019), Cuba, 2019.
G. Betarte, M. Cristiá, C. Luna, A. Silveira, D. Zanarini, "Set-Based Models for Cryptocurrency Software". CoRR abs/1908.00591, 2019.
A. Carlozzi, A. Fleitas, V. García, C. Luna, X. Otegui, "Experiencia de trabajo Espacio de Orientacińn y Consulta - Unidad de Enseñanza para la orientación y el seguimiento estudiantil en la Fing". En III Encuentro Latinoamericano de Prácticas de Asesorías Pedagógicas Universitarias, Setiembre de 2019, Uruguay.
D. Barreiro, L. Barzilai, L. Canuti, F. Carpani, L. Del Arco, C. Luna, and C. Raimondi, "OpenFING: A Project based on a Digital Library of Recorded Courses". Journal of Interactive Media in Education, 2018(1), p.17.
C. Luna, G. Betarte, J. Campo, C. Sanz, M. Cristiá, F. Gorostiaga., "A formal approach for the verification of the permission-based security model of Android". In CLEI electronic journal, Volume 21, Number 2, Paper 3, August 2018.
G. Betarte, I. Galuppo, C. Luna, "Security in iOS and Android: a comparative analysis". In SCCC 2018, Chile, Nov. 2018. To be published and indexed by the IEEE Xplore.
G. Bressan, A. Gonzalez, C. Luna, "Mutation Testing for Java based on Model-Driven Development". In SLISW - CLEI 2018, Brasil, Oct. 2018. Published and indexed by the IEEE Xplore.
G. Betarte, J. D. Campo, F. Gorostiaga, C. Luna, "A certified reference validation mechanism for the permission model of Android". In Logic-Based Program Synthesis and Transformation; 27th International Symposium, LOPSTR 2017, Namur, Belgium, October 10-12, 2017, Revised Selected Papers; F. Fioravanti and J.P. Gallagher (Eds.): LOPSTR 2017, LNCS 10855, 2018.
G. Betarte, J. D. Campo, F. Gorostiaga, C. Luna, "A certified reference validation mechanism for the permission model of Android". In the 27th International Symposim on Logic-Based Program Synthesis and Trasformation (LOPSTR), Namur, Belgium, 2017.
G. Betarte, J. Campo, M. Cristiá, F. Gorostiaga, C. Luna, C. Sanz, "Towards formal model-based analysis and testing of Android's security mechanisms". In SLISW-CLEI 2017, Argentina, 2017.
C. Luna, P. Babino, D. Alessandrini, X.Otegui, L. Chiavone, A. Viscarret, "Student orientation and academic performance in engineering". In InterCambios, Vol. 4, nro.1, 2017.
L. Canuti, F. Carpani, L. Del Arco, F. Falco, C. Luna, C. Raimondi, "An educational project based on a digital library of filmed courses". WREA-LACLO, Argentina, 2017.
G. Betarte, J. D. Campo, C. Luna, A. Romano, "Formal Analysis of Android's Permission-Based Security Model". In Scientific Annals of Computer Science, Vol. 26; 27-68, 2016.
G. Gonzalez, C. Luna, et al. "UML State Machine as Modeling Language for DEVS Formalism". CLEI 2016, Chile.
G. Betarte, J. D. Campo, C. Luna, A. Romano, "Verifying Android's Permission Model". In Theoretical Aspects of Computing-ICTAC 2015 (pp. 485-504). Springer International Publishing (2015).
G. Betarte, C. Luna, "Formal Analysis of Security Models for Mobile Devices, Virtualization Platforms, and Domain Name Systems". CLEI Electronic Journal, Vol. 18, Number 3, Paper 3, December 2015.
G. Gonzalez, C. Luna, M. Daniele, "Towards an automatic model transformation mechanism from UML state machines to DEVS models". CLEI Electronic Journal, Vol. 18, Number 2, Paper 3, August 2015.
G. Barthe, G. Betarte, J. D. Campo, C. Luna, D. Pichardie: "System-level non-interference for constant-time cryptography". Proceedings of the 21st ACM Conference on Computer and Communications Security, Arizona, USA (2014)
G. Barthe, G. Betarte, J. D. Campo, J. M. Chimento, C. Luna, "Formally verified implementation of an idealized model of virtualization". Proceedings of 19th International Conference on Types for Proofs and Programs (TYPES, 2013), Dagstuhl LIPIcs post-proceedings, Vol.26; 45-63, 2014.
A. Gonzalez, C. Luna, et al. "Automatization of the Instantiation Process for the Behavior of Software Product Lines". IEEE Latin America Transactions, Volume 12, Issue 6, September 2014.
A. Gonzalez, C. Luna, et al. "Metamodel-based transformation from UML state machines to DEVS models". CLEI 2014, Uruguay.
A. Gonzalez, C. Luna, N. Szasz, F. Zorzán, "Automatic Derivation of Behavior of Products in a Software Product Line". IEEE Latin America Transactions, Vol.12; Sept. 2014.
L. Etcheverry, C. Luna, L. Tansini. "Pedagogical Experiences in a Highly Populated Undergraduate Programming Course Teaching How to Develop Medium Size Information Systems". CLEI Electronic Journal, Vol. 17, Number 3, Paper 7. December 2014.
G. Barthe, G. Betarte, J. D. Campo, C. Luna, D. Pichardie: "System-level non-interference for constant-time cryptography". IACR Cryptology ePrint Archive 2014: 422 (2014)
Books:
C. Luna, C. Raimondi and F. Carpani (January 11th 2021). An Educational Project Based on a Digital Library of Filmed Courses [Online First], IntechOpen, DOI: 10.5772/intechopen.95549.
R. Kantor, J. Hurtado, C. Luna, L. Sierra, D. Zanarini, "Temas de Teoría de la Computación". Este libro forma parte de la Iniciativa Latinoamericana de Libros de Texto abiertos (LATIn), proyecto financiado por la Unión Europea en el marco de su Programa ALFA III EuropeAid. March, 2014.
C. Luna, "Matemática discreta y lógica". Capítulo de libro (páginas 13-50). Proyecto UTU-ANII-UDELAR. Tecnólogo Informático de Paysandú. Experiencia de capacitación docente en modalidad e-learning.
C. Luna, "Programación inicial". Capítulo de libro (páginas 51-100). Proyecto UTU-ANII-UDELAR. Tecnólogo Informático de Paysandú. Experiencia de capacitación docente en modalidad e-learning.
"Formal analysis of security models for mobile devices, virtualization platforms, and domain name systems". August 2014, PEDECIBA Informática, Uruguay. Primer premio en el concurso de tesis de la Academia Nacional de Ingeniería de Uruguay, Uruguay, 2015.
"Especificación y Análisis de Sistemas de Tiempo Real en Teoría de Tipos" (Specification and Analysis of Real Time Systems in Type Theory). Primer premio en el concurso de tesis de maestría CLEI'2000, México. Reporte Técnico - Thesis.
