Lisex  
 
 

 

Frequently asked questions about Lisex
  1. What is Lisex?
  2. What is GIDIS Trusted Linux?
  3. When did the project started and what is its state now?
  4. Where has Lisex been developed?
  5. Is there any prototype available?
  6. What are the differences between Lisex 0.0 and Linux?
  7. Why does Lisex include multi-level security?
  8. What is multi-level security?
  9. In order to develop Lisex, why do you use formal methods?
  10. What are formal methods?
  11. What particular formal methods have you used for this case?
  12. Are you planning new versions?
  13. In Lisex development, what stages were performed with formal methods?
  14. What is a Trojan horse?
  15. Why do you try to solve a confidentiality problem and not an integrity or availability one?
  16. Where can I find more information about issues related with Lisex?
  17. What is confidentiality?
  18. What is a multi-level security model?
  19. What is the Bell-LaPadula model?
What is Lisex?
Lisex is a project which goal is to increase the resistance of UNIX-like operating systems to attacks against confidentiality performed by means of Trojan horses.

During the '70 and '80, the USA computer security research community created a body of knowledge which postulate that resistance to this kind of attacks is obtained by implementing a multi-level security model inside the operating system kernel and using formal methods to develop the system.
What is GIDIS Trusted Linux?

  The funding for Lisex coming from our previous sponsor has finished. Thus, GIDIS started a new project, named GIDIS Trusted Linux, to develop the successor of Lisex. GIDIS Trusted Linux needs partners or sponsors, it needs you.

When did the project started and what is its state now?
Formally, the project begun October, 1º 2001; but, since a couple of years ago Maximiliano Cristiá was writing his MSc thesis what gave place to the formal model used to implement Lisex 0.0.

Lisex as a funded project has finished. But, now at GIDIS we will pursue to get funding for its successor: GIDIS Trusted Linux.
Where has Lisex been developed?
The project has been developed in Rosario, Santa Fe, Argentina. Due to our scarce resources, the team still lacks offices. However, formally, the project lies at the Computer Science Department of the Engineering Faculty, National University of Rosario.

To contact us send an email to any of our team members or write a letter to

GIDIS
Departamento de Computación
F.C.E.I.A
Pellegrini 250
(2000) Rosario
Argentina

Is there any prototype available?
Yes. Since a couple of month you can download Lisex 0.0.

Lisex 0.0 might be rudimentary and simple, but it has all the essential security features of a more advanced version: it implements a multi-level security model in the file system, and it was developed using formal methods. Being a prototype, it is intended to be used by security experts.

Lisex 0.0 is not apt for a production environment.
What are the differences between Lisex 0.0 and Linux?
Differences between Linux and Lisex 0.0 are bounded to the file system. Lisex 0.0 includes a multi-level security model in the file system as well as ACL and other security features not present in Lisex. Moreover, Lisex 0.0 redefines the semantics of some security capabilities available in Linux.

Even so, both systems are highly compatible: Lisex 0.0 does not modify the signature of any system call nor it removes any of them. In consequence, any Linux application should run on Lisex 0.0. However, due to the inclusion of a more restrictive security model, it is possible that some applications do not run because lack of permissions. We have confidence that GIDIS Trusted Linux (Lisex successor) will reduce these problems to a minimum.

Other difference is that Lisex 0.0 was developed with an intensive use of formal methods.
Why does Lisex include multi-level security?
Because is the only way we know that increases the resistance to attacks against confidentiality performed by means of Trojan horses.

We believe that inspecting each and every program to decide if it is a Trojan horse or not, is inefficient, error prone, and impossible in practice for most administrators and installations.

What is multi-level security?
To answer this question in just a few words, multi-level security (MLS) are those security policies which classify individuals and information in access or security classes, define a partial order on the set of access classes, and allow an individual to read a document if and only if his or her access class is greater than or equal to the document's one.

