Como
se mencionó en la Introducción, el GIDIS no es nuevo en el desarrollo
de sistemas operativos MLS. Personal del GIDIS desarrolló un prototipo
de MLS sobre Linux, denominado Lisex 0.0. En efecto, Lisex 0.0
es un prototipo rudimentario e incompleto pero que podría ser
el punto de partida de un sistema capaz de ranquear en la clase
B1 del TCSEC, lo cual constituye sin dudas un avance importante
frente a el Linux estándar.
Las
características de seguridad de Lisex 0.0 y del proceso de desarrollo
seguido para finalizarlo son las siguientes:
ACLs
de longitud fija, configurable en tiempo de compilación del núcleo.
Las ACLs pueden incluir usuarios y grupos.
Lista
de propietarios para cada archivo y directorio (esta información
está incluida en cada ACL respectiva).
Grupo
de usuarios root equivalente al usuario root (en lo que a administración
del sistema de archivos se refiere).
Cuenta
y grupo de usuarios secadm a cargo de la administración de los atributos
MAC de objetos y sujetos.
Implementación
de un modelo formal de seguridad MLS para el sistema de archivos
ext2 (que es donde se almacenan los datos del usuario).
Formalización
y verificación formal del modelo de seguridad efectuado en Coq.
Documentación
(presentada en castellano y en formato PDF y HTML):
Modelo
formal de seguridad
Interpretación
del modelo formal de seguridad en términos de la implementación
y del vocabulario propio del sistema de archivos ext2.
Scripts
de todas las pruebas formales efectuadas sobre el modelo formal.
Casos
de prueba seleccionados a nivel de la especificación
