From df4666fab8195d398f67fd20b6c42179045d290c Mon Sep 17 00:00:00 2001 From: RadioPotin Date: Tue, 27 Aug 2024 15:59:23 +0200 Subject: [PATCH] add paper listing, fix typos, add en/fr switch when in single blogpost page --- assets/sass/main.scss | 5 + content/en/_index.md | 125 ++++++++-------- .../en/post/00_kickoff_of_project_decysif.md | 2 +- content/fr/_index.md | 134 +++++++++--------- ...if.md => 00_kickoff_of_project_decysif.md} | 2 +- hugo.toml | 2 +- layouts/_default/single.html | 67 +++++++++ layouts/index.html | 63 +++++--- layouts/partials/site-navigation.html | 9 +- 9 files changed, 250 insertions(+), 159 deletions(-) rename content/fr/post/{00_kickoff_du_projet_decysif.md => 00_kickoff_of_project_decysif.md} (95%) create mode 100644 layouts/_default/single.html diff --git a/assets/sass/main.scss b/assets/sass/main.scss index f37ebb3..102cf34 100644 --- a/assets/sass/main.scss +++ b/assets/sass/main.scss @@ -3,6 +3,11 @@ p { text-justify: auto; } +.pv5 { + padding-top: 1rem; + padding-bottom: 1rem; +} + #sitelogo { max-width: 15rem ; } diff --git a/content/en/_index.md b/content/en/_index.md index 94fd6cb..104983b 100644 --- a/content/en/_index.md +++ b/content/en/_index.md @@ -5,7 +5,7 @@ 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. +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." @@ -18,10 +18,10 @@ project: tools for Rust.

- It is as a direct answer to that question that INRIA have developped Creusot, a + 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 Inria, and a collections of SMT-Solvers such as Alt-Ergo, developped by OCamlPro.

@@ -39,63 +39,9 @@ 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.
- 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.
- 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. -
- 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.
- 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." +publications: + - papername: "Formally Verified Rounding Errors of the Logarithm-Sum-Exponential Function" + url: "https://inria.hal.science/hal-04674600" software: sectiontitle: "Our softwares" @@ -144,7 +90,7 @@ software: polymorphism, its compatibility with the SMT2 format, and several theories that allow it to formally handle basic types. The Alt-Ergo Club brings together a group of industrials (Thales, MERCE, Trust In Soft, - Adacore, etc.) using Alt-Ergo in their activities and helps to fund the + AdaCore, etc.) using Alt-Ergo in their activities and helps to fund the evolution of Alt-Ergo." - name: "SPARK, an industrial tool for deductive verification of the Ada language." @@ -169,4 +115,61 @@ software: url: - "https://www.trust-in-soft.com/trustinsoft-analyzer" description: "Soon..." + +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.
+ 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.
+ 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. +
+ 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.
+ 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." --- diff --git a/content/en/post/00_kickoff_of_project_decysif.md b/content/en/post/00_kickoff_of_project_decysif.md index 77b9522..a4b88ee 100644 --- a/content/en/post/00_kickoff_of_project_decysif.md +++ b/content/en/post/00_kickoff_of_project_decysif.md @@ -9,7 +9,7 @@ title: "Formal Cyber-Security Diagnostic: DéCySif" On Tuesday, December 19, 2023, all partners of the Decysif project ([TrustInSoft](https://trust-in-soft.com/), -[Adacore](https://www.adacore.com/), [OCamlPro](https://www.ocamlpro.com), and +[AdaCore](https://www.adacore.com/), [OCamlPro](https://www.ocamlpro.com), and the [LMF](https://lmf.cnrs.fr/) team) gathered at the TrustInSoft offices in the 14th arrondissement of Paris for the project kickoff meeting! diff --git a/content/fr/_index.md b/content/fr/_index.md index 63feac7..5927081 100644 --- a/content/fr/_index.md +++ b/content/fr/_index.md @@ -4,8 +4,8 @@ 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é +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: @@ -18,9 +18,9 @@ project:

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 + 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 + Why3 développée par l'Inria et les mêmes prouveurs automatiques dont le prouveur Alt-Ergo d'OCamlPro.

