SecurOCaml (2015-2018)

The SecurOCaml project project aims at defining a subset of the OCaml language to use for the development of security applications to cover the recommendations developed during the LaFoSec project.

SafeRiver was the leader of the LafoSec project in which security recommendations were elaborated on OCaml 3.12.0, and is responsible for the security study of the new OCaml version 4.02.1. From this the SecurOcaml will be defined and tools to check for the conformance of the applications to this restriction will be defined.

LabOSSec (2015-2016)

The LabOSSec project has been commissioned by the French Network and Information Security Agency ANSSI and is carried out by a consortium: Airbus Group Innovations, Oppida and SafeRiver.

SafeRiver is the leader of the LabOSSec project which aims at studying the usage of static tools for software security and elaborating a standard to certify static tools and their configuration throughout their responses on flaws or vulnerabilities test cases.

This work will be carried out by the consortium responsible for deliverables with the help of an open workgroup gathering the main actors in software static security: tool providers, end users, CESTI, academics. The open workshop has started, gathers nearly once a month and shares information on a private Wiki.

All the results will be published by ANSSI ont its portal at the end of the project.

PISCO (2013-2014)

The PISCO project objective is the implementation of a hardware integration platform for trusted services which will support the installation of secure applications.

SafeRiver is responsible for one work package focused on the development of methods and tools enabling the evaluation of the security of trusted components on the PISCO platform. SafeRiver develops tools for the verification of security levels on software components.

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

Corac - Panda (2013-2014)

The Council for Civil Aeronautics Research (CORAC) has defined a technological roadmap for aeronautics research focusing on the management of the environmental footprint of air transport by 2020.

The PANDA project belongs to the Demonstrator for the future plateform 2: PDT - Extended Modular Avionic (MDE).

In this project SafeRiver works on:

  • Structuring and verifying functional security requirements using formal methods
  • Allocating these requirements on the modular architecture
  • Analyzing vulnerabilities and evaluating software protection levels using source code static analysis.

SafeRiver also contributes to the implementation of a "compositional insurance approach" to take advantage of the component's security proof or certification: security kernels, composition of functional security properties.

Prometheus (2009-2012)

Kalray leads this OSEO Project. Kalray is a silicon fabless & software company which develops and sells a new generation of manycore processors for high performance applications called MPPA® (Multi-Purpose Processor Array). Appart from Kamray and SafeRiver, the Prometheus project had seven contributors: ASYGN, IS2T , DOCEA POWER , BLUE EYE VIDEO, COFLUENT DESIGN , EVERSAT , and IFOTEC.

SafeRiver contributed to this project by the development of a dedicated prototype of SafeRiver Carto-C tool for the verification of communication rules between multiple applications (one main application and several different spawned applications) implemented using the MPPA library. This verification is based on new verification modules generic enough to be extended for the verification of other sets of communication rules.

LaFoSec (2010-2012)

The LaFoSec project is a study of the intrinsic security of functional languages commissioned by the French Network and Information Security Agency ANSSI and carried out by a consortium led by SafeRiver.

The purpose of the LaFoSec project is to provide a theoretical study of the security of functional programming traits through an analysis of the OCaml, F# and Scala languages with regard to security, and an in depth analysis of OCaml's runtime system. Following these analyses, a set of security recommendations for secure OCaml developments were issued.

As part of an experimentation for the project, SafeRiver has developed a validator of XML files with respect to an XSD description. This application has been developed in OCaml respecting the security recommendations. This application has been evaluated at the EAL4+ level.

The results of this study have been presented at JFLAs 2013 (Tuesday 17h-19h45).

The public results are available on the ANSSI Web site.

BACCARAT (2010-2011)

BACCARAT is a collaborative R&D project, cofinanced by the European Union ("L'Europe s'engage en Ile de France avec le Fonds Européen de Développement Régional (FEDER)").

The aim of this project is the elaboration of a security-oriented cartography tool for identifying specific points in ESL descriptions or in applicative code embedded into FPGA.

The functionalities developed in the context of the BACCARAT project are:

  • Cartography of input/output points and localization of all places where I/O interfaces are used
  • Detection and localization of instructions vulnerable to "format string attacks"
  • Cartography of assets and control access mechanisms for these assets
  • Cartography of protection function declared by the designer.

These functionalities shall be integrated into the MDS (Magillem Design Services) design flow, developed by Magillem, partner and leader of the BACCARAT project.