作者:wzt
原文链接:https://mp.weixin.qq.com/s/_2jDAIZjmFPtC_eq1aABhw

1 简介

Sel4是l4微内核家族中的一员,se代表security的意思,它采用了形式化验证的手段确保了源码的安全性,大概是对形式化验证有很足的信心,sel4没有使用任何漏洞利用缓解措施,仅仅使用了intel cpu的smep/smap功能。

2 安全功能

2.1 kaslr

现在的内核地址随机化不止包含内核代码段地址随机化, 还包括了内核自身页表、内核的堆等等。

2.1.1 内核代码段地址随机化

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

​     );

}

后续的加载地址直接设置为了固定地址。

2.1.2 内核页表地址随机化

在商用os系统里了,windows nt内核首先将内核页表做了地址随机化处理,linux和xnu都没有实现。

Sel4内核也同样没有实现。

2.2 aslr

进程栈地址未使用地址随机化

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函数对任何代码段地址都未使用地址随机化算法。

2.3 heap

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完整性验证功能。

\- 未提供地址混淆功能。

2.4 系统调用过滤

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:

}

2.5 NULL Page Protection

Sel4在提供的mmap接口中,没有禁止映射内存0的限制,而这个功能在linux和NT内核中都做了限制。

libsel4muslcsys/src/sys_morecore.c

mmap的主体函数中没有对addr地址做限制。

2.6 mmap/mprotect w^x保护

同上, mmap/mprtect接口中没有对可写、可执行权限做限制, linux、xnu、nt都实现了此保护功能。

2.7 kernel/module rwx保护

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

2.8 cpu SMEP/SMAP

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);

​    }

}

}

2.9 intel spectre v1漏洞缓解

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指令。

2.10 intel spectre v2漏洞缓解

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的指令段转换。

2.11 shadow stack

未提供shadow stack保护。

2.12 CFI

未提供CFI保护.

2.13 PAC

未提供PAC保护。

2.14 Code sign

未提供代码签名保护。

3 关于形式化验证

由于c语言的语法复杂和灵活,形式化验证手段要将c语言转化为一个能够被数学逻辑验证的语言。这个语言要依赖一些威胁模型,这些模型源自于对内核行为的一些预测。如果威胁模型在构建的时候就忽略了一些条件和情况外,那么这个形式化验证就不够全面。这个威胁模型完全取决于人的经验,如果人的经验不足,就会漏掉很多模型。举个例子,给stack smashing做威胁模型,如果程序员只知道overflow会覆盖return address才叫漏洞的话,那么就会漏掉函数指针覆盖这种情况,它同样会改变程序的执行流程。笔者始终认为一个好的商用微内核系统,除了使用形式化验证外,基本的漏洞利用缓解措施还是有必要加上的。


Paper 本文由 Seebug Paper 发布,如需转载请注明来源。本文地址:https://paper.seebug.org/1593/