Kind2

Kind2是一个多引擎、并行、基于SMT的自动模型检查工具，用于Lustre程序的安全性验证。

Kind2是一个命令行工具，接受一个Lustre文件作为输入，输出所有输入中的属性是否为真。为了便于外部工具处理，结果可以以JSON和XML格式输出。

参考网站：Kind 2 (uiowa.edu)

Kind2在线工具：Kind (uiowa.edu)

  1. 所需环境

  2. 安装docker

    打开虚拟机终端，输入命令行。

    1
    $ curl -fsSL https://get.docker.com | bash -s docker --mirror Aliyun

    image-20210811182047842

    1
    $ sudo curl -L "hhtps://github.com/docker/compose/releases/download/1.26.2/docker-compose-$(uname -s)-$(uname -m)" -o /usr/local/bin/docker-compose
    1
    sudo chmod +x /usr/local/bin/docker-compose

    验证Docker Compose安装结果：

    1
    $ docker-compose --version

  3. 用docker安装Kind2

    在用户权限下docker命令需要sudo，否则权限不足：

    image-20210811174615175

    通过将用户添加到docker用户组可以将sudo去掉，命令行如下：

    1
    2
    3
    $ sudo groupadd docker
    $ sudo gpasswd -a $USER docker
    $ newgrp docker

    再进行docker安装：

    1
    $ docker pull kind2/kind2

    image-20210811185222763

    在sudo权限下，也可以直接安装，无需上述步骤授权：

    1
    $ sudo docker pull kind2/kind2

    image-20210811175600302

    查看docker本地所有镜像。

    1
    $ docker images

    image-20210811185942125

  4. 使用手册

    参考：Kind 2 (uiowa.edu)