Sec Typeでチェックすべきことの性質を考え直す

[2222-42]

why

Lemma 9.12 (Anti-monotonicity)と

Concrete Semantics p.130の以下の記述とで不一致を感じてしまったから。

Checking for explicit
flows, i.e., assignments from high to low variables, is easy.For implicit flows,
the main idea of the type system is to track the security level of variables
that decisions are made on, and to make sure that their level is lower than or
equal to variables assigned to in that context.