Room 206 (2nd floor, badged access)
28 avril 2023 - 11h00
An information flow logic based on partial equivalence relations
par Thomas Jensen de 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.
