基于seL4的分区隔离方法
2016-11-01 19:47:31 0 举报AI智能生成
基于seL4的分区隔离方法是一种安全操作系统中用于实现内存隔离的技术。该方法通过将系统内存划分为多个独立的区域，每个区域只能被分配给特定的进程或任务使用，从而实现了内存的隔离和保护。同时，在每个区域中还设置了访问控制机制，确保进程之间不会相互干扰或破坏彼此的数据。这种分区隔离方法不仅可以提高系统的安全性和稳定性，还可以有效地防止恶意软件的攻击和窃取用户信息的行为。因此，基于seL4的分区隔离方法在现代操作系统中得到了广泛的应用，并成为了保障计算机信息安全的重要手段之一。
作者其他创作
大纲/内容
背景（为什么要分区）
嵌入式硬件性能大幅提高
不同安全级别的程序集成在同一硬件
导致安全问题，增大成本
解释1：例如恶意进程大量malloc，耗尽内存资源
解释2：例如恶意进程通过管道、共享内存都手段，利用机密程序的bug窃取信息
解释3：对各种安全级的程序进行整合测试，成本比单独测试高安全级程序要复杂得多，成本提高
扩展解释：一个简单的方案就是使用虚拟化，对OS进行隔离
在嵌入式环境下，虚拟机太“大”了，虽然安全性高，但不够灵活和高效
因此，使用“分区”是一个好的方案，那什么是分区呢？见下一章：
分区的研究现状
ARINC 653标准
提出对进程进行分区，由操作系统对分区进行隔离
介绍ARINC 653的几个方面
分区调度
内存隔离
分区间通信
标准接口APEX
调度方面的研究现状
Linux 653基于Linux的CFS实现分区调度
缺陷：过于死板，构建系统时如果需要修改分区时间片，需要重新编译内核
L4/IMA 基于L4的调度队列实现分区调度
同上
内存隔离的研究现状
现在进程基本都采样基于MMU的地址空间隔离
因此分区内存自然是隔离的
只需要OS内存管理控制内存使用即可
没有技术瓶颈
分区间通信研究现状
以Linux 653为代表，基于Linux内核的消息队列实现分区间通信控制
缺陷1：内核需要提供消息缓冲区，恶意进程能导致缓冲区溢出
缺陷2：不能阻止恶意进程绕过APEX直接使用Linux的各种IPC，例如管道等
以L4/IMA为代表
标准接口APEX的提供与控制
现有的分区系统都采用库函数形式提供标准接口
库函数进一步使用系统调用获取内核服务
缺陷：如果恶意进程直接调用系统调用（通过陷入指令）
例如，Linux653中，如果一个进程直接调用exit()，内核其实是会直接执行这个系统调用
seL4的出现
第一个验证的内核
形式化角度保证内核没有BUG
资源管理交给用户态来做
为我们实现基于用户态的分区调度、内存隔离提供了条件
强大的权限控制机制
保障恶意进程不能直接调用系统调用
基于endpoint的IPC
允许我们在用户态实现分区间通信
配合上一条，杜绝进程绕过APEX直接通过内核进行IPC的可能性
局限性：不能修改内核代码
改内核代码会导致验证失效
研究目标
在不修改seL4内核代码的前提下，通过用户态进程或者库，在seL4中实现ARINC 653标准的分区隔离，并通过原型系统进行验证和测试。
研究内容
1. 设计并实现一种用户态的分区调度器
解决调度策略写死到内核的不灵活性问题
2. 设计并实现一种基于用户空间的分区间通信息机制
解决占用内核缓冲区带来的隐患
解决用户进程绕过标准接口直接通过内核进行IPC的问题
3. 解决用户进程绕过标准接口直接调用内核系统调用的问题
方案与关键点实现
总体方案
1. 初始化线程掌握所有权能
2. 用户态分区调度器执行调度
3. 初始化线程提供APEX接口（例如getpid等）
4. 通信服务器提供通信相关的APEX接口（收、发消息）
关键点1：用户态调度
1. 分区调度器作为一个线程，周期性启动进行调度
分区时间片等信息保存在用户态中
2. 分区时间片到时，进行分区切换
切换方法是利用seL4内核接口，挂起上一个分区的线程，恢复下一个分区线程
难点：如何不破坏用户线程的IPC状态？
方法：调度器优先级<初始化线程优先级
从而保证分区切换时，其他线程的IPC一定已经结束
关键点2：基于用户态的分区间通信
1. 通信服务器作为一个线程，通过RPC方式提供服务
2. 在用户态分配消息缓冲区
难点：通信服务器找谁要内存？答：找初始化线程
为提高效率，采用加倍增长的算法预分配内存，减少开销
关键点3：防止用户进程直接调用内核系统调用
1. 所有权能由初始化线程掌握
用户进程没有权能就不能调用系统调用（这一点由seL4保证）
2. 所有的APEX接口（例如getpid）都在初始化线程/通信服务器中实现，用户进程通过RPC获取这一服务
3. 用户进程只能跟初始化线程/通信服务器通信
分区间通信是由通信服务器进行消息转发实现的
测试与评估
测试环境
主机环境环境：Linux Ubuntu 14.04 32bit
仿真环境：QEMU仿真的x86 intel core2 2.4GHz的CPU 512MB内存
功能测试
1. 正常功能测试
benchmark采用ARINC 653标准的benchmark
2. 恶意程序测试
1编写用户程序直接调用seL4内核系统调用接口
性能测试
1. 调度器性能
进程切换开销：约40us
分区切换开销：约100~200us
结论：进程切换开销相对来说不大，分区切换开销略大
2. APEX接口调用开销
1. getpid调用延时
2. set_partition_status调用延时
.....等等
结论
总结我们解决三个方面的分区关键技术的情况
性能测试发现，开销可以接受
0 条评论
下一页
