Room 206 (2nd floor, badged access)
28 April 2023 - 11h00
An information flow logic based on partial equivalence relations
by Thomas Jensen from INRIA
Abstract: Information flow control (IFC) is a key element for ensuring that programs do not leak confidential data, and a number of enforcement mechanisms (based on static analysis, run-time monitoring, or combinations thereof) have been proposed. In this talk we will present a logic for reasoning about information flow properties formalised in an assertion language based on partial equivalence relations. The logic is a relational program logic dedicated to proving PER-based information flow properties but general enough to incorporate classical Hoare logic. The talk will present examples of the verification of complex IF properties that illustrate the expressiveness of the logic.
