Information Technology Reference
In-Depth Information
The research of secure operating system begins in 1967's Adept-50 project.
From that time on, the theories, technologies, and methods are established step
by step. Adept-50 is also the first attempt to implement multi-level military se-
cure mathematical model on running systems. A most influential result in the
infancy stage of secure operating system research is Bell&LaPadula model (BLP)
proposed by Bell and LaPadula in 1973. They give a formal description and an
informal notation of BLP and the interpretation of its implementation in Multics
system [3]. This is the beginning of application of formal methods in secure oper-
ating system. The UCLA Data Secure UNIX formally realizes BLP model later
and uses XIVUS's theory prover to do formal proves. In the year 1985, United
States' Department of Defense published the complete edition of Trusted Com-
puter System Evaluation Criteria (TCSEC)[4]. TCSEC have 7 different security
evaluation levels: D, C1, C2, B1, B2, B3 and A1. Each level corresponds to a set of
particular security characters and insurances. United States Army Secure Oper-
ating System [5] is a family of operating system developed according to TCSEC.
There are in fact two different systems: a TCSEC C2 level operating system and
a TCSEC A1 level operating system. ASOS A1 operating system constructs for-
mal specification and proofs in two levels: Abstract Security Model and Formal
Top-Level Description. ASOS developed a flow analysis tool working in Gypsy
Verification Environment to analysis convert channels in the system design. An-
other TCSEC A1 level secure operating system Logical Coprocessing Kernel
(LOCK) [6] is developed by United States National Security Agency (NSA) also
uses Gypsy specification language and GVE as its formal tool [7]. There is plenty
of other secure operating systems use formal method to insure design consistence,
but none of them has reached such a high security level as ASOS and LOCK do.
In the process of developing Security in Mind Operating System (SECIMOS),
we use Z specification language to formalize the secure policy models and use
ordinary English to describe top level security functionalities and informally
prove the correspondence between the policy model and top level security func-
tionalities. The rest of the paper is organized as follows, the basic architecture is
discussed in section 2, the Z specification of the secure policy models is discussed
in section 3, we compare several of formal tools and their potential for secure
operating system use in section 4, and we conclude our paper in section 5.
2
Basic Architecture of SECIMOS
Security in Mind Operating System (SECIMOS)[8] is a customizable secure op-
erating system developed by Institute of Software, Chinese Academy of Science
based on Linux 2.6 kernel which has already absorbs LSM (Linux Security Mod-
ule) framework as an indispensably part. This project makes uses of four secu-
rity policies each of which is implemented as a separate module Fig. 1. These
four modules are: module for Multilevel Security policy (MLS), module for Dis-
cretionary Access Control (DAC), module for Controlled Privilege Framework
(CPF) (This is used to control the behaviors of Trusted Process), module for
Privileged User (PUSER). To solve the policy conflicts, SECIMOS assign each
module an unsigned 16 bit “order” and an unsigned 8 bit “type”. The “order”
