Information Exposure by Error Signalling
Axis: ComEx Task 3: Terminal-centric design of networks and SciLex
Subject : Information Exposure by Error Signalling
Thesis Supervisor: Dietmar Berwanger, LSV; Laurent Doyen, LSV; Pascale Le Gall, MICS
Institutions : LSV, ENS Paris-Saclay
PhD : Mengqi XIE
Scientifics productions :
Error handling is one of the most common software vulnerabilities. Information leakage due to detailed error messages is listed in the top of common security weaknesses.
This project is aimed at developing formal methods for the verification and synthesis of error handling mechanisms with the objective of avoiding exposure of private or sensitive data. Towards this, we set up a game-theoretic framework for monitoring the information exposed by signalling events and we adapt techniques from supervisory control theory for constructing error-signalling protocols that avoid information leakage.
Our ultimate goal is to design error messages that expose no sensitive information, but offer yet enough detail to help the user make a reasonable decision, in view of applications to web services and distributed databases.
To develop game-theoretic techniques for the automated design of error handlers that prevent leakage of sensitive information to the user, we pursue the following tasks:
- to set up a formal model for describing the information content of action-failure signals in distributed systems;
- to devise monitoring procedures for diagnosing whether a run exposes sensitive information;
- to develop automated synthesis procedures for supervisory controllers with the ob- jective of avoiding information leakage.
One important challenge is to cover systems that are already in an advanced design phase. In contrast to existing approaches, our methods should not rely on dedicated programming constructs in the specification and implementation of the system, such as, e.g., pre/post-conditions, repair mechanisms, or information filters.
Our general methodology is based on literature from the theory of games on graphs and discrete-event systems.