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