This project chooses information flow analyses (henceforth IFA for short)
as the PA topic this project will focus, out of many possible PAs.
Flow analyses are central to various PA techniques, including control flow, i.e. how a thread of activation runs through program
points, or a data flow, i.e. how a datum flows through a program
text. IFA integrates these two kinds of traditional flow analyses, and
is a fundamental part of secrecy analysis, which intuitively
ensures the lack of leakage of information from a given program, the
concern which goes back to the early work by Lampson and
Denning&Denning [20]. As a very simple
example, consider a call-by-value 
-term
is a function from integers to integers
and ``
'' denotes a multiplication. The result of evaluating this
term can be either 
times 
(if 
terminates) or divergence
(if diverges). Thus both control flow
and data flow exist from to the result, which are together counted
as information flow. But if always
terminates, there is only a data flow: and, in
, there is only a control flow from to the result.
IFA is essential for secrecy analysis because, in practice,
information leakage (which secrecy analysis wishes to preclude) are
generally attributable to the existence of insecure information flow
in a program. Here a flow is insecure if it transmits high-level
(private) information to low-level (public) channels (so if is
high in (1) and the result is low there is insecure flow).
As a practical example, if a user downloaded an applet for calculating
tax payment, the user does not want the applet to reveal her/his
income information to the general public. Thus IFA is a fundamental
instance of PA for software safety, which is one of the basic reasons
why we choose IFA as a central topic of the present project. Another
reason is because IFA integrates two other prominent flow analyses in
PA, control flow analyses and data flow analyses, so that the full
understanding of IFA will directly and indirectly lead to that of
other flow-based PAs.
The final reason is the experience we have accumulated so far in the
fields of IFAs. For a last couple of years
[45,41,46,75,68], we experimented with the
-calculus-based framework to develop secure information flow
analyses for higher-order procedure, general references and
concurrency, presenting a basic paradigm of the use of -calculi
in PAs. Concretely, we first develop IFA for the -calculus
extended with state and concurrency, which is then reflected it onto
programming languages, resulting in a series of type-based IFAs which
are more powerful than the state-of-the-art techniques
[,,,,,]. The correctness of the IFAs for languages is
automatically ensured through their embedding into the -calculus.
The fine-grained type structure of the linear/affine -calculus
plays an essential role in developing the IFA. From our experience, a
general picture of the -calculus-based PAs has emerged, as found
in Figures 1 and 2 at the end of this proposal, The experience gives
us a firm basis for further extensions.
The present project considers one basic extension to this general picture, quantitative secrecy, which is another area of IFA the authors of the present proposal have an expertise in. The traditional secrecy analysis, including our own [45,41,46,75,68], gives us a method to obtain (a safe approximation to) an answer to the following question:
Does a given program incur information leakage?Since we expect a Yes-No answer in such a secrecy analysis, it is generally known as qualitative secrecy. Recently researchers observed that, in practical situations, we need a more fine-grained notion of secrecy, which is often called qualitative secrecy. For example, consider a common bank or credit card which allows the user to withdraw cash from an ATM (Automatic Teller Machine). Usually the secret PIN (Personal Identification Number) is stored in encrypted form on the card itself. However -- even assuming that the encryption method used for encoding the PIN code is effectively unbreakable -- it is impossible to claim that the PIN code (or an application which uses it) is perfectly secure, since each time an incorrect trial by an attacker (who got hold of the card by, say, stealing) can obtain a piece of information. For example, assume that the PIN is a four digit number, then there are less than
possible codes available (as banks usually
exclude certain combinations like 
, etc. as valid PINs).
Every time the thief tries a random number a certain amount of
information about the PIN is revealed. The point is that even though
the chances of success of a trial is low (in the order of 
in
this instance), there is a small amount of information revealed even
if the attacker is ``unlucky'' and the chosen number is rejected.
So, for all practical purposes, the ATM program has only to ensure PINs to be ``approximately secret''. From the viewpoint of program analyses, we wish to have a method which can answer the following more refined question:
How much information leakage does a given program incur?Many practical secrecy examples are best analysed using quantitative secrecy. For example, one of the significant attacks against cryptography includes timing attacks, in which the time a program spends on a certain operation, such as decryption, leads to revelation of information. As shown in [25,26], vulnerability of programs w.r.t. timing attacks can be cleanly understood using quantitative secrecy.
Quantitative secrecy is an emerging field whose leading researchers
include the authors of the present proposal (cf. [55]).
Successful development of this theory in the context of the typed
-calculus would mean scaling its key ideas
to a broad class of language constructs, which has been difficult
so far.
