رئاسـة البـحث : Antoine MINÉ
The goal of the PhD is to develop new sound and semantic static analysis methods based on the theory of abstract interpretation that target security properties.
Static analysis by abstract interpretation has been applied with some success to the verification of safety properties, which concern the absence of run-time errors. However, extending these methods to verify more complex properties while keeping a focus on analyzing realistic languages and maintaining scalability is challenging. In this PhD, we will perform such an extension towards security properties, which are critical to the software industry. A first class of security properties considered will concern information flow, which ensures that an unauthorized user cannot get access to private data. Existing taint analyses either ignore implicit flows or program values. The research will leverage abstract interpretation and the abstract domains proposed for safety to improve sound semantic taint analyses. The research will then consider related extensions, such as formalizing and analyzing declassification, as well as inferring sanitation functions instead of relying on user knowledge. In order to reduce the false alarm rate, output more relevant information and avoid reporting errors unnecessarily, the research will also focus on exploitable errors, that is, errors that can effectively result in an attack. The PhD will study this novel notion in relation to responsibility analyses, proposed récently by P. Cousot. The PhD will first develop a proper semantic formalization, and then new abstractions to achieve a sound static analysis.