关于

SeaHorn是一个基于LLVM的语言的自动化分析框架。此版本针对LLVM 14进行编译。

支持的一些特性包括

• 基于抽象解释的静态分析
• 基于统一的上下文敏感指针分析
• 基于SMT的有界模型检查(即符号执行)
• 基于CHC的软件模型检查(即不变量推理)
• 可执行的反例(即没有报告,只有bug!)

SeaHorn主要作为进行自动化验证研究的框架而开发。该框架提供了许多可以以多种方式组合在一起的组件。然而,它不是一个"开箱即用"的静态分析工具。

该框架提供了许多分析工具和示例。我们一直在寻找新的应用并为新用户提供支持。有关正在发生的事情的更多信息,请查看我们(不经常更新的)博客。

许可证

SeaHorn在修改的BSD许可证下分发。详情请参阅license.txt。

介绍

SeaHorn提供了一个名为sea的Python脚本与用户交互。给定一个带有断言注释的C程序,用户只需输入:sea pf file.c

sea-pf的结果是unsat,如果所有断言都成立;如果任何断言被违反,则为sat。

选项pf告诉SeaHorn将file.c转换为LLVM位代码,生成一组验证条件(VC),最后求解它们。主要的后端求解器是spacer。

命令pf提供了以下选项(其中包括):

• --show-invars:如果答案是unsat,显示计算出的不变量。

• --cex=FILE:如果答案是sat,将反例存储在FILE中。

• -g:使用调试信息进行编译,以获得更可追踪的反例。

• --step=large:大步编码。每个转换关系对应一个无循环的片段。

• --step=small:小步编码。每个转换关系对应一个基本块。

• --track=reg:仅模拟(整数)寄存器。

• --track=ptr:模拟寄存器和指针(但不包括内存内容)

• --track=mem:同时模拟标量、指针和内存内容

• --inline:在验证之前内联程序

• --crab:将Crab抽象解释工具生成的不变量注入spacer中。在这里阅读有关所有Crab选项(前缀为--crab)的详细信息。您可以通过键入选项--log=crab来查看Crab推断的不变量。

• --bmc:使用BMC引擎。

sea pf是一个运行多个命令的管道。管道的各个部分也可以单独运行:

1. sea fe file.c -o file.bc:SeaHorn前端将C程序转换为优化的LLVM位代码,包括混合语义转换。

2. sea horn file.bc -o file.smt2:SeaHorn从file.bc生成验证条件,并以SMT-LIB v2格式输出它们。用户可以通过添加以下内容在不同的编码风格之间进行选择,具有多个精度级别:

   • --step={small,large,fsmall,flarge},其中small是小步编码,large是块大编码,fsmall是生成平面Horn子句的小步编码(即它生成只有一个谓词的转换系统),flarge是生成平面Horn子句的块大编码。

   • --track={reg,ptr,mem},其中reg只模拟整数标量,ptr模拟reg和指针地址,mem模拟ptr和内存内容。

3. sea smt file.c -o file.smt2:以SMT-LIB2格式生成CHC。是sea fe后跟sea horn的别名。命令sea pf是sea smt --prove的别名。

4. sea clp file.c -o file.clp:以CLP格式生成CHC。

5. sea lfe file.c -o file.ll:运行传统前端

要查看所有命令,请键入sea --help。要查看每个单独命令CMD(例如horn)的选项,请键入sea CMD --help(例如sea horn --help)。

使用抽象解释进行静态分析

使用Crab推断归纳不变量

SeaHorn默认不使用Crab。要启用Crab,请在sea命令中添加选项--crab。

抽象解释器默认是过程内的,并使用Zones域作为数值抽象域。这些默认选项对于普通用户来说应该足够了。对于开发人员,如果您想使用其他抽象域,您需要:

1. 使用cmake选项-DCRAB_USE_LDD=ON -DCRAB_USE_ELINA=ON进行编译
2. 使用选项--crab-dom=DOM运行sea,其中DOM可以是:
   • int表示区间
   • term-int表示具有未解释函数的区间
   • boxes:表示不相交区间
   • oct表示八面体
   • pk表示多面体

要使用crab过程间分析,您需要使用选项--crab-inter运行sea

默认情况下,抽象解释器仅推理标量变量(即LLVM寄存器)。使用选项--crab-track=mem --crab-singleton-aliases=true运行sea可以推理内存内容。

如何在Spacer中使用Crab生成的不变量

Crab主要是路径不敏感的,而我们的Horn子句求解器Spacer是路径敏感的。虽然路径不敏感分析更高效,但通常需要路径敏感性来证明所关注的属性。这促使我们决定首先运行Crab(如果选项为--crab),然后将生成的不变量传递给Spacer。目前Spacer有两种方式使用Crab生成的不变量。sea选项--horn-use-invs=VAL告诉spacer如何使用这些不变量:

