其他分享
首页 > 其他分享> > Hyperkernel验证实验的复现与z3环境初识

Hyperkernel验证实验的复现与z3环境初识

作者:互联网

Hyperkernel验证实验的复现与z3环境初识


前言

建议顺序阅读本文!禁止转载。--@CarpVexing

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,自动检测光驱。

1

前置环境配置

首先,我们需要编译器环境。但是在此之前,需要先将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

安装对应的pip工具(参考链接),下载文件,解压安装:

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 下载如下源码包:

2

假设当前路径为~/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是验证错误。需要说明的是,内存错误和线程错误都会带来验证错误。完整验证估计需要耗费20h以上的时间。

3

单独验证可以执行:

make hv6-verify -- -v --failfast HV6.test_sys_set_runnable

4

运行 Irpy 测试套件(似乎完整验证完成前无法执行):

make irpy/test

结语

本文由@CarpVexing发布于2022.2。Hyperkernel实际上已然是五年前的项目了,已经有了不少Applications and extensions,值得一看。接下来笔者考虑深入了解一下z3,有机会再作新文。

标签:5.0,src,Hyperkernel,tar,apt,初识,ubuntu,z3
来源: https://www.cnblogs.com/CarpVexing/p/15948336.html