Petite précision : le SLH ne permet de se prémunir uniquement de Spectre v1, et encore, pas totalement, la couverture des branchements conditionnels n'est pas complète. C'est cependant mieux que rien.
Une option non documentée de llc permet en outre d'insérer automatiquement l'instruction LFENCE, préconisée par Intel pour contrer Spectre v1, et ce sur tous les branchement conditionnels, pour le coup. L'impact sur les performances reste néanmoins très élevé pour cette dernière solution, mais c'est la seule connue actuellement offrant des garanties de complétude.
Justement la question est ouverte sur toutes les méthodes formelles, puisque je n'ai pas de visibilité sur ce qu'il se fait actuellement dans le domaine sur ce sujet.
Mais dans le cas de LinuxBoot, ça serait plutôt de savoir si il y a un intérêt quelconque et une plus-value à utiliser des méthodes formelles (lesquelles, comment ?) pour le développement ou la validation, et en particulier vis à vis d'exigences de sécurité, type celles Critères Communs.
Merci pour cette annonce, les talks des conférences citées ont effectivement l'air super intéressant !
Pour ma culture personnelle, sais-tu quel usage est fait des méthodes formelles, notamment dans une optique sécurité, dans les différents développement des firmwares ? Je vois bien des talks à propos de Trustzone, l'usage des IOMMU, etc, mais c'est déjà plus "haut niveau".
Je me posais notamment la question de savoir si l'usage des méthodes formelles pouvait intéresser vos utilisateurs (dans le cadre de la certification de vos firmwares pour des usages étatiques, entre autres).
Merci pour cette annonce, les talks ont effectivement l'air super intéressant !
Pour ma culture personnelle, sais-tu quel usage est fait des méthodes formelles, notamment dans une optique sécurité, dans les différents développement des firmwares ? Je vois bien des talks à propos de Trustzone, l'usage des IOMMU, etc, mais c'est déjà plus "haut niveau".
Je me posais notamment la question de savoir si l'usage des méthodes formelles pouvait intéresser vos utilisateurs (dans le cadre de la certification de vos firmwares pour des usages étatiques, entre autres).
Tout le monde n'a pas le même cahier des charges que l'Etat français en terme de sécurité ou de robustesse pour ses logiciels de communication, il faudrait donc que tous les autres se retrouvent avec des solutions non auditées ou non qualifiées parce qu'une alternative existe déjà ?
C'est tout à fait normal, ce rapport, dans le cadre d'une CSPN, n'a pas vocation a être rendu public, il sert à l'ANSSI pour dire si oui ou non ils certifient le produit, rien d'autre.
Et ça se comprend tout à fait dans le cadre d'une évaluation d'un produit commercial couvert par le secret industriel : aucune entreprise ne ferait certifier ses produits si tous les détails techniques des implémentations sont rendus publics pour le faire.
La description des fonctions de sécurité évaluées se trouvent dans le cible de sécurité, et c'est bien suffisant pour un utilisateur final du produit pour décider de la pertinence d'utiliser ou non ledit produit en fonction de son cahier des charges.
Deux points de pinaillage concernant les deux messages précédents :
précisez pour les nouveaux venus que la courbe Curve25519 bénéficie d'une "confiance" accrue sur P-256 dans la mesure ou elle n'a pas été conçu par le NIST américain et que c'est cet aspect qui la rend si populaire et demandée bien qu'elle soit de "même résistance" : clefs elliptique de 256 bits.
Curve25519 offre 128 bits de sécurité équivalent symétrique, pas 256.
En fait, d’après Bernstein and Lange (2016) (full disclosure : Daniel J. Bernstein est l’un des principaux auteurs derrière la courbe 25519)
Pour être totalement full : DJB est bien l'auteur de la courbe, mais il faut rajouter que la la co-autrice de l'article, Tanja Lange, est sa femme à la vie publique.
Utiliser une clé de sécurité type Yubikey pour faire de l'OTP (si pas confiance dans le plugin Google), avec toujours un PAM à rajouter côté serveur
Utiliser une enclave sécurisée pour stocker sa clé privée et avoir un second facteur pour la déverrouiller lors de l'accès au serveur. Une application type Kryptonite peut remplir ce rôle. Il faut cependant désactiver les autres méthodes d'authentification sur le serveur et n'autoriser que cette clé.
Dans la plupart des distribs, les noyaux sont compilés avec un support générique de l'architecture. Pour que le noyau soit "optimisé" pour ton processeur spécifiquement, il vaut mieux le recompiler avec un patch du genre de celui de Graysky : https://github.com/graysky2/kernel_gcc_patch
Avec l'option "native" (-march=native pour le compilo) et un compilateur qui supporte Ryzen, tu auras un noyau optimisé pour ton archi.
Si tu parles du support du processeur par le noyau, il est inclus dans la version 4.10 comme mentionné précédemment.
A noter que CompCert est utilisé comme base de nombreux autres projets de recherche/industriels, notamment le projet Verified Toolchain (qui fait parti du projet plus grand DeepSpec) qui vise à avoir la maîtrise complète de chaîne de compilation : http://vst.cs.princeton.edu/
DeepSpec vise à atteindre la même maîtrise, mais sur un écosystème entier : http://deepspec.org/
Ca passe par un noyau et un OS formellement vérifiés (CertikOS), et d'autres choses.
Dixit les représentants de l'ANSSI, quand le code ne sera plus classifié et quand ils auront épuré le code du noyau, auquel ils ont rajouté de la crypto "étatique", classifiée également.
Pour l'instant, ils souhaitent se concentrer sur la dissémination auprès des OIV (et encore, se concentrer sur les postes d'administration un peu "critiques" chez ces OIV), et avec pour plan B de balancer une ISO et/ou un dépôt Git dans les moi à venir.
Bon le discours était un peu confus, au final je pense personnellement que ça va resté cantonné chez eux et qu'il n'y aura pas de version publique "à la Fedora/Debian/whatever".
A comparer également avec QubesOS, qui n'a pas du tout la même approche pour le cloisonnement.
CLIP utilise des containers LXC pour faire la séparation "état haut/état bas" (comprendre, environnement sécurisé/non sécurisé), tandis que QubesOS se base sur un hyperviseur bare-metal (Xen) et tire profit des extensions processeurs VT-x et VT-d (et équivalents AMD). D'ailleurs les ptits gars de l'ANSSI marchaient un peu sur des oeufs quand on leur parlait de Qubes, avec l'argument que Qubes faisait trop confiance au matériel selon eux, alors que justement, les devs de Qubes sont très critiques vis-à-vis des boîtes noires d'Intel (le Management Engine, voir ici : http://blog.invisiblethings.org/2015/10/27/x86_harmful.html) et sont très conscients des différentes attaques connues contre VT-d/VT-x. Bref.
Sinon, CLIP fait aussi usage du patch de sécurité Grsecurity pour son noyau custom, et ça c'est plutôt bien :)
Mais peut-être pourrais tu me dire où, dans ce post, ou même dans le programme de la conférence, nous faisons du placement produit de l'école ? Nous avons des intervenants qui sont effectivement élèves chez nous, dans notre labo sécu ou en master spé, et qui viennent présenter leurs travaux. Mais à part ce point précis, j'aimerais bien savoir à quel moment l'école est mise en avant de façon démesurée.
C'est une question sincère, puisque le but de cette conférence, c'est de faire venir des gens pour qu'ils nous parlent de leur vision de la sécu, qu'elle soit technique, ou politique, ou autre.
Quant a la tentative de troller sur le dos de DAVFI, je t'arrête tout de suite. Je peux m'exprimer au nom de l'équipe d'orga de la conférence et répondre sur ce sujet, mais je ne suis pas habilité (et je m'en contrefous d'ailleurs, de ce sujet) à parler de projets auquel je ne prends pas part. Si tu as des questions, tu peux écrire directement aux membres du labo sécu, ou alors tu peux venir samedi, certains chercheurs de l'école seront présents, tu leur demanderas directement (et on verra si le ton goguenard sera toujours là, au passage :))
Une partie de PolarSSL a été formellement prouvé par les ptits gars de chez TrustInSoft (un outil qui se base sur l'excellent outil Frama-C), avec en prime un kit de vérification :
# Speculative Load Hardening
Posté par Harvesterify (site web personnel) . En réponse à la dépêche Sortie de LLVM, Clang, lld, lldb 8.0.0. Évalué à 8.
Petite précision : le SLH ne permet de se prémunir uniquement de Spectre v1, et encore, pas totalement, la couverture des branchements conditionnels n'est pas complète. C'est cependant mieux que rien.
Une option non documentée de llc permet en outre d'insérer automatiquement l'instruction LFENCE, préconisée par Intel pour contrer Spectre v1, et ce sur tous les branchement conditionnels, pour le coup. L'impact sur les performances reste néanmoins très élevé pour cette dernière solution, mais c'est la seule connue actuellement offrant des garanties de complétude.
Mes messages engagent qui je veux.
[^] # Re: Classique ?
Posté par Harvesterify (site web personnel) . En réponse au journal IKOS, un analyseur statique développé à la NASA. Évalué à 2.
En effet, la plupart des analyseurs sérieux reposent sur l'interprétation abstraite (Frama-C, Astrée, CodeProver, cités dans le post originel).
Il serait intéressant de comparer les fonctionnalités offertes vis à vis des autres outils cités précédemment
Mes messages engagent qui je veux.
[^] # Re: Méthodes formelles ?
Posté par Harvesterify (site web personnel) . En réponse à la dépêche Un peu d’Open Hardware pour la rentrée (et beaucoup de LinuxBoot). Évalué à 3.
Justement la question est ouverte sur toutes les méthodes formelles, puisque je n'ai pas de visibilité sur ce qu'il se fait actuellement dans le domaine sur ce sujet.
Ce qui m'intéresse, c'est l'usage possible/avéré des méthodes formelles pour la sécurité des architectures matérielles. Pour donner un exemple, je suis avec attention ce genre de chose : https://www.researchgate.net/publication/327027099_Implementing_a_hardware-assisted_memory_management_mechanism_for_ARM_platforms_using_the_B_method
Mais dans le cas de LinuxBoot, ça serait plutôt de savoir si il y a un intérêt quelconque et une plus-value à utiliser des méthodes formelles (lesquelles, comment ?) pour le développement ou la validation, et en particulier vis à vis d'exigences de sécurité, type celles Critères Communs.
Mes messages engagent qui je veux.
# Méthodes formelles ?
Posté par Harvesterify (site web personnel) . En réponse à la dépêche Un peu d’Open Hardware pour la rentrée (et beaucoup de LinuxBoot). Évalué à 3.
Crossposting à partir du journal initial :
Hello,
Merci pour cette annonce, les talks des conférences citées ont effectivement l'air super intéressant !
Pour ma culture personnelle, sais-tu quel usage est fait des méthodes formelles, notamment dans une optique sécurité, dans les différents développement des firmwares ? Je vois bien des talks à propos de Trustzone, l'usage des IOMMU, etc, mais c'est déjà plus "haut niveau".
Je me posais notamment la question de savoir si l'usage des méthodes formelles pouvait intéresser vos utilisateurs (dans le cadre de la certification de vos firmwares pour des usages étatiques, entre autres).
Mes messages engagent qui je veux.
# Méthodes formelles ?
Posté par Harvesterify (site web personnel) . En réponse au journal Un peu d'Open Hardware pour la rentrée (et beaucoup de linuxboot). Évalué à 1.
Hello,
Merci pour cette annonce, les talks ont effectivement l'air super intéressant !
Pour ma culture personnelle, sais-tu quel usage est fait des méthodes formelles, notamment dans une optique sécurité, dans les différents développement des firmwares ? Je vois bien des talks à propos de Trustzone, l'usage des IOMMU, etc, mais c'est déjà plus "haut niveau".
Je me posais notamment la question de savoir si l'usage des méthodes formelles pouvait intéresser vos utilisateurs (dans le cadre de la certification de vos firmwares pour des usages étatiques, entre autres).
Mes messages engagent qui je veux.
[^] # Re: latence ou debit en upload
Posté par Harvesterify (site web personnel) . En réponse au journal Une bosse sur la ligne pour combattre le bufferbloat ?. Évalué à 4.
Un cache Web à l'heure où l'HTTPS est majoritaire, quelle est l'utilité ?
Mes messages engagent qui je veux.
# Déjà en 2014...
Posté par Harvesterify (site web personnel) . En réponse au journal Légalité de l'interception du flux SSL au sein d'une entreprise. Évalué à 2.
Plus d'infos sur les aspects juridiques de la chose, dans cet article de 2014 : https://www.silicon.fr/5-questions-comprendre-dechiffrement-ssl-100250.html/
Mes messages engagent qui je veux.
[^] # Re: vs Matrix/Riot
Posté par Harvesterify (site web personnel) . En réponse à la dépêche Tixeo, une solution propriétaire de visioconférence sécurisée sous GNU/Linux. Évalué à 2.
Tout le monde n'a pas le même cahier des charges que l'Etat français en terme de sécurité ou de robustesse pour ses logiciels de communication, il faudrait donc que tous les autres se retrouvent avec des solutions non auditées ou non qualifiées parce qu'une alternative existe déjà ?
Mes messages engagent qui je veux.
[^] # Re: Une honte
Posté par Harvesterify (site web personnel) . En réponse à la dépêche Tixeo, une solution propriétaire de visioconférence sécurisée sous GNU/Linux. Évalué à 6.
C'est tout à fait normal, ce rapport, dans le cadre d'une CSPN, n'a pas vocation a être rendu public, il sert à l'ANSSI pour dire si oui ou non ils certifient le produit, rien d'autre.
Et ça se comprend tout à fait dans le cadre d'une évaluation d'un produit commercial couvert par le secret industriel : aucune entreprise ne ferait certifier ses produits si tous les détails techniques des implémentations sont rendus publics pour le faire.
La description des fonctions de sécurité évaluées se trouvent dans le cible de sécurité, et c'est bien suffisant pour un utilisateur final du produit pour décider de la pertinence d'utiliser ou non ledit produit en fonction de son cahier des charges.
Mes messages engagent qui je veux.
[^] # Re: Excellent article. Quelques précisions et ajouts
Posté par Harvesterify (site web personnel) . En réponse à la dépêche Gnuk, NeuG, FST-01 : entre cryptographie et matériel libre. Évalué à 6.
Deux points de pinaillage concernant les deux messages précédents :
Curve25519 offre 128 bits de sécurité équivalent symétrique, pas 256.
Pour être totalement full : DJB est bien l'auteur de la courbe, mais il faut rajouter que la la co-autrice de l'article, Tanja Lange, est sa femme à la vie publique.
Mes messages engagent qui je veux.
# Root et sécurité
Posté par Harvesterify (site web personnel) . En réponse à la dépêche Utiliser son Android de façon plus sécurisée. Évalué à 7.
Recommander de rooter son téléphone et de déverrouiller le bootloader dans un article sur la sécurité Android, vraiment ?
Mes messages engagent qui je veux.
[^] # Re: À moins que...
Posté par Harvesterify (site web personnel) . En réponse au journal Conséquences sociales des cryptomonnaies. Évalué à 3.
Le problème de ces calculs, c'est qu'ils ne servent à rien, d'où les récentes propositions de se servir de cette puissance "perdue" à des fins utiles : https://blog.acolyer.org/2017/09/06/rem-resource-efficient-mining-for-blockchains/
Mes messages engagent qui je veux.
[^] # Re: (en plus des règles habituelles de sécurité)
Posté par Harvesterify (site web personnel) . En réponse au journal De l'exploitation des logs de fail2ban…. Évalué à 1.
Pour cela tu as plusieurs possibilités :
Mes messages engagent qui je veux.
[^] # Re: Programmation au collège
Posté par Harvesterify (site web personnel) . En réponse au journal TuxBot non, Scratch oui !. Évalué à 1.
C'est normal le champ de login et de mot de passe sur une page non-HTTPS ?
Mes messages engagent qui je veux.
[^] # Re: Bizarre le comportement de base non?
Posté par Harvesterify (site web personnel) . En réponse au journal Freebox Révolution — modification matérielle du Wi‐Fi. Évalué à 5.
Tu as essayé de jouer sur le canal Wi-Fi configuré ? (Par défaut, c'est certainement sur Auto, mais qui sait…)
Mes messages engagent qui je veux.
[^] # Re: Compatible Linux ou complètement supporté ?
Posté par Harvesterify (site web personnel) . En réponse au journal AMD RyZen débarque (bientôt). Évalué à 5.
Dans la plupart des distribs, les noyaux sont compilés avec un support générique de l'architecture. Pour que le noyau soit "optimisé" pour ton processeur spécifiquement, il vaut mieux le recompiler avec un patch du genre de celui de Graysky : https://github.com/graysky2/kernel_gcc_patch
Avec l'option "native" (-march=native pour le compilo) et un compilateur qui supporte Ryzen, tu auras un noyau optimisé pour ton archi.
Si tu parles du support du processeur par le noyau, il est inclus dans la version 4.10 comme mentionné précédemment.
Mes messages engagent qui je veux.
[^] # Re: Preuve formelle et supervision de la fabrication et de la distribution
Posté par Harvesterify (site web personnel) . En réponse au journal HiFive1: Un Arduino à 320Mhz entièrement libre pour 2017. É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.
# Verified toolchain
Posté par Harvesterify (site web personnel) . En réponse au journal Xavier Leroy est le lauréat 2016 du Prix Milner.. Évalué à 9.
A noter que CompCert est utilisé comme base de nombreux autres projets de recherche/industriels, notamment le projet Verified Toolchain (qui fait parti du projet plus grand DeepSpec) qui vise à avoir la maîtrise complète de chaîne de compilation : http://vst.cs.princeton.edu/
DeepSpec vise à atteindre la même maîtrise, mais sur un écosystème entier : http://deepspec.org/
Ca passe par un noyau et un OS formellement vérifiés (CertikOS), et d'autres choses.
Mes messages engagent qui je veux.
[^] # Re: Confiance
Posté par Harvesterify (site web personnel) . En réponse au journal Utiliser un noyau grsecurity sous Debian. Évalué à 0.
Là tu en dis trop ou pas assez.
Mes messages engagent qui je veux.
[^] # Re: Disponibilité
Posté par Harvesterify (site web personnel) . En réponse au journal Nuit du Hack 2016 & ANSSI. Évalué à 1.
Dixit les représentants de l'ANSSI, quand le code ne sera plus classifié et quand ils auront épuré le code du noyau, auquel ils ont rajouté de la crypto "étatique", classifiée également.
Pour l'instant, ils souhaitent se concentrer sur la dissémination auprès des OIV (et encore, se concentrer sur les postes d'administration un peu "critiques" chez ces OIV), et avec pour plan B de balancer une ISO et/ou un dépôt Git dans les moi à venir.
Bon le discours était un peu confus, au final je pense personnellement que ça va resté cantonné chez eux et qu'il n'y aura pas de version publique "à la Fedora/Debian/whatever".
A comparer également avec QubesOS, qui n'a pas du tout la même approche pour le cloisonnement.
CLIP utilise des containers LXC pour faire la séparation "état haut/état bas" (comprendre, environnement sécurisé/non sécurisé), tandis que QubesOS se base sur un hyperviseur bare-metal (Xen) et tire profit des extensions processeurs VT-x et VT-d (et équivalents AMD). D'ailleurs les ptits gars de l'ANSSI marchaient un peu sur des oeufs quand on leur parlait de Qubes, avec l'argument que Qubes faisait trop confiance au matériel selon eux, alors que justement, les devs de Qubes sont très critiques vis-à-vis des boîtes noires d'Intel (le Management Engine, voir ici : http://blog.invisiblethings.org/2015/10/27/x86_harmful.html) et sont très conscients des différentes attaques connues contre VT-d/VT-x. Bref.
Sinon, CLIP fait aussi usage du patch de sécurité Grsecurity pour son noyau custom, et ça c'est plutôt bien :)
Mes messages engagent qui je veux.
[^] # Re: Des vidéos prévus ?
Posté par Harvesterify (site web personnel) . En réponse au journal ESIEA Secure Edition 2016 : conférence et CTF. Évalué à 1.
Bonjour,
Malheureusement non, mais nous ferons sans doute un compte-rendu post-événement sous la forme d'un billet de blog :)
Mes messages engagent qui je veux.
[^] # Re: sans placement de produits
Posté par Harvesterify (site web personnel) . En réponse au journal ESIEA Secure Edition 2016 : conférence et CTF. Évalué à 8.
C'est ton avis, soit.
Mais peut-être pourrais tu me dire où, dans ce post, ou même dans le programme de la conférence, nous faisons du placement produit de l'école ? Nous avons des intervenants qui sont effectivement élèves chez nous, dans notre labo sécu ou en master spé, et qui viennent présenter leurs travaux. Mais à part ce point précis, j'aimerais bien savoir à quel moment l'école est mise en avant de façon démesurée.
C'est une question sincère, puisque le but de cette conférence, c'est de faire venir des gens pour qu'ils nous parlent de leur vision de la sécu, qu'elle soit technique, ou politique, ou autre.
Quant a la tentative de troller sur le dos de DAVFI, je t'arrête tout de suite. Je peux m'exprimer au nom de l'équipe d'orga de la conférence et répondre sur ce sujet, mais je ne suis pas habilité (et je m'en contrefous d'ailleurs, de ce sujet) à parler de projets auquel je ne prends pas part. Si tu as des questions, tu peux écrire directement aux membres du labo sécu, ou alors tu peux venir samedi, certains chercheurs de l'école seront présents, tu leur demanderas directement (et on verra si le ton goguenard sera toujours là, au passage :))
Mes messages engagent qui je veux.
[^] # Re: sécurisée et moderne
Posté par Harvesterify (site web personnel) . En réponse à la dépêche LibreSSL 2.3.3. Évalué à 5.
Une partie de PolarSSL a été formellement prouvé par les ptits gars de chez TrustInSoft (un outil qui se base sur l'excellent outil Frama-C), avec en prime un kit de vérification :
http://trust-in-soft.com/polarssl-verification-kit/
C'est déjà bien plus qu'OpenSSL, en un sens :)
Mes messages engagent qui je veux.
# Pour aller plus loin
Posté par Harvesterify (site web personnel) . En réponse au journal À propos de la petite bête dans votre ordinateur. Évalué à 3.
Cela fait déjà un certain temps que c'est connu, cette problématique du ME, notamment grâce au(x) papier(s) de Joanna Rutkowska "x86 considered harmful" (qui détaille les problèmes : http://blog.invisiblethings.org/papers/2015/x86_harmful.pdf) et "State considered harmful" (qui propose une solution élégante : http://blog.invisiblethings.org/papers/2015/state_harmful.pdf)
Mes messages engagent qui je veux.
[^] # Re: Let’s Encrypt
Posté par Harvesterify (site web personnel) . En réponse au journal L'avenir de la sécurité de nos sites oueb : DNSSEC / HPKP / DANE TLSA / CSP. Évalué à 0.
D'où ma remarque :
Mes messages engagent qui je veux.