Gidis Trusted Linux


GIDIS Trusted Linux ancestor's: Lisex

It has been pointed out in the Overview, that the R+D Group on Software Engineering (GIDIS) is not new in developing MLS operating systems. With the economic help of Lifia, GIDIS personnel developed a Linux MLS prototype, named Lisex 0.0. Lisex version 0.0 is a basic and incomplete prototype, but it could be the starting point of a product able to rank at TCSEC's B1 class or even higher.

The following are the security features of Lisex 0.0 and its development process:

  Fixed length ACLs, configurable in kernel compilation time. ACLs may contain users and groups.

List of owners for each file and directory (this data is contained in each appropriate ACL).


root user group, equivalent to user root.


secadm account and user group in charge of the administration of the MAC attributes of objects and subjects.


Implementation of a MLS Security Model for the ext2 file system (where user information is stored).


Formalization and formal verification of the security model conducted in Coq.

  Documentation (in Spanish and in Latex, PDF and HTML format):
  Formal security model

Formal security model interpretation according to the implementation and the ext2 file system own vocabulary.

  Scripts of every formal test conducted on the formal model.
  Test cases selected at specification level

User and Administrator's Manual

  Programmers' Reference Manual


© 2003 por Grupo Gidis. Todos los derechos reservados.
Sitio diseñado por Lorena Cantarini [mailto]