Vérification formelle de politiques d'identification et d'accès
Les services cloud, comme Amazon Web Services (AWS), Microsoft Azure ou Google Cloud Platform, hébergerent des données et des services sensibles. L’accès à ces données et services doit être rigoureusement contrôlé pour garantir leur sécurité. Des politiques d’accès (Identity and Access Management1) sont mises en place pour autoriser ou interdire l’accès, selon l’utilisateur, l’action à réaliser, son adresse IP, etc.
Problématique et sujet
Les politiques d’accès deviennent rapidement complexes. L’enchevêtrement des règles d’accès peut conduire à des failles de sécurité qui rendent accessibles des données secrètes, ou exposent indûment des services. Il est donc nécessaire de vérifier automatiquement les politiques d’accès afin de les valider et d’y détecter d’éventuelles failles.
Une approche consiste à encoder les politiques de sécurité en logique des prédicats (first-order logic), puis à utiliser un prouveur SMT pour la validation2. Cette approche est aujourd’hui mise en oeuvre par AWS pour valider les politiques d’accès de différents services3.
L’objectif du projet est de développer un prototype qui reproduit ces approches2. Ce prototype sera développé en Python. Il lira les politiques de sécurité au format JSON4. Il produira un modèle logique au format Z3 SMT Lib5. Puis il utilisera le prouveur Z36 pour valider la politique de sécurité.
Si le temps le permet, des optimisation37 seront implémentées.
Les bases d’exemples8 et9 seront utilisées pour valider le prototype sur une large palette d’exemples. Ils seront utilisés pour créer des exemples de politiques valides et invalides.
Démarche
Compréhension et reproduction
La première étape consiste à comprendre l’approche Zelkova2, en particulier l’encodage des politiques de sécurité en logique des prédicats.
Le premier déliverable attendu est une reproduction des exemples de2, à la main, avec le prouveur Z3.
Prise en main des outils
La deuxième étape consiste à prendre en main les packages Python nécessaires au projet:
- le module
jsonpour la lecture des politiques IAM - le module
z3permettant l’interactions avec le prouveurz3
Le deuxième déliverable consiste en un prototype permettant de lire un fichier IAM et d’afficher son contenu à l’écran, et d’un second prototype permettant de reproduire, en Python, l’un des exemples du premier déliverable.
Architecture du prototype
La troisième étape consistera à définir l’architecture de l’application. Un soin particulier sera apporté à la génération des formules Z3. Il est en effet plus simple de valider la formalisation à partir d’une architecture bien construite, avec quelques tests unitaires, que de valider les formules produites, qui requièrent des tests fatidieux à mettre en place.
Le troisième déliverable est une interface de programmation et des algorithmes permettant de valider la formalisation d’une politique IAM en formule SMT Z3.
Programmation du prototype
La quatrième étape consiste à implémenter le prototype selon l’architecture prévue, et à valider celui-ci sur les exemples issus de8 et9.
Le déliverable attendu est le prototype validé
Validation et limites
La dernière étape consiste à valider le résultat obtenu vis-à-vis des critères pré-établis, et à discuter les limites de l’approche mise en oeuvre en s’appuyant sur l’article3. Des propositions d’amélioration seront élaborées à partir des articles3 et7. Si le temps le permet, certains seront mises en oeuvre et évaluées.
Les déliverables attendus sont:
- le prototype mis à jour, s’il y a lieu;
- et l’étude de validation vis-à-vis des objectifs et des articles3 et7.