Information Exposure by Error Signalling
Début du financement: 15/01/2018
Axe DigiCosme & tâche:ComEx Task 3: Terminal-centric design of networks and SciLex Task 1: Safe and reusable distributed programs
Sujet : Information Exposure by Error Signalling
Directeurs de thèse: Dietmar Berwanger, LSV; Laurent Doyen, LSV; Pascale Le Gall, MICS
Institution : LSV, ENS Paris-Saclay
Doctorant : Mengqi XIE
Productions scientifiques :
Ressources :
Contexte
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.
Objectif scientifique
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.