Downgrading policies and relaxed noninterference

In traditional information-flow type systems, the security policy is often formalized as noninterference properties. However, noninterference alone is too strong to express security properties useful in practice. If we allow downgrading in such systems, it is challenging to formalize the security policy as an extensional property of the system. This paper presents a generalized framework of downgrading policies. Such policies can be specified in a simple and tractable language and can be statically enforced by mechanisms such as type systems. The security guarantee is then formalized as a concise extensional property using program equivalences. This relaxed noninterference generalizes traditional pure noninterference and precisely characterizes the information released due to downgrading. Categories and Subject Descriptors D.3.3 [Programming Languages]: Language Constructs and Features--Constraints, Data types and structures, Frameworks; F.3.1 [Logics and Meanings of Programs]: Specif...

• Type: Conference
• Year: 2005
• Where: POPL
• Authors: Peng Li, Steve Zdancewic
• Keywords: Extensional Property, General Terms Languages, POPL 2005, Programming Languages, Traditional Information-flow Type