Hyperkernel驗證實驗的復現與z3環境初識
前言
建議順序閱讀本文！禁止轉載。--@CarpVexing（http://www.rzrgm.cn/CarpVexing/p/15948336.html）
Boss的項目，要求對os驗證的典型研究進行一些研究，于是我花費半個禮拜復現了一下Hyperkernel這個實驗。關于z3證明器在os驗證方面的潛力與前景，本文不做探討，僅將復現過程簡單做個備忘。
筆者之前還想復現中科大μC_OS-Ⅱ驗證實驗，奈何項目主頁給出的驗證文件和虛擬機鏡像打包文件掛載在“中科大·耶魯高可信軟件聯合研究中心”的服務器下，但是這個服務器寄了，東西都down不到了。
論文來源
這是項目主頁： UNSAT: Hyperkernel (washington.edu)
這是github地址（基礎用法）： GitHub - uw-unsat/hyperkernel
這是論文地址：https://unsat.cs.washington.edu/papers/nelson-hyperkernel.pdf
系統選擇
我沒有完全按照它們給出的配置進行設置，而是盡量靠近他們所要求的版本。實驗平臺為win10的vmware。
虛擬機環境：VMware? Workstation 16 Pro ver.16.1.2 build-17966106
系統：Linux Ubuntu 17.10
鏡像：ubuntu-17.10.1-desktop-amd64.iso
分配硬盤20G，內存8G，自動檢測光驅。
前置環境配置
首先，我們需要編譯器環境。但是在此之前，需要先將apt下載源進行更改。不同版本ubantu有不同的改法，筆者設置如下：
sudo su
vi /etc/apt/sources.list
東西全刪了，改為：
deb https://mirrors.cloud.tencent.com/ubuntu/ bionic main universe
deb http://mirrors.aliyun.com/ubuntu/ bionic main restricted universe multiverse
deb-src http://mirrors.aliyun.com/ubuntu/ bionic main restricted universe multiverse
deb http://mirrors.aliyun.com/ubuntu/ bionic-security main restricted universe multiverse
deb-src http://mirrors.aliyun.com/ubuntu/ bionic-security main restricted universe multiverse
deb http://mirrors.aliyun.com/ubuntu/ bionic-updates main restricted universe multiverse
deb-src http://mirrors.aliyun.com/ubuntu/ bionic-updates main restricted universe multiverse
deb http://mirrors.aliyun.com/ubuntu/ bionic-proposed main restricted universe multiverse
deb-src http://mirrors.aliyun.com/ubuntu/ bionic-proposed main restricted universe multiverse
deb http://mirrors.aliyun.com/ubuntu/ bionic-backports main restricted universe multiverse
deb-src http://mirrors.aliyun.com/ubuntu/ bionic-backports main restricted universe multiverse
接下來所有腳本默認管理員權限了，不再sudo。對apt-get進行更新：
apt-get update
如果你在之后的環境配置中遇到依賴包需要降低版本的問題，可以先裝一個aptitude工具：
apt-get install aptitude
接著安裝編譯環境：
apt install build-essential
apt install cmake
apt install lang
build-essential包括了gcc,g++,make等。筆者版本如下：gcc version 7.3.0 (Ubuntu 7.3.0-16ubuntu3)；GNU Make 4.1。
如果發現gcc、g++、make、cmake、clang中的任何一個不能再shell中直接調用，請用apt或aptitude重新單獨安裝。
由于直接在Ubuntu環境下下載文件可能不太方便，建議利用VMware tools設置一處共享文件夾，方便資源的轉移。
配置python
python選的是2.7的默認版本，2.7.6。直接apt下載即可。
apt install python2.7
tar -zxvf pip-9.0.1.tar.gz
cd pip-9.0.1
python2.7 setup.py install
請注意，pip并不是必須安裝的，只是怕出現py包依賴出現莫名其妙的問題，可以臨時查缺補漏。
請注意，pip和pip2此時都會指向pip-9.0.1。
接下來，由于本項目中用到的不同腳本對py的調用有多種寫法，我們需要將python、python2都鏈接到默認環境變量名python2.7上。建議使用純凈的環境進行配置，倘若存在python3環境可能與2.7產生沖突。設置如下：
echo alias python=python2.7 >> ~/.bashrc
echo alias python2=python2.7 >> ~/.bashrc
source ~/.bashrc
安裝Z3
請不要用pip安裝z3-solver！這可能導致嚴重的版本偏差和文件錯誤依賴。我們需要自己編譯并安裝z3環境。
操作如下（參考鏈接）：
git clone https://github.com/Z3Prover/z3.git
cd z3
python scripts/mk_make.py
cd build
make
sudo make install
如果這一步出現問題，請重新驗證編譯器GCC或clang環境是否正常。
另外給出卸載z3的方法：
cd z3/build
sudo make uninstall
筆者的z3版本是Z3 version 4.8.15 - 64 bit。
請注意，此時應該可以直接在腳本中調用Z3，但是在python2.7中無法import z3。因此需要添加py的庫依賴路徑：
vi /etc/profile
在文本最后添加（注意改成你自己的z3路徑）：
export PYTHONPATH=$PYTHONPATH:/usr/local/z3/build/python/
保存更改：
source /etc/profile
此時在python2.7中應當可以import z3。出現任何報錯，都說明依賴路徑沒有設置到位。
安裝LLVM5.0.0
這是本項目復現最麻煩的一步！請耐心做完，直接apt會導致llvm缺少工具，無法使用！
首先在這里下載llvm5.0.0： LLVM Download Page 下載如下源碼包：
假設當前路徑為~/llvm/，且下載好的內容都在這里。解壓并整理：
tar -xf cfe-5.0.0.src.tar.xz
tar -xf clang-tools-extra-5.0.0.src.tar.xz
tar -xf compiler-rt-5.0.0.src.tar.xz
tar -xf libcxx-5.0.0.src.tar.xz
tar -xf llvm-5.0.0.src.tar.xz
mv cfe-5.0.0.src clang
mv clang/ llvm-5.0.0.src/tools/
mv clang-tools-extra-5.0.0.src extra
mv extra/ llvm-5.0.0.src/tools/clang/
mv compiler-rt-5.0.0.src compiler-rt
mv compiler-rt llvm-5.0.0.src/projects/
整理后路徑下應該只剩下libcxx-5.0.0.src和llvm-5.0.0.src了。保持在這個路徑，進行操作：回到上一級創建build文件夾
cd ..
mkdir build
cd build
cmake ../llvm -DLLVM_TARGETS_TO_BUILD=X86 -DCMAKE_BUILD_TYPE=Release -DLLVM_USE_LINKER=gold
../llvm是你自己的路徑。若遇到錯誤，請檢查你的cmake、g++環境是否正常。
接下來進行編譯與安裝，這一步非常耗時，且容易出錯：
make -j4
sudo make install
安裝完成后，llvm應當能夠在shell中直接調用。
驗證Hyperkernel
先把多線程數拉滿：
cat /proc/sys/kernel/threads-max
echo 333333 > /proc/sys/kernel/threads-max
cat /proc/sys/kernel/threads-max
下載項目 GitHub - uw-unsat/hyperkernel 。
將工作目錄移到項目目錄下。
完整的驗證，直接輸執行：
make hv6-verify
圖中.是驗證成功，E是error，F是failure。需要說明的是，內存錯誤和線程錯誤都會帶來驗證錯誤。完整驗證估計需要耗費20h以上的時間。
單獨驗證可以執行：
make hv6-verify -- -v --failfast HV6.test_sys_set_runnable
運行 Irpy 測試套件(似乎完整驗證完成前無法執行)：
make irpy/test
結語
本文由@CarpVexing發布于2022.2。Hyperkernel實際上已然是五年前的項目了，已經有了不少Applications and extensions，值得一看。接下來筆者考慮深入了解一下z3，有機會再作新文。
浙公網安備 33010602011771號