Transcription
ÉtudeLaFoSecJFLA1/16LaFoSec: Étude de la sécurité intrinsèque des langages fonctionnels1Partie III sur IVIntroductionEvolutionsPropositions d'évolution du langage OCamlConclusionConclusions de la Tranche FermeConclusionde laTrancheFermeContactsDamien Doligez, Christèle Faure, Thérèse Hardin, Manuel MaarekJFLA - février 2013Safety & Security Forge1.NormationEtude commanditée par l'Agence Nationale de la Sécurité des Systèmes d'Information
lutions3Conclusion4Conclusion de la Tranche Ferme5ContactsEvolutionsConclusionConclusionde laTrancheFermeContacts
ÉtudeLaFoSecIntroductionEvolutions de OCaml recommandées par LaFoSecJFLA3/16IntroductionEvolutionsL'étude LaFoSec propose 30 recommandations d'évolution pourConclusionle langage OCaml ou ses outils associés. On peut les classer enConclusiontrois catégories :de laTrancheFermeContactsévolutions faciles à implémenter5 sans impact sur les programmes normaux5 avec impact : à activer explicitement8 évolutions à long terme12 évolutions à étudier
lutions3Conclusion4Conclusion de la Tranche Ferme5ContactsEvolutionsConclusionConclusionde laTrancheFermeContacts
ÉtudeLaFoSecEvolutionsEvolutions faciles nde laTrancheFermeContactsEvolutions sans impact sur les programmes normauxavertissement sur les variables globales non utiliséesdéjà fait par A. Frisch, warnings 32 à 37avertissement sur les annotations de typequand le type déclaré par l'utilisateur est moins général que letype inféré par le compilateurajouter une fonctionBigarray.mlockavertissement lorsqu'unopenmasque des identi cateursborne optionnelle sur le temps de calculs des fonctions dela bibliothèqueStr
ÉtudeLaFoSecEvolutionsEvolutions faciles 2JFLA6/16IntroductionEvolutions a ectant les performancesEvolutionsConclusionConclusionde laTrancheFermeContactsGC : e acement des données déplacéesdi érence entre déplacer et recopier : irrelevante en fonctionnel,très importante en sécuritéenvironnement (CAML DEBUG SOCKET,String.createetunsafe (pas si simple)encapsulation obligatoire de chaqueajout d'une fonctionOCAMLRUNPARAM)dprintf.mlpar unpour le debug.mli
ÉtudeLaFoSecEvolutionsEvolutions à long terme nde laTrancheFermeContactsanalyse statique des exceptionsanalyse des exceptions levées par chaque fonctionanalyse des types des données transportées par lesexceptions (fuite de données)véri cation des débordements d'entierssérialisation/désérialisation typéespour éviter les erreurs, et les attaques si on s'assure que ladonnée ne peut pas être modi ée après sérialisationdésérialisation blindéepour résister aux entrées non contrôlées
ÉtudeLaFoSecEvolutionsEvolutions à long terme nde laTrancheFermeContactssuppression des initialisations/codes inutilisés dans leruntime (ex : ottants)pas facile à faire : touche toute la chaîne de compilationutile au-delà de la sécurité : codes embarqués, processeurssans ottants, programmes stand-aloneannotation explicite de la récursion terminaledocumentercamlp4,l'utiliser pour instrumenter lesrecommandationsvéri cateur de byte-code OCaml
ÉtudeLaFoSecEvolutionsEvolutions à étudierJFLAchaînes de caractères non mutables9/16renforcement de clusionde laTrancheFermeContactssuppression des comparaisons polymorphesdé nition d'un noyau du langage pour la sécuritépour éviter les constructions douteuses ou di ciles à évaluerdéveloppement d'un outil d'analyse statique dédié à lasécuritébyte-code typévéri cation du code chargé dynamiquementcloisonnement de la mémoirecontrôle du code d'initialisation des modules liés auprogrammetypage avec unités de mesureoutils de test, debug, pro lage
olutions3Conclusion4Conclusion de la Tranche Ferme5ContactsEvolutionsConclusionConclusionde laTrancheFermeContacts
ÉtudeLaFoSecConclusionEvolutions de lusionde laTrancheFermeContactscertaines évolutions sont déjà en coursd'autres sont faisables (question de moyens)pour aller plus loin, deux stratégies possibles :dé nir un sous-ensemble de OCaml et développer les outilsd'analyse correspondantsun nouveau langage basé sur OCaml
olutions3Conclusion4Conclusion de la Tranche Ferme5ContactsEvolutionsConclusionConclusionde laTrancheFermeContacts
ÉtudeLaFoSecConclusion de la Tranche lusionde laTrancheune liste de problèmes déjà connus mais jamaisrassemblés dans un même documentexemple : une optimisation de la compilation des modulespermet de casser l'encapsulation : problème connu au niveau del'e cacité, mais pas comme problème de sécuritéFermel'étude porte sur une partie relativement restreinte duContactslangage, pas de :foncteursvariants polymorphesarguments étiquetésGADT.importance de la relecture du code pour la certi cation
ÉtudeLaFoSecLaFoSec : un point de départJFLA14/16IntroductionOCaml : des apports indéniables pour la sécurité desEvolutionsapplicationsConclusionConclusionde laTrancheFermeContactsdes recommandations d'utilisationdes propositions d'évolution pour OCamlune idée à creuser : SecureMLquels traits faudrait-il retirer de OCaml ?quels traits faudrait-il ajouter ?quelles garanties demander au compilateur ?quels outils auxiliaires implémenter ?comment le rendre utilisable par l'industrie ?
olutions3Conclusion4Conclusion de la Tranche Ferme5ContactsEvolutionsConclusionConclusionde laTrancheFermeContacts
nsConclusionConclusionde laTrancheFermeContactsVéronique Delebarre : veronique.delebarre@safe-river.comChristèle Faure : christele.faure@safe-river.com
Evolutions de OCaml recommandées par LaFoSec L'étude LaFoSec propose 30 recommandations d'évolution pour le langage OCaml ou ses outils associés. On peut les classer en trois catégories : évolutions faciles à implémenter 5 sans impact sur les programmes normaux 5 avec impact : à activer explicitement 8 évolutions à long terme
