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.

错误:搜索内容不能为空,请输入英文关键词
错误:关键词超出字数限制,请精简
高级检索

Noninterference Through Bisimulation

  • April Tune,
  • Wendy Yang,
  • G. A. Kavvos

摘要

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.