An information-flow analysis views a program as a system that processes “high security” secret information, e.g. passwords; but sometimes programs’ treatment of secrets can be correlated to observed behaviour, or other data of “low security”. Those programs then “leak” information when an adversary can infer something about the “high security” secret by using their knowledge of the program code, and observing real-time behaviours such as control flow, timings, or low- security correlations. In such programs verification usually entails quantifying the amount of information that the program leaks. Interestingly, some inputs are more vulnerable than others and an important goal of such formal analysis is to identify which inputs are most vulnerable.

In this talk I shall explain how to specify leakage bounds on programs that can be verified directly using a logic of information leakages. The leakage logic is based on the g-leakage framework for analysing quantitative security propeties; importantly verification steps are similar to the backwards reasoning in standard functional verification.