SecurOCaml (2015-2018)

Le projet SecurOCaml vise à définir un sous-ensemble du langage OCaml afin de l'utliser pour le développement d'applications de cyber-sécurité, en couvrant les recommandations émises lors du projet LaFoSec.

SafeRiver était pilote des recommandations de sécurité émises pour OCaml 3.12.0 et est responsable de l'étude de sécurité sur la nouvelle version OCaml 4.02.1. Une fois cela fait, SecurOCaml pourra être défini et le projet proposera des outils pour vérifier la conformité des applications aux restrictions correspondant à SecurOCaml.

LabOSSec (2015-2016)

Le projet LabOSSec project a été commissionné par l'ANSSI (Agence National de la Sécurité des Systèmes d'Information) et est porté par un consortium composé de : Airbus Group Innovations, Oppida et SafeRiver.

SafeRiver pilote ce projet dont l'objet est l'étude de l'usage des outils d'analyse statique pour la cyber-sécurité, étude qui doit permettre l'élaboration d'un standard pour certifier ces outils d'analyse avec leurs configurations par rapport à des cas de tests sur un large panel de failles et des vulnérabilités.

Ce travail sera porté par un consortium responsable de livrables produits à l'aide d'un groupe de travail ouvert qui rassemble les acteurs principaux du domaine de l'analyse de logiciels orientée cyber-sécurité: fournisseurs d'outils, utilisateurs, CESTI, chercheurs. Cet atelier ouvert a d'ores et déjà commencé, se réunit une fois par mois et partage les informations entre ses membres sur un Wiki privé.

Tous les résultats seront publiés sur le portail de l'ANSSI à la fin du projet.

PISCO (2013-2014)

L'objectif de ce projet est la mise en oeuvre d'une plateforme d'intégration de services de confiance basée sur un HSM et un noyau de virtualisation permettant un accès cloisonné aux ressources cryptographiques. Cette plateforme générique devra permettre l'installation de d'applications telles que : horodatage, archivage sécurisé, administration PKI, etc.

SafeRiver est responsable de la tâche de développement des méthodes et outils permettant l'évaluation de la sécurité des composants de confiance de la plateforme PISCO. SafeRiver développe également des outils pour la vérification des niveaux de sécurité des applications logicielles.

Partenaires : Bertin Technologies, Bull, Cassidian, CEA-List, Cryptolog, CS, INRIA, OPPIDA, SafeRiver, Serpikom

Corac - Panda (2013-2014)

Le conseil pour la recherche aéronautique civile (Council for Civil Aeronautics Research -- CORAC) a défini la feuille de route pour les recherches aéronautiques ciblées sur des objectifs de gestion de l'impact environnemental des transports aériens d'ici à 2020.

Le sous-projet PANDA fait partie du démonstrateur pour la plateforme du futur IMA 2 : PDT - Extended Modular Avionic (AME).

Dans ce projet SafeRiver travaille sur :

  • La formalisation et la vérification des exigences fonctionnelles de sécurité (SSI)
  • L'allocation de ces exigences sur l'architecture modulaire
  • L'analyse des vulnérabilités et l'évaluation des niveaux de protection logicielle en utilisant l'analyse statique de programmes.

SafeRiver contribue également à l'implémentation d'une "approche d'assurance compositionnelle" pour profiter de la certification ou la preuve de sécurité des composants : noyaux de sécurité, composition de propriétés de sécurité fonctionnelles.

Prometheus (2009-2012)

Ce projet OSEO est porté par Kalray, une société fabless et éditrice de logiciels, qui développe et fournit des processeurs multicoeurs nouvelle génération pour des applications haute performance appelées MPPA® (Multi-Purpose Processor Array). En plus de Kalray et SafeRiver, ce projet a sept contributeurs : ASYGN, IS2T, DOCEA POWER, BLUE EYE VIDEO, COFLUENT DESIGN, EVERSAT et IFOTEC.

SafeRiver a contribué à ce projet via le développement d'un prototype dédié appelé Carto-C pour la vérification de règles de communication entre plusieurs applications (une application principale et plusieurs applications filles différentes) implémentées à l'aide la bibliothèque MPPA. Cette vérification se base sur de nouveaux modules de vérification suffisamment génériques pour être étendus à la vérification d'autres ensembles de règles de communication.

LaFoSec (2010-2012)

Le projet LaFoSec est une étude de la sécurité intrinsèque des langages fonctionnels commandée par l'ANSSI (Agence Nationale pour la Sécurité des Systèmes d'Information) et réalisée par un consortium piloté par SafeRiver.

L'objectif du projet LaFoSec est de fournir une étude théorique de la sécurité des traits de programmation fonctionnelle via l'analyse des langages OCaml, F# et Scala vis-à-vis de la sécurité, ainsi qu'une analyse en profondeur du moteur d'exécution OCaml. Un ensemble de recommandations de sécurité pour les développements OCaml sécuritaires a été produit à l'issue de ces analyses.

Dans la partie expérimentale du projet, SafeRiver a développé un valideur de fichiers XML vis-à-vis d'une description XSD. Cette application a été développée en OCaml en respectant les recommandations de sécurité émises. Elle a de plus été évaluée en sécurité.

Les résultats de cette étude ont été présentés aux JFLA 2013 (Mardi, 17h-19h45).

Les résultats publics sont disponibles sur le site de l'ANSSI.

BACCARAT (2010-2011)

BACCARAT est un projet de recherche et développement collaboratif, cofinancé par l'Union Européenne. L'Europe s'engage en Ile de France avec le Fonds Européen de Développement Régional (FEDER).

Ce projet a pour objectif de réaliser un outil de cartographie de sécurité permettant d'identifier des points particuliers dans des descriptions ESL ou sur du code applicatif embarqué dans des FPGA.

Les fonctionnalités développées dans le cadre du projet BACCARAT

  • La cartographie des points d'entrée et de sortie et la localisation de tous les points d'utilisation des interfaces d'entrée et de sortie
  • La détection et la localisation d'instruction vulnérables aux « format string attack »
  • La cartographie des biens à protéger et des mécanismes de contrôle d'accès à ces biens à protéger
  • La cartographie des fonctions de protection déclarées par le concepteur.

Ces fonctionnalités seront intégrées dans le flot de conception MDS (Magillem Design Services), développé par Magillem, partenaire et leader du projet BACCARAT.