本文以一个实际的安全操作系统SECIMOS开发实践为基础，对安全操作系统可信进程机制及一些相关问题进行了研究，取得了以下四个方面的研究成果。第一，在对可信进程基本性质进行了深入研究基础上，从可信进程可信性出发给出了一个一般化的可信进程定义，消除了原有定义中存在的片面性，为实现一个较为完善的可信进程机制提供坚实的理论指导。以此定义为指导，在SECIMOS中实现了一个可信进程机制的原型系统，从多个方面保障了可信进程的可信性，提供了一个较为完善的可信进程解决方案。第二，为有效地支持最小特权原则，针对传统特权机制存在的局限性，提出了一种新的特权控制模型——基于状态的特权控制(State-based Privilege Control，SBPC)，并在SECIMOS中实现了一个Linux平台上的SBPC原型系统——受控特权框架(Controlled Privilege Framework，CPF)。SBPC该机制以程序逻辑为中心，引入了特权状态的概念来进行特权控制；构建了特权与特权参数之间的显式关系；完善了特权进程的特权计算机制。通过CPF的实现，系统能进行细粒度的、自动的特权控制，且对应用软件完全透明，恶意入侵的危害性被大大降低，系统能有效地支持最小特权原则。第三，对轻量级形式化方法的核心思想进行了发展，将其应用到安全系统的FSPM规格说明和验证中，提出了一种轻量级的基于Z语言的安全操作系统FSPM规格说明及验证方法——LFSV(Lightweight Formal Specification and Verification)。LFSV使用简洁单一的形式化技术完成了FSPM的规格说明和验证，降低了模型复杂度和形式化建模的难度。使用LFSV方法为SECIMOS系统所实施的访问控制策略提供了精确易懂的FSPM，发现了一些与模型要求不一致的错误实现，特别是在一致性证明过程中发现了最新版的Linux内核特权机制中存在的一个致命错误，保障了SECIMOS系统安全控制的正确实施，提高了基础平台(Linux)的安全性。实践表明LFSV是一种有效的、容易掌握的FSPM规格说明和验证方法。第四，对一种公认的经典的由Sandhu等人提出的以RBAC实施BLP模型的方法进行了研究分析，指出并证明存在的错误，并揭示了其存在的不足，尤其是未能容纳BLP模型所不可缺少的可信主体概念。为此，提出了一种改进的方法——ISandhu方法，修正了原有方法的错误，提供了对可信主体概念的支持，面向实际应用扩展了其实施范围，保证了强制访问控制策略在RBAC中的正确实施，为在大量商业系统中以较小的代价引入强制访问控制提供了理论基础。总而言之，本文的研究成果将有助于研究开发完善的可信进程机制及构建高可信级别的安全操作系统。