Paper Info
Title
A formal description of SECIMOS operating system
Abstract
The application of formal methods in secure operating system experiences a procedure of development and maturity with the eminence 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 secure operating system should introduce formal methods in the process development and evaluation. Security in Mind Operating System (SECIMOS) 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.
Year
DOI
Venue
2005
10.1007/11560326_22
MMM-ACNS
Keywords
Field
DocType
formal tool,formal method,common criteria,customizable secure operating system,defenses trusted computer system,secure operating system,security policy,process development,secimos operating system,formal description language,high security level,operating system,specification language,trusted computing
HOL,Specification language,Formal language,Computer security,Computer science,Formal specification,Common Criteria,Trusted Computer System Evaluation Criteria,Security policy,Formal methods,Operating system
Conference
Volume
ISSN
ISBN
3685
0302-9743
3-540-29113-X
Citations 
PageRank 
References 
1
0.39
7
Authors
5
Name
Order
Citations
PageRank
Zhouyi Zhou1171.38
Liang Bin223954.58
Li Jiang310.39
Wenchang Shi419824.17
Yeping He57714.64