Computationally secure information flow [Elektronische Ressource] / von Peeter Laud

Sujets

• Informatik

Informations

• Publié par: universitat_des_saarlandes
• Publié le: 01 janvier 2004
• Nombre de lectures: 9
• Langue: English
• Poids de l'ouvrage: 1 Mo

Extrait

Computationally Secure Information Flow
Dissertation
Zur Erlangung des Grades eines
Doktors der Ingenieurwissenschaften (Dr.-Ing.)
der Naturwissenschaftlich-Technischen Fakultat I
der Universitat des Saarlandes
von
Peeter Laud
Saarbrucken
April, 2002ISBN 9985-78-703-X
Tag des Kolloquiums: 16.09.2002
Dekan: Prof. Dr. Philipp Slusallek
Gutachter: Prof. Dr. Reinhard Wilhelm
Prof. Dr. Birgit P tzmann
Vorsitzender: Prof. Dr. Harald GanzingerAbstract
This thesis presents a de nition and a static program analysis for
secure information o w. The of secure information o w is not
based on non-interference, but on the computational independence of
the program’s public outputs from its secret inputs. Such de nition al-
lows cryptographic primitives to be gracefully handled, as their security
is usually de ned to be only computational, not information-theoretical.
The analysis works on a simple imperative programming language
containing a cryptographic primitive|encryption|as a possible opera-
tion. The analysis captures the intuitive qualities of the (lack of) infor-
mation o w from a plaintext to its corresponding ciphertext. We prove
the analysis correct with respect to the de nition of secure information
o w 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.
iiiZusammenfassung
In dieser Dissertation wird eine De nition und eine statische Pro-
grammanalyse fur sicheren Informations u prasen tiert. Die De nition
des sicheren Informations usses basiert nicht auf der Unbeein u bar-
keit, sondern auf der komplexitatstheoretisc hen Unabhangigkeit der of-
fentlichen Ausgaben des Programms von seinen geheimen Eingaben.
Eine solche De nition erlaubt uns, kryptographische Primitiven elegant
zu bearbeiten, weil ihre Sicherheit meistens nur komplexitatstheoretisch
und nicht informationstheoretisch de niert ist.
Die Analyse arbeitet auf einer einfachen imperativen Programmier-
sprache, die eine kryptographische Primitive|Verschlusselung|als eine
moglic he Operation enthalt. Die Analyse gibt die intuitive Eigenschaft
des (nicht vorhandenen) Informations usses von einem Klartext zu dem
entsprechenden Schlusseltext wieder. Wir geben den Korrektheitsbeweis
der Analyse in Bezug auf die obengegebene De nition des sicheren In-
formation usses. Im Beweis nehmen wir an, da die Verschlusselungs-
primitive die Identitat der Klartexte und Schlussel versteckt.
Diese Dissertation behandelt auch den Fall, da die Verschlusse-
lungsprimitive die Identitat der Klartexte und Schlussel nicht versteckt,
d.h. da man aus zwei Schlusseltexten moglic herweise heraus nden kann,
ob die entsprechenden Klartexte gleich sind oder nicht. Wir geben eine
Analyse auch fur diesen Fall an, obwohl sie nicht auf ganze Program-
me anwendbar ist, da wir keine Schleifen analysieren konnen. Mit Hilfe
dieser Analyse kann man feststellen, ob zwei formale Ausdrucke (die
gleichwertig zu der Ausgabe der Programme ohne Schleifen sind) glei-
che Interpretation als Bitfolgen haben.
iiiivExtended Abstract
When is a program safe to run? One aspect of safety is con den tiality, which arises
when the inputs and outputs of the program are partitioned into several di eren t
security classes. Typically, some inputs of the program may be public and some
con den tial; some outputs of the program may become public and some remain
private. In this case one wants the to have secure information ow | one
wants that nothing about the con den tial inputs of the program can be deduced
by observing the public outputs.
A standard tool for keeping information con den tial is encryption. A ciphertext
must not reveal the corresponding plaintext to someone that does not have the key.
Theoretically, this hiding of information is not absolute (at least when the encryp-
tion key is shorter than the plaintext), though, someone with (unrealistically) high
computing power may be able to uncover the plaintext from only the ciphertext.
In this thesis we present a de nition for secure information o w that considers
a program to be secure if no reasonably powerful attacker can learn something
about the secret inputs of the program by only observing its public outputs. Such
computational security contrasts with most of de nitions proposed earlier, which
assert information-theoretical security, requiring that no attacker at all (irrespective
of its power) can deduce something about the secret inputs from public outputs.
Cryptology is the branch of computer science where the de nitions stating the
inability of reasonably powerful adversaries are common. Our de nition of secure
information o w also has cryptographic nature. The main notion used in the de ni-
tion is that of independence. Classically, two random events are independent if the
probability that the rst one happens is the same no matter whether the second one
has happened or not. When we are talking about the events happening, then we
always assume that it is easy to gure out, whether the event has indeed happened
or not. For example, we do not consider events like\formulaX is satsi able" , where
X is a random formula of the propositional calculus.
In computational independence, there may be a di erence of the probabilities
of the rst event happening, depending on whether the second event happens or
not, but this di erence must be negligible. If we had not required the outcomes
of events to be explicit, then the de nition of computational independence would
have been more complex (the negligibility of the di erence of probabilities would
still have been su cien t, but no longer necessary). The notion of independence
also generalises to the case, where the rst and the second event can have more
voutcomes than just two (either happening or not). We de ne a program to have
computationally secure information o w, if its public outputs are independent of
its secret inputs.
In this thesis we also present a static program analysis for secure information
o w. The concrete semantics of the program is de ned to be a mapping over the
probability distributions of program states | the program transforms the proba-
bility distribution of its inputs to the probability distribution of its outputs. We
abstract the probability distributions over program states by pairs of sets of pro-
gram variables | if (X; Y ), where X and Y are sets of variables, belongs to the
abstraction of a distribution over program states, then the values of variables in X
are independent from the values of variables in Y in this distribution. The abstract
semantics (i.e. the analysis) is a mapping over the set of pairs of sets of program
variables. Given an abstraction of the probability distribution of program’s inputs,
the abstract semantics maps it to an abstraction of the probability distribution of
the program’s outputs.
Note that formally there can be several di eren t abstractions of the same prob-
ability distribution | if the values of the variables in X are independent of the
values of the variables in Y , then the pair (X; Y ) can either belong or not belong
to the abstraction of that distribution. On the other hand, if the values of the
variables in X are not independent from the values of the variables in Y , then the
pair (X; Y ) certainly cannot belong to the abstraction of that distribution. We see
that there exists a best abstraction of a distribution | it is the abstraction that
contains all pairs (X; Y ) that it can correctly contain. \Program analysis is allowed
to err on the safe side" | given the best abstraction of the probability distribution
of the program’s inputs, the abstract semantics maps it to an abstraction of the
probability distribution of the program’s outputs, but not necessarily to the best
abstraction. Finding the best abstraction of the distribution of program’s outputs
is in general uncomputable, therefore we have to be content with a possibly sub-
optimal abstraction. Now the aim is to get an abstraction that is still\good enough"
and we believe that the analysis that we have devised gives such an abstraction.
This analysis assumes that the encryption operation satis es some rather strong
(but still totally realistic) security properties. Namely, given two ciphertexts it must
be impossible to nd out whether their underlying plaintext is the same or not (note
that for satisfying this property, the encryption operation cannot be deterministic)
and whether they are created with the same key or not. The encryption operations
with such properties are usually constructed from simpler, \primitive" op
that themselves satisfy some weaker security properties. Mostly, these primitive op-
erations are considered to be pseudorandom permutations, i.e. they are assumed to