Adversaries and Information Leaks (Tutorial)

Secure information flow analysis aims to prevent programs from leaking their H (high) inputs to their L (low) outputs. A major challenge in this area is to relax the standard noninterference properties to allow “small” leaks, while still preserving security. In this tutorial paper, we consider three instances of this theme. First, we consider a type system that enforces the usual Denning restrictions, except that it specifies that encrypting a H plaintext yields a L ciphertext. We argue that this type system ensures security, assuming strong encryption, by giving a reduction that maps a noninterference adversary (which tries to guess which of two H inputs was used, given the L outputs) to an IND-CPA adversary (which tries to guess which of two plaintexts are encrypted, given the ciphertext). Second, we explore termination leaks in probabilistic programs when typed under the Denning restrictions. Using a notion of probabilistic simulation, we show that such programs satisfy an app...

• Type: Conference
• Year: 2007
• Where: TGC
• Authors: Geoffrey Smith
• Keywords: Applied Computing, Denning Restrictions, Standard Noninterference Properties, TGC 2007, Usual Denning Restrictions