Security via Insecurity

             Pasquale Malacaria
          (Queen Mary, University of London)
Any password matching software (unix password checker, cash machine pin
number checker) is, by its own nature insecure.
Confidential information is leaked to the user of these systems at each
use; in the case of a legittimate user (trivial case) that will be the
whole secret (i.e. the password), in the case of an illegittimate one
trying to guess a password it will be either the whole secret (very
unlikely) or (more likely) the information that the secret is not the
one tried (and hence the guessing space is reduced).

The way common sense deals with these insecure systems is by considering
this leakage as "insignificant", i.e. so small that a guesser would need
"on average" an unavailable number of attempts to enter the system.

But what exactly this mean? For example how small would the leakage be
in a program where several passwords could be sharing part of the
secret? Or what is the relation between the way the secrets are
distributed and the amount leaked?
(these questions are related for example to countermeasures for password
cracking software for Unix)

In order to give precise answers to these problems,
we propose a theory to measure the amount of secrecy leaked by a small
imperative language.
The theory is based on Shannon's entropy and relates to the idea of the
average number of attempts needed to guess the secret.

We then develop a program analysis which statically provides a safe
estimate of this leakage in terms of a pair of reals which bounds the
theoretical leakage.

This is a joint work with Sebastian Hunt and David Clark.