seL4微內(nèi)核入門(mén)-代碼下載運(yùn)行及資料

不廢話，老一套：編譯環(huán)境準(zhǔn)備，代碼下載，代碼編譯，qemu代碼運(yùn)行。本文介紹的內(nèi)容都是好東西，提供全方位的微內(nèi)核入門(mén)指導(dǎo)，就看毅力怎么樣了，就像那句話：笨鳥(niǎo)先飛。

1. sel4簡(jiǎn)介

sel4是微內(nèi)核操作系統(tǒng)，號(hào)稱世界上最安全，最高效的微內(nèi)核。提供非posix兼容的編程接口，它只提供了少量的服務(wù)，創(chuàng)建和管理虛擬地址空間、線程以及進(jìn)程間通信(IPC)。亮點(diǎn)是capability機(jī)制，管理每個(gè)進(jìn)程所擁有的資源。這個(gè)機(jī)制的引入也導(dǎo)致了sel4較難理解和應(yīng)用開(kāi)發(fā)。關(guān)于微內(nèi)核的介紹參考上一篇：

2. Turorial練習(xí)

從官網(wǎng)提供的學(xué)習(xí)教程hello world開(kāi)始練習(xí)，

2.1 環(huán)境準(zhǔn)備

這里同樣，采用的開(kāi)發(fā)方式為VitrualBox+Ubuntu，下載VitrualBox和Ubuntu鏡像（版本>= 20.04），安裝虛擬機(jī)，具體不再描述。

環(huán)境搭建是否正常，以能運(yùn)行第一個(gè)helloworld工程為準(zhǔn)，詳細(xì)步驟為:

1）repo工具安裝

mkdir~/binPATH=~/bin:$PATH curl  https://storage.googleapis.com/git-repo-downloads/repo > ~/bin/repochmod a+x ~/bin/repo

2）lib依賴庫(kù)和編譯工具安裝

#ThebasicbuildpackageonUbuntuisthe build-essentialpackage.Toinstallrun:sudo apt-get updatesudo apt-get install build-essential #AdditionalbasedependenciesforbuildingseL4 projectsonUbuntuincludeinstalling:sudo apt-get install cmake ccache ninja-build cmake-curses-guisudo apt-get install libxml2-utils ncurses-devsudo apt-get install curl git doxygen device-tree-compilersudo apt-get install u-boot-toolssudoapt-getinstallpython3-dev python3-pippython-is-python3sudoapt-getinstallprotobuf-compiler python3-protobuf sudoapt-getinstallqemu-system-arm qemu-system-x86qemu-system-miscsudoapt-getinstallgcc-arm-linux-gnueabi g++-arm-linux-gnueabisudoapt-getinstallgcc-aarch64-linux-gnu g++-aarch64-linux-gnu

3）Python 依賴庫(kù)

pip3 install--user setuptoolspip3 install--user sel4-deps# Currently we duplicate  dependencies for python2 and python3 as a python3 upgrade is in processpip install--user setuptoolspip install--user sel4-deps

4） 編譯庫(kù)依賴

sudo apt-get install clang gdbsudo apt-get install libssl-dev libclang-dev libcunit1-dev libsqlite3-devsudo apt-get install qemu-kvm

5）證明依賴

sudo apt-get installpython3 python3-pippython3-devgcc-arm-none-eabi build-essentiallibxml2-utilsccachencurses-dev librsvg2-bindevice-tree-compilercmakeninja-build curlzlib1g-devtexlive-fonts-recommendedtexlive-latex-extra texlive-metapost texlive-bibtex-extra mlton-compiler haskell-stack

2.2 下載代碼 下載代碼前安裝python依賴用于編譯教程

pipinstall--useraenumpip install --user pyelftools

下載代碼前配置repo郵箱信息

gitconfig --globaluser.email"you@example.com"gitconfig--globaluser.name "Your Name"

下載代碼（這里使用sel4官方的代碼進(jìn)行練習(xí)，從github上下載）?

mkdirsel4-tutorials-manifestcd sel4-tutorials-manifestrepo init -u  https://github.com/seL4/sel4-tutorials-manifestrepo sync

2.3 Hello World應(yīng)用生成 初始化hello-world文件夾?

./init--tuthello-world--solution

hello-world是示例名字，練習(xí)其他示例更換這個(gè)名字就可以，命令加 --solution后綴，可以補(bǔ)全代碼。可以看到生成了下面的hello-world文件夾，里面有c代碼。

2.4 代碼編譯

cdhello-world_buildninja

編譯成功后顯示：

2.5 代碼運(yùn)行

# In build directory, hello-world_build./simulate

成功后顯示：

運(yùn)行后Ctrl-A, X退出qemu模擬工具。

3. Hello World代碼分析

編譯的時(shí)候，我們使用了ninja這個(gè)命令，Ninja 是Google的一名程序員推出的注重速度的構(gòu)建工具，一般在Unix/Linux上的程序通過(guò)make/makefile來(lái)構(gòu)建編譯，而Ninja通過(guò)將編譯任務(wù)并行組織，大大提高了構(gòu)建速度。

可見(jiàn)ninja跟makefile同級(jí)別的都是構(gòu)建工具，生成編譯器使用的規(guī)則。

在sel4-tutorials-manifest/hello-world_build/build.ninja文件中可以看到

執(zhí)行ninja命令就會(huì)通過(guò)這個(gè)build.ninja進(jìn)行編譯，會(huì)找到hello-world的代碼

cmake是makefile之上的一層封裝。

CMakeLists.txt – cmake使用的腳本，將根任務(wù)合并到更廣泛的 seL4 構(gòu)建系統(tǒng)中的文件。

