Introducción a la seguridad de Lisex 0.0, PostScript version.

This paper is for those interested in learning about MLS models and topics related. Those with more experience in this field might want to read the MSc. thesis [Cristiá] or the information about formal specification and verification to obtain a detailed description regarding the security model implemented in Lisex 0.0. For further information, please see [AJP95,Gas88].

Lisex is an operating system designed to resist confidentiality attacks made by Trojan horses in environments where security is a critical feature or at least very important. According to the research done mainly in the US during the '70s and '80s, such threats should be defended against using:

 

	a Multi-level Security (MLS) model in the system kernel, and
	formal methods for system development.

The MLS model available in the current release of Lisex [Cristiá], called Lisex Security Model 0.0 (LSM0.0), is adapted from the Bell and La Padula model [BL73a,BL73b], introduced in 1973. LSM0.0 is just available in the file system of Linux Kernel 2.4.14 and it was developed using the Coq proof assistant. Formal specification and verification were integrated with the development of Lisex 0.0. Lisex's successor, GIDIS Trusted Linux, will implement equivalent models in different parts of the kernel.

In addition, Lisex 0.0 implements access control lists (ACL) in order to improve the traditional DAC mechanism used in Linux and other minor security features.