lundi 23 octobre 2017

Accueil du site > Informatique > Sécurité Informatique > La NSA met un projet de logiciel sécurisé pour la communauté Open (...)

La NSA met un projet de logiciel sécurisé pour la communauté Open Source

Marc Jacob, GlobalSecurityMag.fr

lundi 6 octobre 2008, sélectionné par Spyworld

logo

Le développement de logiciels hautement sécurisés va être fortement encouragé par la mise à disposition du projet Tokeneer à la communauté open-source, par l’Agence nationale de sécurité américaine (NSA). Le contenu complet du projet est dès à présent disponible sur www.adacore.com/tokeneer. Il comprend notamment les exigences, la cible de sécurité, les spécifications, les documents de conception, le code source et les preuves.

Le projet Tokeneer a été attribué par la NSA à la société britannique Praxis High Integrity Systems en vue de créer un exemple d’ingénierie logicielle à haute garantie. Développé suivant la méthodologie Correctness by Construction (CbyC) mise au point par Praxis, il utilise le langage SPARK Ada et l’environnement de développement GNAT Pro d’AdaCore. Le projet a démontré comment atteindre et même franchir le niveau d’assurance de l’évaluation[1] (EAL) 5 des Critères communs[2], porte d’entrée vers les niveaux les plus élevés.

C’est la première fois qu’un projet d’une telle ampleur est mis à disposition de la communauté open-source. Il vise à montrer comment des logiciels hautement sécurisés peuvent être développés en optimisant le rapport performances-coût, améliorant ainsi la pratique industrielle et offrant un point de départ pour l’enseignement et la recherche. Présenté à l’origine dans un article publié en 2006, le projet a comme objectif à long terme d’améliorer les pratiques de développement des fournisseurs de la NSA. Tokeneer a en effet été développé dans le cadre d’un projet à prix fixe. Il représente un effort de 260 homme-jours seulement pour le développement de quelque 10 000 lignes de code à qualité garantie. Son coût est donc significativement inférieur à ceux obtenus grâce aux méthodes traditionnelles.

Tokeneer a été écrit en SPARK Ada, un langage de programmation de haut niveau conçu pour les applications à haute assurance. Reposant sur un sous-ensemble du langage Ada, il est conçu de manière à ce que tout programme écrit en SPARK soit un programme Ada valide. De par son savant dosage entre flexibilité, fiabilité et facilité de mise en œuvre, Ada est le choix naturel pour les systèmes critiques à haute intégrité. SPARK y ajoute une chaîne d’outils de vérification statique qui combine profondeur, exactitude, performance et preuves formelles.

Le projet est destiné à la fois aux communautés industrielle et académique. Il établit une base idéale tant pour la poursuite de la recherche dans le domaine de la vérification de programmes que comme support d’enseignement. Il va aussi être inclus dans le Verified Software Repository, sous les auspices de l’actuel Grand Challenge du groupe Dependable Systems Evolution.

[1] Evaluation Assurance Level, http://fr.wikipedia.org/wiki/Evaluation_Assurance_Level

[2] Common Criteria, http://fr.wikipedia.org/wiki/Critères_communs


Envoyer : Newsletter Imprimer : Imprimer Format PDF : Enregistrer au format PDF PartagerPartager :