|
Como
se explica en la sección Especificación formal, se cuenta con una especificación
formal de cada una de las operaciones del modelo de cómputo
y con una especificación formal de cada una de las propiedades
que se espera que el modelo verifique.
El
modelo verifica una propiedad si tal propiedad es un invariante
del modelo. Un predicado es un invariante de un modelo si
cada una de las operaciones del modelo preserva el predicado.
Una operación preserva un predicado si, partiendo de un estado
donde el predicado es cierto, la operación deja al sistema
en un estado donde el predicado también es cierto.
En
consecuencia, verificar que el modelo cumple con una propiedad
implica, por lo general, probar que cada operación preserva
esa propiedad. Más técnicamente, el trabajo de verificación
consiste en probar que
s,t:Estado · P(s) /\ TR(s,Op,t) -> P(t)
para
cada operación Op, donde
- Estado
- es
el conjunto o tipo de todos los estados posibles en los
que puede estar el sistema; s y t están cuantificadas universalmente
sobre ese conjunto.
- P
- es
la propiedad o predicado que se espera que la operación
preserve; notar que es un predicado que depende de un estado.
- TR
- es
la relación de transición de estados que relaciona dos estados
(s y t) y una operación (Op). La interpretación es que la
operación Op lleva el sistema del estado s al estado t.
Luego,
se prueba que
n:Nat; s1,...,sn:Estado ·
P(s1) /\ (i:Nat · i < n -> (EX Op:Operacion · TR(si,Op,si+1))) -> P(sn)
donde
- Nat
- es
el conjunto o tipo de los números naturales.
- EX
- es
el operador lógico de cuantificación existencial.
- Operacion
- es
el conjunto o tipo de todas las operaciones del sistema.
En
Lisex los lemas enunciados más arriba toman una forma ligeramente
diferente. Lisex Security Model define cuatro propiedades
de interés que se espera que el modelo preserve:
Las
dos primeras se combinan en un único predicado (SecureState),
y la última es una propiedad de transición (no de estado)
por lo que no debe asumirse que vale en el estado de partida.
Por lo tanto, se deben probar tres lemas por cada operación
del sistema:
- OpPSS
- acrónimo
de Op Preserves Secure State (por ejemplo, ChmodPSS); los
lemas de esta forma prueban que cada operación preserva
la dos primeras propiedades (DACSecureState y SimpleSecurity)
- OpPSP
- acrónimo
de Op Preserves Star Property (por ejemplo, AddUsrGrpToAclPSP);
los lemas de esta forma prueban que cada operación preserva
la propiedad de confinamiento (recordar que star property,
*-property y confinamiento son sinónimos).
- OpPCP
- acrónimo
de Op Preserves Control Property (por ejemplo, ClosePCP);
los lemas de esta forma prueban que cada operación preserva
la propiedad de cambio de atributos de seguridad.
Por
ejemplo, en lenguaje Coq el lema OpenPSP se escribe de la
siguiente forma:
Lemma OpenPSP:
(s,t:SFSstate; u:SUBJECT)
(FuncPre5 s)
->(StarProperty s)->(TransFunc u s Open t)->(StarProperty t).
donde
(FuncPre5
s) es un predicado que asegura que secmat
es una función
parcial finita, lo cual es un requisito para poder probar
que open preserva confinamiento. Observar que,
con respecto a la forma general que tienen estos lemas, se
cambia /\ por -> lo que es lógicamente
correcto. Además, la relación de transición captura el sujeto
(proceso) que efectúa la llamada o ejecuta la operación por
lo que es necesario cuantificar universalemente sobre todos
los posibles sujetos que pueden ejecutar la operación. De
esta forma, se puede estar seguro de que sin importar el estado
de cual se parta ni el sujeto que ejecuta la operación, si
el estado de partida es ``seguro'' el estado de llegada también
lo será.
Los
tres lemas se agruparon en un archivo por cada operación:
Finalmente
se probó un lema que asegura que el sistema preserva DACSecureState,
SimpleSecurity y StarProperty. En la teoría de seguridad,
a este lema se lo conoce como Basic
Security Theorem (BST). Notar que en ese mismo módulo
se prueba que el estado inicial del sistema es seguro.
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.
La
verificación formal presentada en esta página sólo asegura
que el modelo es correcto con respecto a varias propiedades.
Esto no da ninguna seguridad que la implementación del modelo
sobre el núcleo de Linux sea correcta con respecto al modelo.
El testing funcional efectuado apunta a comprobar la corrección
de la implementación con respecto a la especificación.
|
