摘要：形式化、半形式化规范的理论和实践是高安全等级操作系统设计所必须解决的问题,但我国高安全等级操作系统形式化设计方面十分薄弱,没有实践过程和相关理论的技术积累.本文借助Lapadula给出的规则集建模方法,基于Linux系统调用给出了一个实际开发的安全文件系统NeoFs的顶层功能规范的方法和过程.

关键词：安全操作系统设计 安全文件系统 半形式化 功能规范 

单位：上海中标软件有限公司; 上海200233; 解放军信息工程大学电子技术学院; 河南郑州450004