# 論文紹介 Cache Audit 後半
状態数が膨大になるので、$Col\subseteq Traces$の計算は現実的でない
抽象化して$Col^\sharp \in Traces^\sharp$を求めたい
このとき、$Col^\sharp$とLeakage Bitの関係は以下のようになる

##### 具体化関数と満たすべき健全性
$$
\gamma:Traces^\sharp \rightarrow \wp(Traces)\\
next^\sharp: Traces^\sharp \rightarrow Traces^\sharp\\
\forall a \in Traces^\sharp:next(\gamma(a)) \subseteq \gamma(next^\sharp(a))
$$
適切に$next,\sqcup^\sharp$を定義して、関数$F^\sharp$の最小不動点$\text{lfp}F^\sharp = Col^\sharp$を求める
$$
F^\sharp(X^\sharp) = I^\sharp \sqcup^\sharp\ next^\sharp(X^\sharp)
$$
## Abstraction
とりあえず天下り的に定義していく
### Abstract Memory
- Domain $\mathcal{M}^\sharp$
- concretize $\gamma_\mathcal{M}:\mathcal{M}^\sharp\rightarrow \wp(\mathcal{M})$
### Abstract Cache
- Domain $\mathcal{C}^\sharp$
- concretize $\gamma_\mathcal{C}:\mathcal{C}^\sharp\rightarrow \wp(\mathcal{C})$
### Abstract Sequence of Events
- Domain $\mathcal{E}^\sharp$
- concretize $\gamma_\mathcal{E}:\mathcal{E}^\sharp\rightarrow \wp(\mathcal{E^*})$
これだけ「Eventの列」の集合を抽象要素として扱う
### Abstract Traces
$L$をプログラムラベルの集合とする(CFGのノード=BasicBlock単位と思って良い)
- Domain $a \in Traces^{\sharp }:L\rightarrow\mathcal{M}^\sharp\times \mathcal{C}^\sharp\times \mathcal{E}^\sharp$
- concretize $\gamma : Traces^\sharp \rightarrow \wp(Traces)$
$l\in L,a\in Traces^\sharp$に対し、$a(l)$の抽象メモリ、抽象キャッシュ、抽象イベント列に対応する要素をそれぞれ$a^\mathcal{M}(l),a^\mathcal{C}(l),a^\mathcal{E}(l)$で表記する
<details><summary>このように抽象化できる根拠</summary>
$Traces$は遷移・イベント列全体の集合
$$
Traces \subseteq (\mathcal{M}\times\mathcal{C})\times (\mathcal{E} \times(\mathcal{M}\times\mathcal{C}))^*\\
Traces=\{\sigma_0e_0\sigma_1...\sigma_n\ |\ n < \infty\ \land\ (\sigma_k,e_k,\sigma_{k+1})\in \mathcal{T})\}
$$
Tracesの各要素に対し、次に実行される機械語のlocation $\sigma_n.m.pc$を加えても等価
$$
Traces \subseteq (L \times (\mathcal{M}\times\mathcal{C})\times (\mathcal{E} \times(\mathcal{M}\times\mathcal{C}))^*)\\
Traces=\{(l,\sigma_0e_0\sigma_1...\sigma_n)\ |\ n < \infty\ \land\ (\sigma_k,e_k,\sigma_{k+1})\in \mathcal{T}\ \land\ \sigma_n.m.pc = l \in L\}
$$
ただし、$L$は各命令のlocationの集合
この直積は写像に変換できて(ISA 4章)、
$$
Traces : L \rightarrow \wp((\mathcal{M}\times\mathcal{C})\times (\mathcal{E} \times(\mathcal{M}\times\mathcal{C}))^*)\\
$$
つまり、$Traces(l)$はラベル$l$に到達するまでにあり得る実行パスの集合を返す
1. 解析にはイベント列の情報があれば良いので、最新以外の状態を落とす
$$
Traces^{1\sharp} : L \rightarrow \wp ((\mathcal{M}\times\mathcal{C}) \times \mathcal{E}^*)\\
$$
2. $(\mathcal{M}\times\mathcal{C} \times \mathcal{E}^*)$の組み合わせ指定の制約を緩める(independentにする)
$$
Traces^{2\sharp} : L \rightarrow \wp (\mathcal{M})\times\wp(\mathcal{C}) \times \wp(\mathcal{E}^*)\\
$$
3. 各ドメインを抽象化する(完成)
$$
Traces^{\sharp }:L\rightarrow\mathcal{M}^\sharp\times \mathcal{C}^\sharp\times \mathcal{E}^\sharp
$$
:::info
直感的な理解
ラベル$l$、$a\in Traces^\sharp$に対し、$a(l)$はラベル$l$に到達したときの
- あり得るメモリ状態の集合の過大近似
- あり得るキャッシュ状態の集合の過大近似
- あり得るイベント列の集合の過大近似
のタプルを返す
:::
説明のため$L$をprogram locationとしたが、実際にはCFGノード単位で良い
</details>
### Concretize Function
ラベル$l$に対し、末尾状態のラベルが$l$となるようなPath集合を返す関数$\gamma_L:L\rightarrow \wp(Traces)$を定義
- 実際にはこんな関数作れないはずなので、恐らく定義のための方便
これを使うと、$a\in Traces^\sharp$の具体化$\gamma(a)$は次のように定義できる
$$
\gamma(a) = \{\sigma_0e_0...\sigma_n\ |\
\forall i\leq n,\ \forall l\in L:\\
\sigma_0e_0...\sigma_i \in \gamma_L(l) \implies \sigma_i.m\in \gamma_\mathcal{M}(a^\mathcal{M}(l))\ \land\ \sigma_i.c\in \gamma_\mathcal{C}(a^\mathcal{C}(l))\ \land\ e_0e_1...e_i\in \gamma_\mathcal{E}(a^\mathcal{E}(l))\}
$$
これ自体はIncrementalに構成できる
が、実際には$a$から出せるサイズに興味があるのでこれは使わないはず
```python=
def concretize(a):
S = {EntryLabel}
R = S
while S is not empty:
trace = s.pop()
for m,c in concretize_m(a(l)), concretize(c(a(l))):
if trace.events + hit in concretize_e(e(a(l))):
new = trace + hit + (m,c)
S.push(new)
R.push(new)
elif trace.events + miss in concretize_e(e(a(l))):
new = trace + miss + (m,c)
S.push(new)
R.push(new)
return R
```
### Abstract Next Function
$next$の抽象化は、各抽象ドメインの$next^\sharp$のタプル
$$
next^\sharp: Traces^\sharp \rightarrow Traces^\sharp\\
next^\sharp(a) = \lambda l.(next_{\mathcal{M}^\sharp}(a,l),next_{\mathcal{C}^\sharp}(a,l),next_{\mathcal{E}^\sharp}(a,l))
$$
各抽象ドメインでの$next^\sharp$の構成は後述
### Abstract Join
論文中には出てこなかったが、$next^\sharp$の定義から考えると、以下の式が自然
$$
(m_1^\sharp,c_1^\sharp,e_2^\sharp)~\sqcup^\sharp~(m_2^\sharp,c_2^\sharp,e_2^\sharp) = (m_1^\sharp\sqcup^{\mathcal{M}^\sharp} m_2^\sharp ,
c_1^\sharp\sqcup^{\mathcal{C}^\sharp} c_2^\sharp,
e_2^\sharp \sqcup^{\mathcal{E}^\sharp} e_2^\sharp)
$$
### Local Abstract Next Function
上述の$next_{\mathcal{M}^\sharp}(a,l),next_{\mathcal{C}^\sharp}(a,l),next_{\mathcal{E}^\sharp}(a,l)$はどのように構成できるか?
#### Transition on CFG
$succ:L\rightarrow L$を以下のように定義
直感的には、それぞれCFG上で$l$の次のラベルの集合、前のラベルの集合
$$
succ(l) = \{k\ |\ next(\gamma_L(l))\cap \gamma_L(k) \neq \emptyset \}\\
pred(l) = \{k\ |\ next(\gamma_L(k))\cap \gamma_L(l) \neq \emptyset \}
$$
<img src=https://i.imgur.com/YS7XNrw.png width=300mm>
#### Abstract Memory Update
抽象メモリのUpdate/Effect Function
$$
upd_{M^\sharp,(k,l)} : \mathcal{M}^\sharp \rightarrow \mathcal{M}^\sharp\\
eff_{M^\sharp,(k,l)} : M^\sharp \rightarrow \wp(\mathcal{E}_\mathcal{M})
$$
- CFG上で遷移先は一意でないので、メモリのupdate関数は親ラベル$k$と子ラベル$l$に依存する
- Effectは、アクセスされうるブロックの集合を返す
#### Abstract Cache Update
抽象キャッシュのUpdate/Effect Function
$$
upd_{C^\sharp} : \mathcal{C}^\sharp \times \wp(\mathcal{E}_\mathcal{M}) \rightarrow \mathcal{C}^\sharp\\
eff_{C^\sharp} : \mathcal{C}^\sharp \times \wp(\mathcal{E}_\mathcal{M}) \rightarrow \wp(\mathcal{E})\\
$$
- キャッシュのupdateはアクセスされるブロックのみに依存する
#### Abstract Sequence of Event Update
$$
upd_\mathcal{E} : \mathcal{E}^\sharp\times \wp(\mathcal{E}) \rightarrow \mathcal{E}^\sharp\\
$$
#### Local Abstract Next: Memory
メモリのAbstract Nextは次で定義できる
$$
next_{\mathcal{M}^\sharp}(a,l) = \bigsqcup_{k \in pred(l)}^{\mathcal{M}^\sharp} upd_{\mathcal{M}^\sharp,(k,l)}(a^\mathcal{M}(k))
$$
<img src=https://i.imgur.com/8wwBhyZ.png width=500mm>
1. $a^\mathcal{M}$から、遷移先にラベル$l$をもつような抽象メモリを抽出
1. 抽出した各抽象メモリで、$upd_M,(k,l)$を適用する
1. 得られた新しい抽象メモリ全てをjoin
#### Local Abstract Next: Cache
CacheのAbstract Nextは次で定義できる
$$
next_{C^\sharp}(a,l) = \bigsqcup_{k \in pred(l)}^{\mathcal{C}^\sharp}upd_{\mathcal{C^\sharp}}\left(a^\mathcal{C}(k),eff_{\mathcal{M}^\sharp,(k,l)}(a^\mathcal{M}(k))\right)
$$
<img src=https://i.imgur.com/FbBDxws.png width=500mm>
1. $a^\mathcal{C},a^\mathcal{M}$から、遷移先にラベル$l$をもつような抽象キャッシュ、抽象メモリを抽出
2. 抽出した抽象メモリに$eff_{M,(k,l)}$を適用し、アクセスされうるブロック集合を出す
3. 1で得た抽象キャッシュと2で得たブロック集合から、$upd_C$を適用し、新たな抽象キャッシュを出す
4. 新たな抽象キャッシュ全てをjoin
### Soundness
$upd_{\{\mathcal{M},\mathcal{C},\mathcal{E}\}},eff_{\{\mathcal{M},\mathcal{C}\}}$を健全に実装できれば全体も健全になる
### Abstract Domain
#### Value Abstract Domain
VariableからValueへのmapping
$$
V^\sharp = \wp(V) = Interval\ |\ FSet\ |\ Relational
$$
- $Interval$ 区間抽象
- $FSet$ 有限集合(要素数が規定値を超えると区間抽象に変換)
- $Relatinal$
#### Memory Abstract Domain
メモリ抽象ドメインの要素は、Address,Registerから値抽象への写像
$$
m^\sharp \in \mathcal{M}^\sharp = \mathcal{A} \rightarrow V^\sharp
$$
#### Flag Abstract Domain
x86の条件分岐はフラグレジスタによって判定される
(通常の)レジスタ間の関係がフラグレジスタによって隠蔽される
→ 分岐によるフィルタがうまくいかない
高レベル言語
```clike
if(x < y)
then{
some operations
}
else{
some operations
}
```
- then節 `x<y`が成立
- else節 `x>=y`が成立
条件分岐によって変数間の関係を簡単に表現できる
同様に考えると・・・
x86バイナリ
```clike
cmp rax rdx // compute rax-rdx and update flag register
ja Label // jump above = goto Label if CF=0 && ZF=0
```
上のコード片において、
- Jump Edgeでは `rax - rdx > 0`が成り立つ
- Fallthrough Edgeでは `rax - rdx <= 0`が成り立つ
区間抽象化で、`rax=[0,20], rdx=[5,15]`を仮定すると、
- Jump Edgeでは`rax=[5,20],rdx=[5,15]`
- Fallthrough Edgeでは`rax=[0,15],rdx=[5,15]`
が成立すると期待できるが、愚直に実装するとうまくいかない
##### 例
- うまくいかないパターン(フラグレジスタを0/1の値として扱う)
- cmp命令によりCF,ZF命令は`[0,1]`両方の値を取り得る
- jaはフラグレジスタを以下のようにフィルタする
- Jump Edgeでは CF=0かつZF=0
- Fallthrough EdgeではCF!=0またはZF!=0
- フラグレジスタをフィルタしても欲しい関係`rax - rdx > 0`が得られない
このやり方では、rax/rdxレジスタの値をフィルタできないため、精度が低下する
解決策→ フラグレジスタの組み合わせとフィルタ結果の対応付けを保持する
- `cmp rax rdx`を解釈したとき、以下の組み合わせを保持する
- CF=0/ZF=0 `rax=[5,20],rdx=[5,15]`
- CF=0/ZF=1 `rax=[5,15],rdx=[5,15]`
- CF=1/ZF=0 `rax=[0,15],rdx=[5,15]`
- CF=1/ZF=1 bottom(たぶんあり得ない)
- `ja`を解釈
- Jump Edgeでは、CF=0/ZF=0のときの制約を採用
- Fallthrough Edgeでは、その他3つの制約のjoinを採用
- Edgeごとに値を適切にフィルタリングできる
#### Stack Abstract Domain
抽象メモリドメインからスタックを分離
Interprocedualな解析を高精度で実現
#### Cache Abstract Domain
キャッシュ抽象ドメインの要素は、ブロックから値抽象への写像
$$
c^\sharp \in \mathcal{C}^\sharp = \mathcal{B} \rightarrow V^\sharp
$$
- Precisionのため、Reductionを行う
- 具体化して、あり得ないageの組み合わせは削除
#### Trace/Time Abstract Domain
#### Overall module
<img src=https://i.imgur.com/xd3CEWf.png>
実装見ても全体像はイマイチ掴めませんでした
## 5.Tool Design And Implementation
### CFGの構築
- x86バイナリからCFGを構成
- ノードはBasic Block単位
- Chlipalaによるパーサを利用 [Chlipala 2006]

