2. INTEGRITY微内核架构解析
INTEGRITY实时操作系统采用分离内核（Separation Kernel）设计思想，其微内核仅保留最基础、最不可省略的机制：地址空间管理、执行体调度、进程间通信（IPC）和内核对象管理。所有设备驱动、文件系统、网络协议栈乃至安全策略服务，均以用户态任务（Task）或虚拟地址空间（Address Space）的形式运行在内核之外。这种"最小特权内核"结构，使内核攻击面被压缩到极小，也为高等级安全认证（如DO-178C、IEC 61508、Common Criteria EAL6+）提供了可验证的架构基础。
一、微内核基本结构
INTEGRITY微内核在结构上可划分为四个核心子系统：调度器（Scheduler）、地址空间管理器（Address Space Manager）、IPC管理器（IPC Manager）和对象管理器（Object Manager）。内核本身运行在特权模式，但只暴露有限的系统调用接口（约30～50个），用户态组件通过系统调用陷入内核完成受限操作。
内核不包含动态内存分配器，所有内核对象（如Task、Address Space、Semaphore、Queue、Event、Memory Region）在系统构建阶段由配置工具静态分配，运行时不再申请堆内存。这一设计消除了内核态内存碎片和分配失败导致的不可预测行为，使最坏执行时间（WCET）可静态分析。
内核代码通常编译为位置无关、只读的映像，加载后代码段不可写，数据段仅内核自身可访问。用户任务无法通过任何系统调用直接读写内核数据，只能通过句柄（Handle）间接引用内核对象。
二、地址空间隔离机制
INTEGRITY使用MMU（内存管理单元）为每个Address Space建立独立的页表。每个Address Space可包含多个Task，同一Address Space内的Task共享地址映射，不同Address Space之间默认完全隔离。地址空间由内核在创建时分配，其页表基址寄存器（如ARM的TTBR、PowerPC的SDR1）仅在内核切换上下文时更新。
隔离的关键在于：内核维护一张全局的"地址空间—物理页"映射表，任何跨地址空间的内存访问都必须经过内核仲裁。用户任务若访问未映射地址，将触发页错误（Page Fault），内核根据错误地址和当前任务所属Address Space判定为非法访问，并终止该任务或上报错误处理任务。
除MMU隔离外，INTEGRITY还支持MPU（内存保护单元）模式，适用于无MMU的微控制器。MPU模式下，内核为每个Address Space配置一组区域描述符，限定可访问的地址范围和权限（读/写/执行）。两种模式在API层面保持一致，便于跨平台移植。
示例：假设系统中有两个Address Space——AS_FlightControl和AS_Display。AS_FlightControl映射物理地址0x40000000～0x4000FFFF用于控制寄存器，AS_Display映射0x50000000～0x5001FFFF用于帧缓冲。若AS_Display中的任务试图写入0x40000000，MMU将产生页错误，内核记录错误地址、任务ID和时间戳，并调用预注册的错误处理任务，而不会影响AS_FlightControl的正常运行。
三、进程间通信（IPC）模型
INTEGRITY的IPC基于"通道"（Channel）抽象，所有跨Address Space的通信必须通过内核对象进行。内核提供三种基本IPC机制：
- Queue（消息队列）：用于异步、有缓冲的消息传递。发送方将消息写入队列，接收方按FIFO顺序读取。队列深度和消息大小在配置时固定。
- Semaphore（信号量）：用于同步和互斥。支持计数信号量和二值信号量，可用于任务间的事件通知。
- Event（事件）：用于一对多的通知机制。一个任务可等待多个事件，任一事件触发即可唤醒。
IPC的核心约束是：发送方和接收方必须显式持有对方对象的句柄。句柄由内核在连接建立时分配，不能伪造。内核在每次IPC操作时检查句柄的有效性和访问权限，确保只有被授权的任务才能通信。
对于需要高吞吐量的场景，INTEGRITY还支持"共享内存"（Shared Memory）机制。两个Address Space可协商一块公共物理内存，各自映射到自己的地址空间。共享内存的创建和映射由内核完成，但数据读写不经过内核，从而降低IPC开销。共享内存的同步仍需配合Semaphore或Event使用。
四、内核对象管理
INTEGRITY内核对象包括：Task、Address Space、Queue、Semaphore、Event、Memory Region、Interrupt、Device等。每个对象在内核中有一个固定大小的控制块（Control Block），包含对象类型、状态、所有者、访问权限和资源引用计数。
对象生命周期由内核统一管理：创建时从静态池中分配控制块，销毁时归还。对象句柄是一个整数索引，指向内核对象表。用户任务只能通过句柄操作对象，无法直接访问控制块。内核在每次系统调用时验证句柄的合法性，防止越权访问。
对象权限模型基于"能力"（Capability）思想：每个任务持有若干句柄，每个句柄附带一组权限位（如读、写、发送、接收、等待）。权限在对象创建或连接建立时确定，运行时不可提升。若任务试图执行超出权限的操作，内核返回错误码并记录审计事件。
五、架构验证要点
在工程验证中，微内核架构的隔离性可通过以下方式确认：使用调试器读取MMU页表，验证不同Address Space的映射不重叠；向目标Address Space注入非法地址访问，观察内核是否产生页错误并隔离故障任务；通过IPC压力测试，验证Queue在满/空状态下的阻塞与唤醒行为符合预期；检查内核对象句柄表，确认无越权句柄泄漏。
需要特别注意的是，INTEGRITY的隔离强度依赖于MMU/MPU配置的正确性。若配置工具中误将两个Address Space映射到同一物理页，隔离即被破坏。因此，在集成阶段应使用静态分析工具检查地址映射表，并在目标板上运行隔离测试用例，确认跨空间访问被正确拦截。
实践提示：在配置Address Space时，建议为每个空间保留一段"守卫页"（Guard Page），即不映射任何物理内存的虚拟地址区域。当任务发生栈溢出或指针越界时，访问守卫页会立即触发页错误，便于快速定位故障，而不是静默破坏相邻空间的数据。
综上，INTEGRITY微内核通过静态对象分配、MMU/MPU隔离、句柄化IPC和能力权限模型，构建了一个可验证、可预测、高隔离的实时运行环境。理解这四者之间的协作关系，是后续进行安全配置、任务划分和故障分析的基础。