Lisex
Security Model (LSM 0.0)
La
especificación es un modelo abstracto de un sistema de archivos
compatible con Linux (o UNIX en general). Toma la forma de una máquina
de estados. Toda la especificación está escrita en Coq
y documentada con coqdoc.
El código formal de la especificación ha sido comentado mínimamente;
el lector que desee una explicación más detallada puede consultar
[Cristiá].
El código fuente de la especificación y verificación formal listo
para ser compilado en Coq 7.3 está en el archivo LSM00.tar.gz.
Se
define el estado
del sistema de archivos como un registro que comprende los elementos
relevantes al problema de seguridad (archivos, directorios, clases
de acceso, ACLs, archivos abiertos, etc.). En particular se define
un estado
inicial para el sistema.
Se
definen operaciones que representan cada una de las llamadas al
sistema que tienen relación con el sistema de archivos. Cada operación
se define constructivamente mediante un tipo inductivo en términos
de sus precondiciones y post-condiciones. Existen dos tipos de operaciones:
- Consulta
- Aquellas
operaciones que solicitan datos sobre el estado del sistema pero
no tienen la capacidad de efectuar un cambio de estado:
- Modificación
- Aquellas
operaciones que llevan el sistema de un estado a otro:
Debido
a que la especificación es un modelo abstracto del sistema de archivos,
no se describen todas las llamadas al sistema. Sin embargo, se relacionan
todas las llamadas al sistema de archivos con alguna operación del
modelo, dicha información puede hallarse en el documento de diseño.
Además,
se especificaron las propiedades
de seguridad que se espera que el sistema de archivos posea.
Se escribe un predicado por cada propiedad que se desea. En general,
cada predicado define el significado de estado seguro o transición
segura del sistema desde un punto de vista diferente a los demás.
En LSM 0.0 se definieron cuatro predicados:
Finalmente,
se verificó formalmente que el modelo cumple con
todas las propiedades esperadas.
|
