Secure information flow with random assignment and encryption

Type systems for secure information flow aim to prevent a program from leaking information from variables classified as H to variables classified as L. In this work we extend such a type system to address encryption and decryption; our intuition is that encrypting a H plaintext yields a L ciphertext. We argue that well-typed, polynomial-time programs in our system satisfy a computational probabilistic noninterference property, provided that the encryption scheme is IND-CCA secure. As a part of our proof, we first consider secure information flow in a language with a random assignment operator (but no encryption). We establish a result that may be of independent interest, namely, that well-typed, probabilistically total programs with random assignments satisfy probabilistic noninterference. We establish this result using a weak probabilistic bisimulation. Categories and Subject Descriptors F.3.1 [Logics and Meanings of Programs]: Specifying and Verifying and Reasoning about Programs--L...

• Type: Conference
• Year: 2006
• Where: CCS
• Authors: Geoffrey Smith
• Keywords: CCS 2006, Probabilistic Noninterference, Secure Information Flow, Security Privacy, Type Systems