Example: Information-flow Control


Verification requires a specification of intended policy.
(We don't have this today, but we can make reasonable assumptions.)


Controlled export (Export)

Consistent export (Export)

Consistent import (Import)

These conditions are difficult to "eyeball" in practice, 
but easy to check with static analysis.