作者：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 發布，如需轉載請注明來源。本文地址：http://www.bjnorthway.com/1593/