R&D Projects at SafeRiver

LabOSSec (2015-2018)

The LabOSSec project has been commissioned by the French Network and Information Security Agency ANSSI.

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 a consortium (Airbus Group Innovations, Oppida and SafeRiver) with the help of an open workgroup gathering the main actors in software static security in France: tool providers, end users, CESTI, academics. The open workshop gathers nearly once a month and shares information on a private Wiki.

The consortium is accountable for deliverables. All the results will be published by ANSSI on its portal at the end of the project.

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 the security recommendations 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.

PISCO (2013-2015)

The PISCO project objective is the implementation of a hardware integration platform for trusted services. This generic platform will enable the installation of applications that require trusted services.

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.

CORAC - PANDA (2013-2015)

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

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

In this project SafeRiver works on : (a) structuring and verifying functional security requirements using formal methods, (b) analyzing vulnerabilities and evaluating software protection levels using program static analysis. SafeRiver also contributes in the implementation of a "compositional insurance approach" to take advantage of component security proof or certification : security kernels, composition of functional security properties.

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 thought 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 analysis, 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 in accordance to the security recommendations emitted. This application has been evaluated with respect to security.

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

The public results are available on the ANSSI Web site.

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). Apart 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.

Baccarat (2010-2011)

This FEDER project is leaded by Magillem. It proposes to describe complex electronic systems security requirements in the IEEE 1685 IP-XACT (XML) format and propagate them among the several steps of the system design flow: from the whole system down to each electronic board (PCB). One must allocate specification for each board and ensure that the assembly respects the constraints at system level.

SafeRiver contributes in this project by developing a module of the Carto-C tool that computes the software attack surface, and detects format attacks. This tool could be linked to the Magillem development chain as part of the safety demonstration.

2019, Christèle Faure