Information Technology Reference
In-Depth Information
A Formal Description of SECIMOS
Operating System
∗
Zhouyi Zhou
1
,
2
,
3
,BinLiang
4
,
5
,LiJiang
1
, Wenchang Shi
1
, and Yeping He
1
1
Institute of Software, Chinese Academy of Sciences, Beijing 100080, PRC
2
Graduate School of the Chinese Academy of Sciences, Beijing 100049, PRC
3
College of Computer and Communications, Hunan University,
Changsha HN 410082, PRC
4
Department of Computer Science and Technology, Tsinghua University,
Beijing 100084, PRC
5
Beijing Venus Info Tech Inc, Beijing 100081, PRC
{
zhouyi04, jiangli02, wenchang
}
@ios.cn
liangbin@venustech.com.cn
yphe@ercist.iscas.ac.cn
Abstract.
The application of formal methods in secure operating sys-
tem experiences a procedure of development and maturity with the em-
inence and development of secure operating system itself. According to
Common Criteria and United States Department of Defenses Trusted
Computer System Evaluation Criteria (TCSEC), high security level se-
cure operating system should introduce formal methods in the process
development and evaluation. Security in Mind Operating System (SEC-
IMOS) is a customizable secure operating system developed by Institute
of Software, Chinese Academy of Science. In this work, we formally model
the security policies using Z specification language and informally proved
the correspondence between policies and top level functionalities. As a
result, we summarize the gist to choose a formal description language for
modeling a secure operating system and possibility of use Isabelle/HOL
as a formal tool.
1
Introduction
Formal methods have played a more and more important role in the develop-
ment of software and hardware systems. By describing some logic relations in a
system using strict mathematical language, one can prove the system conforms
to a given rule. Formal methods can also make reliability proofs on complex
software and hardware system so as to discover design faults that can not be
discovered by test and simulation previously. Formal methods can better control
software and hardware products' development and provide a criterion for those
products [1] [2].
∗
This work is jointly supported by National Basic Research Program of China (973)
under Grant No. G1999035802, National Natural Science Foundation of China under
Grant No. 60373054 and National High-Tech Research and Development Program
of China (863) under Grant No. 2002AA141080.
