Proyectos
 

Nuestros proyectos carecen de financiamiento y se desarrollan gracias a la colaboración de estudiantes y graduados. Estamos convencidos que muchos de los proyectos tendrían viabilidad comercial si pudieran ser desarrollados con más recursos.

Empresas, universidades u organizaciones que deseen colaborar financiera o académicamente son bienvenidas.
¡¡Por favor, contáctenos!!
gidis-info@fceia.unr.edu.ar

Proyectos Propios

 
Proyecto Estado Descripción
GIDIS Trusted Linux Buscando financiamiento Es el sucesor de Lisex. Incorpora un modelo MLS claramente diferente y superior al de Lisex. Se desarrollará sobre Linux y utilizando Coq.

Palabras clave: MLS, seguridad multi-nivel, Linux, Coq, métodos formales

Lisex Terminado Sistema operativo MLS desarrollado sobre Linux. Se utilizó Coq, la especificación fue verificada formalmente y testing funcional basado en especificaciones formales. Contamos con un prototipo bajo licencia GPL. Fue parcialmente financiado por Lifia.

Palabras clave: MLS, seguridad multi-nivel, Linux, Coq, métodos formales

ModelTest En desarrollo Herramienta semi-automática para efectuar testing basado en especificaciones formales. La especificación del sistema se escribe en un lenguaje formal semejante a Z, luego es traducida a Coq y finalmente se aplican una serie de algoritmos que analizan el texto Coq extrayendo gran cantidad de casos de prueba a nivel de la especificación. Otro módulo de la herramienta proyecta los casos a nivel del programa y un test dirver ejecuta el programa y obtiene la salida. Finalmente, entradas y salidas son comparadas utilizando la especificación como oráculo.

Palabras clave: testing, testing funcional, especificaciones formales, Z, Coq

White-Box Test Assistant En desarrollo Herramienta para asistir la tarea de testing. Implementa criterios de testing estructural basados en el flujo de datos. Los programas a testear pueden incluir arreglos. Está diseñada para soportar cualquier lenguaje imperativo aunque por el momento sólo acepta programas COBOL. Incluye una interfaz que permite al operador seleccionar casos de prueba con el objetivo de cumplir criterios estándar.

Palabras clave: testing, testing estructural, flujo de datos, COBOL

 
Participación de miembros de GIDIS en proyectos de otras instituciones
 
Algunos de nuestros miembros participan o han participado en proyectos de I+D o actividades de consultoría en las instituciones listadas a continuación. En todos los casos las actividades realizadas involucran Métodos Formales y/o Seguridad Informática.
  • Stevens Institute of Technology (USA)
  • Universidade Nova de Lisboa (Portugal)
  • ATX Software (Portugal)
  • Oblog (Portugal)
  • Presidencia de la República Oriental del Uruguay
  • IPcom (Uruguay)
  • Pragma Consultores (Argentina)
  • Neoris Argentina (ex Amtec)
 
Proyectos en Estudio
 
Proyecto Descripción
ABPL Architecture-Based Programming Languages. Estudiar y desarrollar lenguajes de programación que reduzcan la brecha existente entre ciertos estilos arquitectónicos y los lenguajes de programación más utilizados. Por ejemplo, si la arquitectura de cierto sistema corresponde al estilo de Invocación Implícita, para implementarla convendría utilizar un lenguaje de programación que incluyera primitivas cercanas a las abstracciones del estilo. Lo mismo puede hacerse para otros estilos arquitectónicos como Balckboard Systems, Tubos y Filtro, etc.
Trusted MySQL Implementar controles de seguridad multi-nivel (MLS) en un gestor de bases de datos relacional de dominio público. No necesariamente tiene que ser MySQL pero es un buen candidato dado que es uno de los más utilizados. Este proyecto es semejante a Lisex o GIDIS Trusted Linux. En una primera fase se utilizaría el modelo de seguridad de Lisex y se lo implmentaría sobre MySQL para obtener un prototipo.
Formal Reuse El primer paso es generar una biblioteca de funciones (pertenecientes a un dominio acotado, por ejemplo listas) cada una de las cuales está especificada formalmente. Luego, se desarrolla un programa que toma la especificación de una función (del mismo dominio), llamada función objetivo, y busca en la biblioteca aquellas funciones cuya especificación "implementa" la de la funcón objetivo. En caso necesario, el programa formulará las obligaciones de prueba necesarias. Finalmente, la función objetivo es añadida a la biblioteca. De esta forma, se podrían reutilizar las funciones de la biblioteca de forma precisa. (entradas, salidas, GDES, búsqueda por GDES, varias funciones de la biblioteca implementan la función objetivo).
The Documentary Hypothesis En grandes proyectos de software la generación y el mantenimiento de la documentación es una tarea compleja, propensa a errores y costosa. El proyecto trata de implementar un prototipo de una herramienta que permita gestionar toda la documentación de un proyecto (especificación, requerimientos, diseño, testing, etc.) y no sólo los comentarios a nivel de código (como Doxygen o herramientas semejanes).
Z/Coq Implementar la semántica del lenguaje de especificación Z sobre Coq. La implementación debería preservar la estructura de la especificación Z. De esta forma, Coq podría utilizarse como verificador de tipos (type checker) y asistente de pruebas para especificaciones Z. Concretamente, se trata de desarrollar un compilador que tome código fuente Z y genere código objeto Coq, preservando la estructura de la especificación de entrada.
WRSPM Support Tool El método de Jackson-Zave para requerimientos y especificaciones consta de varios pasos. Cada paso se relaciona con los demás según formas más o menos precisas. Por jemplo, en el paso de requerimientos a especificación, deben "abandonarse" todos los fenómenos no compartidos. Desarrollar una herramienta que asista al ingeniero que utiliza esta metodología sería una contribución interesante.
Apache MLS Este proyecto es semejante a GIDIS Trusted Linux, Trusted MySQL y Lisex. En este caso se trata de incluir controles MLS en el servidor Web Apache, posiblemente como un módulo externo. Como en los otros casos el desarrollo se basa en un modelo formal de seguridad.
MLS Firewall Nuevamente este es un proyecto afin con los otros del área de seguridad. En este caso, se considerarían las redes interconectadas a través de un firewall como los sujetos. Estos sólo podrían comunicarse entre sí si se verifican las propiedades de los modelos MLS.
RCI Support Tool RCI es un modelo para medir la cohesión de módulos dentro del estilo de Orientación a Objetos. El proyecto se trata de programar una herramienta que calcule la medida.
The Security Investment Hypothesis Varios autores han propuesto metodologías que permiten guiar y priorizar la inversión en seguridad informática. Es decir, permiten responder preguntas del estilo, ¿debo comprar un firewall? ¿O endurecer los sistemas operativos? ¿Debo cambiar el sistema operativo? ¿O instlar un IDS? Existe la posibiliad de reunir estas metodologías en un método disciplinado y riguroso. Por otro lado, para llevar adelante un estudio de estas características se requieren grandes cantidades de datos, que además deben ser mantenidos en el tiempo. Programar una herramienta que asista al ingeniero en esta tarea podría tener un buen interés en la industria.

© 2003 por Grupo Gidis. Todos los derechos reservados.
Sitio diseñado por Lorena Cantarini [mailto]