Noninterference Through Bisimulation
摘要
Noninterference properties state that data does not flow in an undesirable manner, e.g. from a high-security to a low-security setting. Within programming languages noninterference is often enforced through the use of modal type systems. Proving the property often requires non-trivial techniques, such as denotational semantics or logical relations. We show that a simple bisimulation technique (due to Choudhury, Eades, and Weirich) can be adapted to show noninterference for a variety of modal type systems.