Description
Date depot: 4 mars 2021
Titre: Static Analysis for Security Properties of Software by Abstract Interpretation
Directeur de thèse:
Antoine MINE (LIP6)
Domaine scientifique: Sciences et technologies de l'information et de la communication
Thématique CNRS : Modèles de calcul, preuve, vérification
Resumé: 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. The methods are mature enough to handle complex programs in real-life languages, such as C, and provide sound and precise answers, scaling to industrial-code sizes. 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 static analyses are taint analyses that either ignore implicit flows or program values. The research will leverage abstract interpretation and the domains proposed for safety to improve sound semantic taint analysis. 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. This novel notion may be related to the concept of responsibility analysis, proposed earlier by P. Cousot. The PhD will first develop a proper semantic formalization, and then new abstractions to achieve a sound static analysis. The intended work will include a theoretical side: developing abstractions for security properties and proving formally their soundness in the framework of abstract interpretation. It will also include a practical side: implementing the analysis of selected security properties and validating their benefit experimentally. The implementation will be included in the Mopsa open-source static analysis platform that the team is developing. The experimental validation should show the benefit of the proposed methods in the context of the analysis of small but realistic and relevant security-related C codes.
Doctorant.e: Parolini Francesco