@@ -37,66 +37,9 @@ coordinator: 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.
- 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.
- 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. -
- 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.
- 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." +publications: + - papername: "Formally Verified Rounding Errors of the Logarithm-Sum-Exponential Function" + url: "https://inria.hal.science/hal-04674600" software: sectiontitle: "Les logiciels" @@ -149,7 +92,7 @@ software: domaines, grâce à son support inné du polymorphisme, sa compatibilité avec le format SMT2 et plusieurs théories lui permettant de manipuler formellement les types de base. Le Club Alt-Ergo rassemble un groupe - d’industriels (Thales, MERCE, Trust In Soft, Adacore, etc.) utilisant + d’industriels (Thales, MERCE, Trust In Soft, AdaCore, etc.) utilisant Alt-Ergo dans leur activité et permet de financer l’évolution d’Alt-Ergo." @@ -176,4 +119,65 @@ software: url: - "https://www.trust-in-soft.com/trustinsoft-analyzer" description: "Bientôt..." + +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.
+ 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.
+ 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. +
+ 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.
+ 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." --- diff --git a/content/fr/post/00_kickoff_du_projet_decysif.md b/content/fr/post/00_kickoff_of_project_decysif.md similarity index 95% rename from content/fr/post/00_kickoff_du_projet_decysif.md rename to content/fr/post/00_kickoff_of_project_decysif.md index b6e3815..d2a1305 100644 --- a/content/fr/post/00_kickoff_du_projet_decysif.md +++ b/content/fr/post/00_kickoff_of_project_decysif.md @@ -9,7 +9,7 @@ title: "Diagnostic de Cyber-Sécurité Formel: DéCySif" Ce mardi 19 décembre 2023, tous les partenaires du projet Decysif ([TrustInSoft](https://trust-in-soft.com/), -[Adacore](https://www.adacore.com/), [OCamlPro](https://www.ocamlpro.com) et +[AdaCore](https://www.adacore.com/), [OCamlPro](https://www.ocamlpro.com) et l’équipe [LMF](https://lmf.cnrs.fr/)) se sont réunis dans les locaux de TrustInSoft dans le 14ème arrondissement de Paris pour la réunion de lancement du projet ! diff --git a/hugo.toml b/hugo.toml index 464928e..749fb4c 100644 --- a/hugo.toml +++ b/hugo.toml @@ -26,7 +26,7 @@ Paginate = 10 legal = "DéCySif is a project funded by the i-Démo call and the Ile-de-France region." [params] - site_logo = 'images/logo_decysif_excellence_for_security_blank_bg_rectangle.svg' + site_logo = '/images/logo_decysif_excellence_for_security_blank_bg_rectangle.svg' text_color = "" recent_posts_number = 5 [params.contact] diff --git a/layouts/_default/single.html b/layouts/_default/single.html new file mode 100644 index 0000000..df8181b --- /dev/null +++ b/layouts/_default/single.html @@ -0,0 +1,67 @@ +{{ define "header" }} + {{/* We can override any block in the baseof file be defining it in the template */}} + {{ partial "page-header.html" . }} +{{ end }} +{{ define "main" }} + {{ $section := .Site.GetPage "section" .Section }} +
+
+ + {{ partial "social-share.html" . }} +

+ {{- .Title -}} +

+ {{ with .Params.author | default .Site.Params.author }} +

+ {{ $.Render "by" }} + {{- if reflect.IsSlice . -}} + {{ delimit . ", " | markdownify }} + {{- else -}} + {{ . | markdownify }} + {{- end -}} + +

+ {{ end }} + {{/* Hugo uses Go's date formatting is set by example. Here are two formats */}} + {{ if not .Date.IsZero }} + + {{end}} + + {{/* + Show "reading time" and "word count" but only if one of the following are true: + 1) A global config `params` value is set `show_reading_time = true` + 2) A section front matter value is set `show_reading_time = true` + 3) A page front matter value is set `show_reading_time = true` + */}} + {{ if (or (eq (.Param "show_reading_time") true) (eq $section.Params.show_reading_time true) )}} + - {{ i18n "readingTime" .ReadingTime }} + - {{ i18n "wordCount" .WordCount }} + {{ end }} +
+
+ {{- .Content -}} + {{- partial "tags.html" . -}} +
+ {{ if .Site.Config.Services.Disqus.Shortname }} + {{ template "_internal/disqus.html" . }} + {{ end }} + {{ if .Site.Params.commentoEnable }} + {{- partial "commento.html" . -}} + {{ end }} +
+
+ + + +
+{{ end }} diff --git a/layouts/index.html b/layouts/index.html index 137e981..94e9527 100644 --- a/layouts/index.html +++ b/layouts/index.html @@ -5,25 +5,23 @@
-

{{ .Params.sectiontitle }}

-
{{ .Params.synopsis | markdownify }}
+
+
-

{{ .Params.project.sectiontitle }}

-
{{ .Params.project.content | markdownify}}
@@ -37,30 +35,54 @@

{{ .Params.coordinator.content | markdownify}}
+
    + {{ if (eq .Site.Language.Lang "fr") }} +

    + Publications Scientifiques +

    + {{ else }} +

    + Scientific Papers +

    + {{ end }} + {{ range $.Params.publications }} +
  • + {{ .papername }} +
    • + {{ end }} +

- +
-

- {{ .Params.collaborators.sectiontitle }} +

+ {{ .Params.software.sectiontitle }}

- {{ range $.Params.collaborators.consortium }} + {{ range $.Params.software.tools }}
-

{{ .name }}

-
+

+ {{ .name }} +

+

{{ .description | markdownify }}

-
- {{ .url }} +
+
    + {{ range .url }} +
  • + {{ . }} +
    • + {{ end }} +
{{ end }} @@ -68,16 +90,16 @@

{{ .name }}

- +
-

- {{ .Params.software.sectiontitle }} +

+ {{ .Params.collaborators.sectiontitle }}

- {{ range $.Params.software.tools }} + {{ range $.Params.collaborators.consortium }}

{{ .name }}

@@ -88,13 +110,7 @@

{{ .name }}

-
    - {{ range .url }} -
  • - {{ . }} -
    • - {{ end }} -
+ {{ .url }}
{{ end }} @@ -102,5 +118,6 @@

{{ .name }}

+
{{ end }} diff --git a/layouts/partials/site-navigation.html b/layouts/partials/site-navigation.html index 4bf4361..0afe3bb 100644 --- a/layouts/partials/site-navigation.html +++ b/layouts/partials/site-navigation.html @@ -17,8 +17,8 @@
  • - - {{ .Params.project.sectiontitle }} + + {{ .Params.software.sectiontitle }}
  • @@ -26,11 +26,6 @@ {{ .Params.collaborators.sectiontitle }}
    • -
  • - - {{ .Params.software.sectiontitle }} - -
    • {{ end }} {{ with .Site.GetPage "/post/_index.md" }}