CFGの例
:::warning
indirect jumpがあるとCFGを作れないので、これを含むバイナリ対象外
:::
### Iteration
- 愚直に$F^\sharp$の計算を繰り返すのは効率が悪い
- 遅い
- 収束しないかも/Wideningし過ぎで精度が落ちる
- 解決策
- 走査順を工夫する
- Wideningする場所を適切に決める
### Efficient chaotic iteration strategies with widenings
By Bourdoncle[1993]
#### Weak Topological Orderで整列
:::info
**Topological Sort**
有向非巡回グラフ上でのノードの順序づけ
子は全ての親より後ろにいる、が全てのノードについて保証

は有向非巡回グラフで、トポロジカルソートできる
- 例 1 2 8 3 4 7 5 6
- 例 1 2 3 4 5 6 7 8
**Weak Topological Order**
上の定義を有効グラフ全体に拡張

は巡回「3 4 7」があるのでトポロジカルソートできない
7から3にFeedbackがあるよ、というのを許容するために
- 例 1 2 8 (3 4 7) 5 6
のように表記する
括弧で括られた単位をComponentと呼ぶ
直感的には、括弧内の要素はその先頭へのFeedbackをもっていい、といえそう
:::
WTOはTarjanのアルゴリズムを少し改造すると求められる
- 概要:何度もDFSして強連結成分をたくさん求める
##### アルゴリズム
各ノードは三種類でラベル付けされる
- 未探索(Value:0)
- 探索中(Value:ルートからの深さ)
- 探索済(Value:無限大)
1. DFSで走査する
- 行きがけに探索中、帰りがけに探索済みのラベルを貼る
3. ノード訪問時の動作
- 探索済でない子がある
- そのラベルが未探索なら、探索を続ける
- そのラベルが探索中なら、その子のラベルを記録(ループの発見)
- 全ての子が探索済
- 記録したラベルがない
- ノード番号を出力にpush
- 記録したラベルがある
1. それらのラベルのうち、最も若いノードまで戻る
1. 現在のラベル・戻りがけのラベルを未探索にし、戻った先のラベルを探索済にする
3. 閉じ括弧を出力にpush
4. 戻ったノードの未探索の子をRootとしてDFSを再開
5. 全ての子でDFSが終わったとき、開き括弧をpush
一度Visitしたノードを未訪問に戻すことで最大でない強連結成分も得られる
計算量はおそらく$O(V^2)$
##### 例
<details><summary>初期状態</summary>

