Carlos Luna

I am a lecturer at Computing Science Department (InCo) at the Engineering School of the Universidad de la República, Montevideo, Uruguay CVUy Carlos Luna (Agencia Nacional de Investigación e Innovación) -- short CV  DBLP: Carlos Luna Google Académico: Citations. Photo (2018) -- photo: InCo 2008 -- photo: InCo 2017 [1][2]

How to reach me

• Email: cluna@fing.edu.uy
• Phone: work +598 (2) 7114244-47/ Int. 12121
• Fax: work +598 27110469
• Room: 121

Teaching 

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 Teoria de Tipos (curso de posgrado - graduate course)
• Iniciación a la Producción Audiovisual y Mutimedia (curso de grado - undergraduate course)

Research interests 

I am a member of the Laboratory of Computing Science - Information Security Group
My areas of interest are: reactive and real time systems, verification tools, constructive type theory, computer security, education

Current work

• Security: Formal analysis of security models for mobile devices, virtualization platforms, and domain name systems
• Formal specification and verification of critical systems
• Model-driven depelopment and formal methods
• Computer science education
  

Projects in progress

• 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-2020)

More recent projects

• "Mecanismos autónomos de seguridad certificados para sistemas computacionales móviles". Proyecto ANII-FCE, Uruguay (2015-2018)

• "VirtualCert: Hacia una Plataforma Certificada de Virtualización - Fase II". Proyecto CSIC, Uruguay (2013-2015)

• "VirtualCert: Hacia una plataforma de virtualización certificada". Proyecto FCE, ANII, Uruguay (2011-2012)

• "LOW COST COMPUTER BASED SYSTEM FOR QUALITY EVALUATION AND PRESERVATION OF GRAINS STORED IN POLYMER BAGS" (investigador). Proyecto Microsoft LACCIR (2009-2010).
• "FMCrypto: Formal Methods for Cryptographically Secure Distributed Computations" (investigador). Proyecto STIC-AMSUD, (2009-2010).
• "Types for Robust Program Development." (participante). Proyecto STIC-AMSUD, (2009-2010).
• "Especificación Formal y Verificación de Sistemas Críticos" (responsable). Proyecto SeCyT-FCEIA, UNR, Argentina1 (2009-2010).
• "Verificación de Transformaciones de Modelos de Comportamiento basados en UML". Proyecto FCE, DINACYT, Uruguay (2009-2010)
• "REVVIS: REUNIÃO DE ESPECIALISTAS EM VERIFICAÇÃO E VALIDAÇÃO DE SOFTWARE" (participante). Proyecto CYTED (2007-2010).
• "Verificación de Sistemas Críticos: de la Especificación al Código" (responsable). Proyecto PDT, DINACYT, Uruguay (2006-2008).
• "STEVE: Seguridad a Través de Evidencia VErificable" (investigador). Proyecto PDT, DINACYT, Uruguay (2007-2008).

Some papers - Publications

