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
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
|
|
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)
|
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. |
|
|