Novedades

Estimadas y estimados estudiantes,

Respecto a temas de investigación y para posibles proyectos de grado o tesinas, van algunas líneas para que consideren. Si tienen interés pueden escribirme directamente (cluna@fing.edu.uy):

• Protocolos de criptomonedas. Adrián Silveira terminó su tesis de maestría en este tema y está comenzando el doctorado. No usó Coq hasta ahora ni herramientas de verificación formal. Pueden surgir varias (sub)líneas de este tema. MimbleWimble, que es el protocolo sobre el cual hemos venido trabajando, ha crecido en popularidad y uso (implementaciones/monedas: Grin, Beam, Litecoin)
  
• Formalización y validación de consentimiento para el control de acceso a datos sensibles. Hay un trabajo de grado previo que plantea la idea de un modelo (una extensión de RBAC con conceptos de privacidad) que no se formalizó. Especificar formalmente este modelo y demostrar algunas propiedades claves tiene interés.
• Con Guido de Luca y Maximiliano Cristiá estuvimos viendo conexiones entre Coq y Setlog. De hecho, publicamos en JAR. Acá hay trabajo para hacer, posiblemente en cooperación con Maxi.
  • avanzar con el caso de estudio del paper en JAR: seguridad en Android
    
  • intentar implementar un traductor de setlog a Coq
• La línea de formalizaciones en torno a temas de seguridad de dispositivos móviles sigue vigente, ya que los desarrollos y versiones siguen cambiando. Guido de Luca hizo su tesina sobre Android 10. Formalizar extensiones nuevas del modelo de seguridad de Android y hacer un reconto de la evolución y las formalizaciones realizadas del sistema de seguridad de Android son temas de interés.
  
• Ver como usar Coq para el análisis de (algunos) contratos inteligentes. Tema abierto y de interés!