Computationally secure information flow

Abstract

This thesis presents a definition and a static program analysis for secure information flow. The definition of secure information flow is not based on non-interference, but on the computational independence of the programs public outputs from its secret inputs. Such definition allows cryptographic primitives to be gracefully handled, as their security is usually defined to be only computational, not information-theoretical. The analysis works on a simple imperative programming language containing a cryptographic primitive encryption as a possible operation. The analysis captures the intuitive qualities of the (lack of) information flow from a plaintext to its corresponding ciphertext. We prove the analysis correct with respect to the definition of secure information flow described above. In the proof of correctness we assume that the encryption primitive hides the identity of plaintexts and keys. This thesis also considers the case where the identities of plaintexts and keys are not hidden by encryption, i.e. given two ciphertexts it may be possible to determine whether the corresponding plaintexts are equal or not. We also give an analysis for this case, though it is not a whole program analysis. Namely, we cannot analyse loops. Nevertheless, with the help of the analysis one can check, whether two formal expressions (which are equivalent to the output of programs without loops) have indistinguishable interpretations as bit-strings.

In dieser Dissertation wird eine Definition und eine statische Programmanalyse für sicheren Informationsfluss präsentiert. Die Definition des sicheren Informations usses basiert nicht auf der Unbeeinflußbarkeit, sondern auf der komplexitätstheoretischen Unabhängigkeit der öffentlichen Ausgaben des Programms von seinen geheimen Eingaben. Eine solche Definition erlaubt uns, kryptographische Primitiven elegant zu bearbeiten, weil ihre Sicherheit meistens nur komplexitätstheoretisch und nicht informationstheoretisch definiert ist. Die Analyse arbeitet auf einer einfachen imperativen Programmiersprache, die eine kryptographische Primitive Verschlüsselung als eine mögliche Operation enthält. Die Analyse gibt die intuitive Eigenschaft des (nicht vorhandenen) Informationsflusses von einem Klartext zu dem entsprechenden Schlüsseltext wieder. Wir geben den Korrektheitsbeweis der Analyse in Bezug auf die obengegebene Definition des sicheren Informationflusses. Im Beweis nehmen wir an, daß die Verschlüsselungsprimitive die Identität der Klartexte und Schlüssel versteckt. Diese Dissertation behandelt auch den Fall, dass die Verschlüsselungsprimitive die Identität der Klartexte und Schlüssel nicht versteckt, d.h. daß man aus zwei Schlüsseltexten möglicherweise herausfinden kann, ob die entsprechenden Klartexte gleich sind oder nicht. Wir geben eine Analyse auch für diesen Fall an, obwohl sie nicht auf ganze Programme anwendbar ist, da wir keine Schleifen analysieren können. Mit Hilfe dieser Analyse kann man feststellen, ob zwei formale Ausdrücke (die gleichwertig zu der Ausgabe der Programme ohne Schleifen sind) gleiche Interpretation als Bitfolgen haben.