Introducción a la seguridad de Lisex 0.0 versión PostScript.

Este artículo está destinado a aquellos que no tienen mayores conocimientos sobre modelos MLS y temas relacionados. Los lectores con más experiencia en este campo pueden leer la tesis [Cristiá] o las secciones Especificación y Verificación formal para una descripción detallada del modelo de seguridad implementado en Lisex 0.0. Aquellos para los cuales esta introducción resulte insuficiente pueden consultar [AJP95,Gas88].

Lisex es un sistema operativo pensado para resistir ataques a la confidencialidad efectuados por medio de caballos de Troya en ambientes donde la seguridad es crítica o al menos muy importante. Según las investigaciones desarrolladas principalmente en Estados Unidos de Norteamérica durante los '70 y '80, tales amenazas se combaten utilizando dos herramientas:

	un modelo de seguridad multinivel (MLS) en el núcleo del sistema, y
	un desarrollo del sistema que utilice métodos formales.

El modelo MLS que incorpora Lisex 0.0 [Cristiá], llamado Lisex Security Model 0.0 (LSM0.0), es una adaptación del modelo introducido por Bell y La Padula [BL73a,BL73b] en 1973. LSM0.0 ha sido incorporado únicamente al sistema de archivos del núcleo 2.4.14 de Linux y desarrollado utilizando el entorno de pruebas Coq. El desarrollo de LSM0.0 incluye especificación y verificación formal. Futuras versiones de Lisex implementarán otros modelos equivalentes en otras porciones del núcleo.

Además, Lisex 0.0 implementa listas de control de acceso (ACL) para mejorar el mecanismo DAC tradicional de Linux y otras características de seguridad menores.

Por el momento, no está planeado generar versiones POSIX de Lisex aunque algunas de las extensiones de seguridad han sido consideradas.