</details>
<details><summary>1,2,3,5,6で探索</summary>

6は子がないので、出力
- 「6」
</details>
<details><summary>4の探索で、FeedbackEdgeを見つける</summary>

</details>
<details><summary>2まで戻り、3から再開</summary>

</details>
<details><summary>3,5,4で探索して、FeedBackEdgeを見つける</summary>
<span style="color:red">誤植: 3,5,4の肩のラベルはそれぞれ2,3,4</span>

</details>
<details><summary>3まで戻り、5から再開</summary>

</details>
<details><summary>4,5と探索</summary>
<span style="color:red">誤植: 5,4の肩のラベルはそれぞれ2,3</span>

4,5ともに探索済でない子をもたないので、出力

出力:「5 4 6」
</details>
<details><summary>3に戻る</summary>

ここで3を起点としたDFSが終わる
出力「(3 5 4) 6」
</details>
<details><summary>最終状態</summary>
2を起点としたDFSも終わり、最後1に戻って終了

最終的に、出力:「1 (2 (3 5 4)) 6」を得る
これはWTOである
</details>
### 問題
以下のCFGでWTOを構成したい。

<details><summary>最初+問1</summary>

- 1〜8をVisitする
- 8に子がないので、出力「8」
- 帰りがけの7でFeedBackEdge 3を見つける
問1. 3まで戻るとき、それぞれのラベルはどのように更新されるか?
</details>
<details><summary>問2の回答+問3</summary>
ラベルは次のように更新され、4から探索を再開