• 如果VAL等于bg,则不变量仅用于帮助spacer证明引理是归纳的。
• 如果VAL等于always,则行为类似于bg,但此外不变量还用于帮助spacer阻止反例。

默认值为bg。当然,如果Crab可以证明程序是安全的,那么Spacer就不会产生任何额外的开销。

属性规范

假定属性是断言。SeaHorn提供了一个静态断言命令sassert,如下例所示

/* 验证命令: sea pf --horn-stats test.c */
#include "seahorn/seahorn.h"
extern int nd();

int main(void) {
    int k = 1;
    int i = 1;
    int j = 0;
    int n = nd();
    while (i < n) {
        j = 0;
        while (j < i) {
            k += (i - j);
            j++;
        }
        i++;
    }
    sassert(k >= n);
}

在内部,SeaHorn遵循SV-COMP的约定,通过调用指定的错误函数__VERIFIER_error()来编码错误位置。当__VERIFIER_error()不可达时,SeaHorn返回unsat,并且程序被认为是安全的。当__VERIFIER_error()可达时,SeaHorn返回sat,并且程序是不安全的。sassert()方法在seahorn/seahorn.h中定义。

检查代码

除了证明属性或生成反例外,有时检查正在分析的代码以了解其复杂性也很有用。为此,SeaHorn提供了sea inspect命令。例如,给定一个C程序ex.c,输入:

sea inspect ex.c --sea-dsa=cs+t --mem-dot
 

选项--sea-dsa=cs+t启用了在FMCAD19中描述的新的上下文敏感、类型敏感sea-dsa分析。此命令为输入程序中的每个函数FUN生成一个FUN.mem.dot文件。要可视化主函数的图,请使用web graphviz界面,或以下命令:

$ dot -Tpdf main.mem.dot -o main.mem.pdf

有关内存图的更多详细信息,请参见SeaDsa存储库:这里。

使用sea inspect --help查看所有选项。目前,可用的选项有:

• sea inspect --profiler打印函数、基本块、循环等的数量。
• sea inspect --mem-callgraph-dot以dot格式打印SeaDsa构建的调用图。
• sea inspect --mem-callgraph-stats将SeaDsa完成的调用图构建的一些统计信息打印到标准输出。
• sea inspect --mem-smc-stats打印SeaDsa可以证明安全的内存访问的数量。

安装

开始使用SeaHorn的最简单方法是通过docker分发。

$ docker pull seahorn/seahorn-llvm10:nightly
$ docker run --rm -it seahorn/seahorn-llvm10:nightly

从探索sea命令可以做什么开始:

$ sea --help
$ sea pf --help

nightly标签每天自动刷新,包含最新的开发版本。我们不频繁地维护所有其他标签(需要手动更新)。请在DockerHub上检查日期,如果它们太旧,请在GitHub上记录问题。

博客上有其他示例和配置选项。博客很少更新。特别是,选项会发生变化,功能会被淘汰,会添加新的东西。如果您在博客中发现问题,请告诉我们。我们至少会更新博客文章,以表明它不应与最新版本的代码一起使用。

您也可以手动安装:

按照Docker文件中的说明进行操作 Dockerfile: docker/seahorn-builder.Dockerfile。

如果这不起作用,请运行:

$ wget https://apt.llvm.org/llvm.sh
$ chmod +x llvm.sh
$ sudo ./llvm.sh 14
$ apt download libpolly-14-dev && sudo dpkg --force-all -i libpolly-14-dev*

前3个命令将安装LLVM 14,第4个命令将安装libpolly,它被错误地从LLVM 14中省略(但包含在后续版本中)

接下来,按照上面的Docker文件中的说明进行操作

开发者专区

从这一点开始的信息仅供开发人员使用。如果您想为SeaHorn做出贡献,基于它构建自己的工具,或者只是对它的内部工作原理感兴趣,请继续阅读。

编译说明

SeaHorn需要LLVM、Z3和boost。库的确切版本不断变化,但使用cmake技巧来检查是否有正确的版本可用。

