New York, Paris et Bath, le 6 octobre 2008 - 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  (EAL) 5 des Critères communs , 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 quelques 10 000 lignes de code à qualité garantie. Son coût est donc significativement inférieur à ceux obtenus grâce aux méthodes traditionnelles.

« Le projet Tokeneer a le potentiel pour révolutionner le développement de systèmes à haute sécurité », affirme Robert Dewar, PDG d’AdaCore. « En mettant le projet Tokeneer à disposition de la communauté open source, la NSA va aider à promouvoir de bonnes pratiques de programmation et démontrer l’importance de SPARK et d’Ada dans le marché émergent de la sécurité. Nous nous réjouissons d’être associés à Praxis et la NSA dans ce projet révolutionnaire. »

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.

« Nous sommes extrêmement fiers du projet Tokeneer », reconnait Keith Williams, Directeur Général de Praxis. « Nous espérons que les communautés de la recherche, de l’enseignement et du logiciel open-source feront bon usage du matériel mis à leur disposition en tant que modèle de développement de logiciel à qualité garantie. »

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.


« Le projet Tokeneer constitue une étape importante du transfert des technologies de vérification de programmes vers les applications industrielles. La publication de l’ensemble des documents du projet a fourni un matériel expérimental sans précédent qui va permettre à la recherche académique d’effectuer encore d’autres développements de la technologie. Il s’agit de la pierre de touche qui va permettre de mesurer les progrès de la science fondamentale de la programmation sur laquelle cette technologie repose. »
Sir Tony Hoare,
Compagnon de la Royal Society, de Microsoft Research, et créateur du Grand Challenge

« La publication par Praxis et la NSA du système Tokeneer est une contribution fantastique à la communauté de l’enseignement et de la recherche en ingénierie logicielle. Les études de cas de qualité ont été très difficiles à trouver, et sont souvent propriétaires. Nous avons enfin un exemple complet et ouvert de développement, par un leader des systèmes à haute intégrité, avec des exigences exemplaires, les spécifications, les documents de conception et le code. Je suis très excité par l’impact que cela pourrait avoir dans notre domaine, que ce soit au niveau de l’enseignement ou de la recherche, et le potentiel que cela pourrait générer en nous poussant vers une communauté plus ouverte où il y aurait une meilleure collaboration entre l’industrie et la recherche académique, et un engagement plus constructif entre la théorie et de la pratique. »
Professeur Daniel Jackson,
Massachussetts Institute of Technology, Laboratoire d’informatique fondamentale


A propos d’AdaCore

Fondée en 1994, AdaCore est le premier fournisseur de solutions logicielles pour Ada, un langage de programmation moderne conçu pour répondre aux besoins de larges applications à longue durée de vie, pour lesquelles la sûreté, la sécurité et la fiabilité sont essentielles. AdaCore dispose d’une large clientèle répartie partout dans le monde. Voir http://www.adacore.com/home/company/customers/ pour plus de détails.
Ada et GNAT Pro sont de plus en plus utilisés pour des applications à haute intégrité et certifiées, dans des domaines tels que l’avionique, les systèmes militaires, la gestion du trafic aérien, le transport ferroviaire ou encore les équipements médicaux, ainsi que dans des domaines comme ceux des services financiers où la sécurité est déterminante. Les sièges d’AdaCore se trouvent à New York et Paris. www.adacore.com

A propos de Praxis et Correctness by Construction

Praxis est une société d’ingénierie logicielle spécialisée dans les systèmes critiques du point de vue de la mission ou de la sécurité. Praxis excelle dans des domaines spécifiques de l’ingénierie des systèmes avancés tels que l’ingénierie des logiciels à taux de défauts ultra réduit, l’ingénierie de la sécurité pour systèmes complexes ou novateurs, et les outils et méthodes pour l’ingénierie des systèmes. Praxis propose à ses clients une large gamme de services comprenant le développement de systèmes clés en main, le conseil, la formation et la R&D. Ses secteurs clés sont l’aérospatial, la défense, la gestion du trafic aérien, le transport ferroviaire et le nucléaire. Praxis est un acteur international avec des projets en cours aux Etats-Unis, en Asie et en Europe. Son siège britannique est implanté à Bath et des bureaux sont situés à Londres, Loughborough et Paris. Praxis est une filiale du groupe Altran Technologies, leader mondial en ingénierie innovante, employant 17 500 ingénieurs de par le monde. www.praxis-his.com

A propos de l’Agence nationale de sécurité

L’Agence de sécurité nationale/Service central de sécurité est l’organisme gouvernemental américain de cryptologie. Pour plus d’information, visitez le site de la NSA. www.nsa.gov