Keynote Speakers

TITLE: Leakage Logic for programs

ABSTRACT: 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.

TITLE: Exploiting incompleteness in software development

ABSTRACT: System development is a dynamic and iterative process that involves refinements and revisions, often resulting in some components being only partially specified. To ensure that the system meets its requirements is essential to have the ability to perform continuous verification after each refinement or revision step. This calls for both models and verification techniques that can effectively handle incompleteness.
In this presentation, I will introduce incomplete models and model-checking techniques designed to address such models. Furthermore, I will show how these techniques can support other steps in the software development lifecycle, including requirements elicitation, design, and specification mining.