-
Notifications
You must be signed in to change notification settings - Fork 5
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
- Loading branch information
1 parent
fc25ae4
commit 3fe5a34
Showing
18 changed files
with
560 additions
and
110 deletions.
There are no files selected for viewing
This file was deleted.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,97 @@ | ||
--- | ||
title: "DéCySif" | ||
sectiontitle: "Home" | ||
cascade: | ||
featured_image: '/images/Decysif.png' | ||
description: "Formal verification in the service of safety and security" | ||
synopsis: "DéCySif is a regional R&D project funded by an i-Démo call and the | ||
Ile-de-France French region gathering Adacore, INRIA, OCamlPro and TrustInSoft. | ||
Its objective is to improve the safety and security of critical systems using | ||
formal verification tools." | ||
|
||
project: | ||
sectiontitle: "The project" | ||
content: "It has been a few years since Rust has proven to be a viable | ||
alternative to languages such as Ada/C/C++ in the world of embedded software, | ||
critical or not. Current and upcoming actors of the Rust critical embedded | ||
software world are now exploring the possibility of using formal analysis | ||
tools for Rust. | ||
<br /> | ||
<br /> | ||
It is as a direct answer to that question that INRIA have developped Creusot, a | ||
tool for Rust. The tool itself is based off the same technological foundations | ||
as AdaCore's and TrustInSoft's formal analysis tools: the Why3 platform, | ||
developped by INRIA, and a collections of SMT-Solvers such as Alt-Ergo, | ||
developped by OCamlPro. | ||
<br /> | ||
<br /> | ||
Project DéCySif is the crucible for the improvement of all these tools and | ||
aims at guaranteeing convergence towards an optimal solution for the safety | ||
and security of embedded systems. " | ||
|
||
coordinator: | ||
sectiontitle: "Coordinator" | ||
content: "TrustInSoft are the coordinators of the project. For any enquiry, | ||
please use the [contact form]({{< ref \"contact.en.md\" >}})." | ||
|
||
|
||
collaborators: | ||
sectiontitle: "The consortium" | ||
consortium: | ||
- name: "Adacore" | ||
url: "https://www.adacore.com/" | ||
description: | ||
"Founded in 1994, AdaCore designs and provides software development and | ||
verification tools for applications where safety, security, and reliability | ||
are critical elements.<br /> | ||
The use of AdaCore products continues to grow in critical applications such | ||
as space systems, commercial avionics, military systems, air traffic | ||
control, railway systems, medical devices, or financial services. AdaCore | ||
enjoys a substantial and constantly growing base of international clients; | ||
visit www.adacore.com/industries/ for more information.<br /> | ||
AdaCore products are free and come with expert online support provided by | ||
the developers themselves. The company has a North American headquarters | ||
based in New York and a European headquarters based in Paris." | ||
|
||
- name: "INRIA - LMF - Toccata" | ||
url: "https://www.inria.fr/en/toccata" | ||
description: | ||
"The [INRIA](https://www.inria.fr) is the French national public institute | ||
for research in computer science. The INRIA members of the DéCySif project | ||
belong to the Formal Methods Laboratory ([LMF](https://lmf.cnrs.fr/)) | ||
and the Toccata research team | ||
([Toccata](http://toccata.gitlabpages.inria.fr/toccata/)), located in | ||
Orsay, France; and jointly affiliated with the University of | ||
Paris-Saclay, CNRS, and the INRIA Saclay - Île-de-France research | ||
center. | ||
<br /> | ||
The general objective of the team is to promote formal specifications | ||
and computer-assisted proofs in the development of software requiring a | ||
high level of confidence in their safety and adherence to expected | ||
behaviors." | ||
|
||
- name: "OCamlPro" | ||
url: "https://www.ocamlpro.com" | ||
description: | ||
"OCamlPro is an R&D consulting firm specializing in engineering problems | ||
related to programming languages, business-specific requirements, or | ||
technical debt. The company is committed to open source and contributes to | ||
the Rust, WebAssembly, and OCaml languages. The company also develops the | ||
Alt-Ergo SMT solver used in DéCySif.<br /> | ||
OCamlPro is also active in the field of Common Criteria certification at | ||
the EAL6 level and the use of formal methods (Coq, Lean4, Why3)." | ||
|
||
- name: "TrustInSoft" | ||
url: "https://trust-in-soft.com/" | ||
description: | ||
"TrustInSoft markets tools and services for exhaustive analysis of C and C++ | ||
source code, providing mathematical guarantees on the quality of their | ||
clients' software. These software analysis solutions ensure the security | ||
and reliability of source code without altering the development process. | ||
These offerings are deployed worldwide among developers and integrators of | ||
software components from the aerospace, automotive, railway, military, | ||
nuclear, telecoms, or IoT industries." | ||
|
||
software: | ||
sectiontitle: "Our softwares" | ||
--- |
This file was deleted.
Oops, something went wrong.
This file was deleted.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,98 @@ | ||
--- | ||
title: "DéCySif" | ||
sectiontitle: "Accueil" | ||
cascade: | ||
featured_image: '/images/Decysif.png' | ||
description: "La vérification formelle au service de la sécurité et la sûreté" | ||
synopsis: "DéCySif est un projet i-Demo régional de R&D regroupant Adacore, | ||
l'INRIA, OCamlPro et TrustInSoft. Il vise à améliorer la sécurité et la sûreté | ||
des systèmes critiques en utilisant des outils de vérification formelle." | ||
|
||
project: | ||
sectiontitle: "Le projet" | ||
content: "Depuis quelques années, le langage de programmation Rust vient | ||
concurrencer les langages Ada/C/C++ établis dans le monde des logiciels | ||
critiques, embarqués ou non. Les acteurs actuels et futurs développant des | ||
logiciels critiques en Rust se posent désormais la question de l'opportunité | ||
d'utiliser des outils d’analyse formelle pour Rust. | ||
<br /> | ||
<br /> | ||
C'est pour répondre à cette question que l'outil Creusot pour Rust a été | ||
développé par l'INRIA. L'outil est basé sur les mêmes fondations technologiques | ||
que les outils d’analyse formelle d’AdaCore et de TrustInSoft : la plateforme | ||
Why3 développée par l'INRIA et les mêmes prouveurs automatiques dont le | ||
prouveur Alt-Ergo d'OCamlPro. | ||
<br /> | ||
<br /> | ||
Le projet DéCySif vie l'amélioration de tous ces outils afin de converger vers | ||
une solution optimale pour la sécurité et la sûreté des systèmes critiques." | ||
|
||
coordinator: | ||
sectiontitle: "Coordinateur" | ||
content: "La société TrustInSoft est le coordinateur du projet. Pour toute | ||
demande d'information, veuillez passer par le formulaire de [contact]({{< ref \"contact.fr.md\" >}})." | ||
|
||
collaborators: | ||
sectiontitle: "Le consortium" | ||
consortium: | ||
- name: "Adacore" | ||
url : "https://www.adacore.com/" | ||
description: | ||
"Fondée en 1994, AdaCore conçoit et fournit des outils de développement et | ||
de vérification de logiciels destinés à des applications pour lesquelles la | ||
sûreté, la sécurité et la fiabilité sont des éléments critiques.<br /> | ||
L'utilisation des produits AdaCore connaît une croissance continue dans des | ||
applications critiques telles que les systèmes spatiaux, l'avionique | ||
commerciale, les systèmes militaires, le contrôle aérien, les systèmes | ||
ferroviaires, les appareils médicaux ou les services financiers. AdaCore | ||
jouit d'une base fournie de clients internationaux en croissance | ||
constante; visitez le site www.adacore.com/industries/ pour de plus amples | ||
informations.<br /> | ||
Les produits AdaCore sont libres et accompagnés d'un support expert en | ||
ligne fourni par les développeurs eux-mêmes. La société possède un siège | ||
nord-américain basé à New York et un siège européen basé à Paris." | ||
|
||
- name: "INRIA - LMF - Toccata" | ||
url: "https://www.inria.fr/fr/toccata" | ||
description: | ||
"L'[INRIA](https://www.inria.fr) est l'institut national public | ||
français de recherche en sciences de l'informatique. Les membres INRIA | ||
du projet DéCySif appartiennent au Laboratoire Méthodes Formelles | ||
([LMF](https://lmf.cnrs.fr/)) et à l'équipe de recherche | ||
[Toccata](http://toccata.gitlabpages.inria.fr/toccata/), localisés à | ||
Orsay, France ; et communs à l'Université Paris-Saclay, au CNRS, et au | ||
centre de recherche INRIA Saclay - Île-de-France. | ||
<br /> | ||
L'objectif général de l'équipe est de promouvoir les spécifications | ||
formelles et les preuves assistées par ordinateur dans le cadre du | ||
développement de logiciels requérant un haut niveau de confiance dans | ||
leur sûreté de fonctionnement et le respect de comportements attendus." | ||
|
||
- name: "OCamlPro" | ||
url: "https://www.ocamlpro.com" | ||
description: | ||
"OCamlPro est un cabinet d'étude en R&D spécialisé dans les problèmes | ||
d'ingénieurie liés aux langages de programmation, aux spécificités métiers | ||
ou à la dette technique. La société est engagée dans l'*open source* | ||
et contribue aux langages Rust, WebAssembly et OCaml. La société développe | ||
aussi le prouveur SMT Alt-Ergo utilisé dans DéCySif.<br /> | ||
OCamlPro est également active dans le domaine de la certification | ||
Critères Communs au niveau EAL6 et l'utilisation des méthodes formelles | ||
(Coq, Lean4, Why3)." | ||
|
||
|
||
- name: "TrustInSoft" | ||
url: "https://trust-in-soft.com/" | ||
description: | ||
"TrustInSoft commercialise des outils et services d'analyse exhaustive de | ||
code source C et C++ permettant d'apporter des garanties mathématiques sur | ||
la qualité des logiciels de ses clients. Ces solutions d'analyses de | ||
logiciel permettent d'avoir des garanties sur la sécurité et la fiabilité | ||
du code source sans modifier le processus de développement. Ces offres | ||
sont déployées dans le monde entier chez les développeurs et intégrateurs | ||
de composants logiciels issus des industries aéronautique, automobile, | ||
ferroviaire, militaire, nucléaire, télécoms, ou l'IoT." | ||
|
||
software: | ||
sectiontitle: "Les logiciels" | ||
--- |
This file was deleted.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,7 +1,6 @@ | ||
--- | ||
title: "Actualités" | ||
date: 2017-03-02T12:00:00-05:00 | ||
type: page | ||
featured_image: '/images/Decysif.png' | ||
--- | ||
Lisez toutes les dernières avancées du projet ici ! |
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,59 @@ | ||
<!DOCTYPE html> | ||
<html lang="{{ site.LanguageCode | default site.Language.Lang }}" {{- with partialCached "func/GetLanguageDirection" "GetLanguageDirection" }} dir="{{ . }}" {{- end }}> | ||
<head> | ||
<meta charset="utf-8"> | ||
<meta http-equiv="X-UA-Compatible" content="IE=edge,chrome=1"> | ||
{{/* NOTE: the Site's title, and if there is a page title, that is set too */}} | ||
<title>{{ block "title" . }}{{ with .Params.Title }}{{ . }} | {{ end }}{{ .Site.Title }}{{ end }}</title> | ||
<meta name="viewport" content="width=device-width,minimum-scale=1"> | ||
<meta name="description" content="{{ with .Description }}{{ . }}{{ else }}{{if .IsPage}}{{ .Summary }}{{ else }}{{ with .Site.Params.description }}{{ . }}{{ end }}{{ end }}{{ end }}"> | ||
{{ hugo.Generator }} | ||
{{/* NOTE: For Production make sure you add `HUGO_ENV="production"` before your build command */}} | ||
{{ $production := eq (getenv "HUGO_ENV") "production" | or (eq site.Params.env "production") }} | ||
{{ $public := not .Params.private }} | ||
{{ if and $production $public }} | ||
<meta name="robots" content="index, follow"> | ||
{{ else }} | ||
<meta name="robots" content="noindex, nofollow"> | ||
{{ end }} | ||
|
||
{{ partial "site-style.html" . }} | ||
{{ partial "site-scripts.html" . }} | ||
|
||
{{ block "favicon" . }} | ||
{{ partialCached "site-favicon.html" . }} | ||
{{ end }} | ||
|
||
{{ if .OutputFormats.Get "RSS" }} | ||
{{ with .OutputFormats.Get "RSS" }} | ||
<link href="{{ .RelPermalink }}" rel="alternate" type="application/rss+xml" title="{{ $.Site.Title }}" /> | ||
<link href="{{ .RelPermalink }}" rel="feed" type="application/rss+xml" title="{{ $.Site.Title }}" /> | ||
{{ end }} | ||
{{ end }} | ||
|
||
{{ if .Params.canonicalUrl }} | ||
<link rel="canonical" href="{{ .Params.canonicalUrl }}"> | ||
{{ else }} | ||
<link rel="canonical" href="{{ .Permalink }}"> | ||
{{ end }} | ||
|
||
{{/* NOTE: These Hugo Internal Templates can be found starting at https://github.com/gohugoio/hugo/tree/master/tpl/tplimpl/embedded/templates */}} | ||
{{- template "_internal/opengraph.html" . -}} | ||
{{- template "_internal/schema.html" . -}} | ||
{{- template "_internal/twitter_cards.html" . -}} | ||
|
||
{{ if eq (getenv "HUGO_ENV") "production" | or (eq .Site.Params.env "production") }} | ||
{{ template "_internal/google_analytics.html" . }} | ||
{{ end }} | ||
{{ block "head" . }}{{ partial "head-additions.html" . }}{{ end }} | ||
</head> | ||
|
||
<body class="ma0 {{ $.Param "body_classes" | default "avenir bg-near-white"}}{{ with getenv "HUGO_ENV" }} {{ . }}{{ end }}"> | ||
|
||
{{ block "header" . }}{{ partial "site-header.html" .}}{{ end }} | ||
<main class="pb7" role="main"> | ||
{{ block "main" . }}{{ end }} | ||
</main> | ||
{{ block "footer" . }}{{ partialCached "site-footer.html" . }}{{ end }} | ||
</body> | ||
</html> |
Oops, something went wrong.