Introduction

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.

According 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 [12], 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.

There are some specific domains where formal methods were used on Xenix such as covert channel identification [8]. This development have also included one kind of functional testing aided with system class specification [9]. 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 [10], 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.

LOCK incorporated a number of features in an attempt to produce a practical system that complied with the A1 requirements:

• TCB separated from the operating system

• Minimized kernel mode software

• Military grade cryptography integrated with the TCB

• Hardware coprocessor for security decision making

• Performance somewhat comparable to a standard Unix system

• Practical use of the type enforcement mechanism in security software

As mentioned 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 [10].

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.

SELinux 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:

• Trust Management (System handling and administration tools)

• Fine-grained System Capabilities

• Access Control Lists

• Security Event Auditing

• Mandatory Access Control

To this 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.

TrustedBSD 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 [11].