要指定任何依赖项的特定版本,请使用通常的<PackageName>_ROOT和/或<PackageName>_DIR(有关详细信息,请参见 CMAKE_BUILD_TYPE的其他合法选项是Debug和Coverage。请注意CMAKE_BUILD_TYPE必须与编译LLVM时使用的兼容。特别是,如果要以Debug模式编译SeaHorn,你需要LLVM的Debug版本。如果决定走这条路,请确保你有足够的耐心、硬盘空间和时间。

或者,也可以使用cmake预设来配置项目。只需运行以下命令:

$ cmake --preset <BUILD_TYPE>-<PRESET_NAME>

来配置cmake,其中<BUILD_TYPE>是Debug、RelWithDebInfo或Coverage之一,<PRESET_NAME>是你想使用的预设。目前可用的预设是:jammy。这些预设假设你已将Z3安装在/opt/z3-4.8.9，将Yices安装在/opt/yices-2.6.1。

这还允许使用VS Code的CMake Tools扩展在VS Code中配置和编译项目。

如果你想使用不同的编译设置,或者在其他目录中安装了Z3或Yices,你需要创建自己的CMakeUserPresets.json文件,其中包含你自己的预设。

在Mac上编译

不要包含-DSEA_ENABLE_LLD=ON。默认编译器是clang,所以你可能不需要明确设置它。

EXTRA目标

SeaHorn提供了几个通过extra目标自动克隆和安装的组件。这些组件可以在SeaHorn之外的其他项目中使用。

• sea-dsa: git clone https://github.com/seahorn/sea-dsa.git

  sea-dsa是一个新的基于DSA的堆分析。与llvm-dsa不同,sea-dsa是上下文敏感的,因此在存在函数调用时可以生成更细粒度的堆分区。

• clam: git clone https://github.com/seahorn/crab-llvm.git

  clam使用抽象解释技术为SeaHorn的其他后端提供归纳不变量。

• llvm-seahorn: git clone https://github.com/seahorn/llvm-seahorn.git

  llvm-seahorn提供了针对验证定制的InstCombine和IndVarSimplify LLVM pass版本,以及将未定义值转换为非确定性调用的LLVM pass等。

SeaHorn没有自带Clang版本,它期望在构建目录(run/bin)或PATH中找到Clang。确保Clang的版本与用于编译SeaHorn的LLVM版本匹配(目前是LLVM14)。提供正确版本Clang的最简单方法是从llvm.org下载,解压到某处,并在run/bin中创建clang和clang++的符号链接。

$ cd seahorn/build/run/bin
$ ln -s <CLANG_ROOT>/bin/clang clang
$ ln -s <CLANG_ROOT>/bin/clang++ clang++

其中<CLANG_ROOT>是解压Clang的位置。

测试

测试基础设施依赖于几个Python包。这些包有自己的依赖项。如果你无法弄清楚它们,请改用docker。

$ pip install lit OutputCheck networkx pygraphviz

覆盖率

我们可以使用gcov和lcov为SeaHorn生成测试覆盖率信息。要启用覆盖率构建,我们需要在不同的目录下运行构建,并在cmake配置期间将CMAKE_BUILD_TYPE设置为Coverage。

为test-opsem目标生成覆盖率报告的示例步骤:

1. mkdir coverage; cd coverage 创建并进入覆盖率构建目录
2. cmake -DCMAKE_BUILD_TYPE=Coverage <其他你想要的标志> ../
3. 像往常一样完成构建
4. cmake --build . --target test-opsem 运行OpSem测试,现在应该在相应的CMakeFiles目录中创建了.gcda和.gcno文件
5. lcov -c --directory lib/seahorn/CMakeFiles/seahorn.LIB.dir/ -o coverage.info 从所需模块收集覆盖率数据, 如果使用clang作为编译器而不是gcc,创建一个bash脚本llvm-gcov.sh:

#!/bin/bash
exec llvm-cov gcov "$@"

$ chmod +x llvm-gcov.sh

然后将--gcov-tool <包装脚本的路径>/llvm-gcov.sh附加到lcov -c ...命令。 6. 从所需目录提取数据并生成html报告:

lcov --extract coverage.info "*/lib/seahorn/*" -o lib.info
lcov --extract coverage.info "*/include/seahorn/*" -o header.info
cat header.info lib.info > all.info
genhtml all.info --output-directory coverage_report

然后在浏览器中打开coverage_report/index.html查看覆盖率报告

另请参阅CI使用的scripts/coverage脚本。每晚构建的覆盖率报告可在codecov上获得

代码索引

使用-DCMAKE_EXPORT_COMPILE_COMMANDS=ON选项为cmake生成seahorn项目及其所有子项目的编译数据库。

让代码索引与编译数据库支持一起工作的一个简单方法是将compilation_database.json文件链接到主项目目录,并按照编辑器特定的说明进行操作。

• Clion -- https://www.jetbrains.com/help/clion/compilation-database.html
• Vim (YouCompleteMe) -- 说明
• Emacs -- 使用lsp-ui和clangd,可在spacemacs开发分支中获得

CLion的远程配置

有关CLion远程工作流的详细指南,请查看Clion-configuration。

Emacs(和其他编辑器)的远程配置

使用我们的mainframer分支。不要错过示例配置。

贡献者

• Arie Gurfinkel
• Jorge Navas
• Temesghen Kahsai
• Jakub Kuderski
• Nham Le
• Charles Lei
• Xiang Zhou
• Siddharth Priya
• Isabel Garcia-Contreras
• Yusen Su
• 如果你的名字应该在这里,请给我发邮件