---
tags: 論文メモ
---

# The Missing Link: Explaining ELF Static Linking, Semantically

## 背景

### 問題意識
- プログラム言語の意味論レベルでは扱えてない挙動をリンカが担っている
- e.g. weak symbol
- 一般のソフトウェアはプログラム言語の意味論だけでなくリンカの挙動にも大いに依存している(Linker Speak)
- 形式検証済みコンパイラでも,こういった部分は扱えていないかごく一部

### 問題への貢献
- ELFバイナリのリンクに関する形式化
- あるべき挙動を形式的に記述するというより現在一般に利用されているリンカの挙動に近い形にする
- リンカが一般のソフトウェアで果たしている役割を分類
- ただの分割コンパイルではない部分を重視
- ELFバイナリのaarch64/amd64/ia32/power64におけるファイル形式の形式モデル
- よく使われるGNU拡張も考慮
- ELFの形式モデルを用いて静的リンカを作った
- executable specificationとあるがおそらくextractionなどで形式化した仕様から実行可能なコードに変換したものを用いて実装したリンカ
- bzip2の静的リンクが可能な程度のもの
- リンカの内部仕様に関する諸性質の証明(isabelle/hol)
- 停止性
- Lemで仕様を書いてOCamlとIsabelleに変換しているらしい

## 具体的な手法など