diff --git a/Makefile b/Makefile index 6856c2b..8637127 100644 --- a/Makefile +++ b/Makefile @@ -32,7 +32,7 @@ all: $(PDFS) watch: while inotifywait -e close_write "src/étude/OCamlPro_PPAQSE-COTS_rapport.typ" || true; do make; done -$(BUILD_DIR)/%.pdf: src/%.typ $$(call deps,src/%.typ) $$(dir src/%)/bibliography.yml Makefile | $$(@D)/. +$(BUILD_DIR)/%.pdf: src/%.typ src/base.typ $$(call deps,src/%.typ) $$(dir src/%)/bibliography.yml Makefile | $$(@D)/. $(TYPST) c $(TYPST_ARGS) $< # force moving file for typst seems to always try building locally oO mv -f src/$*.pdf $@ diff --git a/src/base.typ b/src/base.typ index 65307f0..d3b728d 100644 --- a/src/base.typ +++ b/src/base.typ @@ -66,6 +66,7 @@ dir: ttb, spacing: 2pt, line(length: 100%), + v(5pt), align( center + horizon, [ diff --git "a/src/pr\303\251sentation/OCamlPro_PPAQSE-COTS_pr\303\251sentation.typ" "b/src/pr\303\251sentation/OCamlPro_PPAQSE-COTS_pr\303\251sentation.typ" index e69de29..b2872ae 100644 --- "a/src/pr\303\251sentation/OCamlPro_PPAQSE-COTS_pr\303\251sentation.typ" +++ "b/src/pr\303\251sentation/OCamlPro_PPAQSE-COTS_pr\303\251sentation.typ" @@ -0,0 +1,339 @@ + +#import "../base.typ": * +#import "../étude/links.typ": * + + +#show: presentation + +#title-slide( + title: [ + Écosystèmes COTS de développement et de vérification des logiciels + critiques et temps réel + ], + subtitle: "", + authors: [Julien Blond (julien.blond\@ocaml.pro)], +) + +#slide[ + = OCamlPro + + - PME française créée en 2011 + - ADN recherche et liens étroits avec la recherche académique. + - OCaml : core team, opam & optimisations + - R&D langages (DSL) & dette technque (Cobol) + - Méthodes formelles (Alt-Ergo) + - Certification Sécurité (CC EAL6+) + - Formations (OCaml, Rust, Coq) + + Jane street, Inria, DGFiP, Samsung, Mitsubishi, Thales, CEA, Adacore, + TrustInSoft +] + +#slide[ + = Objectif + + Tour d'horizon des langages de programmation dans la sûreté: + - C + - C++ + - Ada + - Scade + - OCaml + - Rust + + Donner suffisamment d'informations pour faire un choix éclairé +] + +#slide[ + = C + + - Créé en 1972 par Dennis Ritchie + - Programmation système (Unix) + - Langage bas niveau + - Standardisé : C89, C99, C11, C18, C23 (draft)... + - ... mais une sémantique indéterministe. + + +] + +#slide[ + == C : Paradigme + + Essentiellement *impératif* et *procédural* + + ```c + int add_value(struct state *s, int v) + { + int code = KO; + if (nullptr != s) { + s->acc += v; + code = OK; + } + return code; + } + ``` +] + +#slide[ + == C : Mécanismes de protection intrinsèques + + #align( + center, + table( + columns: (auto, auto), + align: (left, left), + align(center)[*Avantage*], align(center)[*Inconvénient*], + [Système de type], [Trop rudimentaire et laxe], + [ ], [Gestion manuelle des pointeurs], + [Analyses des compilateurs], [ + - Pas activées par défaut + - Pas standardisées + ], + ) + ) +] + +#slide[ + == C : Compilateurs + + #align( + center, + table( + columns: (auto, auto), + align: (left, left), + align(center)[*Compilateur*], align(center)[*Remarques*], + [GCC], [La référence], + [Clang], [Le challenger], + [icc/icx], [Intel], + [MSVC], [Microsoft], + [AOCC], [AMD], + [sdcc], [microcontrôleurs], + [CompCert], [Vérifié formellement], + ) + ) +] + +#slide[ + == C : Interfaçage + + #v(2cm) + - Le C permet d'écrire de l'assembleur dans le texte. + + - Il sert de cible pour la plupart des langages. + +] + +#slide[ + == C : Adhérence + + #v(2cm) + Aucune, il faut juste un compilateur pour l'architecture cible. +] + +#slide[ + == C : Gestionnaires de paquets + + - Deux gestionnaires classiques : Conan & vcpkg + - Un gestionnaire de _vendoring_ : Clib + - Possibibilité d'utiliser des gestionnaires agnostriques (Nix, 0install, ...) + + Pour les systèmes embarqués : Buildroot, Yocto, ... ont leur propre + _packaging_. +] + +#slide[ + == C : Communauté + + - Très large + - Entreprises + - OS (FSF) + - Système (Linux) + - Embarqué +] + +#slide[ + == C : Debugueurs + + #{ + set text(size: 16pt) + + figure( + table( + columns: (auto, auto, auto), + [*Debugueur*], [*Architectures*], [*License*], + [*#linaro*], [x86-64, ARM, PowerPC, Intel Xeon Phi, CUDA], [Propriétaire], + [*#gdb*], [x86, x86-64, ARM, PowerPC, SPARC, ...], [GPLv3], + [*#lldb*], [i386, x86-65, AArch64, ARM], [Apache v2], + [*#totalview*], [x86-64, ARM64, CUDA], [Propriétaire], + [*#undo*], [x86-64], [Propriétaire], + [*#valgrind*], [x86, x86-64, PowerPC, ARMv7], [GPL], + [*#vsd*], [x86, x86-64], [Propriétaire], + [*#windbg*], [x86, x86-64], [Gratuit], + [*#rr*], [x86, x86-64, ARM], [GPLv2], + ) + ) + } +] + +#slide[ + == C : Tests + + #figure( + table( + columns: (auto, auto, auto, auto, auto), + [*Outil*], [*Tests*], [*Generation*], [*Gestion*], [_*mocking*_], + [*#cantata*], [UIRC], [+++], [✓], [], + [*#criterion*], [U], [+], [], [], + [*#libcester*], [U], [+], [✓], [✓], + [*#novaprova*], [U], [+], [✓], [✓], + [*#opmock*], [U], [++], [], [✓], + [*#parasoft*], [UC], [++], [✓], [], + [*#TPT*], [UINC], [+++], [✓], [], + [*#vectorcast*], [UC], [++], [✓], [✓], + ), + ) +] + +#slide[ + + == C : Parsing + + Il existe beaucoup d'outils d'analyse syntaxique en C mais les plus + connus/matures qui suffisent dans la grande majorité des cas sont: + - Flex/Bison + - ANTLR + + +] + +#slide[ + == C : Méta-programmation + + - Le préprocesseur permet de faire précalculer des expressions simples + par le compilateur (souvent inutile) + - Il existe des _tricks_ d'expansion récursive bornée (à éviter) + ```c + /* #define sum(n) ((n * (n + 1)) / 2) */ + inline int sum(int n) { return (n * (n + 1)) / 2; } + int main() { return sum(10); } + ``` + ```asm + 0x0000000000001040 : endbr64 + 0x0000000000001044 : mov $0x37,%eax + 0x0000000000001049 : retq + ``` +] + +#slide[ + == C : Dérivation + + - Les macros permettent une forme archaïque de dérivation + ```c + #define COULEUR X(ROUGE, 0xFF0000) X(VERT, 0x00FF00) X(BLEU, 0x0000FF) + #define X(c, v) c = v, + typedef enum { COULEUR } couleur_t; + #undef X + ``` +] + + #slide[ + == C : Runtime Errors + + Les analyseurs statiques corrects permettant de se prémunir contre des + erreurs à _runtime_ sont: + - #astree + - #eclair + - #framac + - #polyspace + - #tisanalyser + ] + + #slide[ + == C : Formalisation + + #[ + #set text(size: 18pt) + - Par transpilation (automatique ou manuelle) vers Coq (VerifiedC): + #align(center, + grid( + columns: (auto, auto, auto, auto, auto), + [C], [$=>$], [Coq], [$=>$], [Preuves (Hoare, WP)] + ) + ) + + - Par annotation et preuve (semi) automatiques (Frama-C, RedefinedC, VerCors): + ```c + /*@ requires \valid(a) && \valid(b); + @ ensures A: *a == \old(*b) ; + @ ensures B: *b == \old(*a) ; + @ assigns *a,*b ; + @*/ + void swap(int *a,int *b); + ``` + ] + + ] + + +#slide[ + == C : WCET + + Il existe plusieurs outils basés sur une analyse statique binaire : + - #chronos (IR) + - #bound-T + - #aiT + - #sweet (IR) + - #otawa (modulaire) + - #rapidtime + +] + +#slide[ + == C : Pile + + Pour l'analyse statique de la pile: + - #gcc + - #stackanalyser + - #t1stack (+ annotations) + - #armlink +] + +#slide[ + == C : Qualité numérique + + #[ + #set text(size: 18pt) + Se prémunir contre les erreurs numériques (overflow, précision, ...) + - par analyse statique: + - #fluctuat + - #astree + - #polyspace + - #gappa (+ annotations #framac) + - par un calcul dynamique: + - #cadna + - #mpfr + - #gmp + ] + +] + +#slide[ + == C : Assurances + + Niveau d'assurance donné par le C est paradoxal : + - quasiment pas de sécurité intrinsèque + - l'histoire et l'usage ont apporté des outils externes qui fiabilisent le C + + Le développpement reste relativement peu productif et coûteux: + - même un bon programmeur fait des erreurs + - A/R entre services de développement et de vérification + - licences, formations, ... +] + +#slide[ + == C : Critique + + Le C est utilisé dans tous les domaines critiques soit + - directement pour écrire le système (en entier ou au moins les interfaces + avec le matériel); + - indirectement comme langage cible (#Ada, #Scade, ...). +]