Secure information flow with random assignment and encryption

10 years 2 months ago
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...
Geoffrey Smith
Added 20 Aug 2010
Updated 20 Aug 2010
Type Conference
Year 2006
Where CCS
Authors Geoffrey Smith
Comments (0)