Safe Programming in Finite Precision: Controlling Errors and Information Leaks

Programmation sûre en précision finie : Contrôler les erreurs et les fuites d'informations

Ivan Gazeau (1, 2, 3)

1 PARSIFAL - Proof search and reasoning with logic specifications
2 COMETE - Concurrency, Mobility and Transactions
3 COMETE / PARSIFAL

In this thesis, we analyze the problem of the finite representation of real numbers and we control the deviation due to this approximation. We particularly focus on two complex problems. First, we study how finite precision interacts with differentially private protocols. We present a methodology to study the perturbations on the probabilistic distribution induced by finite representation. Then we show that a direct implementation of differential privacy protocols is not safe while, with addition of some safeguards, differential privacy is preserved under finite precision up to some quantified inherent leakage. Next, we propose a method to analyze programs that cannot be analyzed by a compositional analysis due to ''erratic'' control flow. This method based on rewrite system techniques allows us to use the proof of correction of the program in the exact semantics to prove the program is still safe in the finite representation.

Dans cette thèse, nous analysons les problèmes liés à la représentation finie des nombres réels et nous contrôlons la déviation induite par cette approximation. Nous nous intéressons particulièrement à deux problèmes. Le premier est l'étude de l'influence de la représentation finie sur les protocoles de confidentialité différentielle. Nous présentons une méthode pour étudier les perturbations d'une distribution de probabilité causées par la représentation finie des nombres. Nous montrons qu'une implémentation directe des protocoles théoriques pour garantir la confidentialité différentielle n'est pas fiable, tandis qu'après l'ajout de correctifs, la propriété est conservée en précision finie avec une faible perte de confidentialité. Notre deuxième contribution est une méthode pour étudier les programmes qui ne peuvent pas être analysés par composition à cause de branchements conditionnels au comportement trop erratique. Cette méthode, basée sur la théorie des systèmes de réécriture, permet de partir de la preuve de l'algorithme en précision exacte pour fournir la preuve que le programme en précision finie ne déviera pas trop.

Mots clés: Finite precision; Static analysis

Mots clés: Précision finie; Analyse statique; Differential privacy

Domaines: Analyse numérique [cs.NA]

Ivan Gazeau. Programmation sûre en précision finie : Contrôler les erreurs et les fuites d'informations. Analyse numérique [cs.NA]. Ecole Polytechnique X, 2013. Français. ⟨NNT : ⟩. ⟨pastel-00913469⟩