A Monadic Approach to Relational Verification:
Applied to Information Security, Program Equivalence, and Optimizations
Niklas Grimm (Logics and Computation, Vienna University of Technology, Vienna, Austria)
Kenji Maillard (Prosecco, INRIA, Paris, France)
Cédric
Fournet (Programming Principles and Tools, Microsoft Research, Cambridge, United Kingdom)
Catalin
Hritcu (Prosecco)
Matteo
Maffei (Logics and Computation, Vienna UT)
Jonathan Protzenko
(RiSE: Research
in Software Engineering, Microsoft Research, Redmond, WA, USA)
Tahina Ramananandro (RiSE)
Aseem
Rastogi (Microsoft Research, Bengaluru, Karnataka, India)
Nikhil
Swamy (RiSE)
Santiago
Zanella-Béguelin (Programming Principles and Tools)
- Final version (at the ACM Digital Library)
- Paper preprint
- Submission versions on arXiV
Relational properties describe multiple runs of one or more programs. They
characterize many useful notions of security, program refinement, and
equivalence for programs with diverse computational effects, and they have
received much attention in the recent literature. Rather than developing
separate tools for special classes of effects and relational properties,
we advocate using a general purpose proof assistant as a unifying
framework for the relational verification of effectful programs. The
essence of our approach is to model effectful computations using monads
and to prove relational properties on their monadic representations,
making the most of existing support for reasoning about pure programs.
We apply this method in F* and evaluate it by encoding a variety of
relational program analyses, including information flow control, semantic
declassification, program equivalence and refinement at higher order,
correctness of program optimizations. By relying on SMT-based automation,
unary weakest preconditions, user-defined effects, and monadic
reification, we show that, compared to unary properties, verifying
relational properties requires little additional effort from the F* programmer.