伊莎拉

伊莎拉是用于 的符号执行引擎，同时也是一种变位词。

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

这里有一个在线的 Web 界面

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 库。

伊莎拉解释由 Sail 生成的 IR。要在正确格式生成此 IR，在 isla-sail 目录中有一个工具。构建此工具需要各种神秘的 OCaml 祈祷语，但大多数人可以遵循 Sail 安装指南 此处，然后遵循 此处 的说明。它仅适用于 Sail 仓库中 sail2 分支的最新 HEAD。

对于使用 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 快照计算加法指令的足迹，可以使用以下命令：

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

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

项目结构

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

• isla-axiomatic 包含处理特定于在 isla-lib 上检查公理并发模型的 rust 代码，例如解析石蕊测试、分析指令足迹以及定义运行石蕊测试的高级接口。

• isla-cat 是一个从 herdtools 使用的 (部分) cat 内存模型到 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: Rigorous Engineering for Mainstream Systems"，部分受欧盟委员会的欧洲地平线 2020 研究和创新计划（协议 No 789108，"ELVER"）支持，部分受英国政府工业战略挑战基金 (ISCF) 在数字安全设计 (DSbD) 计划下支持，以提供 DSbDtech 启动的数字平台，由 Innovate UK 资助，项目编号 105694。