操作系统是整个计算机系统的基础,它的可靠性、安全性影响到整个系统的可靠性、安全性。操作系统中最重要的部分是系统内核,因此必须要确保内核的可靠性。在可靠的内核下,同时也要保证内核向外提供的操作的可靠性。内核调用是内核为用户级进程提供内核特权操作的接口,因此必须确保这些接口函数的正确性和安全性。目前公认的可以保证操作系统的安全性、可靠性的方法是采用形式化对操作系统从设计到实现都进行验证。形式化方法以严格的数学逻辑为基础,将系统抽象成以逻辑语言表示的形式化系统,通过逻辑推理的方式来验证系统满足某些安全特性。微内核架构对于缩减内核代码量、提高系统的可扩展性具有很强的优势。为了向微内核架构下的用户级服务器、用户级设备驱动提供内核的特权操作,采用形式化方法设计了内核级的系统任务进程,并且对其函数正确性进行验证。本文的主要工作如下：1.为VTOS设计和实现了一个向用户级服务器和驱动提供内核特权操作的内核进程。采用独立的内核进程而不是通过中断处理的方式,能够对权限进行更好的隔离,同时也能够为系统在多核、分布式环境下,提供良好的可扩展性。实验证明采用独立进程的方式能够提供系统的可扩展性,且性能代价较小。2.为了形式的描述系统任务的行为,使用基于自动机理论的操作系统自动机模型描述系统任务的整体结构：系统任务的数据对象、影响其行为的内核事件以及对每个事件的处理函数。并且为系统任务建立了状态自动机模型,定义了系统任务的一些安全属性。3.使用已建立的Isabelle/HOL处理器模型,采用霍尔逻辑,对系统任务自动机模型中的转换函数设置前置和后置条件,并结合相应的定理,证明转换函数函数语义的正确性。