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. © Springer-Verlag Berlin Heidelberg 2005.
Cite
CITATION STYLE
Zhou, Z., Liang, B., Jiang, L., Shi, W., & He, Y. (2005). A formal description of SECIMOS operating system. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 3685 LNCS, pp. 286–297). https://doi.org/10.1007/11560326_22
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
