Cryptographically-Masked Flows
Aslan Askarov (Chalmers University of Technology), Daniel Hedin (Chalmers University of Technology) and Andrei Sabelfeld (Chalmers University of Technology)
Abstract
Cryptographic operations are essential for many security-critical systems. Reasoning about information flow in such systems is challenging because typical (noninterference-based) information-flow definitions allow no flow from secret to public data. Unfortunately, this implies that programs with encryption are ruled out because encrypted output depends on the secret inputs: the plaintext and the key. However, it is desirable to allow flows arising from encryption with secret keys provided that underlying algorithm is strong enough. In this paper we conservatively extend the noninterference definition to allow safe encryption, decryption, and key generation. To illustrate the usefulness of this approach, we define a small imperative language with primitive cryptographic operations and suggest a type system that guarantees noninterference. The type system prevents dangerous program behavior (e.g., giving away a secret key or confusing keys and non-keys), which we exemplify with secure implementations of cryptographic protocols. Because the model is based on a standard noninterference property, it allows us to develop some natural extensions. In particular, we consider public-key cryptography and integrity, which accommodate reasoning about primitives that are vulnerable to chosen ciphertext attacks.