• 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. 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, "Towards a formally verified implementation of the MimbleWimble cryptocurrency protocol". CoRR abs/1907.01688, 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)
• G. Gonzalez, F. Zorzan, C. Luna, N. Szasz, "Automatization of the Instantiation Process for the Behavior of Software Product Lines". Proceedings of CIBSE 2013, Uruguay, 2013.
• G. Barthe, G. Betarte, J. D. Campo, C. Luna, "Cache-leakage resilient OS isolation in an idealized model of virtualization". Proceedings of CSF2012: the 25th IEEE Computer Security Foundations Symposium, IEEE Computer Society Press, pp. 186-197, 2012.
• E. Bazán, G. Betarte, C. Luna, "A Formal Specification of the DNSSEC Model". Proceedings of OpenCert 2011: the 5th International Workshop on Foundations and Techniques for Open source Software Certification, Electronic Communications of the EASST, vol. 48, 2012.
• D. Zanarini, C. Luna, L. Sierra, "Alternating-time Temporal Logic in the Calculus of (Co)Inductive Constructions". R. Gheyi and D. Naumann (Eds.): SBMF 2012, LNCS 7498, pp. 210--225. Springer, Heidelberg (2012).
• C. Luna et. al. "Delayed completion of Final Project of the career Computer Analyst: Seeking its causes". Proceedings of CIESC 2012, Colombia, 2012.
• G. Barthe, G. Betarte, J. D. Campo, C. Luna. "Formally verifying isolation and availability in an idealized model of virtualization". FM 2011: 17th International Symposium on Formal Methods, Ireland. LNCS 6664, pp. 231-245, 2011.
• C. Pons, D. Calegari, C. Luna, N. Szasz. "Un Lenguaje Específico de Dominio para la Generación Automática de Código en Sistemas de Monitoreo Inalámbrico de Silos Bolsa". Proc. of LACCEI 2011, Colombia, 2011.
• C. Luna, G. Betarte. "Especificación y Verificación Formal de Sistemas Críticos. Análisis de Modelos de Seguridad para Dispositivos Móviles". WICC, Argentina, 2011.
• A. Gonzalez, C. Luna, F. Zorzán. "Transformación de Máquinas de Estados con Variabilidad usando el lenguaje QVT", Proc. of CLEI, Ecuador, 2011.
• C. Luna, L. Etcheverry. "Experiencias en la Enseñanza de Programación de Sistemas de Porte Mediano en un Contexto de Masividad". CIESC, Ecuador, 2011.
• D. Calegari, C. Luna, N. Szasz, A. Tasistro. "A Type-Theoretic Framework for Certified Model Transformations". SBMF'2010, Brasil. LNCS 6527/2011, pp. 112-127.
• Ramin Roushani Oskui, Gustavo Betarte, and Carlos Luna. "A Certified Access Controller for JME-MIDP 2.0 enabled Mobile Devices", XXVIII International Conference of the Chilean Computer Science Society, to be published by IEEE CS Press in 2010.
• Gustavo Mazeikis, Carlos Luna, and Gustavo Betarte. "Formal Specification and Analysis of the MIDP 3.0 Security Model", XXVIII International Conference of the Chilean Computer Science Society, to be published by IEEE CS Press in 2010.
• C. Luna, and A. Gonzalez. "Specification of Products and Product Lines" (extended version), Electronic Proceedings in Theoretical Computer Science, Volume 15, pp. 44-55. DOI: 10.4204/EPTCS.15, ISSN: 2075-2180, January 2010.
• D. Calegari, C. Luna, N. Szasz, C. Pons, M. Canabé, F. Sierra . "Ingeniería Dirigida por Modelos Aplicada al Control Automático del Almacenamiento en Silos bolsa". Proc. of II Congreso de AgroInformática (CAI 2010), 39 JAIIO, Argentina, 2010.
• D. Calegari, C. Luna, N. Szasz, A. Tasistro. "Experiment with a Type-Theoretic Approach to the Verification of Model Transformations". II Chilean Workshop on Formal Methods (ChWFM), Chile, November 2009.
• Gustavo Mazeikis y Carlos Luna. "Autorización de Acceso en MIDP 3.0", Congreso Iberoamericano de Seguridad Informática, CIBSI’09, Uruguay, Noviembre de 2009.
• Carlos Luna y Cristian Rosa. "Análisis Formal del Estándar NIST para modelos RBAC", Congreso Iberoamericano de Seguridad Informática, CIBSI’09, Uruguay, Noviembre de 2009.
• Carlos Luna y Ariel Gonzalez. "Specification of Products and Product Lines", 9th International Workshop on Reduction Strategies in Rewriting and Programming (an RDP workshop 2009, Federated Conference on Rewriting, Deduction, and Programming), Brasil, June 2009.
• J. M. Crespo, G. Betarte, and C. Luna. "A Framework for the Analysis of Access Control Models for Interactive Mobile Devices". S. Berardi, F. Damiani, and U. de’Liguoro (Eds.): Types for Proofs and Programs (TYPES) 2008, LNCS 5497, pp. 49–63, 2009. Springer-Verlag Berlin Heidelberg 2009.
• Carlos Luna, Gustavo Betarte. "Taller de Producción de Producción de Programas sin Fallas", International Conference on Engineering and Computer Education, ICECE’09, Buenos Aires, Argentina, March 2009. Organization: COPEC (Council of Researches in Education and Sciences, Brasil) and IEEE-Ed.Soc. (Education Society of the Institute of Electrical and Electronics Engineers, Argentina).
• C. Luna, A. Gonzalez. “Behavior Specification of Product Lines via Feature Models and UML Statecharts with Variabilities”, XXVII International Conference of the Chilean Computer Science Society, Published by IEEE CS Press, pp. 32-41, ISBN 978-0-7695-3403-9, November 10-14 de 2008, Punta Arenas, Chile.
• Gustavo Mazeikis, Carlos Luna, y Gustavo Betarte. “Formalización y Análisis del Modelo de Seguridad de MIDP 3.0. Seguridad a Nivel de Aplicación”, First Chilean Workshop on Formal Methods, ChWFM 2008, 10 págs, ISBN 978-956-319-507-1, Punta Arenas, Chile, 10-15 November 2008.
• C. Luna, Luis Sierra, Paula Echenique. “Hacia una Especificación Formal de un Microcontrolador usado en Marcapasos”, XXXIV Conferencia Latinoamericana de Informática (CLEI 2008), 10 páginas, ISBN 978-950-9770-02-7, Setiembre de 2008, Argentina. Reporte Técnico 08-09 del PEDECIBA Informática, InCo, Montevideo, Uruguay. Agosto de 2008.
• S. Zanella Béguelin, G. Betarte, and C. Luna. “A formal specification of the MIDP 2.0 security model”. T. Dimitrakos et al. (Eds.): FAST 2006, LNCS 4691, pp. 220–234, 2007. Springer-Verlag Berlin Heidelberg 2007.
• G. Betarte, C. Luna y L. Sierra. "Especificación y Verificación Formal de Sistemas Críticos en el Instituto de Computación de la Universidad de la República (Uruguay)". REUNIÃO DE ESPECIALISTAS EM VERIFICAÇÃO E VALIDAÇÃO DE SOFTWARE - REVVIS, Octubre de 2007, Brasil.
• N. Szasz, C. Luna y Ariel Gonzalez. “Hacia una Formalización de Líneas de Productos mediante Máquinas de Estados con Variabilidades”, CLEI´07, Costa Rica, Octubre de 2007 (trabajo realizado en el marco de la Universidad ORT Uruguay).
• C. Luna, M. Pedemonte, M. Viera, E. Fraschini. "Organización para un Curso de Programación en un Contexto de Pasividad. Resultados tras Experiencia de 4 Años", publicado en la Revista Iberoamericana de Tecnología en Educación y Educación en Tecnología: TE&ET, vol.2, páginas 83-91, Julio de 2007. Versión online disponible en http://teyet-revista.info.unlp.edu.ar.
• C. Luna. "Enseñando Métodos Formales con COQ", publicado en la Revista Iberoamericana de Tecnología en Educación y Educación en Tecnología: TE&ET, Vol 1, páginas 55-64, Dic. 2006.
• C. Luna, E. Fraschini, M. Pedemonte, M. Viera. "Organización para un Curso de Programación en un Contexto de Masividad. Una Experiencia". XIV Congreso Iberoamericano de Educación Superior en Computación (CIESC-2006), Santiago, Chile, Agosto de 2006.
• C. Luna. "Enseñando Métodos Formales con COQ". I Congreso de Tecnología en Educación y Educación en Tecnología (TE&ET’06), La Plata, Argentina, Agosto de 2006.
• M. Martinez, C. Luna (Univ. ORT), S. Blanco. "Schema-Matching with Neural Networks: A new approach using Representing Schemas". XXXII Conferencia Latinoamericana de Informática CLEI 2006, Santiago, Chile, Agosto de 2006.
• C. Luna. "Model Checkers" + "Proof Assistants" en la Verificación de Sistemas de Tiempo Real. SPL2006 - II Southern Conference on Programmable Logic, 2nd SURLabs - Regional Joint Latin-American Laboratories on FPGA Technology, March 8-10, 2006 - Mar del Plata, Argentina. E. Boemo, G. Sutter, E. Todorovich, S. Lopez-Buedo (Editors), "FPGA BASED SYSTEMS", ISBN 84-609-8998-4. Chapter 7: System Verification and EDA Tools, 347-354.

Books:

PhD thesis

• "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. 

Master thesis

• "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.

Links

• Ingeniería deMuestra
• CLEI
• RIO2014: 21 Escuela de Verano de Ciencias Informáticas. Curso: "Seguridad certificada de un modelo idealizado de hypervisor usando el asistente de pruebas Coq"
• CSIC UDELAR
• ANII - DINACYT
• Universidad Nacional de Rosario (Arg.)
• Universidad Nacional de Río Cuarto (Arg.)
• Universidad ORT Uruguay
• Coq Page