For a more detailed explanation you may read this introduction
In order to develop Lisex, why do you use formal methods?
For two reasons:
  1. We are interested in applying formal methods to industrial problems. Thus, we want to show that including formal methods in non trivial projects increases the quality of the final product not extending the development time.
  2. There are organizations who need systems capable of resisting attacks against confidentiality and have determined that Trojan horses are a threat. They usually consider their information as a particularly valuable asset, sometimes critical. If a system must implement a critical mission, it must have high quality and a low fault rate. One way to reach these goals is to use formal methods to develop the system or at least its core modules.
What are formal methods?
Shortly, formal methods are mathematically based languages, techniques, and tools for specifying and verifying software or hardware systems.

We suggest you to visit the Oxford University's formal methods site. There you will find lots of information for beginners as well as experts.

What particular formal methods have you used for this case?
To develop Lisex 0.0 we used Coq in many development phases.
Are you planning new versions?
No, we are not planning new versions of Lisex. Instead, we decided to launch a new project, namely GIDIS Trusted Linux. But, whether there will be any version of GIDIS Trusted Linux depends upon how much funding we can get for it. Are you interested in supporting us in any way? Please, contact us! gidis-info@fceia.unr.edu.ar
In Lisex development, what stages were performed with formal methods?
  • The stages are the following:
    Requirement specification. Security requirements were modeled with Coq.
    Modelverification. Using Coq as theorem assistant, three dozens of proofs have been carried out. These theorems prove that the model verify the security properties stated in the Bell-LaPadula security model.
    Functional testing. Specification-based functional testing was applied to generate test cases to verify implementation correctness.


    No formal verification of the implementation has been conducted. However, we have an informal agreement with researchers from FAMAF (Córdoba National University, Argentina) in order to jointly verify the implementation using logics capable of dealing with pointers.

What is a Trojan horse?
A computer program with an apparently or actually useful function that contains additional (hidden) functions that surreptitiously exploit the legitimate authorizations of the invoking process to the detriment of security -for example, making a "blind copy" of a sensitive file for the creator of the Trojan horse.

Lisex focus on Trojan horses which disclose information, that is on programs that are a threat to confidentiality.

Clearly, any program could be a Trojan horse (text editors, games, commands, clients, servers, and so on). Trojan horses do not need a faulty operating system to complete their attacks; one can say that the operating system is fundamentally flawed. Moreover, the user who executes them need not be a traitor, on the contrary he is a victim.

Why do you try to solve a confidentiality problem and not an integrity or availability one?
For many reasons:
The bulk of computer-security research has centered around confidentiality, primarily because the military funded much of the early research. In fact, they value much higher confidentiality than integrity or availability.
So there are much more information available about confidentiality.
Integrity is harder to precisely define, so, at least in principle, confidentiality looks simpler.
Techniques to protect against information modification are almost always the same as (or a subset of) techniques to protect against information disclosure.
We believe that there exists many organizations for which protecting the secrecy of their information is critical or mission-critical.
Where can I find more information about issues related with Lisex?
We think of our links section as a good place to start. There you will find a number of referenced Web sites treating these issues from different perspectives.

Also, you can take a look at the project documentation, particularly this introduction.
What is confidentiality?
The assurance that information is not disclosed to inappropriate entities or process.

The property that information is not made available or disclosed to unauthorized entities.

The prevention of the unauthorized disclosure of information.

The concept of holding sensitive data in confidence, limited to an appropriate set of individuals or organizations.

What is a multi-level security model?
A multi-level security model is an obvious representation of a multi-level security policy. Usually, is not possible to assume the same hypothesis and conditions on the real world (of humans and papers) and in the computer system. For this reason, it is necessary to rewrite the policy (making it a computer security model) so the same security properties are true both of the system and the real world.

As a model, it is an abstraction of the policy. It is not a program nor a computer but the machine that finally will be in use is derived form it.

It is customary to express multi-level security models in a formal notation.
What is the Bell-LaPadula model?
A formal state-transition model of computer security policy that describes a set of multi-level access control rules obeying the US military security policy. This model was one of the first multi-level security models, and, no doubt, the most studied, referenced, and implemented.

Here you will find an electronic version of one of the seminal works by D. Elliot Bell y Leonard J. La Padula.
   
© 2003 por Grupo Gidis. Todos los derechos reservados.
Sitio diseñado por: Lorena Cantarini