4,5,6,7とDFSするとする
<span style="color:red">誤植: 4,5,6,7の肩のラベルはそれぞれ3,4,5,6</span>

7には未探索でない子がないので、出力「7 ) 8」

問3. 7の探索が終わったので、6に戻る
6の探索によってラベルはどのように更新されるか?
ヒント:「探索済でない」子を探す

</details>
<details><summary>問3の解答+問4</summary>
- FeedBack Edge 5が見つかるので、5まで戻る
<span style="color:red">誤植: 4の肩のラベルは3</span>

- 6から探索を再開するが、6には子がないので、出力「6 ) 7 ) 8」

- 5の子を全て探索したので、1つのDFSが終わる
- 問題:出力はどのように更新されるか?
前:「6 ) 7 ) 8」
解:?
</details>
<details><summary>問4の解答+最後まで</summary>
出力「(5 6) 7) 8」

- 4と3を順に探索して、3の子を探索していたDFSも終わる
出力「(3 4 (5 6) 7) 8」
- 2、1も探索済みでない子がないので、順に出力
出力「1 2 (3 4 (5 6) 7) 8」
これはこのCFG上のWTOである
</details>
#### Iterative Strategy
- WTOのComponentは強連結成分の単位
- つまりループ
- Componentの先頭へのEdgeに対し、Wideningを使うことで収束性を保証
- 最も外側のComponentを収束するまで反復
- 中身はいちいち反復しない
```python=
env = map(BasicBlock to AbstractElement)
while wto is not empty:
label = wto.popleft()
# if find scc, start iterate.
if label is head of scc:
labels = scc
# iterate until all elements in scc are stable
while not labels.all_stable():
for l in labels:
new_envs = interpret(env[label]) # set of abstract elements
for next_l in l.succ:
# propagate
if next_l is widening_point:
env[next_label] = widen(new_envs[next_label],env[next_label])
else:
env[next_label] = join(new_envs[next_label],env[next_label])
else if label is not part of scc:
new_envs = interpret(env[label]) # set of abstract elements
# propagate
for next_label in label.succ:
env[next_label] = join(new_envs[next_label],env[next_label])
else:
env.update(bb)
```

