Existe una importante cantidad de desarrollos de versiones seguras de sistemas operativos propietarios tipo-UNIX (y también S.O. no-UNIX). Aparentemente, muchos de estos desarrollos no tuvieron éxito comercial debido a su dependencia con el éxito de las versiones no seguras. Una lista incompleta es: System V/MLS, Trusted XENIX, Harris CX/SX, HP-UX BLS, Trusted Solaris, and ULTRIX MLS, etc.

Basándonos en la información disponible, System V/MLS y Trusted Xenix OS parecen estar entre aquellos en los cuales se aplicaron métodos formales en alguna de las fases del desarrollo (aunque es muy posible que otros también los hayan usado). Por otro lado, los datos disponibles indican que ninguno de los productos listados habrían sido desarrollados mediante la utilización intensiva de técnicas formales, como es el caso de la presente propuesta. Por ejemplo, System V/MLS, el primer UNIX en obtener la certificación B1 del TCSEC [13], utilizó métodos formales para especificar las propiedades de seguridad [12], pero no hay evidencia de que se haya especificado la interfaz del núcleo ni que se haya verificado formalmente la concordancia de una con respecto a las otras, como es nuestro caso.

Existen ciertos dominios específicos donde fueron aplicados los métodos formales para el desarrollo de Xenix, tales como identificación de canales encubiertos [8]. El proyecto Xenix también incluyó un tipo de testing funcional guiado por la especificación del sistema [9].

Más allá de estos productos comerciales, es interesante mencionar los primeros sistemas A1 (del TCSEC) desarrollados en los '80 por empresas como Gemini, Honeywell o Boeing, en asociación con el Departamento de Defensa estadounidense. Estos sistemas tendieron a ser costosos, de propósito restringido y no soportaban las interfaces de desarrollo y programación de los sistemas operativos más familiares. Sin embargo, un proyecto más reciente e interesante, que posiblemente provenga de aquellos, llamado LOCK (Logical Co-processing Kernel) fue desarrollado con la intención de alcanzar o superar la clasificación A1 [10], lo que requiere el uso intensivo de métodos formales. Otro proyecto interesante, aunque menos ambicioso, es el Security Enhanced Linux (SELinux) de la NSA¹⁰. Este es un desarrollo de fuente abierta y uno de los que comparte mayores similitudes con GIDIS Trusted Linux. Existe, además, un proyecto para desarrollar una versión segura de fuente abierta de OpenBSD llamada TrustedBSD.

El sistema LOCK fue diseñado y construido como un sistema interactivo multi-usuario que conecta a los usuarios vía terminales de texto. Esta era la forma dominante de los sistemas medianos a grandes en el inicio del proyecto, y a su vez refleja varios de los requerimientos y suposiciones de diseño implícitas del TCSEC. Este diseño también parecía soportar la más amplia gama de usos potenciales incluyendo acceso de tiempo compartido. Se suponía que se podría reducir este sistema y ejecutarlo en una estación de trabajo dirigida por un microprocesador moderno, o tal vez ampliarlo y correr procesos batch bajo la supervisión de un job monitor. Por otra parte, dado que la terminal de texto era la tecnología más usada en aquel tiempo, LOCK no incluye ninguna capacidad de manejo de gráficos ni ventanas. Los diseñadores de LOCK asumieron que la funcionalidad para trabajo en red podía ser agregada más tarde. De hecho el soporte para TCP/IP se adicionó en 1992 utilizando fondos corporativos para I+D.

LOCK incorporó varias características en un intento por producir un sistema práctico que cumpliera con los requerimientos de la clase A1:

• TCB separada del sistema operativo
• Tamaño mínimo del núcleo
• Criptografía de uso militar incorporada en la TCB
• Co-procesador para toma de decisiones de seguridad
• Desempeño comparable a un sistema UNIX estándar
• Uso práctico de mecanismos de imposición de tipos¹¹ en el software de seguridad

Como ya se mencionó, este proyecto se inició como un proyecto de investigación para desarrollar un sistema A1. A lo largo de siete años, el proyecto se transformó en un esfuerzo por desarrollar y distribuir un producto: el Standard Mail Guard (SMG). Información más detallada puede encontrarse en [10].

Es fácil observar las similitudes de este proyecto con el que nosotros proponemos tanto en los objetivos, las técnicas de implementación y el modelo de ciclo de vida del software. Sin embargo, el proyecto LOCK no intenta desarrollar un sistema seguro compatible con alguna versión no-segura, lo que constituye una diferencia significativa.

Esta versión de Linux está siendo desarrollada por la NSA y afirma tener una arquitectura MAC potente y flexible incorporada en los sub-sistemas más importantes del núcleo. Este Linux mejorado implementa mayormente imposición de tipos por medio de una interfaz general claramente definida que es capaz de soportar una gran variedad de políticas de seguridad incluyendo MLS.

SELinux actualmente cuenta con una versión lista para usar pero aún tiene varios aspectos que mejorar tales como desempeño y usabilidad.

Todo el código fuente es cedido bajo los mismos términos y condiciones que los fuentes originales. Los parches al núcleo de Linux, a las utilidades existentes y los programas nuevos son cedidos bajo los términos y condiciones de la GNU General Public License (GPL), mientras que otros parches son cedidos bajo los términos y condiciones de la licencia BSD.

TrustedBSD provee un conjunto de extensiones seguras con respecto al sistema operativo FreeBSD con el objetivo de alcanzar la categoría B1 del TCSEC. Esto incluye la introducción de:

• Herramientas para administración segura
• Capacidades del sistema de granularidad fina¹²
• Listas de control de acceso
• Auditoría de eventos de seguridad
• Control de acceso obligatorio

En el momento de escribir este documento, la implementación de TrustedBSD está aún en una fase inicial. Sólo algún soporte para MAC, capacidades y ACLs está cerca de completarse.

Las extensiones de TrustedBSD se ponen a disposición del público bajo una licencia del tipo de BSD la cual, en esencia, requiere preservar los derechos de autor y renuncia a responsabilidades. Para mayores detalles consultar [11].