- What is Lisex?
- What is GIDIS Trusted Linux?
- When did the project started and what is its state now?
- Where has Lisex been developed?
- Is there any prototype available?
- What are the differences between Lisex 0.0 and Linux?
- Why does Lisex include multi-level security?
- What is multi-level security?
- In order to develop Lisex, why do you use formal methods?
- What are formal methods?
- What particular formal methods have you used for this
case?
- Are you planning new versions?
- In Lisex development, what stages were performed with
formal methods?
- What is a Trojan horse?
- Why do you try to solve a confidentiality problem
and not an integrity or availability one?
- Where can I find more information about issues related
with Lisex?
- What is confidentiality?
- What is a multi-level security model?
- 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:
- 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.
- 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. |