• seL4支持平台seL4所在的git如下: ...不过我们编译和运行seL4一般不...https://github.com/seL4/sel4test.gitseL4提供了各种平台的配置文件,也提供了用于测试seL4的app。seL4指定了可以运行的平台,按照下面的匹配来编

    seL4支持平台

    seL4所在的git如下:
    https://github.com/seL4/seL4.git

    不过我们编译和运行seL4一般不只是用这个git,而是借助seL4test(seL4的测试框架):
    https://github.com/seL4/sel4test.git

    seL4提供了各种平台上的配置文件,也提供了用于测试seL4的app。


    seL4指定了可以运行的平台,按照下面的匹配来编译它(当然还有其他的匹配)。

    ARCH PLAT ARMV CPU
    arm imx31 armv6 arm1136jf-s
    arm omap3 armv7-a cortex-a8
    arm am335x armv7-a cortex-a8
    ia32 pc99

    另外在seL4官方文档中,指出下列平台也可以运行seL4:

    • Intel platforms

      1. a PC99-style Intel Architecture 32-bit x86 (ia32)
      2. There is also experimental support for the 64-bit Intel x86_64 architecture.
    • ARM platforms

      1. The Arndale dual core A15 ARM development board
      2. The Beagleboard, Omap 3530
      3. The Inforce IFC6410 development board, running a Qualcomm Krait processor that is like an A15.
      4. The KZM-ARM11-01. The kernel for this board is the one that is formally verified.
      5. The Odroid-X Exynos4412 board
      6. The Odroid-XU Exynos 5 board
      7. The Sabre Lite i.mx6 board.
      8. The Beaglebone Black is a community-supported port.

    选择OdroidXU3编译seL4

    根据seL4官方文档所说明的支持平台,并参照seL4test工程中的配置文件,我们选择OdroidXU3开发板来运行seL4。下面就是OdroidXU3:
    OdroidXU3

    这个平台采用Samsung Exynos5422 Cortex™-A15 2.0Ghz quad core and Cortex™-A7 quad core CPUs。而exynos5422在seL4的支持序列当中。同时这个板子支持的操作系统如下:Ubuntu 14.04 + OpenGL ES + OpenCL on Kernel LTS 3.10和Android 4.4.2 on Kernel LTS 3.10。因此是一款能满足时下开发的较新的开发板。
    关于它的相信信息,可以到官网上去查看:
    Hardkernel Odroid


    通过repo获得seL4test工程。工程根目录下有一个configs文件夹,里面就是根据具体平台所设置的配置文件,我们根据我们的板子,选择 odroidxu3_release_xml_defconfig。把它拷贝到seL4test工程根目录下。
    在工程根目录下执行命令: $ make menuconfig
    出现如下界面:
    这里写图片描述

    进入“Load an Alternate Configuration File”,输入刚才拷贝的配置文件的名字:
    这里写图片描述

    ok后,回到上面的界面,进入“Save an Alternate Configuration File”,直接ok。最后Exit退出menuconfig。

    然后运行命令: $ make

    这样你就会在images目录下发现新生成的seL4的elf格式的镜像文件:
    sel4test-driver-image-arm-exynos5

    编译成功!


    制作OdroidXU3的SD卡启动盘

    OdroidXU3默认是eMMC启动,也就是说厂商在eMMC中烧写了u-boot和ubuntu的镜像,我们想通过SD卡启动,所以需要做:

    1. 将OdroidXU3的启动方式改为SD卡启动
    2. 制作SD卡启动盘

    对于1,看下面的图:
    这里写图片描述

    板子上有如图所示的开关,左数第一个开关就是控制启动方式:

    开关状态 启动方式
    ON eMMC
    OFF MICROSD

    下面制作SD卡启动盘:

    • 根据OdroidXU3提供的分区表烧写u-boot
    • 对SD卡分区并拷贝seL4镜像

    下面是OdroidXU3的eMMC卡或microSD卡的分区表:
    这里写图片描述

    如果我们不按照平台指定的SD卡的分区表来烧写u-boot,是不能正确烧写并启动u-boot的。

    OdroidXU3官方也提供了如何编译u-boot的手册和烧写u-boot的shell脚本:
    xu3 building u-boot

    注意:
    首先确认目录 u-boot/sd_fuse/hardkernel/下是否存在 bl1.bin.HardKernel、bl2.bin.HardKernel、tzsw.bin.hardkernel,和配置文件sd_fusing.sh。 将自带的u-boot.bin.hardkernel删掉。
    安装手册会在根目录编译生成u-boot/u-boot.bin,需要将它拷贝到u-boot/sd_fuse/hardkernel目录下,并重命名为u-boot.bin.hardkernel。

    按照手册所说的利用sd_fusing.sh脚本将u-boot烧写到SD卡中。

    我们使用minicom在xubuntu下进行串口调试(minicom配置信息采用默认即可),查看板子启动信息,如果u-boot烧写成功,启动后会出现如下界面:
    这里写图片描述

    进入u-boot命令模式。


    接下来我们先要将上面生成的seL内核镜像放到SD卡中,我们不是用烧写u-boot时的脚本将内核也烧进SD卡中,而是要将SD卡进行分区,然后直接拷贝。

    将SD卡分区需要注意以下两点:
    1. 第一分区位置要从地址3072开始。原因:MBR的需要占用第一个512byte,fwbl1区需要占用1-30 共15KB,bl2区需要占用31-62 共 16KB,u-boot镜像需要占用63-718 共238KB,tzsw.bin需要占用719-1230,共256KB,u-boot的运行环境需要占用1231-1263 共16KB,u-boot的环境变量需要占用1263-3071。而第一分区存储的是SEL4的内核镜像,为保证u-boot运行,以及不干扰第一分区的读写操作,所以地址设定为3072。
    2. 我们将SD卡分为两区(非必须),文件系统类型分别为FAT16(vfat)、LINUX 文件系统(ext4),第一分区应留出足够的空间存储SEL4的内核镜像,至少为3MB以上。

    分好区后,将SD卡插入电脑就可以挂载识别了,我们将seL4的内核镜像sel4test-driver-image-arm-exynos5拷贝到SD卡的第一个分区中(为了下面启动seL4内核的方便,我们将内核重命名为sel4)。

    大功告成!现在试一下是否可以在OdroidXU3上点亮seL4。


    点亮seL4

    在u-boot命令模式下,依次输入如下命令:

    这里写图片描述

    这里显示的是SD卡第一个分区中存放的文件,我们的内核镜像是sel4。

    然后将内核加载到内存指定位置:
    这里写图片描述

    其中0x48000000就是内核在内存中的指定位置。

    最后启动:
    这里写图片描述

    这里写图片描述

    由于我们使用的是seL4test这个官方提供的框架,编译生成的seL4内核镜像包含了一个叫seL4test-driver的app,所以运行所出的信息实际上是这个app在运行,最后会出现“All is well in the universe”。

    至此我们已经在OdroidXU3上成功点亮seL4。

    展开全文
  • seL4 FAQ

    2014-08-24 11:12:41
    seL4是L4微内核家族中最先进的成员,值得注意的是其全面的形式验证,这使它有别于其他任何操作系统。seL4达成这个目标同时不会影响性能。 什么是微内核? 微内核是操作系统(OS)的最小核心。它呈现的是今天通常被...

    本文译至:http://sel4.systems/FAQ/ 译者:萝卜


    什么是seL4?

    seL4是L4微内核家族中最先进的成员,值得注意的是其全面的形式验证,这使它有别于其他任何操作系统。seL4达成这个目标同时不会影响性能。

    什么是微内核?

    微内核是操作系统(OS)的最小核心。它呈现的是今天通常被认为的操作系统的一个很小的子集。微内核的定义由利特克给出[SOSP'95]:一个概念仅在以下条件下是可以容忍放在微内核的,那就是当将它移到内核外时,例如,允许竞争的实现,将防止系统所需功能的实现。

    因此微内核不提供硬件上的高层次的抽象(文件,进程,套接字等),如大多数现代操作系统Linux或Windows所做的那样。相反,它提供了最少的机制用于控制物理地址空间访问,中断和处理器时间。使用这些机制的任何更高级别的结构是建立在微内核之上。这样的更高级别的服务必然封装策略。策略自由是一个精心设计的微内核的一个重要特征。

    在L4微内核使用的模式中(seL4也不例外),一旦内核启动后,一个初始的用户级的任务(根任务),被赋予完全的权限来处理所有的资源(这通常包括物理内存,x86的IO端口和中断)。由根任务来设置其他任务,并给其他任务授予权限来构建一个完整的系统。在seL4中,像其他第三代微内核一样,这样的访问权限是按能力授予的(不可伪造的令牌代表特权),并是完全可委托的。

    什么是L4微内核的家族?

    L4家族是非常小的,高性能的微内核。由约亨·利特克在90年代初研制出的第一个L4微内核演化而业。参见L4微内核的家庭的维基百科入口及 L4HQ了解更多详情。

    和其他微内核相比seL4的性能如何?

    尽我们所知,seL4在通常的乒乓指标方面:跨地址空间的消息传递(IPC)的操作成本,在所支持的处理器上是世界上最快的微内核,欲了解更多信息,请查看关于L4HQ的性能页面。
    但是,请注意,在L4HQ记录的 IPC时间是微优化的结果,这是尚未包括在公开的版本中。发布的内核大约慢了10-20%速度(这仍然使得它快于其他任何我们已经知道的性能数据)。我们正计划一旦他们成熟,就推动这些优化。

    seL4运行在在什么硬件上?

    它支持哪些处理器架构?

    现在seL4运行在ARMv6(ARM11),ARMv7(Cortex A8,A9,A15)和x86核上。支持的ARM平台包括飞思卡尔的i.MX31,OMAP3的BeagleBoard,Exynos Arndale 5250, Odroid-X, Odroid-XU, Inforce IFC6410 和 Freescale i.MX6 Sabre Lite。也支持所有现代的x86机器。
    请告诉我们,如果你有资金支持进一步的架构移植。

    seL4支持什么设备?

    seL4,就像任何真正的微内核一样,在用户模式下执行所有的设备驱动程序,因此设备支持不是内核的问题。唯一的例外是一个时钟驱动程序,seL4需要它执行时间片抢占,还有seL4处理的中断控制器访问。当编译内核时使能了调试的话,内核还包含了一个串口驱动程序。

    除此之外,设备支持是用户的问题。seL4提供了用户模式设备驱动程序的机制,尤其是映射设备内存到驱动和将IRQ做为(异步)消息传递的能力。

    DMA怎么样?

    ARM平台上的seL4的形式化验证假设MMU完全控制内存,这意味着证明假设DMA是关闭的。DMA设备理论上可以覆盖机器上的任何内核,包括内核数据和代码。
    你仍然可以安全地使用DMA设备,但你必须单独确保它们动作良好,也就是说,他们不覆盖内核代码或数据结构,只写到按照系统策略分配给它们的帧上。在实践中,这意味着,驱动程序和DMA硬件设备必须是可靠的。
    未经验证的seL4 x86版本在实验分支上支持VT-d扩展。VT-d扩展允许内核限制DMA,从而使DMA设备能与不受信任的用户级驱动程序交互。目前,我们正在为具备SystemMMU 的A15 ARM板提供类似的验证支持。

    我可以在seL4上运行Linux吗?

    是的,seL4可以在虚拟机上运行Linux。目前这是仅支持x86处理器,同时seL4要求机器支持英特尔 EPT VT-X。另外目前的VMM需要支持MSI delivery 的HPET。我们正在研究基于ARM处理器上的Linux的虚拟化扩展支持(目前是A15 / A7核心),发布应该不会太久。

    为了支持虚拟机,seL4本身作为一个虚拟机管理程序运行(x86 Ring-0 根模式或ARM hyp模式)和转发虚拟化事件到虚拟机监视器(VMM),VMM执行必要的仿真。VMM运行在脱特权模式(x86 Ring-3 根模式或ARM supv模式)。

    seL4支持多核吗?

    在x86上,seL4可以配置为支持多个CPU。目前多核的支持是通过一个多核配置实现,每个启动CPU被分配一部分可用内存。然后,内核可以通过受限的共享内存和内核支持的IPI通信。这个配置目前是高度实验性的。

    我可以在一个没有MMU的微控制器上运行seL4吗?

    在没有一个完整的存储器管理单元(MMU)上使用seL4没有什么意义,因为它的资源管理基本上是基于虚拟内存的。对于只有一个内存保护单元(MPU)或完全没有内存保护的低端处理器可言,你应该看看NICTA的eChronos实时操作系统(RTOS),这是专为这样的处理器,也经过形式化验证。

    seL4是为什么应用程序服务的?

    seL4是一个通用的微内核,所以答案是所有的。主要目标是有安全性或可靠性要求的嵌入式系统,但是这不是唯一的。采用像seL4的微内核就能够提供虚拟内存保护平台,并应用于需要在软件的不同部分之间隔离的应用领域。直接的应用领域是在金融,医疗,汽车,航空电子设备和国防部门。

    什么是形式验证?

    形式软件验证是用数学证明来说明一款软件满足特定属性。传统上,形式验证已被广泛用于说明设计或一个软件的规范都有一定的属性,或者一个设计正确地实现了一个规范。在最近几年,已经可能直接应用形式验证到实现该软件的代码上,并表明该代码具有特定的性质。
    形式验证有两个方式:完全自动化的方法,如有限的系统和属性的模型检验工作,以及交互的数学证明,需要手动操作。
    seL4验证使用了Isabelle/HOL定理证明的形式数学证明。该定理证明是交互的,但提供的自动化程度较高。它也提供了高度的保证来确保所产生的证明是正确的。

    seL4的形式验证意味着什么?

    seL4的独特之处是通过形式验证来实现前所未有程度的保证。具体来说,seL4的ARM版本是第一个(也是目前唯一)带有一个完整的代码级的功能正确性证明的通用操作系统内核,这意味着一个数学证明的实现(用编写C语言)支持其规格。简言之,实现被证明是无缺陷的(见下文)。这也意味着一些其他属性,如避免缓冲区溢出,空指针异常,释放后使用等等。
    更进一步,有在硬件上执行的二进制代码是C代码的正确转换的相关证明。这意味着,编译器不必被信任,并且扩展了二进制的功能正确性属性。
    此外,也有证明来证实seL4的规格,如果使用得当,会强制完整性和保密性,核心安全属性。结合上面提到的证明,不仅在内核模型上(规范),也在执行的二进制的硬件上,这些属性都被保证强制实施。因此,seL4是世界上第一个(也是目前唯一)在一个极强的意义上被证明是安全的操作系统。
    最后,seL4是第一个(也是目前唯一),保护模式的操作系统内核与健全完善的时间性分析。这意味着其有对中断延迟(以及任何其他的内核操作的延迟)的可证明的上限。因此,它是有内存保护的内核中唯一的可以给你硬实时保证的。

    seL4是否具有了零错误?

    功能正确性的证明指出,如果证明假设得到满足,seL4内核的实现它的规格相比就没有偏差。安全证明指出,如果内核是根据证据假设配置的,并进一步满足硬件的假设,本规范(和它的seL4内核实现)强制执行了一些强大的安全属性:完整性,保密性和可用性。
    仍然有可能存在本规格中未意料到的功能,同时一种或多个的假设可能是不适用的。安全属性可能足够满足你的系统的需求,但也可能并非如此。例如,保密证明没有关于不存在的隐藏定时通道的保证。
    因此,问题的答案取决于你对错误的理解。在形式软件验证(代码实现规范)的理解中,答案是肯定的。在一般的软件用户的理解中,答案是有可能,因为还有可能是硬件错误或未得到满足的证明假设。对于高保障系统来说,这不是一个问题,因为硬件的分析和证明的假设比分析具备相同的硬件,和测试假设的大型软件系统容易的多。

    seL4证明是安全吗?

    这取决于你所说安全的意思。在传统的操作系统的安全性的解释,答案是肯定的。特别是,seL4已被证明强制执行特定的安全性能,即在一定条件下的完整性和保密性。这些证明都是关于seL4的程序用于构建安全系统的非常有力的证据。
    一些证据的假设可能有限制条件,例如DMA的使用被排除在外,或仅允许由正式由用户进行验证的受信任驱动程序。虽然这些限制对高保障系统是常见的,我们正在努力地以减少它们,例如通过在x86上使用IOMMU或在ARM上使用System MMU。

    如果我运行了seL4,我的系统就是安全吗?

    这并不是自动保证的,不会这样。安全是一个跨越整个系统,包括与人交互那一部分的问题。OS内核,无论验证与否,并不会自动使系统安全。事实上,任何系统,无论多么安全的,都可能在不安全的方式下使用。
    但是,如果被正确地使用,seL4通过具体的安全理论的支持,给系统架构师和用户提供了强大的机制来实现安全策略。

    什么是证明假设?

    简明的版本是:我们假设在内核的汇编代码是正确的,硬件表现是正常的,内核的硬件管理(TLB和高速缓存)是正确的,启动代码是正确的。硬件模型假设DMA将被关闭或者被信任。安全证明额外给出了一个系统配置的条件列表。
    为了更深入的说明,请参见证明和假设页面。

    我该如何充分利用了seL4的形式证明?

    seL4证明仅仅是在构建安全的系统的第一步。它们提供应用程序和系统开发人员需要的工具来提供证据证明他们的系统是安全的。

    例如,可以使用功能的正确性证明来表明与内核的应用程序接口是正确的。我们可以使用完整属性来证明别人无法干扰私有数据,以及保密的证据来证明其他人将无法访问私有数据。可以将所有的整个(one-machine)系统绑定到一个证明中,而不需要验证整个系统的代码。

    有之前未被验证的操作系统的内核吗?

    操作系统验证至少可以追溯到40年前的20世纪70年代中期,所以关于操作系统内核的验证有大量的前期工作。还可以看一个关于2008年来的OS验证全面性概述的论文以及2014年来的seL4概述论文的相关工作部分。

    seL4的新的和令人兴奋的事情是,a)强大的属性,如功能正确性,完整性,保密性,b)具有直接针对代码的正式验证属性 - 最开始是C,现在可以针对二进制。此外,seL4证明是机器检查,不只是基于笔和纸。
    之前的验证要么没有完成其证明,或只针对更浅的属性,如没有未定义执行,或者它们验证代码的手动构造模型而不是代码本身。
    先前的验证中有一部分是令人印象深刻的成就,它们奠定了基础,没有这些基础,seL4证明就不会被实现。只是在最近五到十年,代码验证和定理证明技术进步到足以使大量的代码级证明是可行的。

    我可以用seL4做什么?

    你可以将seL4用于研究,教育和商业。详情参见标准开放源代码规定的许可证附带的代码。不同的许可证适用于代码的不同部分,但这些条件都是为了方便代码的采用。

    许可证条件是什么?

    seL4内核是在GPL2许可证下发布。用户空间工具和库大多是在BSD。请参阅许可证页面了解更多详情。

    我该如何给seL4做贡献?

    请参阅如何贡献。简单地说,seL4是在拥有代码的合作伙伴之间的复杂协议下发布的。发布的条件是,我们跟踪的所有贡献,并从所有参与者那获取一个签名的协议许可。

    我怎样才能构建seL4系统?

    与Linux操作系统相比,在seL4系统上构建一个系统要求多的多。将你的系统分解为模块,你需要找出每个模块需要访问哪些硬件资源,你需要为你的平台构建设备驱动程序(在libplatsupport下有少量为支持的平台提供的驱动),你必须把它集成成某物来运行。
    为了做到这一点,有两种推荐的方式。

    • CAmKES是基于微内核的嵌入式系统的组件架构。它提供了一种语言用于描述组件的资源的分配和组件的地址空间的分配。
    • 建立在libsel4utils上,它提供了如进程之类的有用的抽象,但一般级别比较低。
    为了构建指令,以及如何开始,请参阅下载页面。此外,新南威尔士大学的先进操作系统课程有一个扩展项目组件来在seL4之上创建一个OS。如果你有机会得到Sabre Lite开发板,你应该能够自己进行项目开发工作来做为熟悉seL4的一种方式。

    我在哪里可以了解更多信息?

    NICTA的了seL4项目和可信赖的系统页面包含更多关于seL4的技术信息,包括链接到所有经过同行评议的出版物。好的出发点是:

    • 从L3到了seL4 - 20年内在微内核我们学到了什么?20年L4微内核的回顾; 
    • 原始的2009论文描述了seL4及其形式化验证;
    • 更长的论文,详细说明了seL4的完整验证的故事,其中包括高层次的安全性证明,二进制校验和时间性分析。它还包含验证成本的分析,以及和传统设计系统的比较。
    展开全文
  • 开源微内核seL4

    2015-07-22 16:11:56
    越大的系统潜在的bug就越多,所以微内核在减少bug方面很有优势,seL4是世界最小的内核之一。 如今,安全越来越成为一个新兴嵌入式设备的关键要素,如智能手机。

    微内核

    越大的系统潜在的bug就越多,所以微内核在减少bug方面很有优势,seL4是世界上最小的内核之一。但是seL4的性能可以与当今性能最好的微内核相比。
    作为微内核,seL4为应用程序提供少量的服务,如创建和管理虚拟内存地址空间的抽象,线程和进程间通信IPC。这么少的服务靠8700行C代码搞定。seL4是高性能的L4微内核家族的新产物,它具有操作系统所必需的服务,如线程,IPC,虚拟内存,中断等。

    形式验证

    除了微内核,seL4另一大特色是完全的形式验证。

    seL4的实现总是严格满足上一抽象层内核行为的规约,它在任何情况下都不会崩溃以及执行不安全的操作,甚至可以精确的推断出seL4 在所有情况下的行为,这是了不起的。
    研究发现常用的攻击方法对seL4无效,如恶意程序经常采用的缓存溢出漏洞。
    使用面向过程语言Haskell实现了一个内核原型,用它来参与形式验证,最后根据它,用C语言重新实现内核,作为最终内核。 顺便提一句,seL4有两只team,kernel team和verification team,而连接这两个team的是 Haskell prototype。

    在用C开发内核的过程中,seL4对使用C进行了如下限制
    1. 栈变量不得取引用,必要时以全局变量代替
    2. 禁止函数指针
    3. 不支持union

    对seL4的formal verification(形式验证)分为两步:abstract specification(抽象规范)和executable specification(可执行规范)之间,executable specification和implementation(实现)之间。有两个广泛的方法来进行formal verification: model checking(全自动)和交互式数学证明(interactive mathematical proof ),后者需要手工操作。seL4验证使用的形式数学证明来自Isabelle/HOL,属于后者。

    具体来说seL4的形式验证步骤
    1. 写出IPC、syscall、调度等所有微内核对象(kernel object)的abstract specification(in Isabelle)
    2. 写出如上对象的executable specification(in Haskell),并证明其正确实现了第一步的abstract specification,利用状态机的原理,abstract specification的每一步状态转换,executable specification都产生唯一对应的状态转换。
    3. 写C实现。通过一个SML写的C-Isabelle转换器,和Haskabelle联合形式证明C代码和第二步的Haskell定义语义一致。

    seL4的实现被证明是bug-free(没有bug)的,比如不会出现缓冲区溢出,空指针异常等。还有一点就是,C代码要转换成能直接在硬件上运行的二进制代码,seL4可以确保这个转换过程不出现错误,可靠。seL4是世界上第一个(到目前也是唯一一个)从很强程度上被证明是安全的OS。
    seL4 is the first (and still only) protected-mode OS kernel with a sound and complete timeliness analysis. Among others this means that it has provable upper bounds on interrupt latencies (as well as latencies of any other kernel operations). It is therefore the only kernel with memory protection that can give you hard real-time guarantees. 从这段英文可以看出,seL4的硬实时性很强。
    实际上OS的verification(验证)早在40年前就开始了,而seL4是振奋人心的,一是它拥有很强的属性(properties):功能正确性(functional correctness),完整性(integrity)和机密性(confidentiality),二是这些属性已经被形式验证到代码级别,先是C,现在又到了二进制。相比于之前人们对于OS的验证,seL4做得更彻底,但正是借助前人的工作,seL4才能如此优秀。


    内核细节

    seL4的API调用分两步:第一,checking,验证参数,然后确定是否授权执行这个调用; 第二,execute,执行调用,永不失败。
    The combined checking phases of all kernel calls are a substantial fraction of the kernel. 看来对内核调用的检查是很重要的部分。

    接下来来了解一下kernel objects

    1. CNodes 用于存放capabilities,给线程权限去调用某个对象上的方法
    2. Thread Control Blocks 表示线程的执行
    3. IPC Endpoints 促进线程间的通信
    4. Virtual Address Space Objects 为一个或多个线程创建虚拟地址空间
    5. Interrupt Objects 让应用程序可以接收和确认来自硬件设备的中断
    6. Untyped Memory 它是seL4内存分配的基石

    我们去了解一个OS,它的内存管理是必不可少的。内存分配模块可以被单独验证。在重新使用一块内存之前,所有对这个内存的引用必须要无效。seL4不动态为内核对象分配内存,内核对象要由应用程序控制的内存区域通过Untyped Memory来创建,这样可以精确控制应用程序使用的物理内存,而且可以做到程序与程序之间物理内存的isolation。
    seL4是一个单内核栈的操作系统,在启动时期,seL4会预先为内核需要的内存如代码区,数据区和栈分配内存。

    seL4实现了一个capability-based的访问控制模型。每一个用户空间的线程有一个相关联的capability space (CSpace),这个空间包含了这个线程处理的capabilities,也就是说它管理着这个线程访问的资源。

    CNode有一些slot,每个slot需要16字节的物理内存,它可以恰恰保存一个capability。同其他对象一样,CNode必须要通过seL4 Untyped Retype()在合适数量的untyped memory上来创建。

    seL4用TCB(thread control block)描述一个线程,每一个TCB对一个CSpace和VSpace(它们可与其他线程共享),一个TCB一般有一个IPC buffer。

    seL4提供了消息传递机制用于线程间的通信。

    seL4采用256个优先级的抢占式轮转调度机制,当一个线程创建或修改了另一个线程,它只能将另一线程的优先级设为比它低或跟它一样,线程优先级用函数seL4 TCB Configure() 和 seL4 TCB SetPriority() 来设置。

    展开全文
  • 另外,若您发现本文分析错误,或seL4版本更新特性变化,您可以发邮件告诉我,以便我能及时更新。考虑到关于信息量较多,在阅读过程中难免出现语义难明的词汇,对于前文出现的所有非公共词汇,后文均会明确其含义,请...

     ab12696@qq.com衷心感谢您的拜读,希望我的分析对您有所帮助;另外,若您发现本文分析错误,或seL4版本更新特性变化,您可以发邮件告诉我,以便我能及时更新。考虑到关于信息量较多,在阅读过程中难免出现语义难明的词汇,对于前文出现的所有非公共词汇,后文均会明确其含义,请耐心阅读。

    seL4综述——可能是一个以权限控制为基础的微内核

    ——————————seL4相关理念——————————

    1. 由于seL4官方文档未区分Thread和Process,因此下文表述均采用线程

    2. 关于权限,seL4描述为能力,明确的抽象出3大基本元素:

    Read、Write、Grant(权限授予,即传递)。

    #define seL4_ReadWrite seL4_CapRights_new(0, 1, 1)

    #define seL4_AllRights seL4_CapRights_new(1, 1, 1)

    #define seL4_CanRead   seL4_CapRights_new(0, 1, 0)

    #define seL4_CanWrite  seL4_CapRights_new(0, 0, 1)

    #define seL4_CanGrant  seL4_CapRights_new(1, 0, 0)

    #define seL4_NoWrite   seL4_CapRights_new(1, 1, 0)

    #define seL4_NoRead    seL4_CapRights_new(1, 0, 1)

    #define seL4_NoRights  seL4_CapRights_new(0, 0, 0)

     

    3. 显式的权限控制

    seL4的权限控制是显式的,seL4的一切操作

    (下文提到的seL4提供的基础服务)

    都要在CSpace存在相关权限的情况下才能执行

     

    4. 权限:Grant

    seL4的权限以CNode为单位可被复制、转移。

    由于权限的可复制即可产生子权限,因此可以形成权限树。

    CSpace即据此组织CNode,形成有向图。

     

    5. 线程的VSpace和CSpace

    线程的创建会建立VSpace和CSpace,VSpace即虚拟地址空间;

    CSpace为Capability Space,

    为seL4内核的Capability全面控制提供基础

    6. 线程的IPC Buffer

    存在于其他线程通讯、与内核通讯需要的线程,

    在创建时即加入IPC Buffer,为后期IPC的基础,

    为设置IPC Buffer的线程不能对外通讯。

     

    7. 内存管理

    seL4仅可能分配出power(2,n)且大于16byte的内存

     

    8. 一般平台无关内存对象大小

    n-bit Untyped对象 power(2,n) bytes(n>=4)

    n-bit CNode对象 16*power(2,n) bytes(n>=2)

    Endpoint对象 16 bytes

    Notification对象 16 bytes

    IRQ Control --

    IRQ Handler --

     

    9. 其他平台相关对象

    TCB对象——一般1KB/512bytes

    页表相关对象

    ASID相关对象

    ——————————seL4词汇解释——————————

     

    1. Capability——权限的复合体,内容丰富

    (可能是seL4最精华的理念,因为seL4的一切据此展开)。

    每个线程不光有地址空间(VSpace),

    还有CapabilitySpace。

     

    线程想要调用系统功能,将会通过调用

    能力空间中的能力来实现系统功能

    (如IPC会调用endpoint capability)

     

    2. CNode(capability node)

    Capability的基础承载者,

    创建时即确定拥有的slot数量(power of 2),

    slot用于保存Capabilities,

    所保存的Capability为更深层的CNode时,即形成有向图。

    也由此,当父CNode的Capability被取消时,

    其子将会递归取消此Capability。

     

    3. TCB 一般线程控制块

     

    4. Endpoints

    为线程间通讯提供支持(详述见IPC)

     

    5. Notification 一般信号机制

    poll

     

    6. Untyped Memory 未类型内存

    Untyepd内存可被Retype成seL4定义的一些内存对象。

     

    7. CDT树(capability derivation tree)

    ——追踪源capability复制出的capability。

     

    CDT虽是独立的概念,但在实际实现是CNode对象的一部分

    (其实现可能是CNode数据结构中)

    seL4_Untyped_Retype()//大致是申请内存

    seL4_CNode_Mint();//复制CNode(可能包含权限降低)

    seL4_CNode_Copy();//复制CNode

    seL4_CNode_Mutate();//迁移CNode(可能包含权限降低)

    上述函数均生成子capability,均被CDT追踪。

    8. Slot——一段物理内存空间的实体。

     

    ——————————seL4基础服务——————————

    1. 线程(Threads)

    上下文切换、处理器时间分片的基本单位。

    1.1 每一个线程,都会有相应的CSpace(Capability Space)

    和VSpace(Virtual Space);

    同时,线程还会有IPC buffer,

    用于实现线程间通讯(详述见1.3 IPC)。

    1.2 每一个线程都有其归属的调度域

    (此处调度域与linux中存在很大区别)。

    内核在完成编译时就确定了此内核中的调度域的个数,

    内核将会定时、循环的调度各域。

    调度域内可存在多个线程(无上限),

    当且仅当线程所在调度域正在调度中时,线程才可能被调度执行。

    1.3 在调度域内,seL4采用256优先级的抢占式循环调度器。

     

    2. 地址空间(Address space)

    虚拟地址空间,由页表完成地址翻译。

    由于ASID资源限制,seL4设计了一个ASID Pool,

    通过ASID Control能力,线程VSpace与ASID Pool链接,

    以及通过ASID Pool使用ASID。

     

    3. 线程间通讯(IPC Inter-process communication)

    seL4线程间通讯通过endpoint(我认为应该是某种端点的含义)进行,

    消息内容的第一段为tag段,

    含有四部分:标志,消息长度,能力个数,开放能力的区域。

    seL4在IPC通讯时,会尽可能多的使用CPU寄存器,

    很多短内容的消息会直接通过CPU寄存器完成传递。

    seL4对IPC通讯的支持并不关心内容,

    需要用户层根据IPC消息的tag、消息所传来的能力等获得消息全部。

    (感觉类似socket?优化了的socket。)

    其他细节还很多,在此仅给以简述。

     

    4. Notification

    非阻塞的信号机制(与linux类似),比如对多路复用I/O的支持等。

     

    5. Device primitive

    seL4驱动是作为非特权程序执行在内核外,

    内核通过IPC实现硬件终端的分发。

     

    6. Capability Spaces(CSpace)

    CSpace是一个线程下CNode组成的的有向图的集合;

    也就是线程所拥有的Capability的集合。

     

    seL4以线程为单位拥有CSpace,

    内核启动第一个用户线程时即为之创建CSpace,

    此CSpace将包含所有其创建的CNode,

    当然也就包含所有其子线程的CSpace。

     

    CSpace含有CNodes,CNode中address可以找到slot,

    slot中有(或无)capability;

    当slot的Capability为另一个CNode,即可形成有向图;

    对每个线程,其CSpace都存在root CNode,可连通所有节点,

     

    另:

    线程发生系统调用,就会找到线程CSpace中,

    关于这个系统调用Capability的address,

    进而读取到相应slot,slot内容决定此系统调用是否执行。

     

    内核通过CNodes对象管理线程的CSpace;

    (简单说就是所有CNode都是连在一起的,有着共同的根,

    根据父子进程,CSpace通过CNode产生逐级依赖)

     

    ——————————seL4创建线程——————————

     

    1. seL4_Untyped_Retype()

    Retype对象来创建线程的TCB

     

    2. seL4_TCB_SetSpace()/seL4_TCB_Configer()

    设置TCB的CSpace、VSpace和EndPoint等

     

    3. seL4_TCB_WriteRegisters()

    关于栈指针和指令指针的一些操作

     

    4. seL4_TCB_Resume()

    激活线程,线程将会加入其父所在CPU调度

     

    5. 至此,线程将会被执行

     

    6. seL4_TCB_SetAffinity()

    在多核平台,可设置此线程的执行CPU

     

     

    ——————————seL4一些特点——————————

     

    1.缓存溢出免疫(基于严苛的capability设计)

    Buffer overflows are a classic security attack against operating systems, trying to make the software crash or even to inject malicious code into the cycle. We have proved that no such attack can be successful on seL4.

     

    2.访问空指针免疫(原理未知)

    Null pointer dereferences are another common issue in the C programming language. In applications they tend to lead to strange error messages and lost data. In operating systems they will usually crash the whole system. They do not occur in seL4.

     

    3.C中指针指错数据类型免疫(原理未知)

    In C it is possible to accidentally use a pointer to the wrong type of data. This is a common programming error. It does not happen in the seL4 kernel.

     

    4.内存泄漏免疫(基于严苛的capability设计)

    Memory leaks occur when memory is requested, but never given back. The other direction is even worse: memory could be given back, even though it is still in use. Neither of these can happen in seL4.

     

    5.算术溢出/异常免疫(原理未知)

    Humans and mathematics usually have a concept of numbers that can be arbitrarily big. Machines do not, they need to fit them into memory, usually into 32 or 64 bits worth of storage. Machines also generate exceptions when you attempt to do things that are undefined like dividing by zero. In the OS, such exceptions would typically crash the machine. This does not occur in seL4.

     

    6.未定义行为免疫(原理未知)

    There are many static analysis and verification tools that check for the absence of undefined behaviour in C. Our proof explicitly checks that no such undefined behaviour occurs.

     

     

    ——————————seL4总结————————————

    1. seL4内核层面的显式权限控制可以提供很高的安全保障,如DDOS不再有效。

     

    2. seL4提供的内存管理类类似于伙伴系统,能够有效减少内存碎片的产生,同样,不灵活的内存管理模式应该难以对内存充分利用。

     

    3. seL4的IPC基于Endpoint,受制于Capability,短消息由于采用CPU寄存器传递,效率不会明显下降,但长消息机制依赖于IPC Buffer的复制,效率不高。

     

    4. seL4的调度域根本隔离,带来的安全保障我并未想到,但调度域的静态设置应该会带来域内线程对用户响应的延迟,造成用户操作卡顿。

     

    因此,基于上述分析, 

    seL4的形式验证是一大亮点,

    其显式的权限管理也可以带来安全,

    但seL4还很年轻,社区活跃度不是非常高;

    seL4的应用开发框架基于C语言,必须采用接口-实体开发模式,

    不支持变长参数函数、函数指针等,因此代码移植可能存在难度。

    基础设施建设不完善,基于其设计思想的工业应用很少,

    若要真正投入使用,需要详尽分析其内核细节,

    详细分析其可能存在的缺陷、困难再考虑是否应用。

     

     

    seL4后续

    1.seL4中断通过Notification分发

    中断触发后,内核signal特定Notification,

    线程会seL4_Wait()/seL4_Poll()这个notification

     

    用户态用

    seL4_IRQHandler_SetNotification()

    之后线程开始seL4_Wait()/seL4_Poll()这个notification

     

    中断到达,线程处理完后

    seL4 IRQHandler Ack()提示内核处理完,内核可以发进一步的数据或后续中断

     

    seL4_IRQHandler_Clear()接触这个Notification的注册

     

    seL4没在主线中支持DMA

    但对于x86

    seL4支持了IOMMU

     

    也是作为一种能力

     

    seL4使用musl libc

    seL4可能会有文件系统(同济裴喜龙)

    seL4用的是gcc -O1,

    有形式验证过的编译器CompCert

     

    Norman Feske是搞Genode的,

    Genode是微内核之上的系统框架,

    这个系统框架类似linux的rootfs,

    Norman Feske把Genode移植到seL4了。

     

    写于2018.10

    展开全文
  • seL4 构建和测试

    2014-08-29 08:57:39
    转载至:https://source2014.hackpad.com/seL4--IJItb9IDncR

    转载至:https://source2014.hackpad.com/seL4--IJItb9IDncR

    取得核心程式碼

      • mkdir -p seL4-test && cd seL4-test
      • repo sync

    KZM-ARM11-01

    • ARM1136 532MHz (Freescale i.MX31) based evaluation board
    • 通过 QEMU 模拟和验证
      • make kzm_simulation_release_xml_defconfig
      • TOOLPREFIX=arm-none-eabi- ARCH=arm make
      • make simulate-kzm
    參考執行輸出:
    ...
        <testcase classname="sel4test" name="TEST_IPC0001">
    INFO :sel4utils_elf_load_record_regions:276:  * Loading segment 00008000-->000445e4
    INFO :sel4utils_elf_load_record_regions:276:  * Loading segment 0004d000-->00165df8
            <system-out>  TEST_IPC0001
    </system-out>
    ...
        <testcase classname="sel4test" name="TEST_CNODEOP00012">
    INFO :sel4utils_elf_load_record_regions:276:  * Loading segment 00008000-->000445e4
    INFO :sel4utils_elf_load_record_regions:276:  * Loading segment 0004d000-->00165df8
            <system-out>  TEST_CNODEOP0001
    </system-out>
        </testcase>
    </testsuite>
    
    126/126 tests passed.
    All is well in the universe.

    這時候可以準備執行 pkill qemu-system-arm

    seL4 Tests

    • BSD License
    • Directory
      • apps/sel4test-driver
      • apps/sel4test-tests

    seL4 Verification

    • 取得原始程式碼
      • mkdir -p verification &&cd verification
      • repo sync
    • 準備相關套件
      • sudo apt-get install libwww-perl texlive-bibtex-extra texlive-latex-extra
      • sudo apt-get install python-lxml
      • sudo apt-get install mlton python-tempita
    • 由於 Isabelle 需要額外的套件如 jdk7, jfreechart, scala, xz-java,得自網路抓取
      • cd l4v
      • mkdir -p ~/.isabelle/etc
      • cp -i misc/etc/settings ~/.isabelle/etc/settings
      • ./isabelle/bin/isabelle components -a
    • 遇到以下的小錯誤,可繼續
      • dirname: 缺少運算元
      • Try 'dirname --help' for more information.
    • 這過程相當耗時,解決方式為預先將檔案置放於 ~/.isabelle/contrib/ 目錄
      • cvc3-2.4.1
      • e-1.8
      • exec_process-1.0.3
      • Haskabelle-2013
      • jdk-7u40
      • jedit_build-20131106
      • jfreechart-1.0.14-1
      • kodkodi-1.5.2
      • polyml-5.5.1-1
      • scala-2.10.3
      • spass-3.8ds
      • z3-3.2
      • xz-java-1.2-1
      • ProofGeneral-4.2
    • Automated theorem proving! 確保可用的記憶體 > 2 GB
      • ./isabelle/bin/isabelle jedit -bf
      • ./isabelle/bin/isabelle build -bv HOL-Word
    • 參考輸出
    ML_PLATFORM="x86_64-linux"
    ML_HOME="/home/jserv/.isabelle/contrib/polyml-5.5.1-1/x86_64-linux"
    ML_SYSTEM="polyml-5.5.1"
    ML_OPTIONS="-H 2000"
    
    Session Pure/Pure
    Session HOL/HOL (main)
    Session HOL/HOL-Word (main)
    Building Pure ...
    Finished Pure (1:36:49 elapsed time, 0:00:51 cpu time, factor 0.00)
    Building HOL ...
    HOL: theory Code_Generator
    HOL: theory HOL
    HOL: theory SATz
    

    • 執行證明 (相當慢)
      • ./run_tests
    參考輸出:
    Running 31 test(s)...
    
      running isabelle ...              pass
      running CamkesAdlSpec ...         pass
      running CamkesGlueSpec ...        
      ...
      running CamkesAdlSpec ...          FAILED *
      running CamkesGlueSpec ...        FAILED *
    所有的 Test  都是一定會過 ?
    要安裝 mlton (已送 pull request)


    Issues



    展开全文
  • seL4环境配置

    2019-07-13 22:15:10
    转载声明:希望大家能够从这里收获知识之外,也... 既然奔着seL4来的,那么对于宏内核与微内核的区别应该是很清楚的了,在此就简单地介绍两者的区别,本文主要用来完成seL4环境配置工作。  对于小白来说,自己独...
  • x86架构下Linux初始化流程中GDT建立和切换 1、代码流:_start()–>start_of_setup()–>main()–>go_to_protected_mode()–>protected_mode_jump(); 函数所属文件: arch/x86/boot/head.S: _start()/...
  • seL4 下载

    2014-08-30 17:44:26
    本文译至:http://sel4.systems/Download/ 代码 所有的seL4代码和证明都可以在GitHub找到: https://github.com.au/seL4, 在标准的开放源代码许可证下。...l4v seL4 证明seL4 seL4 内核 seL4 项目 seL4
  • seL4:一个大的内核锁已经足够 论文戳这里 ,公开演讲PPT戳这里 前情提要 seL4 是一个安全的嵌入式系统,只支持有MMU的开发板,现在的移动CPU也在堆核心,所以要研究是否用更细的锁来提高可扩展性(Scalability)。 ...
  • Spring Tools 4 is the next generation of Spring tooling for your favorite coding environment. Largely rebuilt from scratch, it provides world-class support for developing Spring-based enterprise ...
  • linuxx86平台下在用户空间操作并口有两种方式,要么写成驱动,用户应用程序通过IO设备模块实现对并口读写,还有就是直接在用户空间I/O内存地址 PC25针并口. 接口定义如下: 针 方向 ...
  • Linux系统无法识别RTL8723网卡 装linux系统有一段时间了,但坑爹的是,我的网卡无法被系统识别出来,所以一直用的是有线连接。型号是:RTL8723BE。上网一搜,喵了个咪,怎么都是这款坑爹的型号存在问题!!之前有...
  • x86 分段机制

    2019-02-07 13:10:14
    4.段描述符 5.LDTR是什么 6.直达底部 段的定义 段的介绍 分段机制就是把虚拟地址空间中的虚拟内存组织成一些长度可变的称为段的内存单元。 80386虚拟地址空间中的虚拟地址(逻辑地址)由一个段部分和一个偏移部分...
  • Android x86镜像分析

    2020-02-06 15:40:55
    这几天学习Android,基于x86平台。先了解一下android的安装过程。在其官方网站下载了Android的iSO,就解压出来看看,需要说明的是以下的操作都是在root用户下进行的。以下是学习过程中,从网上找到的文件,这篇...
  • =-|================================================-{ www.enye-sec.org }-====|=-[ LKM Rootkits on Linux x86 v2.6 ]-========================================|=-|======================================
  • [zz]LKM Rootkits on Linux x86 v2.6 收藏 转载自水木KernelTech版。关于hack系统调用表的一篇文章,里面还涉及了学期ICS Lab中的二进制代码注入,很好很强大。略作整理(为什么技术博客默认的字体不是等宽的 T.T...
  • Linux系统调用劫持:其实就是修改内核符号表,来达到一个劫持的作用。因为系统调用实际是触发了一个0x80的软中断,然后转到了系统调用处理程序的入口system_call()。system_call()会检查系统调用号来得出到底是...
  • 话说,东汉末年,群雄并起,天下纷争。于是乎,产生了各种各样的引导方式。 linux下的引导方式就比较多了,从早期的lilo、grub到grub2、burg等等,以及Livecd的...先从win的引导方式说起,win就是群雄逐鹿的
1 2 3 4 5 ... 20
收藏数 1,480
精华内容 592
热门标签