1. Cristiá, M., "Verificación formal de una extensión segura de un sistema de archivos compatible con UNIX", Tesis de Maestría, Instituto de Computación, Universidad de la República (Uruguay), 2002.

2. Gasser, M., Building a Secure Computer System, Van Nostrand Reinhold, New York, 1988.

3. Abrams, M., and H. Podell, and S. Jajodia, Information Security-An Integrated Collection of Essays, IEEE Computer Society Press, 1995.

4. Loscoco, P., et. al., "The inevitability of failure: The Flawed assumption of security in modern computer environments", www.nsa.gov/selinux.

5. Schneier, B., Secrets & Lies: Digital security in a networked World, Wiley Computer Publishing, 2000.

6. Stocks, P., "Applying formal methods to software testing", Doctoral Thesis, Department of Computer Science, University of Queensland, 1993.

7. Bell, D., and L. LaPadula, "Secure Computer Systems: Mathematical Foundations and Model", Vols. I-II, ESD-TR-73-278, The MITRE Corporation, Bedford, MA 1973/74.

8. Tsai, C., V.D. Gligor, and C.S. Chandersekaran, "A Formal Method for the Identification of Covert Storage Channels in Source Code," Proceedings of the 1987 IEEE Symposium on Security and Privacy, pp. 4-87, April 1987.

9. Gligor, V.D., and et. al.,. "A New Security Testing Method and Its Application to the Secure Xenix Kernel", TSE 13(2): 169-183, 1987.

10. Smith, R., "Cost Profile of a Highly Assured, Secure Operating System", ACM Transactions on Information and System Security, 4(1), February 2001.

11. http://www.trustedbsd.org

12. Amoroso, E., et. al. "Toward an Approach to Measuring Software Trust", Proceedings of the IEEE Symposium on Research in Security and Privacy, Oakland, CA, May 1991.

1We may also think in any system managing sensitive information whose confidentiality must be preserved, for instance, medical, banking, legal, military data.

2Program with two functions: one visible and profitable for some user (for example, a game), and the other undocumented and intended to obtain confidential data from the user/s who execute it.

3Besides, the device for communicating with the corporate's network may have a higher access class, thus allowing transmission of that data to other hosts inside the company, but never outside.