Applying Cryptography’s Real/Ideal Paradigm to PL Security

Abstract

The Real/Ideal Paradigm is the standard approach for defining security in theoretical cryptography. In this paradigm, the real and ideal worlds are parameterized by an adversary with certain powers of observation or corruption. The real world is a model of an actual protocol/system. The ideal world consists of an ideal functionality with the same API as the real world, but which is connected with a simulator whose job is to try to convince the adversary it is interacting with the real world, but where the simulator must work with the limited information leaked to it by the ideal functionality. If the adversary can only tell the difference between the real and ideal worlds with negligible probability, we say the real world is secure.

Beginning with a paper I presented at PLAS'14, I’ve been arguing in favor of using the real/ideal paradigm for defining security in a programming languages context, even when systems are entirely non-probabilistic. E.g., even though a system might be implemented using information flow control, its definition of security could be given using the real/ideal paradigm. I will illustrate this approach using the two party game Battleship, giving a definition of when one player is secure against a possibly malicious opponent, and showing two secure implementations, one using information flow control (Haskell/LIO), and one using access control in Concurrent ML.