-
Listas
de control de acceso (ACL), disponibles para todos los objetos
del sistema de archivos. 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.
-
Cuenta
y grupo de usuarios secadm a cargo de la administración de los
atributos MAC de objetos y sujetos.
-
Implementación
del modelo GIDIS Trusted Linux Security Model (LMLS,
ver sección "GIDIS Trusted Linux Security Model") que se aplica
a todo el sistema, es decir:
-
Sistema
de archivos (ext2, dev, proc, kmem)
-
Comunicación
de procesos (memoria compartida, pipes, sockets,
semáforos, señales, colas de mensajes)
-
Mecanismos
de red (sockets, datagrams)
-
Administración
de memoria
-
Proceso
seguro de inicialización del sistema, es decir este proceso
deja al sistema en un estado inicial seguro respecto de LMLS.
-
Implementación
de criptografía de clave pública (semejante a IPSec) de formal
tal que todos los procesos que envíen datos hacia el exterior
del equipo lo hagan a través de un túnel criptográfico que garantice
la confidencialidad de los datos transmitidos.
-
En
esta versión no se incluye una verificación formal de los algoritmos.
-
Se
utilizará una implementación de dominio público.
-
No
se efectuará testing de estos algoritmos.
-
Incorporación
de mecanismos de camino confiable (trusted path).
-
Formalización
y verificación formal del LMLS efectuado en Coq.
-
Testing
funcional basado en especificaciones formales de todo el código
modificado o añadido como parte de la implementación del LMLS
(exceptuando los algoritmos criptográficos).
-
Documentación
(presentada en formato PDF y HTML):
-
Modelo
formal de LMLS e interpretación, esta última incluye:
-
Designaciones
de todos los términos formales primitivos
-
Argumentación
que indica los motivos por los cuales ciertos aspectos presentes
a nivel de la implementación no están presentes en el modelo
formal
-
Descripción
informal del modelo formal (pre-condiciones y post-condiciones
de cada operación del modelo)
-
Scripts
de todas las pruebas formales efectuadas sobre el modelo formal.
-
Descripción
informal de la arquitectura utilizada para implementar LMLS.
-
Páginas
de manual de las nuevas llamadas al sistema y modificación de
las páginas de manual de aquellas llamadas existentes que fueron
alteradas de manera tal de documentar los cambios.
-
Testing:
-
Casos
de prueba seleccionados a nivel de la especificación
-
Casos
de prueba a nivel de la implementación
-
Reporte
de errores detectados y corregidos
