There are several developments
of trusted versions of many proprietary Unix-like OS (and also
not Unix-like). Apparently, most of these developments did not
succeed mainly due to their dependency on the success achieved
by its untrusted versions. The following is a list of some of
them: System V/MLS, Trusted XENIX, Harris CX/SX, HP-UX BLS, Trusted
Solaris, and ULTRIX MLS among others.
to the available information, System V/MLS and Trusted Xenix OS
seem to be the ones that used formal methods at some stage of
its development (though it is quite possible that others may have
used them). Besides, available data shows that none of the listed
products have been developed with intense using of formal techniques,
as happens in this project. For instance, System V/MLS, the first
Unix that obtained the B1 certification, used formal methods for
property specification as part of a detailed framework for security
assessment , but there is not evidence that the kernel interface
has been specified, nor that concordance between them has been
formally verified, as in our project.
some specific domains where formal methods were used on Xenix
such as covert channel identification . This development have
also included one kind of functional testing aided with system
class specification . Apart from these commercial products
it is interesting to mention earlier A1 systems developed in the
80ís by Companies such as Gemini, Honeywell or Boeing, some of
them in association with the DoD of the United States. These systems
tend to be expensive, special-purpose, and did not support the
programming interfaces of more familiar operating systems. However
a more recent and interesting research project of Secure Computing
Corporation, that possibly arose from them, called LOCK (Logical
Co-processing Kernel) was developed with the aim of meeting or
even exceeding the A1 requirements , which requires intensive
use of formal methods. Another interesting but less ambitious
project of the NSA is the Security Enhanced Linux (LinuxSE). This
is an open source project and it shares several similarities with
Lifia Secure Linux project. There is also another similar open
source project based on a trusted version of OpenBSD called TrustedBSD.
The LOCK system was
designed and built as an interactive multi-user system that connects
users via character based ASCII terminals. This was the prevailing
form of medium and large-scale systems at the time, and reflected
many requirements and implicit design assumptions of the TCSEC.
This design also appeared to support the broadest range of potential
uses in addition to time-shared interactive access. It was supposed
that it was possible to scale it down and run it on a workstation
driven by a modern microprocessor, or perhaps scale it up and run batch jobs under a job monitor. Besides, character oriented
graphics were the prevailing technology at that time, so LOCK
did not include any workstation graphics or windowing capabilities.
LOCK designers assumed that networking could be added at a later
date. In fact, TCP/IP support was added to LOCK using corporate
R&D funds in 1992.
a number of features in an attempt to produce a practical system
that complied with the A1 requirements:
from the operating system
cryptography integrated with the TCB
for security decision making
comparable to a standard Unix system
use of the type enforcement mechanism in security software
before, this project began as a research project for building
an A1 system. Over the span of seven years,
the project was transformed into an effort to develop and deploy
a product: The Standard Mail Guard (SMG). Detailed information
can be found in .
As we may
see, there are several similarities between this project and the
one we are designing, such as their goals, implementation techniques
and the software life cycle model. However, LOCK project does
not attempt to develop a secure system compatible with non-secure
versions, which is a major difference.
This version of Linux is being
developed by NSA and claims to have a strong, flexible mandatory
access control architecture incorporated into the major subsystems
of the kernel. This security-enhanced Linux implements mostly
Type Enforcement by a well-defined general interface that is capable
of supporting a wide variety of security policies, including MLS.
currently have available ready-to-use versions, but yet some issues
have to be enhanced, such as performance and usability.
All source code is released under the same terms and conditions
as the original sources. Patches to the Linux kernel, to many
existing utilities, and to new programs and libraries are released
under the terms and conditions of the GNU General Public
License (GPL), other patches are released
under the terms and conditions of the BSD license.
TrustedBSD provides a set of trusted
extensions to the FreeBSD operating system, targeting the B1 evaluation
criteria, they include:
date, TrustedBSD implementation status is still in an early stage.
Only some support code for MAC and also capabilities and ACL components
are nearing completion.
extensions will be made freely available under a BSD-style license,
which essentially requires the preservation of the copyright,
and disclaims liability. For more details see .