Isla

Isla 是 Sail 指令集架构规范的符号执行引擎，也是一个词谜游戏。

它可以用来评估在 Sail 中指定的指令集架构的放宽内存行为，使用 herd7 工具使用的 cat 语言子集中的公理内存模型。例如

这里有一个在线网页界面

https://isla-axiomatic.cl.cam.ac.uk

它还可以用于测试生成，为具体操作码生成简化语义（摘要），以及许多其他可能的用例。

构建

当前使用（稳定）Rust 1.39 测试

cargo build --release

默认情况下，我们要求 z3 作为共享库可用。在 Ubuntu 20.04 LTS 及以上版本中，只需运行 apt install libz3-dev 就可以。但是，在较旧的 Ubuntu LTS 版本（以及可能的其他 Linux 发行版）中可用的 z3 版本相当古老，因此您可能会遇到链接错误。build.rs 脚本配置为可以使用放置在本存储库根目录中的 libz3.so 共享库。如果这样做，那么在执行时也必须设置 LD_LIBRARY_PATH，以便使用较新的 z3 库。

Isla 解释由 Sail 产生的 IR。要在正确的格式生成此 IR，isla-sail 目录中有一个工具。构建此工具需要各种神秘的 OCaml 咒语，但主要可以遵循 这里 的 Sail 安装指南，然后遵循 这里 的说明。它只能与 Sail 存储库中最新 HEAD 的 sail2 分支一起使用。

对于使用herd7的.litmus格式的酸碱测试，在isla-litmus目录中还有一个基于herd7本身解析代码的OCaml工具。这个工具将这种格式转换为简单的TOML表示。这个OCaml程序是独立的，不依赖于任何库，并且应该使用dune >= 1.2构建。

模型快照

Isla执行Sail生成的IR。为了避免生成此IR，我们可以在以下存储库中找到预编译的ISA模型快照：

https://github.com/rems-project/isla-snapshots

示例

编译Isla后，要使用上述aarch64快照计算加法指令的footprint，可以使用以下命令：

target/release/isla-footprint -A aarch64.ir -C configs/aarch64.toml -i "add x0, x1, #3" -s

参数是编译后的Sail模型、控制初始状态和其他选项的配置文件以及我们想要运行的指令。-s标志执行一些基本的死代码消除以简化生成的footprint。

项目结构

• isla-lib 是一个Rust库，包含核心符号执行引擎以及与之交互的API。

• isla-axiomatic 包含处理各种特定于在isla-lib之上检查归纳并发模型的rust代码，例如解析litmus测试、分析指令footprint以及定义运行litmus测试的高级接口。

• isla-cat 是一个将herdtools使用的（猫内存模型的片段）转换为SMTLIB定义的翻译器。它有自己的README 在此。

• isla-litmus 是一个（可选）OCaml实用程序，将herdtools使用的.litmus文件映射为我们能读取的格式。

• isla-sail 是一个（可选）OCaml实用程序，将Sail规范映射为我们能进行符号执行的IR。

• web 包含了用于axiomatic并发工具的Web界面的服务器和客户端。

• src 定义了基于isla-lib的多个小型可执行实用程序。

资助

本软件由剑桥大学计算机实验室（计算机科学与技术系）开发，部分受DARPA/AFRL合同FA8650-18-C-7809（“CIFV”）资助，部分受EPSRC项目资助EP/K008528/1“REMS：主流系统的严格工程”，部分受欧盟委员会第七框架计划下欧洲研究理事会（ERC）的资助（协议号789108，“ELVER”），部分受英国政府工业战略挑战基金（ISCF）在数字安全设计（DSbD）计划下的资助，以交付一个DSbDtech enabled digital platform，在Innovate UK资助项目105694下。