Journal HiFive1: Un Arduino à 320Mhz entièrement libre pour 2017

31
29
nov.
2016

À l'heure où j'écris ces lignes a lieu le 5 ème workshop sur jeux d'instruction libre (ISA Risc-V au campus google à Mountain View.

Et c'est à cette occasion qu'est présenté la carte HiFive1 composée d'un microcontrôleur Freedom Everywhere 310 (FE310) à cœur SiFive (utilisant le jeux d'instructions Risc-V). Une carte compatible Arduino mais 10 fois plus puissante et entièrement libre, jusqu'au silicium.

La description hardware en Chisel/Verilog est disponible sur github et il est possible de simuler intégralement le modèle qui tournera sur la carte.

Contrairement à l'open-v, le développement du HiFive1 est déjà terminé et le crowdfunding organisé n'est là que pour les précommandes.

La société SiFive se base sur ce microcontrôleur ainsi que sur un microprocesseur Freedom U500 pour promouvoir son savoir faire et proposer à ses clients des puce «full-custom» à base de briques opensource.

Visiblement, pour 60$ il est donc possible de se procurer le kit compatible arduino intégralement open-source qui sera disponible en février 2017.

  • # Ça évolue vite !

    Posté par . Évalué à 10.

    L'Open hardware évolue drôlement vite depuis un an. Ça fait plaisir. Ça fera peut-être bouger les choses vers moins de blobs binaires.

    En tout cas, un grand merci à tous ceux qui nous font part de ses projets via des journaux et des dépêches.

    Cette signature est publiée sous licence WTFPL

  • # Preuve formelle et supervision de la fabrication et de la distribution

    Posté par . Évalué à -10.

    Le projet présenté ici me semble très intéressant. Cependant, il convient de noter que des portes dérobées peuvent toujours se glisser :

    • dans la conception, surtout tant qu'il n'y a pas de preuve formelle sur les schémas de conception (conformité des schémas avec les spécifications, ce qui revient à de la preuve formelle sur le code Chisel/Verilog). Les spécifications étant disponibles, l'audit et la preuve formelle peuvent être réalisés à postériori ;
    • particulièrement à la fabrication, tant qu'elle n'est pas opérée ou au moins supervisée par une communauté de confiance ;
    • pendant la distribution du matériel, par substitution malveillante.

    Pour aller plus loin, je propose la lecture de ce commentaire (et des commentaires source, dans lesquels je propose des pistes comme, entre autres et à minima, la supervision de la fabrication par une équipe d'assesseurs techniques tirés au sort parmi la communauté de hackers compétents, supervision rendue possible contractuellement avec l'industriel).

    Même en supposant la conception non malveillante, je considère qu'il n'est pas sérieux de faire confiance aveuglément à un fabricant sans supervision approfondie, du fait qu'il est lié par des intérêts financiers à des donneurs d'ordre, donc potentiellement à des pressions d'ordre politique et géostratégique. La distribution du matériel est également une phase critique.

    • [^] # Re: Preuve formelle et supervision de la fabrication et de la distribution

      Posté par . Évalué à 3.

      la supervision de la fabrication par une équipe d'assesseurs techniques tirés au sort parmi la communauté de hackers compétents

      Qui désigne ces hackers ?

      • [^] # Re: Preuve formelle et supervision de la fabrication et de la distribution

        Posté par . Évalué à -10. Dernière modification le 30/11/16 à 09:16.

        Qui désigne ces hackers ?

        • ça peut être moi qui suis quasi omniscient. Que je sorte ? Déjà ? Snif…
        • ça peut être une coterie comme les franc-maçons, comme ça on maximise le potentiel d'échec.
        • entre les deux, ça peut être tous les terriens reconnus par leurs pairs comme ayant porté un intérêt un peu soutenu sur le sujet du matériel libre.

        Je développe sur le pouce la troisième hypothèse qui me semble plus raisonnable, en assumant le fait que le protocole nécessite d'être muri :

        a) les terriens désignent leurs semblables reconnus comme ayant porté un intérêt un peu soutenu sur le sujet du matériel libre, intérêt identifiable idéalement par des sources (des commentaires sur le net, par exemple). Voici un protocole envisageable : chacun des terriens peut désigner jusqu'à 10 personnes et fournit pour chacune quelques sources pour justifier le choix, si possible. On pourra envisager d'étendre les critères à la simple implication dans une activité professionnelle sur le sujet de la fabrication du matériel (notamment la gravure des circuits intégrés), mais il faudra prévoir des garde-fous comme un quota de témoignages de probité morale…

        b) dans la liste de noms obtenus avec un nombre de citations défini pour chacun, on pourra appliquer différents protocoles pour s'assurer de leur compétence et de leur intégrité. Une possibilité est de garder uniquement les 80 centiles au centre du panel (écartant les 10 centiles les moins nommés, pour écarter ceux probablement moins compétents, à l'arrache, et les 10 centiles les plus nommés, pour écarter les biais liés à la sur-médiatisation et l'exposition aux pressions que cela peut impliquer, à l'arrache).

        Parmis ceux nommés et retenus à ce stade, on identifiera ceux qui acceptent de s'impliquer dans la suite du protocole de désignation et ceux qui acceptent l'éventualité de s'impliquer comme assesseur technique après tirage au sort.

        Pour compenser les défaillances de la sélection des 80 centiles du milieu, on pourra accorder un repêchage de façon ciblée et justifiée (des sources), qui puisse être opéré par la majorité absolue (ou un autre mode de votation) des 80 centiles du milieu.

        La compétence des futurs tirés au sort devra être évaluée pour dépasser un seuil minimum, avec des critères choisis par l'ensemble des hackers retenus à ce stade, le choix des critères étant réalisé par vote (à la majorité absolue, par exemple, ou par vote plus subtil comme le vote de valeur — cf. Vote_par_valeurs et ).

        c) Le tirage au sort a lieu parmi ceux retenus. La compétence de ceux tirés au sort est évaluée selon les critères définis. Ceux qui n'atteignent pas le seuil de compétence ne sont finalement pas retenus et un nouveau tirage au sort a lieu pour atteindre le nombre d'assesseurs techniques nécessaires. Dans ce cas, la compétence des nouveaux tirés au sort est évaluée, et s'il y en a qui ne sont pas qualifiés, on reprend le processus de tirage au sort, et ainsi de suite.

        d) pour les hackers nommés puis tirés au sort et reconnus compétents au-dessus d'un certain seuil, une formation complémentaire a lieu, que ce soit pour acquérir quelques bases manquantes ou que ce soit plus spécifiquement pour opérer la supervision de la fabrication.

      • [^] # Re: Preuve formelle et supervision de la fabrication et de la distribution

        Posté par (page perso) . Évalué à 2.

        Je propose d'adopter le même système que l’élection du doge de Venise.

        Pour info: https://fr.wikipedia.org/wiki/Doge_de_Venise#.C3.89lection

    • [^] # Re: Preuve formelle et supervision de la fabrication et de la distribution

      Posté par (page perso) . Évalué à 4.

      À quand les captchas sur les commentaires linuxfr ?
      Histoire d'éviter ce genre de robot pipotron-complotiste.

    • [^] # Re: Preuve formelle et supervision de la fabrication et de la distribution

      Posté par . Évalué à 2.

      tant qu'elle n'est pas opérée ou au moins supervisée par une communauté de confiance ;

      Pourriez vous ce donner le nom d'au moins une personne de cette "communauté de confiance" qui à fait la preuve formelle de votre processeur AMD ou Intel dans votre PC ou ARM de votre téléphone ou tablette ?

      kentoc'h mervel eget bezan saotred

      • [^] # Re: Preuve formelle et supervision de la fabrication et de la distribution

        Posté par . Évalué à -10.

        Pour faire de la preuve formelle sur les schémas des circuits intégrés numériques, il faut les schémas. File-moi les schémas (ou mieux, le code Bluespec (1) et la licence du soft à 100.000 dollars) des processeurs AMD, Intel, ou ARM, et on en reparle. Et s'il te plait, fais-le légalement (bonne chance), je n'ai pas envie d'avoir les chinois du FBI sur le dos, j'en ai assez avec le Mossad et les sayanim pour avoir seulement participé au hacking des racines kabbalistes (2) du sionisme.

        (1) Bluespec est un langage de description matérielle qui nécessite une phase d'apprentissage non négligeable notamment sur la gestion des preuves formelles, cf. par exemple ce journal.

        (2) J'ai relayé par ici ce que révèle l'historien Youssef Hindi, à savoir l'influence néfaste de la kabbale dans le judaïsme, kabbale qui l'a largement perverti de l'intérieur et constitue les racines historiques du sionisme, autour du 13e siècle et au-delà, menant à un projet messianique apocalyptique hégémonique dans lequel il est conseillé d'inverser les valeurs et d'ainsi hâter la venue du Messie. Ah, désolé, là non plus je ne suis pas complotiste, c'est documenté et sourcé.

      • [^] # Re: Preuve formelle et supervision de la fabrication et de la distribution

        Posté par (page perso) . Évalué à 9.

        Ceci dit, au risque d'alimenter les complotistes, l’état de l'art, c'est des choses comme ça:

        http://sharps.org/wp-content/uploads/BECKER-CHES.pdf

        "Stealthy dopant-level hardware trojans"

        Avec la réponse 2 ans plus tard:

        http://eprint.iacr.org/2014/508.pdf

        "Reversing Stealthy Dopant-Level Circuits"

        Autre papier intéressant dans la même veine:

        "Threshold-Dependent Camouflaged Cells to Secure
        Circuits Against Reverse Engineering Attacks"

        http://arxiv.org/pdf/1605.00684

        • [^] # Re: Preuve formelle et supervision de la fabrication et de la distribution

          Posté par . Évalué à -6.

          Merci Misc<. Ce que tu présentes là est important.

          On va expliciter pour les moules non encore farcies de portes dérobées matérielles furtives réalisées au niveau du dopage ! C'est compliqué ? Je t'explique.

          Il y a trois articles présentés, tous en anglais. Dans ce commentaire, je vais traiter du premier. C'est pour ça qu'il n'y a qu'un "1)" et pas de suite en "2)" ni en "3)" à ce stade. Si vous êtes tous sages et si les augures sont propices, je livrerai la suite à la prochaine lune souriante. Si quelqu'un d'autre veut rédiger la suite avec le même niveau d'exigence, qu'il s'exécute sans tarder, car c'est propice pour la communauté des moules, en terme de pré-formation… pour pouvoir opérer une surveillance du processus de fabrication à base de balayage par microscopie électronique ou par rayons ciblés d'ions (mais là, nous anticipons le deuxième article) :)

          1) le premier est titré "Stealthy dopant-level hardware trojans", ce qui peut se traduire par « Cheval de Troie matériel furtif réalisé au niveau du dopage ».

          Il a été rédigé postérieurement à février 2013 (l'article en lui-même n'est pas daté mais l'article le plus récent cité à la fin, en référence, date de février 2013).

          a) Pour expliciter à partir du titre, il y est question de cheval de Troie, au niveau du matériel, mais sans ajout de circuits (pas de transistors supplémentaires gravés dans le silicium, le résumé de l'article décrit cela en disant que c'est "sous le niveau des portes logiques"), rendant la malveillance furtive (du moins ça ne se voit pas au microscope optique) et ça se passe en modifiant le dopage des transistors (en changeant la polarité des dopants au sein des transistors existants), pour réaliser des fonctions non prévues par le concepteur du schéma de gravure légitime du circuit intégré.

          b) J'explicite la question du dopage :

          • bien qu'il y ait différentes variantes de transistors (cf. Transistor), prenons simplement le cas classique d'un transistor bipolaire (cf. Transistor_bipolaire) pour présenter la problématique.

          • le Wikipédia francophone (dans son état actuel) nous dit — dans l'article sur les transistors — que ce dernier est « un dispositif électronique à base de semi-conducteur dont le principe de fonctionnement est basé sur deux jonctions PN (cf. Jonction_P-N), l'une en direct et l'autre en inverse ».

          • bon, pour t'éviter de cliquer sur chaque lien, et parce que les articles ne sont que des ébauches pour l'instant, il s'agit en fait de trois couches de matériau semi-conducteur (par exemple du silicium), dopées chacune (le dopage, c'est un apport d'un matériaux tiers qui est diffusé dans la couche de silicium à la fabrication), soit en positif (noté P, du fait que le matériau diffusé dans le silicium n'est pas électroniquement neutre mais chargé positivement, parce qu'il comporte une déficience d'électrons, c'est à dire un surplus de "trous"), soit en négatif (noté N, du fait que le matériau diffusé dans le silicium est chargé négativement, parce qu'il comporte un surplus d'électrons).

          • le Wikipédia francophone (dans son état actuel) nous dit aussi — toujours dans l'article sur les transistors — qu' « un transistor bipolaire se compose de deux parties de substrat semiconducteur dopées identiquement (P ou N) séparées par une mince tranche de semiconducteur dopée inversement ; on a ainsi deux types : N-P-N et P-N-P. »

          Voilà présenté ce qu'est le dopage, une jonction PN (c'est à dire une diode, en fait) et le transistor bipolaire classique.

          c) voici la traduction (personnelle) du résumé de l'article en français :

          « Dans les années récentes, les chevaux de Troie matériels ont attiré l'attention des gouvernements et de l'industrie aussi bien que de la communauté scientifique. Une des préoccupations principales est que les circuits intégrés, par exemple, dans le domaine militaire ou des applications d'infrastructure critique, pourraient être manipulés malicieusement pendant le processus de fabrication, qui a souvent lieu à l'étranger. Cependant, puisqu'il n'y a pas encore eu de cheval de Troie matériel qui ait été découvert jusqu'alors, nous en savons peu sur l'allure que prendrait un tel cheval de Troie et à quel point il serait difficile en pratique d'en implémenter un.
          Dans cet article, nous proposons une approche extrêmement furtive pour implémenter des chevaux de Troie matériels sous le niveau des portes logiques et nous évaluons leur impact sur la sécurité du dispositif cible. Au lieu d'ajouter des circuits additionnels au schéma de conception ciblé, nous insérons nos chevaux de Troie matériels en changeant la polarité des dopants aux transistors existants. Puisque le circuit modifié apparaît légitime sur toutes les couches gravées (incluant métal et silicium), notre famille de chevaux de Troie est résistante à la plupart des techniques de détection, incluant l'inspection optique à une granularité fine et la vérification pour détecter des "circuits dorés" [NdT : je ne sais pas traduire autrement "Golden chips" (qui est entre guillemets dans le texte) - j'observe que c'est une marque de frites, semble-t-il]. Nous démontrons l'efficacité de notre approche en insérant des chevaux de Troie dans deux schémas de conception — un post-traitement numérique dérivé du schéma d'Intel, dit RNG sécurisé de façon cryptographique, utilisé dans les processeurs Ivy Bridge, et une implémentation SBox résistante à [NDT : une attaque par ?] canal latéral — et en explorant leur détectabilité et leurs effets sur la sécurité ».

          d) épilogue temporaire :

          Alors, la moule, heureuse ? Tu as appris quelque chose ? Tant mieux, car nous sommes là pour nous accompagner mutuellement jusqu'à prendre possession de ce monde. Notre sort n'est pas de finir en bouchées accompagnées de "golden chips", mais de reprendre le contrôle sur le matériel, d'obtenir du matériel de confiance de notre point de vue, pas de celui des industriels aux ordres des financiers, de l'oligarchie, ou d'une quelconque coterie ;)

          • [^] # Re: Preuve formelle et supervision de la fabrication et de la distribution

            Posté par . Évalué à -7.

            Ci-dessus, je n'avais pas su traduire "Golden chips".

            Un "golden chip" est une puce de référence, par exemple celle qui sert pour comparer avec celles de production de masse pour le réglage des processus de dopage. On parle aussi de "golden sample". Cela peut aussi être un "trusted sample" dans le cadre de la sécurité. Voici une source qui aborde le sujet, en anglais.

            La phrase qui comporte l'expression "golden chip" dans le résumé de l'article peut donc être traduite ainsi :

            « Puisque le circuit modifié apparaît légitime sur toutes les couches gravées (incluant métal et silicium), notre famille de chevaux de Troie est résistante à la plupart des techniques de détection, incluant l'inspection optique à une granularité fine et la vérification par rapport à des puces de référence [NdT : puces de référence dites "Golden chips", entre guillemets dans le texte, selon l'expression consacrée en anglais] ».

        • [^] # Re: Preuve formelle et supervision de la fabrication et de la distribution

          Posté par . Évalué à -9. Dernière modification le 02/12/16 à 13:00.

          Vous avez été sage, voici la suite :

          2) Le deuxième article est titré "Reversing Stealthy Dopant-Level Circuits", ce qui peut se traduire par « rétro-ingénierie sur des circuits furtifs réalisés par dopage ».

          Il a été publié en 2014 (reçu le 27 Juin 2014 sur la plateforme d'archivage "Cryptology ePrint Archive", cf. source). Je note que l'article en lui-même n'est pas daté ; l'article le plus récent cité à la fin, en référence, date de 2014).

          Le titre est explicite dans la mesure où les circuits furtifs réalisés par dopage ont été présentés au commentaire parent.

          Voici la traduction (personnelle) du résumé de l'article en français :

          « Une détection réussie du circuit furtif réalisé par dopage (cheval de Troie), circuit proposé par Becker et ses coéquipiers au CHES 2013 [NdT : c'est une référence à l'article présenté dans le commentaire parent], est annoncée. Contrairement à une supposition faite par Becker et ses coéquipiers, les types de dopant dans les régions actives sont visibles sur les images obtenues soit par microscope à balayage électronique (dit SEM, pour "Scanning Electron Microscopy"), soit par faisceau concentré d'ions (dit FIB, pour "focused ion beam"). La mesure réussie est expliquée par une technique d'analyse de défaut sur circuit intégré LSI [NdT : cf. (1)] appelée contraste de voltage passif [NdT : de l'anglais "passive voltage contrast", ou PVC, cf. (2)]. Les expériences sont conduites en mesurant une puce spécialisée. La puce utilise le dispositif programmable de diffusion : une technique empêchant la rétro-ingénierie via le même principe que celui utilisé dans le cheval de Troie furtif réalisé au niveau du dopage. De la puce sont retirées les couches supérieures jusqu'à la couche de contact [NdT : cf. (3)] et des images sont prises avec un microscope optique d'une part, SEM d'autre part, et enfin FIB. Sur les images SEM, on peut distinguer quatre combinaisons possibles de dopants [NdT : le résumé les nomme, sans détailler, p+/n-well, p+/p-well, n+/n-well et n+/p-well]. Une détection partielle mais suffisante est réalisée par FIB. Bien que les circuits furtifs réalisés au niveau du dopage soient visibles, ils rendent potentiellement la détection plus difficile. C'est parce que la couche de contact devrait être mesurée. Nous montrons que rendre en images la couche de contact est au moins 16 fois plus coûteux en nombre d'images que pour une couche métal ».

          (1) LSI signifie "large-scale integration" et définit une échelle d'intégration sortie en 1971, correspondant à 500 à 20.000 transistors par boitier, soit 100 à 9.999 portes logiques — cf. source.

          (2) Dans la section 3.2 du document, la technique PVC est présentée. Elle a été développée dans les années 1990. Elle est maintenant largement utilisée.

          (3) la couche de contact fait l'interface entre le substrat de silicium (dopé par endroits) et les multiples couches de conducteurs métalliques qui sont au-dessus. Vous pourrez vous reporter au schéma présenté à la Fig. 1 en tête de la page 3 du document pour constater l'empilement des couches.

          • [^] # Re: Preuve formelle et supervision de la fabrication et de la distribution

            Posté par (page perso) . Évalué à 3.

            contraste de voltage passif [NdT : de l'anglais "passive voltage contrast", ou PVC, cf. (2)]

            En français, on dit tension, pas voltage.

            • [^] # Re: Preuve formelle et supervision de la fabrication et de la distribution

              Posté par . Évalué à -8.

              Détrompe-toi, on dit tension ou voltage. Voici la preuve pour voltage : http://www.cnrtl.fr/definition/voltage
              J'ai choisi voltage pour éviter d'utiliser tension seul qui prête à confusion avec d'autres acceptions, notamment dans la mécanique. J'aurais pu utiliser tension électrique pour lever toute ambiguïté mais tant qu'à faire, j'ai choisi la version la plus courte.

              • [^] # Re: Preuve formelle et supervision de la fabrication et de la distribution

                Posté par . Évalué à -9. Dernière modification le 02/12/16 à 14:21.

                En regardant sur Tension_électrique, je lis que « voltage » est considéré dans l'article comme étant un anglicisme (et par là incorrect) et renvoie en notes de bas de page à plusieurs recherches menées en 2015 sur différents dictionnaires en ligne. Je considère que CNRTL qui est cité comme une preuve validant l'usage de voltage est une bien meilleure référence que les autres proposées, que je préfère ne pas citer tellement elles sont inférieures en qualité.

                Pendant mes études d'électronique, je privilégiais le mot tension, mais j'étais dans un cadre où seule cette acception avait cours, ou presque, menant à préciser quand l'usage était dans un autre champ de la connaissance (en utilisant, par exemple, l'expression tension mécanique).

          • [^] # Re: Preuve formelle et supervision de la fabrication et de la distribution

            Posté par . Évalué à -10. Dernière modification le 02/12/16 à 14:04.

            Correction : dans le commentaire parent, lorsque je fais référence au "commentaire parent", il s'agit en fait de mon commentaire précédent de même niveau (présentant le premier de la série des trois articles proposés par Misc<). Je pensais initialement publier le commentaire parent en tant que commentaire fils du précédent et je me suis ravisé pour laisser la place à des commentaires réagissant spécifiquement au précédent.

        • [^] # Re: Preuve formelle et supervision de la fabrication et de la distribution

          Posté par (page perso) . Évalué à 0.

          Ne pas oublier les attaques dites "A2" également : https://www.wired.com/2016/06/demonically-clever-backdoor-hides-inside-computer-chip/

          Le papier en question : http://static1.1.sqspcdn.com/static/f/543048/26931843/1464016046717/A2_SP_2016.pdf

          Mes messages engagent qui je veux.

          • [^] # Re: Preuve formelle et supervision de la fabrication et de la distribution

            Posté par . Évalué à -4.

            Merci.

            Voici la traduction (personnelle) du résumé de l'article (le PDF fourni au 2e lien) en français :

            « Alors que le mouvement vers des transistors plus petits a été une aubaine pour la performance, ceci a augmenté de manière spectaculaire le coût de fabrication des puces utilisant ces transistors plus petits. Ceci force la vaste majorité des sociétés de conception de puce à faire confiance à des tierces parties, souvent à l'étranger, pour fabriquer selon leur conception. Pour se protéger d'expédier des puces avec des erreurs (intentionnelles ou autrement), les sociétés de conception de puce comptent sur des tests post-fabrication. Malheureusement, ce type de test laisse la porte ouverte à des modifications malveillantes du fait que les attaquants peuvent implémenter des déclencheurs d'attaque requérant une séquence d'évènements improbables, qui ne sera jamais rencontrée y compris par les testeurs les plus assidus.

            Dans ce document, nous montrons comment un attaquant opérant au moment de la fabrication peut exploiter des circuits analogiques pour créer une attaque matérielle qui est petite (c'est à dire requiert aussi peu qu'une porte logique) et furtive (c'est à dire requiert une séquence de déclenchement improbable avant d'affecter la fonctionnalité d'une puce). Dans l'espace ouvert d'une conception telle que les phases de placement et routage sont déjà réalisées, nous construisons un circuit qui utilise des condensateurs pour siphonner la charge depuis des pistes environnantes à l'occasion de leur transition entre des valeurs numériques. Quand les condensateurs sont pleinement chargés, ils déploient une attaque qui force une bascule (la victime) à une valeur désirée. Nous militarisons cette attaque en une escalade de privilège contrôlable à distance et ceci en attachant le condensateur à une piste contrôlable et en choisissant une bascule victime qui pilote le bit de privilège pour notre processeur. Nous implémentons cette attaque dans un processeur OR1200 et fabriquons une puce. Les résultats expérimentaux montrent que nos attaques fonctionnent, montrent que nos attaques échappent à l'activation par un ensemble varié de tests d'évaluation, et suggèrent que nos attaques échappent aux défenses connues ».

    • [^] # Re: Preuve formelle et supervision de la fabrication et de la distribution

      Posté par . Évalué à -6.

      1) Une dépêche (titrée « Lancement de la branche « Software Toolchain » de l’Open Compute Project ») a été publiée. Dans le cadre du projet Open Compute qui vise à définir des conceptions ouvertes de matériel, cette dépêche présente une avancée importante qui a été réalisée avec la perspective d’utiliser une chaîne d’outils logiciels de conception ouverte, dont les implémentations de référence seront faites en utilisant des logiciels libres (sont concernés notamment : la conception électronique et mécanique, l’affichage sur le Web de contenus 3D, de données de type CAO électronique, de résultats de simulations physiques — analyse thermique, analyse mécanique… — etc.). Cette avancée aboutira les 8 et 9 mars 2017 à une démonstration lors de l’évènement Open Compute Summit.

      2) Dans la section addendum de cette dépêche figure désormais une formulation synthétisée présentant :

      • l'intérêt, dans le cadre du matériel libre, de la preuve formelle de code (privilégiant des approches génériques pour favoriser la production de conceptions dérivées couvertes par la preuve de code) ;
      • la problématique des chevaux de Troie matériels furtifs incitant avantageusement la communauté à superviser la phase de fabrication (et celle de distribution pour éviter la substitution malveillante).

Suivre le flux des commentaires

Note : les commentaires appartiennent à ceux qui les ont postés. Nous n'en sommes pas responsables.