1 简介
Sel4是l4微内核家族中的一员，se代表security的意思，它采用了形式化验证的手段确保了源码的安全性，大概是对形式化验证有很足的信心，sel4没有使用任何漏洞利用缓解措施，仅仅使用了intel cpu的smep/smap功能。
现在的内核地址随机化不止包含内核代码段地址随机化， 还包括了内核自身页表、内核的堆等等。
Sel4内核并没有支持内核地址随机化， 以下x86架构为例：
src/arch/x86/64/head.S
追踪sel4内核的启动代码: _start->_start64->_entry_64->boot_sys->try_boot_sys:
static BOOT_CODE bool_t try_boot_sys(void)
{
boot_state.ki_p_reg.start = KERNEL_ELF_PADDR_BASE;
boot_state.ki_p_reg.end = kpptr_to_paddr(ki_end);
printf("Kernel loaded to: start=0x%lx end=0x%lx size=0x%lx entry=0x%lx\n",
boot_state.ki_p_reg.start,
boot_state.ki_p_reg.end,
boot_state.ki_p_reg.end - boot_state.ki_p_reg.start,
(paddr_t)_start
);
}
后续的加载地址直接设置为了固定地址。
在商用os系统里了，windows nt内核首先将内核页表做了地址随机化处理，linux和xnu都没有实现。
Sel4内核也同样没有实现。
进程栈地址未使用地址随机化
seL4_libs/libsel4utils/src
int sel4utils_spawn_process(sel4utils_process_t *process, vka_t *vka, vspace_t *vspace, int argc,
char *argv[], int resume)
{
uintptr_t initial_stack_pointer = (uintptr_t)process->thread.stack_top - sizeof(seL4_Word);
process->thread.initial_stack_pointer = (void *) initial_stack_pointer;
}
thread.stack_top地址通过sel4utils_reserve_range_aligned函数分配，此函数未使用任何随机化算法。
代码段未使用地址随机化
seL4_libs/libsel4utils/src
load_segment函数对任何代码段地址都未使用地址随机化算法。
seL4_libs/libsel4allocman/src/allocman.c
- 未提供redzone，不可检测overflow。
- 未提供poison，不可检测UAF。
- 不可检测double free。
- 未提供双向链表的安全删除操作。
- 未提供初始化chunk随机化功能。
- 未提供cookie完整性验证功能。
- 未提供地址混淆功能。
seL4_libs/libsel4utils/src/slab.c
- 未提供redzone，不可检测overflow。
- 未提供poison，不可检测UAF。
- 不可检测double free。
- 未提供双向链表的安全删除操作。
- 未提供初始化chunk随机化功能。
- 未提供cookie完整性验证功能。
- 未提供地址混淆功能。
Sel4系统没有提供系统调用审计和过滤的功能，因为sel4目前只支持几下几个系统调用：
seL4/src/api/syscall.c：
exception_t handleSyscall(syscall_t syscall)
{
switch (syscall)
{
case SysSend:
case SysNBSend:
case SysCall:
case SysRecv:
case SysReply:
case SysReplyRecv:
case SysWait:
case SysNBWait:
case SysReplyRecv: {
case SysNBSendRecv: {
case SysNBSendWait:
case SysNBRecv:
case SysYield:
}
Sel4在提供的mmap接口中，没有禁止映射内存0的限制，而这个功能在linux和NT内核中都做了限制。
libsel4muslcsys/src/sys_morecore.c
mmap的主体函数中没有对addr地址做限制。
同上， mmap/mprtect接口中没有对可写、可执行权限做限制， linux、xnu、nt都实现了此保护功能。
Sel4内核在启动之初调用setup_pml4函数对内核代码段的属性设置为rwx，而在后续直到内核启动完毕，仍没有将w可写属性去掉，将会把内核暴露为一个可写的危险环境。
src/arch/x86/64/head.S
BEGIN_FUNC(setup_pml4)
movl $_boot_pd, %ecx
orl $0x7, %ecx
movl $boot_pdpt, %edi
movl %ecx, (%edi)
movl %ecx, 4080(%edi)
addl $0x1000, %ecx
movl %ecx, 8(%edi)
addl $0x1000, %ecx
movl %ecx, 16(%edi)
addl $0x1000, %ecx
movl %ecx, 24(%edi)
Ret
Sel4内核提供了cpu smep/smap功能：
seL4/src/arch/x86/kernel/boot.c：
BOOT_CODE bool_t init_cpu(
bool_t mask_legacy_irqs
)
{
if (cpuid_007h_ebx_get_smap(ebx_007)) {
if (!config_set(CONFIG_PRINTING) && !config_set(CONFIG_DANGEROUS_CODE_INJECTION)) {
write_cr4(read_cr4() | CR4_SMAP);
}
}
if (cpuid_007h_ebx_get_smep(ebx_007)) {
if (!config_set(CONFIG_DANGEROUS_CODE_INJECTION)) {
write_cr4(read_cr4() | CR4_SMEP);
}
}
}
Sel4未提供intel cpu spectre v1漏洞类型的缓解机制：
src/arch/x86/64/traps.S：
#define MAYBE_SWAPGS swapgs
BEGIN_FUNC(handle_syscall)
LOAD_KERNEL_AS(rsp)
MAYBE_SWAPGS
push %r11
push %rdx # save FaultIP
push %rcx # save RSP
Swap指令后并没有lfence指令做序列化保护，cpu指令预测执行可绕过swapgs指令。
Sel4未提供intel cpu spectre v2漏洞类型的缓解机制：
src/arch/x86/64/head.S
BEGIN_FUNC(_start64)
movabs $_entry_64, %rax
jmp *%rax
END_FUNC(_start64)
缺少return trampline的指令段转换。
未提供shadow stack保护。
未提供CFI保护.
未提供PAC保护。
未提供代码签名保护。
由于c语言的语法复杂和灵活，形式化验证手段要将c语言转化为一个能够被数学逻辑验证的语言。这个语言要依赖一些威胁模型，这些模型源自于对内核行为的一些预测。如果威胁模型在构建的时候就忽略了一些条件和情况外，那么这个形式化验证就不够全面。这个威胁模型完全取决于人的经验，如果人的经验不足，就会漏掉很多模型。举个例子，给stack smashing做威胁模型，如果程序员只知道overflow会覆盖return address才叫漏洞的话，那么就会漏掉函数指针覆盖这种情况，它同样会改变程序的执行流程。笔者始终认为一个好的商用微内核系统，除了使用形式化验证外，基本的漏洞利用缓解措施还是有必要加上的。
