Linux (fr)

  • Coup de gueule contre internet (Journaux LinuxFR)

    Ce matin, je tape www.online.net, mon doigt dérape et tape www.noline.net. Et comme mon ordi est dans le salon, je vous laisse imaginer les dégâts que cela aurait pourrait causer…

    Si on enlève d'internet les sites porno, de médicaments douteux, de jeux d'argent, de téléchargement illégal, le SPAM, internet serait-il plus léger? Et enfin, qu'en resterait-il? Est-ce le reflet de la société actuelle ? Sommes nous déjà en décadence?

    Je vais de ce pas installer dansguardian, mais honnêtement, j'aimerais que free propose un filtre - même configurable - sur sa freebox, et pas une appli windows à télécharger…

    Ou alors, je débranche tout et je me reconvertis dans l'élevage de chèvres et l'agriculture bio.

    Il y a des jours comme ça…

    Lire les commentaires

  • Sortie de pfSense 2.2, distribution routeur/pare-feu sur base FreeBSD (Dépêches LinuxFR)

    La version 2.2 de pfSense est sortie vendredi 23 janvier. pfSense est une distribution à base de FreeBSD, utilisable comme routeur et pare-feu. Cette version 2.2 passe de FreeBSD 8.3 à FreeBSD 10.1, en plus du changement de démon IPsec racoon remplacé par strongSwan, une mise à jour de la bibliothèque PHP en version 5.5 avec un remplacement de FastCGI vers PHP-FPM pour l'interface graphique, et l'ajout d'Unbound DNS server.

    pfSense

    Plus de détails dans la deuxième partie de la dépêche.

    Présentation

    pfSense est un système d'exploitation orienté routeur et pare-feu dérivé de m0n0wall et basé sur FreeBSD (NanoBSD pour la version embarquée). Il se veut complet, mais également intuitif au travers d'une interface web donnant accès à l'intégralité des fonctionnalités. On peut ainsi établir des tables de routage, des règles pour le pare-feu, faire des VLAN, activer un service DHCP, et bien d'autres choses.

    pfSense s'administre depuis une interface web moderne ou via CLI/PHP et est facile à utiliser.

    pfSense est léger et peut être embarqué sur du matériel de type mini-ITX (Alix), installé sur carte CompactFlash (la version embarquée charge les composants en mémoire puis n'écrit plus rien). Il peut se substituer à une box domestique ou faire office de pare-feu d'entreprise.

    Fonctionnalités

    • gestion des VLAN taggés ;
    • routage IPv4 et (depuis la version 2.1) IPv6, NAT ;
    • filtrage du trafic entrant et sortant pour tout type de trafic (ICMP, UDP, TCP…) ;
    • limitation des connexions pour un pair ;
    • log du trafic avec génération de graphiques ;
    • log sur serveur syslog externe ;
    • load Balancing, Failover ;
    • agrégation de ports, IP virtuelles ;
    • proxy transparent ;
    • serveur ou client PPPoE ;
    • VPN (client ou serveur) IPsec, PPTP, OpenVPN ;
    • DNS Dynamique ;
    • portail captif ;
    • contrôle d'accès par adresses MAC ou authentification RADIUS ;
    • serveur ou relais DHCP / DNS ;
    • ajout de fonctionnalités via des paquets directement installables dans l'interface.

    Nouveautés

    • pfSense 2.2 est basé sur FreeBSD 10.1 ce qui apporte non seulement de nombreux correctifs de sécurité, mais aussi une meilleure prise en charge du matériel et de la virtualisation ;
    • pf est désormais SMP friendly, ce qui améliore grandement les performances ;
    • l'interface d'administration fonctionne désormais sous PHP-FPM, ce qui apporte un gain de réactivité ;
    • ajout de nouveaux fournisseurs de DNS Dynamique (City Network, OVH DynHOST, GratisDNS, Euro DNS et CloudFlare) ;
    • Changement de démon IPSec racoon par strongSwan avec la gestion d'IKEv2, AES-GCM entre autres ;
    • et bien d'autres, que vous pouvez lire sur cette liste complète des changements.

    Lire les commentaires

  • PEPS : Une nouvelle solution de messagerie (et plus) pour Linux (Journaux LinuxFR)

    Bonjour à tous,

    On le sait tous, pour garder la maîtrise de ses données à commencer par ses mails, mieux vaut garder le contrôle de sa messagerie plutôt que d'utiliser un service "cloud" public. Idem pour le stockage de fichiers. Sinon, la NSA…

    Il existe bien sûr des services et solutions prêtes pour assembler un service qui permette les fonctions de messagerie, partage de fichiers, idéalement intégré à la messagerie (du type Gmail + Google Drive), mais en général c'est plutôt long et fastidieux. Et puis certaines solutions sont assez consomatrices de ressources et pas toujours modernes.

    Je voulais donc vous parler en avant-première d'une solution française qui cherche à répondre à cette problématique : PEPS. En avant-première car pour l'instant la release officielle n'a pas été faite même si le projet est déjà sur GitHub.

    Alors, l'interface ressemble à :

    Interface de PEPS

    et globalement le produit gère pour l'instant les fonctions suivantes :

    • messagerie,
    • partage de fichiers et répertoires,
    • contacts.

    Plus de fonctions sont prévues car une API (bientôt documentée) ce qui permet de développer des extensions. Deux sont déjà bien avancées : la discussion temps-réel "chat" et les calendriers.

    Pour les curieux, PEPS est intégralement développé en Opa et comme vous pouvez le voir, la solution est packagée sous forme de containers Docker, ce qui permet de déployer un nouveau service très rapidement en suivant la doc.

    Les technologies d'exécution sont NodeJS + MongoDB + Solr + Haraka.

    Vos avis ?

    Lire les commentaires

  • ma Global Game Jam 2015 (Journaux LinuxFR)

    Le week end dernier a eu lieu la Global Game Jam. Une game jam est «un hackathon avec pour thème le jeux vidéo» (Wikipedia), c'est-à-dire que sur un temps limité, ici 48h, il faut produire un jeu en suivant le thème de la game jam. Une particularité de la Global Game Jam est qu'il est possible de faire tout type de jeu, y compris des jeux sur table. Même si la majorité des participants font des jeux vidéos.

    Le thème de cette année était : «what do we do now?». Ouais, bien pourri. Trop large pour vraiment être inspirant. Parce que bon, avec n'importe quel jeu, on peut rentrer dans ce thème, pas besoin d'aller chercher très loin.

    Pour ma part, j'étais sur le site de Besançon avec une petite quarantaine d'autres participants. Ce sont mes étudiants qui organisaient, mais les participants venaient d'horizons très divers. Il y avait même une équipe où il y avait des lycéens et des collégiens qui ont fait un jeu en PureBasic. L'ambiance était très cordiale et la nourriture était excellente.

    Mon équipe était composé de quatre personnes : trois développeurs et une graphiste. Cette configuration est assez efficace : il y a assez de boulot pour tout le monde sans qu'on se marche trop sur les pieds. Pour le jeu, on est parti sur l'idée de développer un jeu où on accompagne Flo, une apprentie cambrioleuse, dans une chevauchée pour aller braquer une banque à l'aide de sa complice, Roxy. Le style graphique s'inspire des premiers GTA, avec une vue de haut (mais pas la perspective sur les bâtiments). Ça se raccroche au thème parce qu'à chaque étape, Flo se demande : «et qu'est-ce qu'on fait maintenant ?». Le jeu s'appelle Bank Robbery for Dummies.

    Au niveau technique, on est resté sur du connu : C++, SFML, Box2D. Je compile depuis quelques mois des bouts de codes à droite et à gauche dans un dépôt game skel. Il y a des bouts d'Akagoria, mais aussi de libsuit, ou des bouts de code que j'ai filés à mes étudiants pour le club jeu vidéo que j'anime. Bref, des briques de base pour éviter de réinventer la roue pendant une game jam. J'ai tout mis en MIT pour que ça soit réutilisable au maximum. Au final, le code de notre jeu tient en 5 classes. Le jeu en lui-même est en GPLv3. Vous pouvez bien sûr le télécharger et y jouer (temps de jeu estimé : 10 minutes). Tout est libre, y compris les graphismes. On a également utilisé un son piqué sur OpenGameArt en CC0 et une police de caractère en OFL. Les niveaux sont tirés aléatoirement, donc il se peut que vous tombiez sur un niveau infaisable (mais ça arrive très très très rarement).

    Pour finir, quelques petites captures d'écran (un peu moisie, on les a fait en quatrième vitesse sur une version non-finale du jeu mais ça donne une idée, dans le jeu, les gros points aux carrefours ont disparu au profit d'un petit point par exemple) :

    Le début du jeu

    Arrivée sur un point

    Lire les commentaires

  • Extraction de données du web - introduction à Scrapy (journal bookmark) (Journaux LinuxFR)

    Bonjour,

    Ceci est un journal bookmark.

    Scrapy est un framework python qui permet d'extraire des données structurées trouvées dans des sites web. Du crawling avec traitement de données.

    Comme dit sur le site de présentation : "An open source and collaborative framework for extracting the data you need from websites. In a fast, simple, yet extensible way."

    J'ai fait une présentation du framework hier au python user group de Grenoble (pyuggre comme on dit) ; si ça vous intéresse, la présentation est disponible sur Github, ainsi que les 3 exemples (dont un de crawling des news LinuxFR ;).

    Lire les commentaires

  • Le Port de San Diego migre sous Linux ! (Journaux LinuxFR)

    Port de San Diego

    Même si ce genre de scénario est devenu banal de nos jours, il est intéressant de souligner que même les institutions Américaines migrent sous Linux des applications critiques.

    La solution de backup SEP, mise en valeur dans cet article, tourne sous Linux, ce qui tombe bien puisque ce port migre sous Linux très prochainement.

    Qui doute encore que Linux est viable dans le monde professionnel ?

    Lire les commentaires

  • Sortie de pfSense 2.2, distribution routeur/par-feu sur base FreeBSD (Dépêches LinuxFR)

    La version 2.2 de pfSense est sortie vendredi 23 janvier. pfSense est une distribution à base de FreeBSD, utilisable comme routeur et pare-feu. Cette version 2.2 passe de FreeBSD 8.3 à FreeBSD 10.1, en plus du changement de démon IPsec racoon remplacé par strongSwan, une mise à jour de la bibliothèque PHP en version 5.5 avec un remplacement de FastCGI vers PHP-FPM pour l'interface graphique, et l'ajout d'Unbound DNS server.

    pfSense

    Plus de détails dans la deuxième partie de la dépêche.

    Présentation

    pfSense est un système d'exploitation orienté routeur et pare-feu dérivé de m0n0wall et basé sur FreeBSD (NanoBSD pour la version embarquée). Il se veut complet, mais également intuitif au travers d'une interface web donnant accès à l'intégralité des fonctionnalités. On peut ainsi établir des tables de routage, des règles pour le pare-feu, faire des VLAN, activer un service DHCP, et bien d'autres choses.

    pfSense s'administre depuis une interface web moderne ou via CLI/PHP et est facile à utiliser.

    pfSense est léger et peut être embarqué sur du matériel de type mini-ITX (Alix), installé sur carte CompactFlash (la version embarquée charge les composants en mémoire puis n'écrit plus rien). Il peut se substituer à une box domestique ou faire office de pare-feu d'entreprise.

    Fonctionnalités

    • gestion des VLAN taggés ;
    • routage IPv4 et (depuis la version 2.1) IPv6, NAT ;
    • filtrage du trafic entrant et sortant pour tout type de trafic (ICMP, UDP, TCP…) ;
    • limitation des connexions pour un pair ;
    • log du trafic avec génération de graphiques ;
    • log sur serveur syslog externe ;
    • load Balancing, Failover ;
    • agrégation de ports, IP virtuelles ;
    • proxy transparent ;
    • serveur ou client PPPoE ;
    • VPN (client ou serveur) IPsec, PPTP, OpenVPN ;
    • DNS Dynamique ;
    • portail captif ;
    • contrôle d'accès par adresses MAC ou authentification RADIUS ;
    • serveur ou relais DHCP / DNS ;
    • ajout de fonctionnalités via des paquets directement installables dans l'interface.

    Nouveautés

    • pfSense 2.2 est basé sur FreeBSD 10.1 ce qui apporte non seulement de nombreux correctifs de sécurité, mais aussi une meilleure prise en charge du matériel et de la virtualisation ;
    • pf est désormais SMP friendly, ce qui améliore grandement les performances ;
    • l'interface d'administration fonctionne désormais sous PHP-FPM, ce qui apporte un gain de réactivité ;
    • ajout de nouveaux fournisseurs de DNS Dynamique (City Network, OVH DynHOST, GratisDNS, Euro DNS et CloudFlare) ;
    • Changement de démon IPSec racoon par strongSwan avec la gestion d'IKEv2, AES-GCM entre autres ;
    • et bien d'autres, que vous pouvez lire sur cette liste complète des changements.

    Lire les commentaires

  • Jorani passe la troisième (Dépêches LinuxFR)

    Jorani est un projet de LMS (Leave Mananagement System), une application de gestion des congés et des heures supplémentaires. Disponible sous une licence GPLv3, cette application web (PHP/MySQL) aide les petites et moyennes structures à passer sans douleur d'un processus papier à un processus informatisé.

    Jorani est disponible depuis le 21 janvier dernier en version 0.3.0. Après quelques déploiements et la prise en compte des remarques des lecteurs de LinuxFr.org, le projet revient vous présenter les nouveautés de la dernière version :

    • détection des chevauchements de demandes ;
    • calcul du solde de congé à reporter ;
    • calendrier tabulaire ;
    • multiples améliorations ergonomiques et ajouts de pages utilitaires ;
    • API REST (OAuth2) ;
    • authentification LDAP simple ou complexe ;
    • la documentation ainsi que le site du projet ont été traduits en français.

    Lire les commentaires

  • Prochains meetup Linux embarqué et Android à Toulouse de janvier à mars 2015 (Dépêches LinuxFR)

    Il y a quelques mois, nous annoncions la création d'un Meetup Linux embarqué et Android à Toulouse, avec deux premières rencontres prévues (sur Yocto et sur le Device Tree).

    Ces deux premiers rendez-vous ayant eu un fort succès, nous avons reprogrammé 3 nouveaux événements en ce début 2015:

    N'hésitez pas à vous inscrire à ces événements, dont l'entrée est gratuite. Ils ont lieu à La Cantine Toulouse. Nous sommes également à l'écoute de vos propositions d'interventions.

    Lire les commentaires

  • Libellule n°71 - Février 2015 (Livret d’info libre)article (Journaux LinuxFR)

    Qu’allons-nous vous proposer comme activités, rencontres ou autres événements pour ce mois de février, des crêpes, un carnaval ? Plutôt la reprise de nos ateliers Warmux à la Maison des Adolescent de l’Hérault, un Petit déj’ de la com’ au Club de la Presse, qui traitera du thème de « L’utilisation des données numériques dans la presse », cette journée est une réédition de la journée que nous vous avons proposé en décembre et qui a rencontré un fort succès. Nous y aborderons des thèmes tels que, les enjeux pour les professionnels de la communication, ou encore la recherche d’information se doit d’évoluer pour s’adapter à cette avalanche de données. Cette journée est entièrement ouverte, mais il est conseillé de s’inscrire au préalable. Nous vous proposerons aussi un Apéro Numérique suivi d’une Install-Partie à la Mjc de Castelnau-le-Lez, une « Love Permanence » à Emmaüs de Saint-Aunès, pour notre accompagnement et notre assistance sur les aspects techniques de la distribution Emmabuntüs, une distribution GNU/Linux sociale et équitable.

    Le Collectif Cartopartie Montpellier s’agrandit, puisque l’APF34 nous rejoint pour apporter son expertise en matière de réglementation, ainsi que de son expérience. Montpel’libre quant à elle, fort de trois ans d’expérience de Cartographies participatives qu’elle mène en lien avec de nombreux partenaires dont la ville de Montpellier, partagera son expérience du terrain et sa connaissance des cartes de géolocalisation des lieux accessibles.

    Enfin, comme chaque dernier samedi du mois, nous vous donnons rendez-vous à la médiathèque de Lunel pour les Questions Libres, si vous avez des interrogations sur les logiciels libres ou sur Linux, si vous souhaitez une aide régulière mais vous ne savez pas où chercher, Montpel’libre vous propose des ateliers où vous pouvez venir poser vos questions. Montpel’libre vous présente cet atelier de logiciels libres, répond aux questions que vous vous posez sur Linux. Cet atelier se veut comme une passerelle entre un atelier et une Install-Party, un lien ouvert pour tous les niveaux, il s’adresse également aux débutants.

    Les articles récurrents de Montpel’libre sont ainsi diffusés aux dates indiquées ci-dessous :

    le 20 de mois : Le Logiciel Libre du mois
    le 22 du mois : Présentation membre
    le 25 du mois : Programme des activités de Montpel’libre
    le 28 du mois : Libellule - Le petit journal du libre
    le 30 juin et le 30 décembre : Calendrier Semestriel

    http://montpel-libre.fr/spip.php?article2232

    Lire les commentaires

  • Climat et logiciel (Journaux LinuxFR)

    Bonjour nal.

    description

    Dans l'actualité aujourd'hui, l'état britannique met en place un simulateur d'impact climatique à l'avenir du mode de vie des individus.

    C'est une bonne initiative, ça peut permettre à tout un chacun d'estimer l'impact de son propre mode de vie histoire de voir ce qui se passerait si tout le monde faisait comme soi, et, finalement, rêvons un peu, de responsabiliser chacun d'entre nous face à ce problème global.

    On va aussi sans doute essayer de s'amuser à savoir quelles sont les variables qui ont le plus d'impact, j'attends les commentaires histoire que la communauté libriste d'ici puisse explorer collaborativement cet outil ;-)

    licence

    Note pour rebondir sur un journal récent, l'outil est basé sur une feuille de calcul de tableur sous licence open source, semble-t-il, mais l'interface web est basée sur une licence NC. C'est un détail à mon humble avis mais ça pourrait faire parler ici :)

    Voilà, c'est à vous

    Lire les commentaires

  • Pourquoi cette ordure d'FTPS reste si populaire ?! (Journaux LinuxFR)

    Hey tout le monde !

    Vous savez tous ce qu'est FTPS, c'est le FTP mais avec une sur-couche SSL pour crypter les envois et éviter que tout le monde voient vos fichiers lorsque vous les consulter. Maintenant comment installer serveur FTPS ? Beaucoup proposeront d'installer ProFTPd, d'autres le trouvant trop compliqué préféreront PureFTPd et pour finir globalement les autres utiliseront VsFTPd réputé pour sa sécurité. En somme : soit on utilise un serveur FTP simple, mais pas sécurisé et incomplet (PureFTPd), soit un très complet et plus ou moins sécurisé si bien configuré (ProFTPd), soit la meilleure option à mon avis : VsFTPd, très reconnu en terme de sécurité, un peu plus simple et suffisant en fonctionnalités.

    Mais on a oublié une solution encore plus sûr, plus simple et relativement puissante : SFTP (combiné à MySecureShell) !

    SFTP tranche sur tous les points ! Il est clairement plus avancé, propre et sécurisé, mais ce qui démolie complètement FTPS, c'est qu'il est BIEN PLUS SIMPLE !!!

    Pourquoi autant d'administrateurs réseau se font pirater à cause de leur incapacité à configurer ProFTPd correctement, alors qu'il suffit qu'ils baissent la tête pour observer une solution simple et qui mettra fin à leur manque de sécurité. FTP(S) est dépassé et c'est tout !

    Alors franchement va falloir que vous m'expliquez pourquoi vous, administrateurs réseau, utilisez encore cette vieillerie d'FTPS ?!

    Lire les commentaires

  • Sortie de Coq 8.5 bêta, un assistant de preuve formelle (Dépêches LinuxFR)

    L'assistant de preuve Coq, deux fois primé l'année dernière, vient de sortir en version 8.5 bêta. Attendue depuis plus d'un an déjà, on trouvera au menu de cette version un nombre certain de changements en profondeur.

    Coq est un assistant de preuve sous licence LGPL 2.1, développé entre autres à l'INRIA. Issu des travaux sur la correspondance de Curry-Howard, Coq peut être vu aussi bien comme un langage de programmation que comme un système de preuves mathématiques. Il est, de fait, employé par les deux communautés. Parmi les développements en Coq, on peut citer par exemple le compilateur C certifié CompCert sur le versant informatique et la preuve du Théorème de Feit et Thompson sur le versant mathématique. Plus récemment, une des failles d'OpenSSL a été découverte grâce à Coq[0] . Il est aussi de plus en plus utilisé comme système interactif pour l'apprentissage de la logique dans l'enseignement supérieur.

    On rappellera dans le reste de la dépêche les grands principes qui sous-tendent Coq, ce qu'il est, ce qu'il n'est pas, puis on détaillera les changements introduits dans cette version.

    Sommaire

    Coq, en résumé

    Développé depuis trois décennies, la version 1 datant de 1984, Coq vient d'être consacré dans la cour des grands l'année dernière, en recevant le très prestigieux prix ACM Software System Award de l'ACM, côtoyant ainsi Unix, TCP/IP, TeX, Java, Make et d'autres grands noms faisant partie de notre quotidien  —  LLVM avait ainsi été récompensé l'année précédente.

    Les logiciels de méthodes formelles

    Un « assistant de preuve » fait partie d'une famille plus large de logiciels visant à établir la vérité (ou la fausseté) d'un énoncé mathématique donné. Par exemple, une égalité entre deux expressions mathématiques, ou un énoncé décrivant le fait qu'un certain système formalisé ne tombe jamais dans un état de panne, ou encore le fait qu'il existe une infinité de nombres premiers. Il existe une grande diversité d'approches selon la nature des énoncés concernés et la nature plus ou moins automatique de l'obtention du résultat :

    • On parle de « prouveurs automatiques de théorèmes » pour les logiciels très automatisés qui prennent l'énoncé en entrée et répondent soit « vrai », soit « faux », soit parfois « je ne sais pas » sans aucune information supplémentaire. Par exemple, les solveurs SAT ou SMT essaient de prouver des énoncés logiques utilisant un langage restreint (logique pure, arithmétique, tableaux, un peu de quantificateur, …). Ils ne savent répondre automatiquement que si la réponse peut être trouvée de façon assez « bête », mais peuvent traiter des formules énormes qu'un humain ne saurait pas manipuler ; ils sont donc de plus en plus utilisés dans l'industrie. Le model checking utilise ces outils pour vérifier automatiquement des propriétés de systèmes physiques ou virtuels ayant un nombre d'états possibles fini.

    • Les « analyseurs de programmes » sont une classe d'outils spécialisés pour l'étude des programmes informatiques. Les systèmes de typage statiques en font partie, mais aussi par exemple les outils utilisant l'interprétation abstraite. Ils peuvent garantir l'absence d'une classe d'erreurs variées, allant de l'absence de confusion pointeurs/entiers à l'absence de division par zéro, par exemple. Certains outils permettent d'annoter les programmes avec des invariants et contrats supplémentaires pour prouver des propriétés plus proches encore de la spécification formelle du programme.

    • Les « assistants de preuves » sont des logiciels qui permettent de manipuler des énoncés trop compliqués pour que l'ordinateur les vérifie seul. Ils se présentent comme un langage qui permet de décrire à l'ordinateur non pas un programme informatique, mais les étapes de raisonnement pour justifier un énoncé mathématique. Si le code fourni est accepté par l'assistant, la preuve est correcte et l'énoncé est vrai.

    La plupart des théories mathématiques et des énoncés concernant des langages de programmation Turing-complets, ne sont pas décidables automatiquement (il n'existe pas d'algorithme qui peut toujours répondre « oui » ou « non » sans se tromper). Les outils de preuve automatique ont donc toujours un risque de répondre « je ne sais pas ». De même, quand on conçoit un outil d'analyse de programme, il faut accepter qu'il « ne sache pas » dans certains cas ; selon ses priorités, on décidera alors de rejeter des programmes valides (si on veut garantir l'absence d'erreur) ou d'accepter des programmes incorrects (si on veut prévenir l'utilisateur seulement quand il y a vraiment une erreur).

    Si on veut pouvoir travailler sur des énoncés mathématiques ou programmes quelconques, une idée de plus en plus réaliste est d'utiliser les assistants de preuve pour décrire les parties difficiles d'une preuve, et laisser des prouveurs plus automatiques décider les sous-parties les plus évidentes. Ou bien utiliser un outil d'analyse de programme, mais faire parfois appel à un assistant de preuve sur les quelques cas trop difficiles à gérer entièrement automatiquement.

    Un assistant de preuve

    Coq est un assistant de preuve. Il manipule des preuves, dans un sens mathématique. L'utilisateur énonce des théorèmes et il doit ensuite fournir une preuve formelle de ceux-ci, sous forme d'étapes de raisonnement élémentaires dans la plupart des cas. Une fois la preuve donnée, le logiciel vérifie qu'il s'agit bien d'une preuve correcte, sans erreur de raisonnement, puis la marque comme validée. On peut ainsi construire de manière incrémentale une bibliothèque de preuves vérifiées mécaniquement par ordinateur.

    Le choix de la dénomination « bibliothèque » dans la phrase précédente n'est pas due au hasard. Pour une raison fondamentale, dont on discutera par la suite, l'ingénierie de la preuve est très similaire à l'ingénierie logicielle. Pour l'instant, il est raisonnable de se figurer que des preuves dépendent d'autres preuves de la même manière que les fonctions d'un programme dépendent de fonctions définies auparavant.

    Coq est un assistant de preuve, mais c'est aussi un langage de programmation. En particulier, il fournit un système de modules qui ressemble à celui d'OCaml. L'exemple qui suit définit une fonction multiplicity récursive (mot-clé Fixpoint) qui renvoie le nombre de fois qu'apparaît l'entier n dans une liste l. Ensuite il prouve une propriété simple sur la fonction : la multiplicité de n dans la concaténation de deux listes est la somme des multiplicités de n dans chaque liste.

    (* import de modules pour les listes et l'arithmétique *)
    Require Import List Arith.
    Fixpoint multiplicity (n : nat) (l : list nat) : nat  :=
        (* filtrage par motifs sur la liste "l" *)
        match l with       
        (* cas où la liste est vide *)
        | nil     => 0  
        (* cas où on a un élément "a" en tête de liste, "l'" le reste *)  
        | a :: l' => 
            (* test d'égalité de "n" avec l'élément "a" *)       
            if eq_nat_dec n a             
            (* appel récursif suivi de la fonction successeur d'un entier *)
            then S (multiplicity n l')  
            else multiplicity n l'         
        end.
    
    Lemma multiplicity_app (n : nat) (l1 l2 : list nat) : 
      multiplicity n (l1 ++ l2) = multiplicity n l1 + multiplicity n l2.
    Proof.
      induction l1. reflexivity.
      simpl. destruct eq_nat_dec; auto.
      rewrite IHl1. auto.
    Qed.

    Une des caractéristiques des fonctions récursives en Coq, liée au fait que Coq n'est pas Turing-Complet, est qu'elles terminent — ou autrement dit, s'arrêtent forcément à un moment donné. En effet, Coq vérifie que les arguments de l'appel récursif sont plus petits : il accepte l'exemple, car la liste l' est obtenue à partir de la liste l en lui enlevant son premier élément. Il arrive que certaines fonctions récursives terminent, mais que Coq ne soit pas capable de le deviner : savoir si un objet est plus petit qu'un autre n'est pas toujours évident. Dans ces cas, il faut l'aider un peu pour qu'il accepte la fonction.

    Voici deux preuves plus compliquées, reposant sur des définitions précédentes et bibliothèques de théorèmes. La première énonce qu'un petit langage de programmation est déterministe : si le programme c, partant de l'état mémoire st, peut arriver soit dans l'état st1 soit dans l'état st2, alors ces deux états sont égaux.

    Theorem ceval_deterministic: c st st1 st2,
      c / st  st1 
      c / st  st2 
      st1 = st2.
    Proof.
      introv E1 E2. gen st2.
      induction E1; intros; inverts× E2; tryfalse.
      forwards*: IHE1_1. subst×.
      forwards*: IHE1_1. subst×.
    Qed.

    La seconde fait partie d'une preuve qu'il y a une infinité de nombres premiers : pour tout nombre entier m, on peut trouver un nombre entier premier p strictement supérieur à m.

    Lemma prime_inf m : {p | m < p & prime p}.
    Proof.
      pose c := pdiv m`!.+1.
      have Pc : prime c by apply/pdiv_prime/fact_gt0.
      exists c => //.
      have [cLm|//] := leqP.
      have /Euclid_dvd1 := Pc.
      have /eqP<- := coprimenS (m`!).
      rewrite dvdn_gcd pdiv_dvd.
      by have /fact_div-> : 0 < pdiv m`!.+1 <= m by rewrite prime_gt0.
    Qed.

    Écosystème

    À l'instar des langages de programmation, il existe différents assistants de preuves, qui ne reposent pas tous sur la même base théorique, diffèrent au niveau de la syntaxe ou de l'expressivité. Citons quelques noms à la louche :

    • ACL2 ;
    • PVS ;
    • La famille HOL (HOL4, HOL Light…) ;
    • Isabelle, successeur de HOL ;
    • Agda, qui est probablement l'un des plus proches cousins de Coq à l'état naturel.

    La preuve assistée par ordinateur est une pratique qui se répand de plus en plus, avec aussi bien des théorèmes légendaires formalisés que des systèmes informatiques complexes certifiés sans bugs. Citons deux projets époustouflants et révélateurs de ce qui se fait déjà à l'heure actuelle :

    • Le projet Flyspeck, en HOL Light sous licence BSD, qui visait à prouver la conjecture de Kepler, vient d'arriver à son terme l'été dernier. Cette conjecture, évidente pour n'importe quel vendeur d'oranges, avait tout de même été énoncée en 1611 !
    • Le système d'exploitation seL4 prouvé de bout en bout en Isabelle (et open sourcé GPL / BSD, de surcroît).

    Parmi les gros développements en Coq, on peut citer :

    Il faut savoir que les deux premiers théorèmes ont été prouvés par Georges Gonthier et son équipe, après une quantité impressionnante de travail acharné (6 ans pour Feit-Thompson).

    Usage industriel

    Les débouchés industriels des outils de preuve formelle sont nombreux. L'industrie a adopté en premier les outils de démonstration automatique et de model checking qui sont les plus automatisés et donc les plus faciles à utiliser (voir par exemple l'article A short survey of automated reasoning de John Harrison, 2007). Par exemple, les concepteurs de micro-processeurs utilisent très lourdement des outils de vérification formelle pour garantir la correction des futurs modèles à différents moments de leur conception.

    Les assistants de preuves ont longtemps été réservés à un usage par une petite poignée d'experts (utilisation de la méthode B sur le logiciel critique embarqué de la ligne 14 de métro automatique), mais commencent à se diffuser. En particulier, les industries manipulant des logiciels critiques s'intéressent aux logiciels prouvés corrects utilisant ces méthodes. Par exemple, Airbus s'intéresse à l'usage du compilateur prouvé correct Compcert. Le micro-noyau Sel4 (prouvé correct avec l'assistant Isabelle) a lui été utilisé par un groupe de chercheurs et d'industriels pour construire l'hélicoptère télécommandé « le plus sécurisé au monde » (un projet qui intéresse beaucoup les militaires…).

    Quelques nouveautés de Coq 8.5

    Plus de deux ans et demi après la version 8.4, sortie en août 2012, la version 8.5 de Coq marque de grands changements. Elle intègre en effet quatre branches apportant des fonctionnalités remarquables.

    • Sous le capot, le moteur de tactiques (recherche de preuve) a été refait de fond en comble. Le langage de surface a été changé le moins possible, mais cela constitue une nouvelle base qui ouvre la voie à des changements / structurations / simplifications importantes dans le futur. (Arnaud Spiwack)
    • Le modèle de compilation / vérification des preuves est maintenant asynchrone ; au lieu de vérifier un fichier de preuves ligne par ligne, Coq trace maintenant les dépendances pour calculer en parallèle les résultats indépendants, et recalculer incrémentalement ce qui est nécessaire après un changement. (Enrico Tassi)
    • un nouveau mécanisme d'évaluation des termes, native_compute est disponible : au lieu d'interpréter le calcul ou de le compiler vers un bytecode, il produit des programmes OCaml qui sont compilés à la volée en code natif. Ce mécanisme accélère beaucoup les très gros calculs, mais n'est pas rentable pour les opérations simples où le coût de compilation dominerait. (Maxime Dénès)
    • La logique sous-jacente a été étendue avec de nouvelles notions avancées : polymorphisme d'univers (plus modulaire) et projections natives (plus efficace). (Matthieu Sozeau)

    Quelques autres changements importants sont:

    • Une construction $(...)$ qui permet d'intégrer des bouts de tactique directement dans des programmes  —  on ne pouvait auparavant faire que l'inverse avec la tactice refine. C'est très très pratique.
    • Une restriction de la condition de garde (qui vérifie que les programmes terminent) pour corriger une incompatibilité de la logique avec des axiomes désirables (l'extensionnalité des propositions, et des conséquences de l'univalence).
    • Une nouvelle option -type-in-type qui rend la logique incohérente (on peut prouver False) mais est pratique pour prototyper des idées sans avoir à gérer les niveau d'univers dans un premier temps.
    • Une tactique cbn qui remplace avantagement simpl.
    • Un nouveau motif introductif = x1 .. xn qui applique injection au vol (inspiré de SSReflect, un jeu alternatif de tactiques de base pour Coq)
    • De nouvelles constructions uconstr:c et type_term c pour programmer des tactiques manipulant des termes pas encore typés.

    Le Changelog complet est disponible. La partie cachée de l'iceberg contient de nombreuses modifications et bugfixes (avec en particulier Pierre Boutillier, Hugo Herbelin, Pierre Letouzey et Pierre-Marie Pédrot).

    Preuves et programmes : deux faces de la même pièce

    Cette partie plus historique détaille un aspect important et intéressant de la conception de l'assistant de preuve Coq, qui repose sur une correspondance entre preuves et programmes. Attention à ne pas en faire une idéologie : tous les assistants de preuve ne reposent pas sur ces mêmes bases, et les bons outils obtenus aujourd'hui sont au final assez proches à l'usage, quelle que soit leur tradition scientifique.

    Coq possède une particularité que ne présentent pas la majorité des autres assistants de preuve : il est basé sur la fameuse correspondance de Curry-Howard. Sous ce nom à priori barbare se cache une révolution paradigmatique de la logique, d'importance probablement comparable à l'introduction de la relativité générale en physique. Par un remarquable double effet Kiss-Cool, cette révolution est aussi d'une importance capitale pour l'informatique[1] !

    Un peu d'histoire

    Pour avoir une idée de l'importance de cette révolution, je me permets de faire un détour par la logique, en espérant ne pas perdre le valeureux lecteur en route. Revenons pour cela quelques malheureux 2500 ans en arrière.

    À cette époque, un type nommé Aristote cherche à justifier le raisonnement logique conduisant à produire des énoncés vrais. La logique de cette époque est en effet essentiellement perçue à travers le prisme du langage et de la rhétorique, d'où le nom même de « logique », qui vient en fait du mot λόγος (logos) signifiant « parole ».

    Ce nommé Aristote écrit l'Organon, qui deviendra jusqu'au XIXe siècle à la logique ce que The C Programming Language est au langage C. On y apprend des choses fort intéressantes, dont voici un exemple afin d'en jauger la teneur :

    • Socrate est un homme.
    • Tous les hommes sont mortels.
    • Donc Socrate est mortel.

    Si l'Organon a fait le délice des étudiants en scolastique médiévaux, il faut attendre la fin du XIXè siècle pour que les mathématiques s'emparent vraiment de la logique comme un objet à étudier formellement. Commence alors le règne encore inachevé de la théorie des ensembles.

    Les grands ancêtres

    Le début du XXe siècle est une période fertile pour les progrès de la logique formelle[2]. Le développement du logicisme permet l'élaboration incrémentale d'une théorie permettant de décrire les théories mathématiques sans ambiguïté ni possibilité d'erreurs : la théorie des ensembles. L'histoire n'étant pas un long fleuve tranquille, la formulation de cette théorie fut plusieurs fois mise en défaut. Un des paradoxes les plus connus et les plus simples à expliquer est sans aucun doute le paradoxe de Russell, publié en 1903. Malgré sa mise en équations, la logique conserve alors encore sa nature aristotélicienne, c'est-à-dire qu'on pouvait la résumer à un ensemble de règles à appliquer qui garantissent la correction du raisonnement.

    À peu près à la même époque et pour des raisons liées, se posent les premières questions de la définition de ce qu'on appellait alors « méthodes effectives », mais que l'on appellerait plus volontiers aujourd'hui « algorithmes ». Plusieurs tentatives de création de systèmes capturant physiquement la notion abstraite de calcul mènent à l'élaboration de deux célèbres modèles de calcul encore utilisés de nos jours.

    Si les machines de Turing peuvent être vaguement considérées comme la source d'inspiration des langages de programmation impératifs, le λ-calcul est quant à lui l'ancêtre direct des langages de programmation fonctionnels. Les deux paradigmes ont rapidement été démontrés équivalents, menant à la notion de Turing-complétude. Un langage est dit Turing-complet s'il est aussi expressif qu'une machine de Turing  —  ou que le lambda-calcul. Cela signifie qu'on peut y écrire tous les algorithmes raisonnables.

    Des systèmes de types aux systèmes de preuves

    Les premiers langages fonctionnels comme LISP ne présentaient pas de systèmes de types statiques, conduisant à une sémantique similaires aux langages dynamiques comme Python. Étonnamment, s'il faut attendre 1972 et la publication du langage ML pour obtenir un système de types satisfaisant pour l'usage quotidien, le λ-calcul avait été doté quasiment dès ses origines d'un système de types simple. ML a justement été conçu comme langage pour programmer l'un des premiers assistants de preuves, LCF, et son typage servait à garantir que les utilisateurs ne pouvaient pas manipuler le langage pour fabriquer de « fausses preuves » d'un énoncé. Coq poursuit cette tradition : c'est un descendant de LCF implémenté dans un descendant de ce ML des origines.

    La correspondance de Curry-Howard est la découverte fortuite par Haskell Curry en 1958 puis William Alvin Howard en 1969 que le système de types primitif du λ-calcul correspondait en fait exactement à un système logique minimaliste, la bien nommée logique propositionnelle minimale. C'était là la découverte d'une véritable pierre de Rosette des fondements de l'informatique, comblant le fossé qui séparait la théorie de la calculabilité (et de là l'informatique) avec la logique mathématique (et avec elle les mathématiques).

    La correspondance de Curry-Howard énonce ainsi que :

    • Les preuves mathématiques sont les programmes des langages fonctionnels ;
    • Les formules logiques que démontrent ces preuves sont les types de ces programmes.

    Il ne s'agit pas d'une vague ressemblance : dès lors qu'on a trouvé le bon angle sous lesquels les regarder, ces objets sont exactement les mêmes. Ainsi, on peut donner quelques traductions à travers cette pierre de Rosette pour éclairer le lecteur perdu.

    Informatique Mathématiques
    Type Formule
    Programme Preuve
    Primitive système Axiome
    Fonction de A vers B Preuve de « A implique B »
    Paire de A et B Preuve de « A et B »
    Type somme sur A et B Preuve de « A ou B »
    Interpréteur Théorème de correction
    compilateur Théorème de complétude

    Un des intérêts de cette équivalence est que l'on peut faire des va-et-vient d'un monde à l'autre. Ainsi, certaines primitives venant de la programmation sont traduites comme des lois logiques nouvelles et inversement. Ce changement paradigmatique marque aussi la naissance de la théorie de la démonstration moderne. Puisque les preuves sont des programmes, elles calculent et, donc, deviennent intéressantes en soi.

    De nouvelles fondations

    Peu à peu, des systèmes logiques de plus en plus riches se sont développés sur ce terreau fertile. Coq est ainsi une extension du calcul des constructions (de son petit nom CoC) développé par Thierry Coquand à la fin des années 1980. Il convient de citer aussi la théorie des types de Martin-Löf (MLTT), qui lui est similaire, sur laquelle se base Agda.

    Ce courant de recherche se veut une alternative à la théorie des ensembles du siècle passé, permettant d'unifier logique et calcul en un seul et même formalisme. Le recours à l'ordinateur laisse aussi espérer l'adaptation des techniques du génie logiciel au génie de la preuve, et le passage à l'échelle des mathématiques.

    Tout récemment, le petit monde de la théorie de la démonstration a été secoué par les idées de Vladimir Voïevodski, médaille Fields 2002, qui s'est rendu compte que la théorie des types était un excellent langage pour écrire les preuves d'homotopie. La théorie homotopique des types (HoTT) était née. Coq est un des langages dans laquelle cette théorie est implémentée. On pourra se réferer au pavé collaboratif de quelques 600 pages, le HoTT Book[4].

    Méli-mélo de Coq au Curry-Howard

    Coq est le résultat de ce courant de recherche fondamentale. En effet, il n'y a pas de différence formelle en Coq entre une preuve et un programme. Les deux objets vivent dans le même langage, à tel point qu'on peut calculer avec une preuve et, inversement, enrichir un programme avec des morceaux de preuves. Voici un exemple très simple de la fonction prédécesseur :

    Definition pred : forall n : nat, {m : nat | n = 0 \/ n = S m} :=
    fun (n : nat) =>
    (** analyse de cas sur n *)
    match n return {m : nat | n = 0 \/ n = S m} with
    (** n vaut zéro *)
    | 0 => exist _ 0 (or_introl eq_refl)
    (** n est de la forme n' + 1 *)
    | S n' => exist _ n' (or_intror eq_refl)
    end.

    Ce fragment se lit ainsi :

    • Version informatique : on définit la fonction pred qui prend en argument un entier naturel n et qui renvoie un entier naturel m tel que soit n vaut zéro, soit n = m + 1.
    • Version mathématique : le théorème pred affirme que pour tout entier naturel n, il existe un entier naturel m tel que n vaut zéro ou n = m + 1.

    Et effectivement, on peut calculer le résultat de l'application de cette fonction-théorème (proj1_sig est la fonction qui extrait le témoin de l'existentielle).

    Eval compute in proj1_sig (pred 42).
         = 41
         : nat

    Coq propose aussi un langage externe dit « de tactiques » qui permet d'écrire des preuves par méta-programmation, appelé Ltac. Un script de preuve n'est pas une preuve, c'est un programme qui manipule des morceaux de preuves pour construire un terme de preuve. Malheureusement, on ne sait pas encore concevoir des langages propres pour faire cela, et le langage actuel est impératif, non-typé et mal compris. Le résultat est aussi sordide que le langage interne de Coq est élégant. On pourra se le figurer comme l'hybride démoniaque entre TeX et PHP, pour les connaisseurs. Le programme précédent peut s'écrire à l'aide de Ltac comme suit.

    Definition pred : forall n : nat, {m : nat | n = 0 \/ n = S m}.
    Proof.
    intros n; destruct n.
    + exists 0; left; reflexivity.
    + exists n; right; reflexivity.
    Defined.

    Le terme produit par cette séquence de commandes est le même que celui qu'on a écrit à la main auparavant. L'avantage de Ltac est qu'il permet d'écrire des morceaux de preuves aisément, au prix d'un moins grand contrôle sur le terme produit.

    Agda, le seul autre assistant de preuve mainstream aussi proche de l'idée de correspondance preuve-programme, a fait un choix différent, qui est de n'avoir qu'un langage de termes (et pas de méta-programmes), et d'essayer de le rendre le plus propre possible pour permettre de l'utiliser directement. Cela a conduit à des idées intéressantes, mais pour l'instant le résultat est moins adapté à l'automatisation des preuves et donc aux formalisations de grande ampleur. (Les utilisateurs Agda essaient de compenser par un mode Emacs de folie qui ré-écrit les termes de preuve pour eux; il y a du bon et du moins bon dans cette approche.)

    Un langage exotique

    En tant que langage de programmation, Coq fait malgré tout figure d'alien aux yeux des programmeurs lambda.

    En premier lieu, Coq est un langage de programmation purement fonctionnel, et ce, encore plus que Haskell. Il n'y a en effet aucun effet de bord possible et cela inclut aussi bien la mémoire mutable que l'affichage sur la ligne de commande. Eh oui, on ne peut même pas écrire le Hello World des familles en Coq ! Imaginez le désarroi de ses promoteurs quand on le leur demande… Pas non plus d'exceptions, de primitives systèmes, etc. On peut cependant toujours se débrouiller en encodant ces effets dans une monade, comme en Haskell.

    Pire encore, quand nous disons que Coq est plus pur que Haskell, cela n'est pas pour rien. Il est en effet impossible en Coq d'écrire un programme qui ne termine pas. Coq est très strict sur les fonctions qu'il accepte et demande souvent un peu de gymnastique au programmeur. Le point positif de cette rigidité est que les programmes sont garantis de respecter leur spécification. En un sens, Coq rend vrai l'adage souvent appliqué à OCaml et à Haskell : « quand ça compile, c'est que ça marche ».

    Une conséquence inattendue de ce fait : Coq n'est pas Turing-complet. Il existe donc des programmes qu'on ne peut pas écrire en Coq. Ce n'est pas un bug, c'est une feature ! Cette restriction permet de passer outre les limitations dues au théorème d'incomplétude de Gödel  —  mais complique l'écriture de programme dont on ne sait pas prouver la terminaison ou la productivité[3].

    Le futur ?

    Les gens qui travaillent sur les assistants de preuves imaginent un monde où les mathématiciens et mathématiciennes travaillent directement avec des assistants de preuve et où l'on n'a plus jamais besoin de corriger un résultat qui s'avère faux après sa publication. C'est encore une utopie, même si les mathématiciens sont de plus en plus nombreux à prendre ces outils au sérieux. Aujourd'hui, les assistants de preuves restent trop difficiles à utiliser pour des « mathématiques de tous les jours » et il faudra encore des efforts de simplification et d'ergonomie pour rendre cette idée réaliste.

    Des bibliothèques importantes de mathématiques formalisées existent déjà (par exemple le journal Formalized Mathematics présente les nombreux résultats formalisés dans la Mizar Mathematical Library), mais elles soulèvent de nombreuses questions d'ingénérie des preuves et d'inter-opérabilité entre les différents langages de description de preuves.

    La formalisation assistée par ordinateur laisse malgré tout entrevoir la possibilité de faire des mathématiques que l'esprit humain ne saurait appréhender aisément aujourd'hui. Ainsi, une des barrières à la preuve, aussi bien du théorème des quatre couleurs que de la conjecture de Kepler, était la quantité dantesque de cas particuliers à vérifier à la main, que l'ordinateur a pu traiter rapidement. Une nouvelle ère des mathématiques est probablement en train de s'ouvrir sous nos yeux.

    Par ailleurs, on voit fleurir des outils permettant de vérifier formellement que les programmes informatiques respectent une spécification. Alors qu'on peut imaginer que les preuves mathématiques aient toute vocation à être vérifiées, personne ou presque n'espère réellement que tous les logiciels écrits soient un jour prouvés corrects. D'une part, certains logiciels n'ont pas de spécification claire, stable ou que l'on sait exprimer (comment spécifier un économiseur d'écran ?) ; d'autre part, les facteurs économiques jouent contre les preuves formelles. En effet, même si la preuve formelle devenait un jour la façon la plus économique d'éviter les bugs dans les logiciels, cela restera toujours plus difficile et donc plus coûteux que d'écrire du logiciel buggué. On peut cependant rêver au fait que, d'ici quelques dizaines d'années, le dessous de l'iceberg (les bibliothèques standards, compilateurs, runtime, noyaux de système d'exploitation ou navigateurs web) sur lequel reposent les programmes grand-publics soient spécifiés le plus précisément possible et prouvés corrects par rapport à cette spécification.

    L'assistant de preuve Coq, en permettant à chacun de se former à la preuve formelle (ou à la preuve tout court) et de se lancer dans des formalisations qui commencent à être de grande ampleur, est un des outils phare de cette (r)évolution.

    Notes

    [0] Plus précisément, c'est en cherchant à modéliser ce sous-système dans Coq que Masashi Kikuchi a découvert ce défaut de conception. La démarche de la preuve formelle revient à soumettre tout un système à un tyran de rigueur insatiable. Il révèle ses erreurs, ses points faibles et force l'utilisateur à une compréhension au centimètre près. Si la présentation n'est pas structurée et élégante, la preuve en est d'autant plus difficile. Les assistants de preuves poussent à la simplicité et permettent souvent la production de documents pédagogiques remarquables, car leur clarté vient non des détails qu'ils passent sous le tapis, mais de la rigueur qui leur a été imposée. C'est souvent dans un article de la forme Comment prouver formellement X que vous trouverez l'exposition la plus claire du sujet X.

    [1] Peut-être presque autant que la sortie de l'iPhone n + 1, pour un n bien choisi.

    [2] Je recommande la lecture de la captivante BD Logicomix à ceux qui sont intéressés.

    [3] Dans les faits, 99,99% des programmes imaginables peuvent s'écrire en Coq. On dit aussi souvent que cela empêche aussi d'écrire un interpréteur de Coq en Coq, mais cela est plus compliqué en pratique. On pourrait écrire une fonction qui effectue une étape de réduction (et laisser l'utilisateur pédaler), ou imaginer bootstrapper à l'aide d'un axiome bien choisi.

    [4]Quand un mathématicien déclare son amour à git et à l'esprit du libre.

    Lire les commentaires

  • Atelier Musique Assistée par Ordinateur le 14 mars 2015 à Argenteuil (Dépêches LinuxFR)

    Le Gull StarinuX vous convie à l'atelier « La musique assistée par ordinateur (MAO) sous GNU/Linux », qui aura lieu le samedi 14 mars 2015 de 9h à 18h, aux Bains-douches Silicone-banlieue, 9 rue de Calais, 95018 Argenteuil (5 min de la gare de d'Argenteuil, directe 10 min St Lazare).

    Vous êtes musicien(ne), vous souhaitez vous enregistrer, créer vos propres compilations, arranger vos morceaux… et librement avec un logiciel de MAO sous Linux ? On dit souvent que la musique assistée par ordinateur, c'est le domaine réservé de Windows et MacOS. En fait, non : GNU/Linux aussi c'est bien pour faire de la musique ! Alors venez le découvrir et l'apprendre avec des outils Libres !

    Cet atelier sera animé par Yann Collette, un musicien féru de Linux. Le programme prévoit d'aborder plusieurs logiciels musicaux, comme Guitarix, Ardour ou Mixxx.

    Comme à l'accoutumée pour les ateliers StarinuX, il vous est demandé de vous inscrire sur la page prévue à cet effet, sachant que la participation (annuelle) de 20 euros est valable pour plus de 17 ateliers !

    Concernant les commodités, un bar est disponible sur place et lunch sera facile à la pause de midi.

    Au plaisir de vous rencontrer le 14 mars !

    Lire les commentaires

  • Capitole du Libre - Médias (Journaux LinuxFR)

    Bonjour 'nal,

    un petit mot pour t'informer qu'une partie des vidéos est en ligne. Il suffit de parcourir les sujets et les conférences pour voir si la vidéo est présente. Un peu de retard, désolé.
    N'hésites pas à nous faire un retour si tu rencontres des problèmes (sur la vidéo, sur l'audio, sur le fichier de la présentation, …)

    Lire les commentaires

  • Musique libre : Moquettes&Tapis par Sebkha-Chott (Dépêches LinuxFR)

    Sebkha-Chott est un groupe de musique libre, faite avec des logiciels libres.

    Le groupe, qui se compose trois musiciens et de beaucoup de machines, a été en grande partie renouvelé avec l'arrivée d'un nouveau batteur et d'un nouveau guitariste, bassiste, ainsi que divers objets sonores. Il est notamment doté d'une guitare DIY rotative assez singulière.

    "Moquettes&Tapis", leur 6ème album est annoncé en prévente pour le 1er avril 2015.

    Les prémices de ce nouvel album ont pu être découvertes l'été dernier à l'occasion du concert des RMLL 2014 à Montpellier. Ce nouvel album est intitulé "Moquettes&Tapis", est dans la ligne du précédent album ("the Ne[xxx]t Epilog") : mélange d'instruments électriques et électroniques, rock parfois très dur, rythmes fouillés… avec toutefois de nouveaux musiciens et de nouvelles compositions (Sebkha-Chott ayant habitué ses fans aux multiples orchestrations radicalement différentes des mêmes morceaux).

    Le groupe finance en partie sa production par la pré-commande de CD. L'album sera placé comme toujours sous licence libre (licence art libre 1.3 pour la partie artistique et GPL pour la technique).

    "Moquettes&Tapis" bénéficie de la participation de nombreux invités dont les plus illustres sont :

    • Ike Willis (Frank Zappa),
    • Yom (Yom),
    • Fred Gastard (Musiques à Ouïr, Brigitte Fontaine, Melosolex, Journal Intime),
    • Mathieu Metzger (Klone, Marc Ducret, Louis Sclavis, Anthurus d'Archer…)
    • Gabriel Yacoub (Malicorne)

    Un clip a été réalisé pour l'occasion, pour donner un avant goût de ce sixième album.

    Lire les commentaires

  • Faille de sécurité glibc (Journaux LinuxFR)

    Je me permets de faire un copier coller de l'annonce relayée sur le FRench SysAdmins Group (FRsAG):

    **
    /Cette vulnérabilité sévère détectée dans la bibliothèque C de GNU/Linux donne le contrôle aux attaquants sans nécessiter d’identifiants système.
    - Patchs disponibles dès aujourd’hui - /

    *
    Le 27 janvier 2015 –– *Qualys, Inc.(NASDAQ : QLYS), le principal fournisseur de solutions de sécurité et de conformité dans le Cloud, annonce que son équipe chargée de la recherche en sécurité a découvert dans la bibliothèque C de GNU/Linux (glibc) une vulnérabilité critique qui permet aux pirates de prendre le contrôle à distance de tout un système, en se passant totalement des identifiants système.
    Qualys a travaillé de manière étroite et coordonnée avec les fournisseurs de distributions Linux pour proposer un patch pour toutes les distributions de systèmes Linux touchés.
    Ce patch est disponible dès aujourd’hui auprès des fournisseurs correspondants.

    Baptisée GHOST (CVE-2015-0235) parce qu’elle peut être déclenchée par les fonctions gethostbyname et gethostbyaddr, cette vulnérabilité touche de nombreux systèmes sous Linux à partir de la version glibc-2.2 publiée le 10 novembre 2000. Les chercheurs de Qualys ont par ailleurs détecté plusieurs facteurs qui atténuent l’impact de cette vulnérabilité, parmi lesquels un correctif publié le 21 mai 2013 entre les versions glibc-2.17 et glibc-2.18.
    Malheureusement, ce correctif n’ayant pas été classé comme bulletin de sécurité, la plupart des distributions stables et bénéficiant d’un support à long terme ont été exposées, dont Debian 7 (« Wheezy »), Red Hat Enterprise Linux 6 & 7, CentOS 6 & 7 et Ubuntu 12.04.

    Les clients Qualys peuvent détecter GHOST à l’aide de la signature QID 123191 fournie par le service Cloud Qualys Vulnerability Management(VM). Lorsqu’ils lanceront le prochain cycle de scan, ils obtiendront des rapports détaillés sur l’exposition de leur entreprise à cette vulnérabilité sévère. Ils pourront ainsi estimer son impact sur leur activité et suivre efficacement la vitesse de résolution du problème.

    « GHOST expose à un risque d’exécution de code à distance qui rend l’exploitation d’une machine par un pirate terriblement enfantine.Il suffit par exemple qu’un pirate envoie un mail sur un système sous Linux pour obtenir automatiquement un accès complet à cette machine »,
    explique Wolfgang Kandek, Directeur technique de Qualys, Inc. « Compte tenu du nombre de systèmes basés sur glibc, nous considérons qu’il s’agit d’une vulnérabilité sévère qui doit être corrigée immédiatement.La meilleure marche à suivre pour atténuer le risque est d’appliquer un patch fourni par votre fournisseur de distributions Linux. »

    Les correctifs sont disponibles pour Debian wheezy.

    Lire les commentaires

  • Mettre en place un serveur Jabber avec du TLS et du Forward Secrecy (Dépêches LinuxFR)

    J'ai publié il y a quelques mois un tuto pour mettre en place "facilement" un serveur XMPP/Jabber avec Prosody et du SSL/TLS plutôt bien configuré sous Debian, j'ai eu pas mal de retours positifs depuis et je pense qu'il pourrait intéresser d'autres personnes.

    Sommaire

    Installation

    Pour installer Prosody sous Debian, il suffit de rajouter le dépôt dans son sources.list, on peut utiliser la ligne suivante pour le faire. Elle permet de simplifier énormement la manipulation (pour les détails, c'est ici) :

    echo "deb http://packages.prosody.im/debian $(lsb_release -sc) main" | sudo tee -a /etc/apt/sources.list
    

    Puis on ajoute la clé GPG du dépôt :

    wget https://prosody.im/files/prosody-debian-packages.key -O- | sudo apt-key add -
    

    On met à jour les dépôts, puis on installe Prosody :

    aptitude update && aptitude install prosody
    

    Le paquet lua-sec dans Debian est légèrement… ancien, si vous voulez les derniers algorithmes de chiffrement et que le Perfect Forward Secrecy soit pris en compte, il faut le mettre à jour.

    Sur Debian Wheezy :

    echo "deb http://ftp.debian.org/debian wheezy-backports main" >> /etc/apt/sources.list
    aptitude update && aptitude -t wheezy-backports install lua-sec-prosody
    

    Configuration

    L'ensemble de la configuration se fait dans un seul fichier :

    /etc/prosody/prosody.cfg.lua
    

    La première partie est commune à l'ensemble des VirtualHosts que vous allez mettre en place. Ce qui sera écrit sous chaque VirtualHost "exemple.com" (en bas) sera propre à chaque VirtualHost.

    Ce qui veut dire que si vous mettez votre configuration SSL dans la première partie, elle sera commune à tous les VirtualHosts. Faites attention aux répercussions que ça peut avoir ;-)

    La première brique

    Ouvrez le fichier avec votre éditeur préféré (pour moi ça sera vim)

    vim /etc/prosody/prosody.cfg.lua
    

    Il faut modifier/compléter les champs suivants (avec évidemment vos informations à la place de example.tld) :

    Qui est administrateur du serveur (tout en haut du fichier) ?

    admins = {"admin@exemple.tld"}
    

    Voulez-vous autoriser les inscriptions sur votre serveur ? À moins de savoir ce que vous faites, je vous conseille grandement de le mettre sur false afin d'éviter de servir aux spammeurs et aux bots.

    allow_registration = false;
    

    Quel domaine voulez-vous utiliser (tout en bas du fichier) ? N'oubliez pas de changer example.tld pour votre domaine.

    VirtualHost "example.tld"
    enabled = true
    

    Les logs

    C'est très important (et déjà partiellement configuré). Ils permettent de trouver où est le problème quand ça ne marche pas (pour plus de détails sur la configuration : logging), la modification par rapport au fichier original consiste à mettre le prosody.log en warn et non plus en info et à faire la même manipulation pour le syslog :

    log = {
            warn= "/var/log/prosody/prosody.log";
            error = "/var/log/prosody/prosody.err";
            { levels = { "error" }; to = "syslog";  };
    

    Si vous avez un problème à régler, je vous conseille de rechanger le premier warn pour debug, puis de redémarrer prosody (via la commande prosodyctl restart), vous aurez alors toutes les informations qu'il vous faut dans /var/log/prosody/prosody.log et bien plus encore pour trouver d'où ça vient.

    Un minimum de sécurité

    De base, Prosody enregistre les mots de passe des comptes en clair sur le serveur, pour qu'ils soient hashés, il faut modifier la ligne authentication = "internal_plain" par la ligne suivante :

    authentication = "internal_hashed"
    

    prosodyctl

    Prosody vient avec une commande qui aide à communiquer avec lui facilement : prosodyctl, et qui s'utilise sous la forme suivante :

    prosodyctl COMMAND [OPTIONS]
    

    COMMAND peut être :

    • adduser - exemple@exemple.tld - crée le compte utilisateur
    • passwd - exemple@exemple.tld - configure le password de l'utilisateur
    • deluser - exemple@exemple.tld - supprime l'utilisateur
    • start - démarre Prosody
    • stop - arrête Prosody
    • restart - redémarre Prosody
    • reload - recharge la configuration de Prosody
    • status - indique le status actuel de Prosody

    Plutôt utile non ? :]

    Nous allons ajouter un utilisateur (il vous demandera un mot de passe), puis nous rechargerons la configuration pour prendre en compte les changements (exemple.tld doit être le même que vous avez mis pour votre VirtualHost) :

    prosodyctl adduser exemple@exemple.tld
        prosodyctl reload
    

    Et là, c'est l'instant de plaisir, si vous essayez de vous connecter avec un client jabber (comme pidgin), ça devrait se connecter. Si ce n'est pas le cas (faire dans l'ordre) :

    • voir les logs de prosody,
    • voir les logs de votre client jabber,
    • changer les logs de prosody de info à debug,
    • boire un thé (ou une bière)
    • vérifier votre firewall,
    • rebrancher la box,
    • reprendre un thé,
    • changer de FAI.

    Les modules

    Comme vous pouvez le voir dans le fichier de configuration, il y a déjà un certain nombre de modules qui sont activés par défaut (roster, saslauth, tls, posix…). ils sont dans la partie modules_enabled = { }.

    Si je vous parle de ça, vous vous doutez que ce n'est pas pour rien, il existe beaucoup de modules, dont un pour Tor :

    Chiffrons tout pour tout le monde

       Manifesto - *[A public statement about ubiquitous encryption on the XMPP network.](https://github.com/stpeter/manifesto)*
    

    Si vous ne connaissez pas (ou mal) le SSL/TLS, je ne peux que vous conseiller d'attaquer le sujet par la conférence de Benjamin Sonntag dans le cadre du cycle de conférence « Il était une fois Internet ».

    Création du certificat

      Si votre certificat n'est pas reconnu « valide » par votre client jabber, par exemple en cas de certificat auto-signé, il demandera autorisation pour l'utiliser.
    
    La méthode simple (et vraiment rapide)

    La méthode « simple » consiste à la création d'un certificat auto-signé avec l'aide de prosodyctl :

    # exemple.tld étant le domaine que vous avez mis dans prosody.cfg.lua
    prosodyctl cert generate exemple.tld
    
    • vérifier l'emplacement des certificats une fois qu'ils sont générés
    • vous pouvez les bouger dans /etc/prosody/certs/ si vous avez envie (on part du principe que c'est le cas pour la suite)
    • N'oubliez pas les deux lignes suivantes :
    chmod 600 /etc/prosody/certs/exemple.tld.key
    chown prosody:prosody /etc/prosody/certs/exemple.tld.key
    chown prosody:prosody /etc/prosody/certs/exemple.tld.crt
    

    Pour aller plus loin :

    La méthode un peu moins simple mais qui est vachement mieux

    Nous allons créer ce dont nous avons besoin en faisant une requête à startssl.com :

    openssl req -sha256 -out /etc/prosody/certs/exemple.csr -new -newkey rsa:2048 -nodes -keyout /etc/prosody/certs/exemple.key
    

    Cette commande génère (openssl req -out) une CSR (-new) ainsi qu'une nouvelle clé RSA de 2048 bits (-newkey rsa:2048) qui ne sera pas chiffrée (-nodes). Si vous voulez encore plus de détails, c'est sur openssl.org.

    Je vous laisse sur startssl.com réaliser les différentes étapes pour s'inscrire (bonne chance !), il faut choisir la première formule (celle qui est gratuite). Après la création de votre compte, la validation de votre nom de domaine, etc. etc. nous pouvons passer à la suite.

    • Après votre authentification sur le site, cherchez l'onglet « Certificates Wizard » qui se trouve normalement vers la gauche de votre écran,
    • il vous demande alors pourquoi vous voulez un certificat ("Select Certificate Purpose"), vous choisissez donc XMPP (jabber) SSL/TLS certificate,
    • le site vous demande de créer une clé privée ("Generate Private Key") : VOUS NE LE FAITES PAS !, vous appuyez au contraire sur skip (nous avons créé la clé privée quelques lignes au dessus),
    • vous arrivez maintenant sur la page de demande de certificat ("Submit Certificate Request (CSR)"), toujours dans un terminal, vous devez taper la commande suivante :
    cat /etc/prosody/certs/exemple.csr
    

    Cette commande vous donnera un résultat qui devrait ressembler à

    -----BEGIN CERTIFICATE REQUEST-----
    MIIChjCCAW4CAQAwQTELMAkGA1UEBhMCRlIxCzAJBgNVBAgMAkZSMQswCQYDVQQH
    DAJGUjELMAkGA1UECgwCRlIxCzAJBgNVBAsMAkZSMIIBIjANBgkqhkiG9w0BAQEF
    AAOCAQ8AMIIBCgKCAQEAsoJcj6/bwl9naKG9C9seKt4HjBicV5o96zqoO0YxtJAe
    X9k2t4KTp0CrzQ85c9DfggY8oAMq/DX/xRFL0cPxamxSwwW5ttVoBQ04wBWDhjEo
    a2ixpe5UMmfakuY3Q56HsIbhh7Vo4RZS1OtPOv7E2J0CfDVUhrNCpDjZbtM8akTE
    9P86BkXdroJgU8tfwONMFDBF2K8ElhN6mqftb89KGIUpgm1fcDq8woRpnFER7A3H
    OwfCfnlkLrtMWVca1smEWnlutBKw6cgk6uSMK9V9/Y44wMKZHoOrOQE0R26+MGrA
    MLhprqPaANIvhamq+tSsSASYZDeajDS3R1JWX188awIDAQABoAAwDQYJKoZIhvcN
    AQEFBQADggEBAHYSpBxHhRP87qmWNqp9Sf8dYz3oQfJLA2cLpQV2MOIfFW0mmOyz
    JG6TVISKVmiEHZtHqgW4TL3BSKBAWENBM8mjAjmxXCmy2MBSWBVhDVaGz4w+x3hO
    UMtNMubYxkkc/xgX5vwbuReH6y1sbkMUQm1UETb6Fnmm8dyDzwPI0zV+NdzUqqhI
    ARjMM2RrwPH7QZ2lSAOiB/X+fXKhwMSg0qUExYiln20JKBi6f58GdyOu6Hp/Fi+m
    r8xnIcnZ2ZIIyjh4B2bfAfybTOWHHRtOaI9yH8pTP3HnKqgbtxZJYqioTAAAQxjQ
    hFmXThFFrfhTDnqJ0Fc+bjcoiLoy46FtLz8=
    -----END CERTIFICATE REQUEST-----
    

    Copiez-le dans la fenêtre en bas (de -----BEGIN CERTIFICATE REQUEST----- à -----END CERTIFICATE REQUEST----- !).
    Vous aurez alors votre certificat peu de temps après, transférez-le sur votre serveur, dans /etc/prosody/certs/ avec comme nom « exemple.tld.crt ».

    Création d'un certificat chaîné

    Pour créer un certificat chaîné, faites la manipulation suivante (startssl.com vous donne les liens vers ces deux certificats juste au dessus du bouton finish »» de la page Save Certificate) :

    • télécharger le certificat intermédiaire de startssl :
    wget https://www.startssl.com/certs/sub.class1.server.ca.pem
    
    • puis le certificat root :
    wget https://www.startssl.com/certs/ca.pem
    
    • puis on forge le certificat chaîné (ne pas oublier les 2 >>) :
    cat sub.class1.server.ca.pem >> /etc/prosody/certs/exemple.tld.crt
    cat ca.pem >> /etc/prosody/certs/exemple.tld.crt
    

    Génération du dhparam

    Création du dhparam (prosody.im/dhparam) :

    openssl dhparam -out /etc/prosody/certs/dh-2048.pem 2048
    

    Java ne peut pas utiliser un dhparam supérieur à 1024 bits, ce qui empêche d'utiliser par exemple le logiciel Jitsi. Pour éviter cela (c'est tout de même un client grandement utilisé), on peut générer un dhparam de 1024 bits avec la commande suivante (ne pas oublier de modifier la configuration pour remplacer dh-2048.pem par dh-1024.pem) :

    openssl dhparam -out /etc/prosody/certs/dh-1024.pem 1024
    

    Configuration du SSL/TLS

    On retourne dans /etc/prosody/prosody.cfg.lua :

        ssl = {
            key = "/var/lib/prosody/exemple.tld.key";
            certificate = "/var/lib/prosody/exemple.tld.cert";
            dhparam = "/etc/prosody/certs/dh-2048.pem";
            options = { "no_sslv2", "no_sslv3", "no_ticket", "no_compression",
            "cipher_server_preference", "single_dh_use",
            "single_ecdh_use" };
            ciphers = "EECDH+ECDSA+AESGCM EECDH+aRSA+AESGCM EECDH+ECDSA+SHA384 EECDH+ECDSA+SHA256 EECDH+aRSA+SHA384 EECDH+aRSA+SHA256 EECDH EDH+aRSA !RC4 !aNULL !eNULL !LOW !3DES !MD5 !EXP !PSK !SRP !DSS";
        }
    
    • c2s signifie « Client TO Server »,
    • s2s signifie « Server TO Server ».
    c2s_ports = { 5222 }
    s2s_ports = { 5269 }
    c2s_require_encryption = true
    s2s_require_encryption = true
    s2s_secure_auth = false
    allow_unencrypted_plain_auth = false;
    

    s2s_secure_auth est sur false pour les raisons suivantes (TL;DR: possibilité de certificat auto-signé en face). Peut marcher avec s2s_auth_fingerprint mais c'est douloureux.

    Les options s2s_secure_domains et s2s_insecure_domains peuvent aussi vous intéresser, surtout si vous voulez parler avec des personnes qui sont sur gmail (ce qui veut dire que ça ne sera pas chiffré).

    Concernant la ciphersuite, le choix par défaut de Prosody est déjà pas mal :

    ciphers = "HIGH+kEDH:HIGH+kEECDH:HIGH:!PSK:!SRP:!3DES:!aNULL";
    

    Il faut tout de même enlever RC4 et eNULL, et tant qu'à faire, autant faire une liste de ciphers avec seulement du PFS (Perfect Forward Secrecy) (c'est à mettre dans le bloc ssl { }) :

    ciphers = "EECDH+ECDSA+AESGCM EECDH+aRSA+AESGCM EECDH+ECDSA+SHA384 EECDH+ECDSA+SHA256 EECDH+aRSA+SHA384 EECDH+aRSA+SHA256 EECDH EDH+aRSA !RC4 !aNULL !eNULL !LOW !3DES !MD5 !EXP !PSK !SRP !DSS";
    

    DNS

    N'oubliez pas d'ajouter les enregistrements SRV dans vos DNS :

    _xmpp-client._tcp.jabber        IN      SRV     0 5 5222 host.exemple.com.
    _xmpp-server._tcp.jabber        IN      SRV     0 5 5269 host.exemple.com.
    

    Firewall

    En cas de firewall, il faut ouvrir les ports 5269 et 5222 (IN et OUT) en TCP. La configuration pour iptables donne ceci :

    iptables -I INPUT -p tcp --dport 5269 -j ACCEPT
    iptables -I OUTPUT -p tcp --sport 5269 -j ACCEPT
    iptables -I INPUT -p tcp --dport 5222 -j ACCEPT
    iptables -I OUTPUT -p tcp --sport 5222 -j ACCEPT
    

    Test

    Comme SSLLabs pour tester le SSL/TLS sur les serveurs webs, il existe xmpp.net pour les serveurs XMPP. Je vous conseille vivement de tester votre site !

    Il faut toujours vérifier, même quand on pense pouvoir avoir confiance.

    Si vous vous demandez comment améliorer votre note, c'est là : xmpp.net/about.

    Lire les commentaires

  • Revue de presse de l'April pour la semaine 4 de l'année 2015 (Dépêches LinuxFR)

    La revue de presse de l'April est régulièrement éditée par les membres de l'association. Elle couvre l'actualité de la presse en ligne, liée au logiciel libre. Il s'agit donc d'une sélection d'articles de presse et non de prises de position de l'association de promotion et de défense du logiciel libre.

    Sommaire

    [L'Informaticien] Interdiction des machines à voter? Une proposition de loi est sur la table

    Par Emilien Ercolani, le vendredi 23 janvier 2015. Extrait:

    «Marginal», «en sursis», «dysfonctionnements»… Le député centriste de la Loire François Rochebloine n'a pas de mots assez durs pour décrire les machines à voter, qu’il souhaite définitivement interdire dans une proposition de loi déposée le 21 janvier.

    Lien vers l'article original: http://www.linformaticien.com/actualites/id/35507/interdiction-des-machines-a-voter-une-proposition-de-loi-est-sur-la-table.aspx

    Et aussi:

    [Le Monde Informatique] L'UE doit-elle obliger les géants de l'Internet à céder leurs clés de chiffrement

    Par Serge Leblal, le jeudi 22 janvier 2015. Extrait:

    La montée en puissance du terrorisme en Europe relance le débat sur le chiffrement des communications et la création de backdoors réservés aux forces de l'ordre européenne. Le coordinateur antiterrorisme de l'UE, Gilles de Kerchove, demande sans détour un accès aux clefs de chiffrement des géants de l'Internet.

    Lien vers l'article original: http://www.lemondeinformatique.fr/actualites/lire-l-ue-doit-elle-obliger-les-geants-de-l-internet-a-ceder-leurs-cles-de-chiffrement-59993.html

    Et aussi:

    [Libération.fr] Le lobby anti-DRM s’étoffe

    Par Camille Gévaudan, le jeudi 22 janvier 2015. Extrait:

    Le journaliste et auteur de science-fiction Cory Doctorow est un fervent défenseur du partage en ligne et un grand penseur des technologies, qui ne doivent pas selon lui brider l’accès du public à la culture. On ne s’étonne donc pas de le voir rejoindre l’Electronic Frontier Foundation (EFF) en tant que consultant spécial chargé du lobby anti-DRM.

    Lien vers l'article original: http://ecrans.liberation.fr/ecrans/2015/01/22/le-lobby-anti-drm-s-etoffe_1186627

    [Numerama] Droit d'auteur: les propositions du rapport de l'eurodéputée pirate Julia Reda

    Par Guillaume Champeau, le lundi 19 janvier 2015. Extrait:

    L'eurodéputée pirate Julia Reda présentera mardi en commission son rapport sur la mise en oeuvre de la directive de 2001 sur le droit d'auteur dans la société de l'information, dans lequel elle plaide pour un large assouplissement des conditions de réutilisation des oeuvres. Mais sans remettre en cause les fondements du droit d'auteur ni exiger de révolution.

    Lien vers l'article original: http://www.numerama.com/magazine/31920-droit-d-auteur-les-propositions-du-rapport-de-l-eurodeputee-pirate-julia-reda.html

    Et aussi:

    [FrenchWeb] Comaking: les start-up doivent-elles adopter la tendance?

    Par Camille Adaoust, le lundi 19 janvier 2015. Extrait:

    Le comaking, un phénomène qui nous vient des Etats-Unis. Il s’installe petit à petit en France. Paris, Lyon, Marseille, Bordeaux, dans les grandes villes, ces espaces de production partagés prennent leurs marques.

    Lien vers l'article original: http://frenchweb.fr/comaking-les-start-up-doivent-elles-adopter-la-tendance/179886

    [Next INpact] Plan e-éducation: davantage de numérique dans les enseignements à partir de 2016

    Par Xavier Berne, le lundi 19 janvier 2015. Extrait:

    À l’occasion du débat organisé mercredi dernier à l’Assemblée nationale à propos de la stratégie numérique de la France, la secrétaire d’État au Numérique Axelle Lemaire est revenue sur le grand «plan pour le numérique à l’école» promis l’été dernier par François Hollande. Non sans une certaine impression de réchauffé…

    Lien vers l'article original: http://www.nextinpact.com/news/91755-plan-e-education-davantage-numerique-dans-enseignements-a-partir-2016.htm

    Et aussi:

    [Le Monde.fr] Numérique: des images deux fois moins lourdes

    Par David Larousserie, le lundi 19 janvier 2015. Extrait:

    Un ingénieur français a développé un nouveau format de compression plus efficace que l’incontournable JPEG.

    Lien vers l'article original: http://www.lemonde.fr/sciences/article/2015/01/19/des-images-deux-fois-moins-lourdes_4559136_1650684.html

    Lire les commentaires

  • FOSDEM 2015 ce week-end du 31 janvier à Bruxelles (Dépêches LinuxFR)

    C'est devenu une habitude, le premier week-end de février des milliers de développeurs se réunissent dans le cadre du FOSDEM.

    Le FOSDEM (Free and Open Source software Developers' European Meeting) est le plus grand congrès gratuit pour les développeurs du Libre, organisé uniquement par des bénévoles.

    Le congrès se déroule à Bruxelles dans les locaux de l'ULB sur le campus du Solbosch.

    fosdem

    FOSDEM15'

    Programme

    Keynotes

    Main tracks

    Developer rooms

    Lightning talks

    Les lightning talks sont de courtes présentations de 15 minutes sur d'un projet pour donner envie aux gens d'y participer. Il y a quarante-et-une présentations de prévues.

    Examens

    En plus des certifications Linux Professional Institute (LPI), une certification BSD et une certification LibreOffice sont disponibles.

    Et, si vous avez un peu de temps disponible, venez donner un coup de main dans l'organisation : il y a des tâches de tout niveau.

    Lire les commentaires

  • Actualités NAS (Journaux LinuxFR)

    Bonjour,

    Leecher sur DLFP, ceci est mon premier journal.

    Les NAS, c'est mon actuel centre d'intérêt, et je trouve qu'il y a trop peu d'infos les concernant sur DLFP, alors un petit coup de plume pour tenter d'y remédier.

    Les plus connus ;
    * FreeNAS
    * NAS4Free
    * OMV, le petit Dernier

    NAS, comme Network Attached Storage, stockage attaché au réseau, en gros c'est un espace de stockage de données accessible par le réseau local.
    Les principaux protocoles proposés sont ;
    * SMB/CIFS de Microsoft, via l'implementation SAMBA, utilisé par les particulier pour sa diffusion (MS-Windows étant très répandu), ça sert à partager les répertoires/fichiers et les imprimantes
    * NFS (Network File System, système de fichier par réseau), du monde UNIX, exclusivement pour les répertoires
    * FTP (File Transfert Protocol, protocole de transfert de fichiers), du temps de la naissance d'internet, utilisé essentiellement pour les mise à jours des systemes d'exploitation et de moins en moins par les particuliers
    * AFS (Apple File ??), c'est un protocole de la pomme que je ne connait pas très bien et que je n'ai jamais eu l'occasion de fréquenter.

    Parmi les points communs ;
    . interface de gestion par HTTP, modifiable en HTTPS
    . plusieurs traductions de l'interface de gestion, dont le français
    . un système d'extensions/plugins plus ou moins riche proposant des trucs comme clamav (anti-virus), owncloud, nut (gestion onduleur), et quelques joyeusetés du genre "media player",
    . prise en charge des differents types de RAID.
    . installation sur un USB de type flash à partir de 2Go (4Go recommandés)

    Maintenant les actualités

    FreeNAS
    Basé sur FreeBSD, la version 9.2 est la dernière à prendre en charge les 32bit, à partir de la version 9.3 c'est exclusivement x86_64, avec comme processeur 64bits et 8Go de RAM
    LA version 9.3 est sortie en decembre 2014, annonce.
    FreeNAS est orienté usage professionnel.
    ZFS par défaut, on est direct dans la catégorie TéraOctets, gros transferts, et utilisation intense, les autres systèmes de fichiers ne sont accessibles qu'en lecture, c'est un choix pour privilégier les performances.
    Les petites configs et les amateurs (non-pro) sont poussés vers NAS4FRee.
    Zfs est assez puissant, riche en fonctionnalités, mais des besoins en calcul (cpu) et mémoire conséquents pour en tirer parti, besoins proportionnels aux volumes de données en jeu et aux capacités des disques utilisés.

    NAS4Free
    Basé sur FreeBSD, elle est la continuité de FreeNAS quand elle a changé pour s'orienter vers le professionnel et a décidé de modifier ses composants (une histoire de base en python/php/perl, qui m'echappe un peu).
    NAS4Free permet encore de mettre à niveau de vieux FreeNAS (0.7.x).
    Les news ne sont pas claires, mais la version 9.3 est sortie en janvier 2015.
    NAS4FRee semble plus orienté récupération de vieux PC.
    UFS par défaut, zfs reste disponible, ext2fs est possible mais non recommandé.

    OMV
    OpenMediaVault est basé sur Debian.
    Dans sa base, on a nginx pour l'interface webgui. FreeNAS et NAS4Free semblent être motorisés par apache.
    OMV peut s'installer à partir d'une Debian opérationnelle par la modification de la liste des dépots (/etc/apt/sources.list), cela confère une petite souplesse qui permet d'utiliser le disque de démarrage comme disque de stockage (partitions séparées). FreeNAS et NAS4Free ont l'exclusivité du disque oû le système est installé, pour le stockage il faudra au minimum un autre disque, d'où l'intéret de l'installation sur USB.
    La dernière ISO d'installation date de début janvier 2015 pour la version 1.9.
    OMV est aujourd'hui disponible en version 1.11, mise à jour par l'interface web.
    Petit dernier sur la scène mais avec une réelle vitalité.
    Particularité, OMV propose une fonction firewall, ça m'a surpris mais ça doit avoir son utilité.
    OMV propose les FS classiques de GNU/Linux (ext2, ext3, ext4, …) mais aussi btrfs et zfs. OMV prend en charge LVM.
    Btrfs est le pendant linux de zfs, ses besoins seraient modestes (par rapport à zfs) sans être négligeables.

    Il y a certainement d'autres systèmes orienté NAS, mais comme on n'en parle pas beaucoup,

    @+

    Lire les commentaires

  • RiP Demis (Journaux LinuxFR)

    Demis Roussos a été bronsonisé dans la nuit de samedi à Dimanche.

    De là à voir un rapport avec la victoire aux élections de la gauche radical en grèce, il n'y a qu'un pas !

    Tu ne sais pas qui est Demis Roussos ?
    Tu n'es pas né au bon moment -prends-en toi à tes parents- pour connaître cet artiste, dont on retiendra, je cite :

    l'étalage oriental de rondeurs extravagantes, enveloppées dans de larges aubes blanches et de turbulents batiks, ou les gros plans sur la barbe hirsute et les cheveux longs, chapeau et cartouchière à la Pancho Villa
    http://lemonde.fr

    Tu ne sais pas ce que veut dire "bronsonisé" ? Prends des orties et flagelle-toi, hérétique !!!!!!!!

    Lire les commentaires

  • Le challenge du logo ANSSI (Journaux LinuxFR)

    Il ne me semble pas que ce soit passé ici alors voilà un petit bookmark : Ceci n'est pas un blog: Le challenge du logo ANSSI

    Lors de la sortie de leur nouveau logo en 2012, l'ANSSI a lancé un challenge planqué dans une image png.

    Le gars l'a finalement résolu deux ans après.

    Lire les commentaires

  • Installation de logiciel : comportement des utilisateurs en fonction du système d’exploitation (Journaux LinuxFR)

    J’ai toujours été amusé par la différence de mentalité entre les utilisateurs de Windows / MacOS / GNU-Linux. L’installation de logiciels est symptomatique de cette différence. J’ai voulu schématiser cette différence en caricaturant très légèrement, j’espère que cela vous semblera pertinent/amusant :

    installation fonction os

    (version svg)

    Lire les commentaires

  • GNU GPL et commercialisation : mauvaise compréhension des licences, l'exemple WPScan (Journaux LinuxFR)

    Bonjour Nal,

    Un litige entre un développeur et une société à propos de l'utilisation d'un logiciel libre sera présenté ci-après. Il fait écho à une question revenant très souvent dans les journaux et commentaires sur LinuxFr : la réticence de certains à mettre leur programme sous licence GPL de crainte de se faire "piller" et que d'autres en profitent pour vendre un outil tirant parti du leur, gagnant de l'argent sans aucune obligation légale de contrepartie autre que le respect de ladite GPL, et les privant de fait d'un potentiel revenu qui leur reviendrait moralement de droit.

    Si le libre offre de nombreux avantages (partage, communauté de contributeurs…), il fait parfois peur à des particuliers ou petites structures ayant la compétence technique mais pas le temps ou le talent commercial pour faire du marketing ou obtenir des contrats. Lorsque le dév' est seul (ou l'équipe très réduite) et porte un programme lourd en investissement (code, correction des bugs, intégration upstream des patchs tiers, communication), c'est difficile de s'en sortir sans un emploi à côté (mais dans ce cas, ajouté à la vie de famille, reste peu de disponibilité et de motivation) ou sans monétisation (sponsor, contrats de support et maintenance).

    Pire, parfois ce dév' voit, après avoir consacré plusieurs années à son projet, débarquer une entité qui reprend son code et l'incorpore à un package commercial, avec une grande force de frappe, mais tout en respectant les termes de la licence.

    Régulièrement de telles polémiques surgissent, ou même des forks dans des contextes légèrement différents (Nexuiz et Xonotic dans le domaine du jeu vidéo ou encore Nagios et Icinga pour la supervision système). Ces derniers jours, une nouvelle discussion a commencé concernant le logiciel WPScan, un scanner de vulnérabilité pour le CMS Wordpress.

    Ses mainteneurs se plaignent que, régulièrement, des sociétés commerciales incorporent leur outil au sein du leur et le vendent, sans que eux bénéficient en retour de la moindre compensation pour leur travail. Ce que la GPL autorise parfaitement, ils le soulignent, à condition que le dérivé soit lui aussi mis à disposition sous une licence compatible.

    Selon eux à chaque fois ce n'était pas le cas, et ils contactaient alors l'entreprise en question pour leur proposer une version commerciale non libre et payante ; tous ont refusé et la plupart cessé d'utiliser WPScan. Récemment, un nouvel acteur entre en jeu avec la même approche.

    Face à cela, les créateurs de WPScan se disent lassés et celui-ci est alors basculé sous une double licence : non libre en cas d'usage commercial et soumise à un paiement, libre GPL en cas d'utilisation non commerciale (particulier, distribution Linux comme BackBox ou Kali, service gratuit…).

    Cette dualité pose deux problèmes : est-il autorisé de modifier ainsi unilatéralement la licence sans l'accord préalable et explicite de tous les contributeurs au projet (il n'y avait pas de transfert de copyright) ? Est-elle compatible avec la GPL ? Il semble que non… Et Delve peut-il agir ainsi ?

    Pour ne pas refaire l'erreur de mon précédent journal (réagir à chaud à une info partielle sur Twitter et rédiger un texte en partie erroné), j'ai attendu un peu et regardé les deux versions avant de publier.

    Là en l'occurrence, le problème des développeurs de WPScan ne semble pas tant être que d'autres gagnent de l'argent grâce à leur produit - on comprend tout de même qu'ils aimeraient en récupérer un peu, ce qui est moralement légitime et compréhensible mais pas juridiquement imposé - que la violation par les boîtes commerciales de la liberté logicielle.

    Dans le cas précis de Delve Labs (ils ne donnent pas les autres exemples précédents), la question à trancher reste donc : respectent-ils ou non la licence GPL ?

    Dewhurst Security prétend que non, Delve rétorque qu'ils lancent simplement l'outil en ligne de commande, ils ne l'incorporent pas à leur propre soft.

    A priori, la solution commerciale (et propriétaire) qu'ils proposent est en effet un service hébergé en ligne, ils ne mettent pas de logiciel à disposition.

    Ce serait bien d'avoir des éclaircissements sur ce point.

    Mais si Delve Labs respecte la GPL, ils ont parfaitement le droit de commercialiser leur outil incluant WPScan. Aucune obligation légale de payer.

    Après, est-ce que le choix de la licence AGPL n'aurait pas été plus pertinent pour WPScan, justement à propos de cette option : "si vous exécutez un programme sur un serveur et laissez d'autres utilisateurs communiquer avec celui-ci, votre serveur doit aussi leur permettre de télécharger le code source correspondant au programme qui est exécuté. Si ce qui s'exécute est votre version modifiée du programme, les utilisateurs du serveur doivent obtenir le code source tel que vous l'avez modifié."

    À noter que, suite à cette polémique, Delve a forké WPScan en reprenant la dernière version distribuée sous GPL, sous le nom de Vane.

    Cas d'école intéressant, à suivre.

    Lire les commentaires

ton âme verdâtre âcre russule
au levant s'amorce de terreurs
lueur rose crêtes avant drame
ruses d'amant où crève la terre

à ras la mort vendeuse recrute
la vertueuse acérant remords
élève âcre mur dans sa torture
sue mercure dans la rate torve

verte lourdeur en cet amas ras
ta carrure admoneste révulse
au sud ta trace renverse l'orme
des manoeuvres le tartare cru

autour des calmes entreverras
l'aurore crémeuse star devant
envoûter la terre du massacre
Autrans Méaudre et le Vercors

-- Chamontin, Élisabeth