- 基本は左から右
- SCC内のみ何度も反復する
- FeedbackEdgeでWidening
### Cache Model
- パラメータ
- Cache Size
- Line Size
- Associativity
- Replacement Policy
- LRU
- FIO
- PLRU
- Write through/no allocate
- write hit -> メインメモリにも書き込み
- write miss -> 書いたデータはキャッシュに読み込まない
## Evalutation
### AES(Polar SSL)
- キャッシュの設定によって、Leakageにどれほど差があるか比較

- Preloading
- ルックアップテーブルのプリロードはLeakの減少に有効
- ただし、キャッシュサイズがテーブルよりも小さいと効果が落ちる
- Line Size
- アクセスベースの攻撃者に対して、大きなラインサイズは有効
- Replacement Policy
- アクセスベースの攻撃者に対して、FIFOが有効
- FIFOのキャッシュヒットからは情報をほとんど得られないため
- Associativity
- Cache Size
- Key Size
## Discussion
### 流出量上限の精度
- この上限は正確ではなく、悲観的な予測を示す
- 静的解析によるOverApproximation
- 流出した情報量 → Secret復元の可能性が上がる
- 理論上の話であって、計算量の話は考えていない
- 健全性と完全性
- 上限が小さいとき、SystemがSecureであることを証明
- 上限が大きいことは、SystemがInsecureであることを示すわけでない
- 異なる2つのSystemの比較に用いることはできない
- 以下の2つを比較すると、実際には前者がよりSecure
- CacheAudit「上限は2bit」& 攻撃者「1bitもわからない」
- CacheAudit「上限は1bit」& 実際「1bitは分かる」
### 不完全なモデル化
- 仮定したモデルに対してのみ有効な結果である
- 複数回の実行
- 単一の実行を仮定
- 複数回の実行を考慮すると上限は変わる可能性がある
- 初期キャッシュ状態
- モデルでは初期状態が空を想定
### Modern Microarchitectureの複雑性(Future Work)
高速化のため、最近のハードウェアはとにかく複雑
CacheAuditは以下の要素をモデルに組み込んでいない
- L2/L3キャッシュ
- L1キャッシュしかモデル化していない
- DRAM
- RAMの読み書きレイテンシは、Accsess Historyによって変わる
- Time-Based adversaryに対するモデル化が適切でない
- 投機実行
- LogicalでないPathも実行され得る
- Out-of-Order実行
- CPUが勝手に命令を並び替える
- Register Renamingとかやって勝手に(命令レベルで)並列化する
- MMU/TLBなどVirtual Memory周り
- Page Walkなどが発生し得る
## Related Work
Cache Side Channelのリスクを低減させる試み
- ハードウェア・OSベース
| 研究 | 対象 | 概要 |
| -------- | -------- | -------- |
| [Tiwari et al. 2011] | ハードウェア | Information-FlowのTrackingを行う |
| [Domnitser et al. 2012] |ハードウェア| 各プロセスが利用可能なCacheLineの本数を制限 |
|[Wang and Lee 2008]|ハードウェア|Replacement PolicyにRandom Algorithmを使う|
|StealthMem [Kim et al. 2012]|OS|VMのPageをキャッシュにLockし、他のVMによりEvictされるのを防ぐ(?)|
|CloudFlow [Baig et al. 2014]| OS | クラウド上でInformation-Control-Layerを設ける? |
## 提案手法との関連
この研究は対象がExecutable
- ほとんどのアドレスが静的に解決できる
- esp/ebp含めレジスタの初期値を決め打ちしてる
- 検体はメモリの動的確保とかしないプログラム
調べた限り、静的Cache解析は静的なアドレス解析に依存
- 特定のプログラムにしか適用できない
- 最新の複雑なCPUモデルに対しては正しくない結果が出る
提案手法は、アドレスに依存せず、最新のCPUモデルに対しても意味のあるCache利用効率の静的解析(になってほしい)
$eff: M \rightarrow B \cup \{\perp\}$
$$
\text{efficiency}_{path}= m_0 e_0 m_1...e_nm_n \mapsto \frac{|\cup e_i|}{count(m_0e_0m_1...)}
$$
$count$は実際に利用した領域の広さ(Byte数)
利用したメモリブロックの個数と実際に使う領域の広さの比を取るとアクセスのSparsityからキャッシュの利用効率を出せないか
- 理論・実装周りで利用する部分
- TraceSemanticsは同様のものを使う
- Iteratorはほぼ同じものを実装する
- パラメータはラインサイズだけになりそう