これは、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
参考文献