src/main.c - 初始任務(wù)的單個(gè)源文件。
hello-world.md - 為教程生成的自述文件。

intmain(intargc,char*argv[]){     printf("Hello, World!
");      printf("Second hello
");    return  0;}

如果修改了應(yīng)用的源碼，重新運(yùn)行重建項(xiàng)目:

Bash# In build directory, hello-world_buildninja

然后再運(yùn)行simulator:

# In build directory, hello-world_build./simulate

4. 學(xué)習(xí)資料

sel4原理熟悉，主要從兩條路進(jìn)行學(xué)習(xí)：

一邊是sel4的參考手冊(cè)，另一邊就是基于Tutorials教程開(kāi)始一步一步的做實(shí)驗(yàn)，這樣可以做到理論和實(shí)踐結(jié)合。

（turorials中camkes相關(guān)的例子可以先不學(xué)習(xí)）

輔助庫(kù)介紹：

tutorials工程中，其他輔助庫(kù)的介紹，除了sel4微內(nèi)核之外，還需要提供一些庫(kù)，才能讓你的應(yīng)用程序運(yùn)行起來(lái)。

sel4內(nèi)核：首先是sel4內(nèi)核。單單的一個(gè)內(nèi)核運(yùn)行起來(lái)，是沒(méi)法運(yùn)行一個(gè)例如hello world這樣的程序的，因?yàn)檫@個(gè)程序需要鏈接其他的庫(kù)，比如stdio中的printf，而且該程序和內(nèi)核交互，就需要知道內(nèi)核提供的標(biāo)準(zhǔn)API有哪些。

libsel4：sel4內(nèi)核提供的api都用內(nèi)核源碼工程里面的libsel4這個(gè)庫(kù)來(lái)描述。里面是sel4內(nèi)核支持的標(biāo)準(zhǔn)api。


sel4_libs：當(dāng)一個(gè)程序連接了這個(gè)libsel4之后，就可以使用sel4內(nèi)核的標(biāo)準(zhǔn)api了，這個(gè)和Linux內(nèi)核提供的標(biāo)準(zhǔn)api類(lèi)似，是和操作系統(tǒng)密切關(guān)聯(lián)的。非posix標(biāo)準(zhǔn)的。另外這個(gè)libsel4庫(kù)不是很好用，因此在這之上又堆疊了一個(gè)sel4_libs庫(kù)，這個(gè)庫(kù)是對(duì)sel4標(biāo)準(zhǔn)api的進(jìn)一步功能性的封裝，比如分配一個(gè)cap對(duì)象，調(diào)用者無(wú)需知道更下層的sel4標(biāo)準(zhǔn)api調(diào)用的細(xì)節(jié)。

musllibc：這個(gè)是開(kāi)源的一個(gè)libc庫(kù)，和sel4是沒(méi)有直接關(guān)系的。用到這個(gè)工程里面來(lái)，主要是提供標(biāo)準(zhǔn)的符合posix標(biāo)準(zhǔn)的api，其他的操作系統(tǒng)也是可以使用的。因此應(yīng)用程序可以直接使用libsel4中的函數(shù)，也可以使用sel4_libs中的函數(shù)，比較標(biāo)準(zhǔn)的功能就可以使用muscllibc中的功能了。為了打通muslibc和sel4_libs，sel4_libs中提供了一個(gè)libsel4muslcsys這樣的一個(gè)庫(kù)，muslibc中的一些功能通過(guò)sys call的方式調(diào)用到libsel4muslcsys這個(gè)接口庫(kù)中，這個(gè)接口庫(kù)就會(huì)調(diào)用sel4_libs中的相應(yīng)函數(shù)。當(dāng)然muslibc中的有些函數(shù)可能會(huì)直接調(diào)用libsel4的函數(shù)接口（目前還沒(méi)有看到muslibc中或者libsel4中有對(duì)這兩個(gè)庫(kù)的對(duì)接口的實(shí)現(xiàn)，可能這個(gè)猜測(cè)不對(duì)）

sel4runtime：一般程序里面都有一個(gè)main函數(shù)，作為該程序的入口位置，但是，這個(gè)程序的運(yùn)行并不是從main開(kāi)始的，在運(yùn)行main之前，其實(shí)還做了其他的一些工作，比如堆棧指針的設(shè)置，環(huán)境變量的獲取，其他的一些準(zhǔn)備工作等等。一般編譯器，比如gcc編譯器編譯一個(gè)比如hello world這樣的一個(gè)代碼的時(shí)候，會(huì)指定該程序的入口地址是 _start, 就是會(huì)找尋源碼，把 _start開(kāi)始的代碼放在該程序代碼段的最開(kāi)始位置，hello_world.c源碼中并沒(méi)有 _start這個(gè)函數(shù)或者標(biāo)號(hào)，所以這個(gè)標(biāo)號(hào)是其他地方的，且是會(huì)被hello_world.c鏈接進(jìn)來(lái)的源碼，在sel4 tutorial工程里，我們用sel4runtime（里面是源碼）和lshello_world.c一起編譯，鏈接。這個(gè)sel4runtime工程里面提供了各個(gè)架構(gòu)的 _start入口標(biāo)號(hào)，該標(biāo)號(hào)緊跟著的是該架構(gòu)的一些匯編語(yǔ)言，處理堆棧等等，之后跳轉(zhuǎn)到一個(gè)簡(jiǎn)單的c函數(shù)處，該c函數(shù)收集環(huán)境變量，傳入參數(shù)等，并最終調(diào)用main函數(shù)。