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

# RockSalt: Better, Faster, Stronger SFI for the x86

## 背景

### 問題意識
- x86などの複雑なアーキテクチャ上のソフトウェアサンドボックスの実装は脆弱になりやすい
- ソフトウェアサンドボックスはバイナリ解析してポリシー守ってるか検証する感じのやつの意
- 形式検証する

### 問題への貢献
- NaClみたいなのを作った
- Coqでx86の大部分のモデルを書いて宣言的な実装からコード生成で解析タスクの処理を作る

## 具体的な手法など
- NaCl互換のポリシーを受け付けるRockSaltを作った
- 抽象仕様からの生成で,抽象仕様の正当性検証済み
- NaClのサポートするx86サブセットの形式モデルがなかったので作った
- 既存手法だとクソ遅かったのをなんとかした
- 某ARMのHOLモデルで作られたやつで300命令に2.5時間とかだったのを1M/sとかにした
- ただ定理証明支援系ではなくDFAと一部のCコードを無条件に信頼している
- Coq上に一般のISAの形式モデルを記述するためのDSLを定義して使っている
- DSL→AST→RTL
- 遷移が形式検証されたDFAを生成して,それを動かすCコードを信頼することで小さなTCBと速度を両立している
- DSLから正規表現を作る