Clefs n°70 mars 2020
Clefs n°70 mars 2020
  • Prix facial : gratuit

  • Parution : n°70 de mars 2020

  • Périodicité : annuel

  • Editeur : CEA

  • Format : (230 x 280) mm

  • Nombre de pages : 52

  • Taille du fichier PDF : 7,8 Mo

  • Dans ce numéro : sacrées mathématiques !

  • Prix de vente (PDF) : gratuit

Dans ce numéro...
< Pages précédentes
Pages : 40 - 41  |  Aller à la page   OK
Pages suivantes >
40 41
LES DOMAINES D’APPLICATION TECHNOLOGIES DE L’INFORMATION CONTRIBUTEURS (Direction de la recherche technologique) Mihail Asavoae est ingénieur-chercheur au Département des systèmes et circuits intégrés numériques du CEA/List. Belgacem Ben Hedia est ingénieur-chercheur au Département des systèmes et circuits intégrés numériques du CEA/List. Mathieu Jan est ingénieur-chercheur au Département des systèmes et circuits intégrés numériques du CEA/List. [1] R.L. Graham. Bounds for Certain Multiprocessing Anomalies. The Bell System Technical Journal, Nov. 1966  : ieeexplore.ieee. org/document/6767827 [2] Mathieu Jan, Mihail Asavoae, Martin Schoeberl, Edward A. Lee. Formal Semantics of Predictable Pipelines : a Comparative Study. In 25th Asia and South Pacific Design Automation Conference (ASP-DAC 2020), Beijing, China, January 2020. [3] Mihail Asavoae, Belgacem Ben Hedia, Mathieu Jan. Formal Executable Models for Automatic Detection of Timing Anomalies. In Proc. of the 18th International Workshop on Worst-Case Execution Time (WCET 2018), Barcelona, Spain, July 2018. 40 - Sacrées mathématiques ! Détecter les anomalies temporelles L’utilisation d’anomalies ou de failles temporelles est un procédé très présent dans le genre cinématographique de science-fiction/fantastique, à l’image des sagas Star Trek, Retour vers le futur ou Terminator. L’enjeu est à chaque fois de venir corriger une décision ponctuelle qui engendre une situation globale problématique dans le futur, le suspens résidant dans l’incertitude des étapes à réaliser pour prendre la bonne décision. Contre-intuitives  : une accélération locale ralentit le temps global d’une exécution. Anomalie se produisant dans l’ordonnancement des accès à des unités fonctionnelles (dans un pipeline, élément d’architecture d’un processeur). ∆ 1 > ∆ 2 ET 1 < ET 2 Bien évidemment, il n’est pas possible de faire de tels retours en arrière pour corriger l’exécution des systèmes embarqués critiques, présents dans un avion ou une voiture ! C’est dans la phase de conception de ces systèmes qu’il faut identifier l’impact de décisions locales sur leur comportement final pire cas. Une anomalie temporelle intervient lorsqu’une décision locale, par exemple une accélération due à une fonctionnalité matérielle ou une augmentation du nombre de ressources matérielles, engendre un phénomène inattendu de ralentissement global. Dès 1966, ces phénomènes ont été étudiés dans l’ordonnancement de programmes informatiques [1] mais ils restent insuffisamment définis au niveau des processeurs et sont présents dès que des programmes se partagent l’accès à un élément matériel durant leur exécution, que ce soit une unité fonctionnelle ou une mémoire. Ceci se manifeste par exemple lorsque le processeur traite les instructions d’un programme en parallèle, si elles ne sont pas interdépendantes, afin d’accélérer leur traitement. Cela peut conduire à ce que deux instructions veuillent être exécutées en même temps sur une même unité fonctionnelle. Les conséquences TYPES D’ANOMALIES TEMPORELLES Δ Δ 2 1 Δ ET 1 ET 2 ET 2 ET 1 Δ g Les voix de la recherche - #70 - Clefs Anomalies d’amplifications  : une variation locale engendre une variation globale plus importante. Anomalie se produisant dans un pipeline ordonné accédant, selon une politique « Premier arrivé, premier servi » (First Come First Served, en anglais), à un arbitre de bus gérant l'accès à une ressource partagée. ∆ g > ∆ l temporelles de ces comportements dans un système embarqué sont largement sur-approximées. Par ailleurs, une fois leur présence identifiée, et les chemins menant à leurs manifestations construits, la difficulté réside dans le fait de s’assurer que des changements locaux intervenant à différents moments dans l’exécution d’un programme (les étapes dans notre analogie cinématographique), n’engendrent pas une dégradation dans le comportement final pire cas mais bien une amélioration de ces systèmes. Le CEA-List développe Leaf, une boite à outils de détection de tels phénomènes, en s’appuyant sur des outils de vérification de modèles (model checking en anglais), puis d’insertions d’éléments de corrections pour les contourner voire les faire disparaître du comportement de système en adaptant la progression de l’exécution des programmes sur les architectures matérielles (la progression de temps « logique »). Les premiers résultats obtenus et publiés dans des conférences [2, 3] sont très encourageants… Espérons que cette solution, qui n’est pas de la science-fiction, obtienne autant de succès au box-office des technologies que les sagas cinématographiques évoquées ! l
o 404 cl it 1 0 10 1 CI CI 0 0101 zn:  :  : x) —qqn, 21)(-,4_v.t.n'jà) l "1 H 1-f-x4y+2alif4-45 tet+,4 Y1-2 a)-(3 èqe,Tii.2t a)-(3i+-21 -45{7Y ; i-ri-x-i- ; +k:2a1-i-X)- s —-..-'î S, if. 1 a CAO 1 °I) 1010 0 1A 0 " 10 ° 0 10 1 o II TECHNOLOGIES DE L’INFORMATION v tiv 0 I La vérification formelle de codes informatiques 0 10 1 0 Les codes informatiques jouent un rôle critique dans nos sociétés modernes  : ils conduisent notamment nos trains et nos voitures, font voler nos avions et nos satellites, contrôlent nos moyens de communication et nos finances et contribuent à nous maintenir en bonne santé. Il est donc indispensable de s’assurer de leur sûreté et de leur sécurité. Alors que ces codes peuvent atteindre des tailles gigantesques (jusqu’à 100 millions de lignes de code dans une voiture hautde-gamme moderne), la moindre petite erreur peut avoir des conséquences dramatiques pour nos vies, notre environnement ou nos économies. Il faut donc s’assurer qu’aucune ne peut survenir  : c’est le problème de la sûreté logicielle. En outre, des individus, des organisations ou des États malveillants peuvent également exploiter des défauts dans ces codes pour attaquer les systèmes qu’ils régissent, afin par exemple d’en prendre le contrôle, les détruire ou obtenir des informations sensibles sur leurs utilisateurs. C’est le problème de la sécurité logicielle. Cependant, qu’il s’agisse de sûreté ou de sécurité, les méthodologies classiquement utilisées dans l’industrie du logiciel, et fondées sur les relectures de code et les tests, ne permettent que de trouver certaines erreurs, mais absolument pas de démontrer leur absence pour toutes les entrées possibles du programme [1]. Dès lors, quoi de mieux que les mathématiques pour effectuer de telles démonstrations ? Principes et approches de vérification formelle Pour raisonner rigoureusement sur des codes informatiques, il convient de les modéliser comme des objets mathématiques afin de pouvoir exprimer et démontrer formellement leurs propriétés. C’est le principe de la vérification formelle. Étant donné la taille gigantesque des codes, il est également indispensable d’outiller ce processus de modélisation et de démonstration, humainement inaccessible. Il s’agit donc de développer des logiciels spécifiques, capables de réaliser cette analyse mathématique, afin d’établir automatiquement et rigoureusement des propriétés sur les comportements des codes à l’exécution, quelles que soient les données manipulées. Malheureusement, le théorème de Rice (1953) démontre qu’une telle analyse ne peut pas exister. Mais il est possible de contourner ces limitations dans une certaine mesure  : calcul automatique correct mais approché (réponse « peut-être » possible, Interprétation LES DOMAINES D’APPLICATION CONTRIBUTEURS (Direction de la recherche technologique) Sébastien Bardin est ingénieur au Laboratoire sûreté et sécurité des logiciels (Département d’ingénierie logiciels et systèmes) au CEA/List. Florent Kirchner est chef du Laboratoire sûreté et sécurité des logiciels (Département d’ingénierie logiciels et systèmes) au CEA/List. Virgile Prevosto est ingénieur au Laboratoire sûreté et sécurité des logiciels (Département d’ingénierie logiciels et systèmes) au CEA/List. Julien Signoles est ingénieur au Laboratoire sûreté et sécurité des logiciels (Département d’ingénierie logiciels et systèmes) au CEA/List. [1] Un petit programme prenant en entrée seulement 4 entiers machine à 2256 (1075) entrées possibles, à comparer aux 1080 atomes de l’Univers visible. Clefs - #70 - Les voix de la recherche Sacrées mathématiques ! - 41



Autres parutions de ce magazine  voir tous les numéros


Liens vers cette page
Couverture seule :


Couverture avec texte parution au-dessus :


Couverture avec texte parution en dessous :