长亭百川云 - 文章详情

sel4微内核安全功能解读

kernsec

109

2024-07-13

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才叫漏洞的话,那么就会漏掉函数指针覆盖这种情况,它同样会改变程序的执行流程。笔者始终认为一个好的商用微内核系统,除了使用形式化验证外,基本的漏洞利用缓解措施还是有必要加上的。

相关推荐
关注或联系我们
添加百川云公众号,移动管理云安全产品
咨询热线:
4000-327-707
百川公众号
百川公众号
百川云客服
百川云客服

Copyright ©2024 北京长亭科技有限公司
icon
京ICP备 2024055124号-2