- ¿Qué
es Lisex?
- ¿Qué es GIDIS Trusted Linux?
- ¿Cuándo comenzó el proyecto y cuál es su estado actual?
- ¿Dónde se desarrolla el proyecto?
- ¿Existe actualmente algún prototipo?
- ¿Qué diferencias tiene Lisex 0.0 con Linux?
- ¿Por qué Lisex incluye seguridad multi-nivel?
- ¿Qué es seguridad multi-nivel?
- ¿Por qué se usan métodos formales para desarrollar Lisex?
- ¿Qué son métodos formales?
- ¿Qué métodos formales se usan en Lisex?
- ¿Se planean otras versiones de Lisex?
- ¿En qué etapas del desarrollo de Lisex se usaron métodos
formales?
- ¿Qué es un caballo de Troya?
- ¿Por qué Lisex intenta resolver el problema de
la confidencialidad y no el de la integridad o la disponibilidad?
- ¿Dónde se puede encontrar más información sobre los
temas vinculados a Lisex?
- ¿Qué es confidencialidad?
- ¿Qué es un modelo de seguridad multi-nivel?
- ¿Qué es el modelo Bell-LaPadula?
|
| ¿Qué
es Lisex? |
Lisex
es un proyecto cuyo objetivo es aumentar la resistencia de los
sistemas operativos tipo UNIX a ataques contra la confidencialidad llevados a cabo por medio de caballos de Troya.
Según las investigaciones desarrolladas en los Estados Unidos
de América desde comienzos de la década del '70, la resistencia
a este tipo de ataques se logra implementado un modelo de seguridad multi-nivel dentro del núcleo del
sistema operativo y utilizando métodos formales durante este desarrollo. |
| ¿Qué
es GIDIS Trusted Linux? |
|
El financiamiento para Lisex proveniente de
nuestro patrocinador anterior terminó. Entonces, en GIDIS
iniciamos un nuevo proyecto, llamado GIDIS Trusted Linux, para desarrollar
el sucesor de Lisex. GIDIS Trusted Linux necesita socios o
patrocinadores, usted puede ser uno de ellos.
|
| ¿Cuándo
comenzó el proyecto y cuál es su estado actual? |
Formalmente,
el proyecto comenzó el 1º de octubre de 2001 aunque desde un
par de años antes Maximiliano Cristiá ya estaba escribiendo
la tesis
que daría lugar al modelo formal que se utilizó para implementar
Lisex 0.0.
Como proyecto con financiamiento, Lisex finalizó con la implementación
de Lisex 0.0. De todas maneras, en GIDIS
intentaremos conseguir financiamiento para su sucesor: GIDIS Trusted
Linux. |
| ¿Dónde
se desarrolla el proyecto? |
El
proyecto se desarrolla en la ciudad de Rosario, provincia de
Santa Fe, República Argentina. Debido a los escasos recursos
económicos, el equipo aun no cuenta con oficinas ni instalaciones
fijas. Sin mebargo, formalmente, el proyecto se lleva a cabo
en el Departamento de Computación de la Facultad de Ciencias Exactas, Ingeniería
y Agrimensura de la Universidad
Nacional de Rosario.
Si desea contactarse con nosotros envíe un e-mail a cualquiera
de los miembros del equipo o por carta a:
GIDIS
Departamento de Computación
F.C.E.I.A
Pellegrini 250
(2000) Rosario
Argentina
|
| ¿Existe
actualmente algún prototipo?
|
Sí.
Desde hace unos meses quien lo desee puede bajar
e instalar Lisex 0.0.
Aunque muy rudimentario, este prototipo posee las características
de seguridad esenciales de una versión más avanzada: implementa
un modelo de seguridad multi-nivel en el sistema de archivos
y fue desarrollado utilizando métodos formales. Debido a que es un prototipo, sugerimos que
sólo sea utilizado por especialistas en seguridad.
Lisex 0.0 no es apto para ser puesto en producción.
|
| ¿Qué
diferencias tiene Lisex 0.0 con Linux?
|
Las
diferencias entre Linux y Lisex 0.0 se limitan al sistema de
archivos. Lisex 0.0 incorpora un modelo de seguridad multi-nivel en el sistema de archivos
así como ACLs y otras características de seguridad. Incluso Lisex 0.0 redefine
la semántica de ciertos aspectos de la seguridad de Linux.
Aun así, en gran medida ambos sistemas son compatibles: Lisex
0.0 no altera la signatura de ninguna llamada al sistema ni
quita llamadas al sistema. Por lo tanto, cualquier aplicación
Linux debería ejecutar sobre Lisex 0.0. Sin embargo, debido
a que Lisex 0.0 incorpora un modelo de seguridad más restrictivo
que el tradicional, es posible que algunas aplicaciones no ejecuten
por falta de permisos. Confiamos que GIDIS Trusted Linux (el sucesor
de Lisex) reducirá estos problemas al mínimo.
Otra diferencia es que Lisex 0.0 fue desarrollado utilizando
métodos formales en varias etapas. |
| ¿Por
qué Lisex incluye seguridad multi-nivel?
|
Porque
es la única forma que conocemos que permite ganar resistencia
a ataques contra la confidencialidad llevados a cabo por medio de caballos de Troya.
Creemos que inspeccionar cada programa para determinar si es
o no un caballo de Troya es ineficiente, propenso a errores,
ineficaz e impracticable en la mayoría de las instalaciones
y para la mayoría de los administradores. |
| ¿Qué
es seguridad multi-nivel? |
En
pocas palabras son aquellas políticas de seguridad que clasifican
los usuarios y la información en clases de acceso o seguridad,
imponen un orden (parcial) sobre las clases de acceso y permiten
que un usuario lea un documento sólo si la clase de seguridad
del usuario es superior a la del documento. El Departamento
de Defensa de los Estados Unidos de América aplica esta política
de seguridad.
Para una explicación más detallada ver esta introducción. |
| ¿Por
qué se usan métodos formales para desarrollar Lisex?
|
Por
dos motivos:
- Nos
interesa la aplicación industrial de los métodos formales.
Por lo tanto nos parece importante mostrar que es posible
aplicarlos en proyectos de envergadura y que la calidad
final del producto es superior a la que se obtiene con la
forma de desarrollo tradicional sin que se alargue el tiempo
de desarrollo.
- Quienes
necesitan que sus sistemas resistan ataques a la confidencialidad
y suponen que una amenaza posible es un caballo de Troya
especial y únicamente construido para atacarlos a ellos,
consideran la seguridad de su información como algo crítico.
Si un sistema debe implementar una misión crítica debe poseer
alta calidad y una tasa de fallas muy baja. Una de las formas
de lograr esas cualidades es la utilización de métodos formales
para desarrollar el sistema.
|
| ¿Qué
son métodos formales? |
En
pocas palabras, los métodos formales son técnicas y herramientas
que utilizan matemática y lógica durante el desarrollo de un
sistema de software.
Sugerimos visitar la página de la Universidad
de Oxford dedicada a métodos formales. Allí podrán encontrar
mucha información tanto para principiantes como para expertos.
|
| ¿Qué
métodos formales se usan en Lisex? |
Durante
el desarrollo de Lisex 0.0 se utilizó básicamente Coq,
y en mucha menor medida Z. Coq se aplicó en varias etapas del desarrollo.
|
| ¿Se
planean otras versiones de Lisex?
|
No,
no para Lisex. En su lugar decidimos lanzar un nuevo proyecto:
GIDIS Trusted
Linux. Aun así, que en algún futuro haya una versión de
GIDIS Trusted Linux depende de qué tanto financiamiento encontremos.
¿Está usted interesado en apoyar este proyecto de alguna forma?
Por favor, ¡contáctenos! gidis-info@fceia.unr.edu.ar
Sí, siempre y cuando tengamos el financiamiento mínimo como
para poder seguir trabajando. La próxima versión de Lisex está
planificada para junio de 2003. |
| ¿En
qué etapas del desarrollo de Lisex se usaron métodos formales?
|
- Las
etapas son las siguientes:
![]() |
Especificación de requerimientos. Los requerimientos
de seguridad se modelaron utilizando Coq.
|
![]() |
Verificación del modelo. Utilizando
Coq se demostraron una serie de teoremas que prueban
que el modelo descripto en la fase anterior verifica
las propiedades del modelo Bell-LaPadula.
|
![]() |
Testing funcional. Se utilizó la técnica de testing
funcional basado en especificaciones formales para
obtener casos de prueba con los que verificar la corrección
de la implementación con respecto al modelo.
|
No se efectuó verificación formal de la implementación;
es posible que durante este año se avance sobre esta etapa
en colaboración con investigadores del FAMAF de la Universidad
Nacional de Córdoba (Argentina).
|
| ¿Qué
es un caballo de Troya? |
Un
caballo de Troya es un programa que se presenta al usuario como
una aplicación útil e inofensiva pero que al ser ejecutado daña,
modifica o divulga toda o parte de la información a la que ese
usuario tiene acceso.
El proyecto Lisex se centra en los caballos de Troya que divulgan
información, es decir los que atentan contra la confidencialidad.
Claramente cualquier programa puede ser un caballo de Troya
(editores, juegos, comandos, clientes, servidores, etc.). Los
caballos de Troya no necesitan que el sistema operativo contenga
algún error para realizar su ataque; puede decirse que el sistema
operativo es erróneo por definición. Tampoco requieren de la
complicidad del usuario que los ejecuta; los usuarios son las
víctimas de este ataque.
|
| ¿Por
qué Lisex intenta resolver el problema de la confidencialidad
y no el de la integridad o la disponibilidad? |
Por
varias razones:
![]() |
Históricamente la comunidad científica atacó el problema
de la confidencialidad (esto se debió a que el primer interesado
fue el aparato militar estadounidense para el cual la
confidencialidad es más importante que la integridad).
|
![]() |
Debido a lo anterior hay mucha más información sobre el
problema de la confidencialidad.
|
![]() |
En principio el problema de la confidencialidad es más
simple que el de la integridad y la disponibilidad.
|
![]() |
Las técnicas y modelos que "resuelven" el problema de
la confidencialidad son, en muchos casos, la base de aquellos
que atacan el problema de la integridad.
|
![]() |
Creemos que existe una multitud de organizaciones para
las cuales preservar la confidencialidad de su información
es algo crítico o muy importante.
|
|
| ¿Dónde
se puede encontrar más información sobre los temas vinculados
a Lisex? |
La
sección de enlaces de nuestro sitio contiene referencias a numerosos
sitios o páginas que tratan el tema desde diferentes puntos
de vista. Creemos que es un buen lugar para comenzar.
Además, pueden consultar la documentación del proyecto, en particular esta
introducción. |
| ¿Qué
es confidencialidad? |
Es
el carácter confidencial de algo. A su vez, confidencial
es aquello que se hace o se dice en secreto.
Por lo tanto, preservar la confidencialidad implica
preservar un secreto. Un secreto se preserva
sólo si quienes lo poseen son los únicos capaces de permitir
(consciente y voluntariamente) que otros lo conozcan.
Sugerimos leer la primera sección de esta introducción para ver la definición de libro de
texto. |
| ¿Qué
es un modelo de seguridad multi-nivel? |
Un
modelo de seguridad multi-nivel es el resultado de adaptar a
un sistema de cómputo una política de seguridad multi-nivel. Normalmente, no se pueden
asumir las mismas hipótesis y condiciones sobre un sistema de
cómputo que sobre el mundo real (de personas y papeles). Por
lo tanto, es necesario adaptar la política de seguridad al sistema
de cómputo de forma tal que valgan las mismas propiedades en
el sistema que en el mundo real.
En tanto modelo, es una abstracción del sistema de cómputo que
verifica ciertas reglas o propiedades. No es un programa ni
una computadora aunque de él se derivará el hardware y el código
que finalmente conformará la máquina que utilizarán los usuarios.
Usualmente los modelos de seguridad multi-nivel se expresan
mediante alguna notación formal. |
| ¿Qué
es el modelo Bell-LaPadula? |
El
modelo Bell-LaPadula (BLP) es uno de los primeros modelos formales
de seguridad multi-nivel. BLP es sin dudas el modelo multi-nivel
más conocido, estudiado, referenciado e implementado.
Aquí
pueden encontrar la versión electrónica de uno de los artículos
seminales de D. Elliot Bell y Leonard J. La Padula. |
