これは、kstm Advent Calendar 2024の3日目の記事になります。@Uni8saiが担当します。

はじめに

ProVerifとは、形式モデルでの暗号プロトコルの安全性を自動検証するツールです。
暗号プロトコルを形式モデル化したコードをツールに流すと、秘匿や認証などの安全性要件を自動で検証してくれます。
ProVerifは、Windows、Mac、Linuxなどでサポートしており、公式サイトからソース・バイナリを直接持ってくる方法とOPAM経由でインストールする方法があります。
今回はOPAM経由でインストールしました。

前提環境

WSL上のUbuntu24.04 LTS
VirtualBox上のAlmaLinux 9

インストールの流れ

Linux（Debian）でProVerifをOPAM経由でインストールする方法について説明します。
ProVerifのマニュアルには、OPAMインストール済み前提でProVerifのインストール方法が書かれているため、今回はOPAMのインストールも合わせて紹介します。

Ubuntuのアップデート

まず、パッケージ全体を更新しておきましょう。

$ sudo apt update 
$ sudo apt upgrade

OPAMのインストール

次に、OPAMをインストールします。

$ sudo apt install opam

OPAMの初期化とアップデートをします。

# 処理中に出てくる選択肢は全てyes
$ opam init
$ opam update

ProVerifのインストール

ここからは、ProVerifの公式マニュアルに記載のやり方と同じです。(出てくる選択肢は全てyes）

$ opam depext conf-graphviz
$ opam depext proverif
$ opam install proverif

opam install proverif の実行時に「gcc 11がない」と怒られる場合があります。その場合は下記のコマンドを実行しgcc 11をインストールしてから再度実行してください。

# Debian系の場合
$ sudo apt install gcc-11

# RHEL 8系の場合
$ sudo dnf install gcc-toolset-11
$ sudo scl enable gcc-toolset-11 bash

RHEL 9系の場合は、公式サイトからgcc 11のソースを直接インストールしてmakeします。

$ wget https://ftp.gnu.org/gnu/gcc/gcc-11.4.0/gcc-11.4.0.tar.gz
$ tar -xvzf gcc-11.4.0.tar.gz
$ cd gcc-11.4.0
$ ./contrib/download_prerequisites
$ mkdir build
$ cd build
$ ../configure --disable-multilib --enable-languages=c,c++
$ make -j$(nproc)
$ sudo make install

最後に、シェルにインストールしたパッケージを適用するために、下のコマンドを実行します。

eval $(opam env)

これで、proverifとコマンドを打ったときに、エラーが出なければ、インストール成功です。

おまけ

OPAMをHomebrew経由でインストールする方法

RHEL 9といった一部環境では、ディストリビューション標準のパッケージ管理システムにOPAMが入っていない場合があります。そのような場合の対処方法として、Homebrew経由でOPAMをインストールする方法があるので、紹介します。
ちなみに、Mac OSでProVerifのインストールをする際もHomebrewとOPAMを通してインストール可能です。

Homebrewのインストール

パッケージ管理システムHomebrewをインストールします。まずは、Homebrewのホームページに書かれているインストールコマンドを実行します。

#インストール中に何度かyesかnoかを聞かれるが、全てyes
$ /bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/HEAD/install.sh)"

インストールが成功すると、次のステップとして、PATH設定とパッケージのインストールをしろという表示が出てくるので、それに従います。下に書かれているコードはその際に出てくる内容と同じです。

# PATH設定
$ echo >> /home/[ユーザー名]/.bashrc
$ echo 'eval "$(/home/linuxbrew/.linuxbrew/bin/brew shellenv)"' >> /home/[ユーザー名]/.bashrc
$ eval "$(/home/linuxbrew/.linuxbrew/bin/brew shellenv)"

brewの実行に必要なパッケージの追加インストール

# Debian系の場合
$ sudo apt-get install build-essential
# RHEL系の場合（8以降）
$ sudo dnf group install "Development Tools"
$ brew install gcc

OPAMのインストール

ProVerifの実行に必要なパッケージをbrewからインストールします。

$ brew install ocaml opam graphviz gtk+

ここまで成功したら、あとは上述のProVerifのインストール作業と同じです。

私のUbuntuでは、opamの実行に必要なbubblewrapがインストールされておらず、エラーを吐きましたので、下のパッケージを追加でインストールしました。

$ sudo apt install bubblewrap

参考文献