La tache principale de Mandrakesoft sera d'adapter sa distribution et de mobiliser les ressources de la communauté du logiciel libre autour de ce projet. À terme, les résultats de ce projet seront publiés sous licence Open Source (NdM : libre ?).
François Bancilhon, directeur général de Mandrakesoft, indique : « C'est [...] notre projet le plus important à ce jour, et un événement majeur pour notre entreprise.» C'est incontestablement un bonne nouvelle pour Mandrakesoft, qui engrange un gros contrat et renforce par la même occasion sa crédibilité vis à vis des grands comptes, mais également pour l'ensemble de la communauté du logiciel libre, qui voit ici reconnue la supériorité du modèle open source en matière de sécurité des systèmes informatiques.
Aller plus loin
- L'annonce officielle (24 clics)
- Mandrakesoft (15 clics)
- Surlog (5 clics)
- Bertin (3 clics)
- Jaluna (3 clics)
- Opida (3 clics)
# calcul de base ...
Posté par Mouns (site web personnel) . Évalué à 7.
cela fait un peu moins de 28 000 euros de chiffres d'affaire brut par mois.
si l'on compte que ce chiffre d'affaire est directement versé en salaire, cela represente 6 salaires à 2 000 euros net.
si l'on inclus les frais generaux que represente un salarié, cela tombe à 4 ou 5 salaires à 2 000 euros net.
"La tache principale de Mandrakesoft sera d'adapter sa distribution et de mobiliser les ressources de la communauté du logiciel libre autour de ce projet"
donc mandrake a x salarié pour sa distrib. doit ajouter y salariés pour adapter la distrib aux criteres de qualités et z pour motiver les benevoles.
x on s'en fout il bougera pas vraiement ( à la rigueur, quelques ressources seront migrés vers y ).
sachant que pour motiver la communaute, on va lui proposer la methode à la mode : le bounty.
1 salarié en moins = 4 000 euros de bounty HT & TCC
avec 4000 euros, on fait combien de bounties à 100-euros-empochés ?
moins de 40 ( je ne sais pas trop comment comptablement passé en france un bounty a part en frais de restauration ).
conclusion, il va y avoir peu de recrutement et des bounty qui ressembleront à "pour 100 balles et un mars, tu me fais du bon patch".
je ne sais plus qui a dit sur une marché idéal les couts structurels se retrouveront exprimer uniquement par des couts minimaux au niveau de la force de production. certains raillait le truc avec un complement du genre "cad le prix d'un bol de riz".
perso, dans ce cas, je dirais "cad le prix d'un bounty et mars" :|
[^] # Re: calcul de base ...
Posté par grumly_gg . Évalué à 2.
http://fr.lolix.org/search/offre/offre.php3?id=4006(...)
[^] # Re: calcul de base ...
Posté par cyberv . Évalué à 2.
Je l'avais vu passé dans la lettre aux actionnaires de Mandrakesoft.
Il n'y a aucune cause à effet, sauf peut-être pour la mise en place de l'annonce sur lolix car maintenant ça doit urger.....
[^] # Re: calcul de base ...
Posté par Pascal Terjan (site web personnel) . Évalué à 10.
Le travail sera fait que la communauté y participe ou pas, la participation de la communauté serait un plus et l'idée est que Mandrakesoft le rende possible grace à son habitude de travailler beaucoup avec des contributeurs externes. Le projet étant intéressant on peut espérer que des gens y participeront ou simplement testeront le logiciel.
Il n'y a pas besoin de 10 personnes pour gérer ca. Il n'y a pas actuellement 10 personnes pour gerer les relations avec les contributeurs sur la distribution normale et là il devrait y avoir moins de contributeurs.
conclusion, il va y avoir peu de recrutement et des bounty qui ressembleront à "pour 100 balles et un mars, tu me fais du bon patch".
Question recrutement, il y en a et ca a commencé. Question bounty, ce n'est pas du tout l'idée... De plus je pense qu'il est plus probable d'avoir des contributions de sociétés intéressées ou d'organismes gouvernementaux que de développeurs qui ne sont pas forcément intéréssés par la problématique (bien que techniquement la solution soit intéressante).
doit ajouter y salariés pour adapter la distrib aux criteres de qualité
Visiblement, ici comme sur tous les sites qui en parlent il y a eu une grosse incompréhension sur le projet. Ce n'est pas l'ensemble de la distribution qui sera certifiée, c'est impossible (ca implique par exemple une tracabilité totale du source). Il y aura un noyau dont ca sera le cas (voir la technologie de Jaluna), avec en plus au dessus un certain nombre de modules également certifiés. Toutes les vérifications de sécurité, le filtrage réseau, la gestion de l'authentification,... seront faites à ce niveau (donc par le code sur). La majorité des logiciels seront considérés comme externes et non surs.
Le but n'est donc pas d'adapter la distribution aux critères de qualité mais à ce noyau spécial, et de gerer ses fonctionnalités de sécurité (en particulier niveau installeur et administration). Seule la partie du code touchant à la sécurité devra être certifiée. Il sera donc ensuite possible de faire une distribution Desktop dessus, les logiciels en question étant juste non sur, ce qui n'est pas trop grave dans la mesure où tout le bas niveau est sur et controle ce qui se passe au dessus.
[^] # Mandrake et la communauté
Posté par Amaury . Évalué à 1.
> participation de la communauté serait un plus et l'idée est que
> Mandrakesoft le rende possible grace à son habitude de travailler
> beaucoup avec des contributeurs externes. Le projet étant
> intéressant on peut espérer que des gens y participeront ou
> simplement testeront le logiciel.
Mandrake repose beaucoup sur la communauté c'est vrai, mais cela est possible parce que Mandrake distribuait tous ses logiciels sous des licences libres et ses distributions gratuitement.
La nouvelle politique de Mandrake, de mon point de vue à moi (un utilisateur lambda qui sait vaguement synchroniser urpmi sur un miroir quelconque), est que depuis quelques temps la boite s'écarte dangereusement de ses principes initiaux :
- certains softs sont publiés sous des licences non libres (ministère défense ? MNF et ses 2 licences)
- certains logiciels libres packagés ne sont volontairement mis que sur les CD commerciaux (et absents des miroirs publics), donc non utilisables par ceux qui n'achètent pas une boite ou ne sont pas inscrits au club
- certaines distributions (Move notamment, prochaine MNF 2 semble-t-il à lire la liste de diffusion) ne sont distribuées qu'en version limitée
- à lire cette news, Mandrake va vouloir faire bosser la communauté sur du code "open source" (il est où le logiciel libre là dedans ?)
Personnellement je trouve regrettable cette nouvelle orientation de la part d'une société qui, certes, semble peiner à trouver un business model rentable à terme, mais qui depuis sa création compte énormément sur la communauté pour l'aider à développer et tester ses produits. La communauté en a bénéficié jusqu'à présent grâce aux ISOs "complètes" en ligne (hormis softs commerciaux, mais on ne peut pas le reprocher à MDK) et aux logiciels libres. Maintenant si la collaboration Mandrake/Communauté se fait dans un seul sens, il ne faut pas s'étonner si la marmotte arrête un beau jour de travailler gratos .
[^] # Re: Mandrake et la communauté
Posté par Pascal Terjan (site web personnel) . Évalué à 3.
En l'occurence, la licence du projet n'est pas choisie, le cahier des charges dit qu'elle doit respecter les principes reconnus pour caractériser une licence dite « libre » tels qu'énoncés par la Free Software Foundation FSF ou l'Open Source Initiative OSI et qu'elle sera choisie parmi les licences libres les plus usitées. Je ne savais pas que l'OSI avait défini les logiciels libres, donc bon on verra quand elle sera choisie dans quelques mois.
Pour MNF et ses 2 licences ca ne me dérange pas dans la mesure ou tout est dispo dans la version libre.
- certains logiciels libres packagés ne sont volontairement mis que sur les CD commerciaux (et absents des miroirs publics), donc non utilisables par ceux qui n'achètent pas une boite ou ne sont pas inscrits au club
Arrete KDE ! Mais oui ca pue :-(
- certaines distributions (Move notamment, prochaine MNF 2 semble-t-il à lire la liste de diffusion) ne sont distribuées qu'en version limitée
Oui en effet, toutefois le changement à apporter à la move pour retirer la limitation est vraiment minime, et la licence te permet de le faire.
Pour la MNF je ne sais pas mais je ne doute pas que tu sois bien au courant :-)
[^] # Re: calcul de base ...
Posté par Mouns (site web personnel) . Évalué à -1.
personnellement, ca pourrait etre pris comme si un organisme ( pas necessairement etatique ) payait les resto du coeur pour encadrer ses benevoles pour la distribution des repas. soit c'est un don, soit c'est une traite. si c'est une traite alors pas de vice de forme et tout travail merite salaire.
j'en arrive aux bounties. la prime est une gratification, un compensation, un appointenement, un salaire. tout travail merite salaire. placons le dans le cadre du droit social europeen. aujourd'hui, peut on proposer un bounty dont la charge de travail represente un salaire inferieur au SMIC horaire ? legalement non.
aujourd'hui, quel est la legalité d'un bounty en france ?
pour les criteres de qualite, il me semble evident que GIMP et plein d'autres ne seront pas necessairement patché pour etre CC-EAL5 ...
... par contre frozen bubble et wmcoincoin doivent l'etre c imperatif. et pour les patcher il en faut des ressources humaines ( surtout pour les benchmarks ). heureusement que ce n'est pas debian qui a chopé le contrat, il aurait fallu tester tous les niveaux de frozen bubble sur 11 archi differentes !!!!!!! ... fin de l'apparté.
je pense que cela sera des patchs dans les fondements : le kernel, certaines libs et applis sensibles. donc il ne faut pas non plus 15 000 salariés. et vu que tu me le confirmes on est donc d'accord :)
[^] # Re: calcul de base ...
Posté par Pascal Terjan (site web personnel) . Évalué à 3.
Linus est payé pour encadrer le développement du noyau, ca te dérange ?
[^] # Re: calcul de base ...
Posté par Mouns (site web personnel) . Évalué à 1.
sinon, linus touche un salaire pour son travail de mainteneur du noyau.
mandrakesoft, redhat,Novell vend du linux, ca ne me derange pas tant que mandrake vends les developpements qu'il fait.
imagine un truc genre une boite qui recupere une debian et la vend en l'etat à un organisme sachant qu'il vend de l'encadrement de benevole et donc d'une certaine maniere il vend le cout que cela represente de chasser un debianiste, de le capturer vivant et d'en faire un esclave.
présenté comme ca, ca fait pas credible ... mais et si ?
le fait que mandrakesoft recrute ne me derange en aucun cas, c meme apreciable. mais le fait que mandrakesoft sur 7 000 000 ¤ ne touche que 1 000 000 ¤ alors qu'il sont 5 . si en plus mandrakesoft doit faire trimer des benevoles pour reussir, je trouve qu'il y a une arnaque ... non dans l'attitude de la société mandrakesoft qui fait ce qu'elle peut, mais dans :
1 - l'inequité du partage
2 - le montant ridicule que cela represente à coté de certains chantiers vides facturés excessivement plus
je ne connais pas les termes du contrat ... donc je m'enerve pour rien peut etre ...
[^] # Re: calcul de base ...
Posté par Prosper . Évalué à 3.
bin y a des distribs basées sur debian ou t'es obligé d'acheter ( je pense a lindows , xandros ,libranet) pour obtenir une iso, je vois pas trop en quoi c' est tellement different.
# C'est cool :)
Posté par Guillaume Knispel . Évalué à 6.
Esperons que ce projet ce déroule bien, et notons que si c'est le cas le résultat dépasserait win2k qui est 'seulement' EAL4 ;) http://www.windowsecurity.com/articles/Windows-Common-Criteria-Cert(...)
[^] # Re: C'est cool :)
Posté par Victor STINNER (site web personnel) . Évalué à 6.
http://tontonth.free.fr/insecure-microsoft.txt(...)
Ce document dit que :
C'est plutôt un truc comme ça, nan ?
D'autres infos sur le "EAL" : http://geek.linuxman.pro.br/article.php?story=2004072911570867.(...) On y lit que "SuSE Linux Enterprise Server V8, Service Pack 3, RC4, January 2004" a reçu un "EAL 3+" (+ pour "presque EAL4). Pas mal nan ?
Haypo
[^] # Re: C'est cool :)
Posté par Gart Algar . Évalué à 9.
J'aime beaucoup linux, mais des fois faut quand même essayer d'être honnete et objectif.
[^] # Re: C'est cool :)
Posté par PloufPlouf (site web personnel) . Évalué à 2.
mais c'est quidquid
je me dis que, vu sons sens, écorcher cette phrase, fait passer pour un cretin aupres des latinistes...
[^] # Re: C'est cool :)
Posté par pasBill pasGates . Évalué à 1.
Quand on lit des trucs du genre :
L'idée est d'expliquer que si la plupart des patchs et mises à jour ne fonctionnent pas, c'est parce que les systèmes et logiciels actuels sont trop vieux pour les supporter
ou
En fait, ce que Microsoft cible, c'est bien évidemment l'énorme marché que la doctrine ultrasécuritaire de George W. Bush ne manquera pas de créer.
Ce papier est un vrai torchon, prends au moins un truc un minimum objectif pour te faire une opinion.
[^] # Re: C'est cool :)
Posté par syntaxerror . Évalué à 5.
Les boites de consultants en sécurité profitent un max de l'effet "11 Septembre"
(comme d'autres avant eux du "bug de l'an 2000")
[^] # Re: C'est cool :)
Posté par Victor STINNER (site web personnel) . Évalué à 1.
Désolé, j'ai pris le premier trouvé pas Google ... Je ne sais même plus où j'ai rangé le MISC en question (et puis là j'suis au boulot ...).
@+ Haypo
# Commentaire supprimé
Posté par Anonyme . Évalué à 4.
Ce commentaire a été supprimé par l’équipe de modération.
# A la fin, il y a quand meme une certification !
Posté par jeff110 . Évalué à 4.
Certe, Le monde GNU/Linux cultive la securité, mais MDK n'est pas vraiment leader dans ce dommaine face à d'autre distributions.
Le point ford de MDK, C'est le coté intuitif, l'interface graphique de la distrib...
En meme temps, j'ai toujours eu l'impression de les MDK x.x manquaient de finition, avec des peitits bugs pas forcement genant, mais en pagaille
C'est donc selon moi un certain challenge que Mandrake doit reussire.
Enfin, un million d'euros, ça me semble leger pour develloper une nouvelle distrib special secure; mais si au final, MDK obtient une certification de l'armée, c'est bon pour son image.
Je vois donc ça un peu comme un investissement.
Et puis comme dit un gag sur Clubic, ce contrat, c'est peu etre un essai, une premiere envellope qui permet à MDK de faire ses preuves ...
[^] # Re: A la fin, il y a quand meme une certification !
Posté par nextgens (site web personnel) . Évalué à 6.
C'est une distribution "desktop" ou "serveur" qu'il veulent faire?
Dans les deux cas :
=========>si c'est pour les serveurs, pourquoi pas openbsd?
=========>si c'est pour les end-user, mandrake n'est'il déja pas mieux que la suite microchiote? (avec les ACL, authentification centralisée via RADIUS, ... )
PS : IMHO la 'certification CC-EAL5' c'est bien beau, mais ca n'empéchera pas l'ex vindosien d'avoir la clickomania... Comment dit-on déja? la principale faille d'un système n'est-il toujours pas la composante humaine?
[^] # Re: A la fin, il y a quand meme une certification !
Posté par harbort1 . Évalué à 6.
Sinon, pour ta citation, moi je préfère :
"le bug est généralement entre la chaise et l'écran"
[^] # Re: A la fin, il y a quand meme une certification !
Posté par Yann Cochard (site web personnel) . Évalué à 7.
"C'est l'interface fauteuil / clavier qui déconne"
[^] # Re: A la fin, il y a quand meme une certification !
Posté par Eric Leblond (site web personnel) . Évalué à 4.
> =========>si c'est pour les serveurs, pourquoi pas openbsd?
securisé n'exclut pas forcément performance. Un serveur multiprocesseur a lui aussi droit à la sécurité.
Désolé, difficille de résister.
[^] # Re: A la fin, il y a quand meme une certification !
Posté par Xavier Teyssier (site web personnel) . Évalué à 4.
Comment ça, j'ai marché dedans ?
[^] # Re: A la fin, il y a quand meme une certification !
Posté par Vanhu . Évalué à 3.
Et puis pour information, pour passer les CC, il ne suffit pas de faire un code prétendument "secure", parait-il super audité, avec plein de méchanismes a 2 balles pour portéger des buffers overflow.
Il faut aussi pondre une doc clean, des explications détaillées sur les modules, les procédures de développement (et un "bah Theo s'en occupe" va pas suffire, je pense....), et a partir de EAL5, un code plutot clean et bien commenté !!!
Et puis pour marcher dedans moi aussi a fond, c'est bien beau de détecter un 2nd processeur, mais ca suffit pas pour avoir des performances raisonnables, faut encore avoir des algos qui ne sont pas trop pourris, au moins dans les endroits critiques.........
[^] # Re: A la fin, il y a quand meme une certification !
Posté par thaodalf . Évalué à 1.
tu peut détailler ?
[^] # Re: A la fin, il y a quand meme une certification !
Posté par ckyl . Évalué à 3.
[^] # Re: A la fin, il y a quand meme une certification !
Posté par Nap . Évalué à 2.
[^] # Re: A la fin, il y a quand meme une certification !
Posté par nextgens (site web personnel) . Évalué à 2.
Setup.exe -> suivant -> ok , suivant -> suivant -> terminé ...
qui conduit à accepter ce genre de chose ( CLUF de WMP9 http://www.chez.com/nextgens/files/(...) )
ou a effectuer des opérations non recommandées ( Etes vous sur de vouloir exécuter la pièce jointe non signée, contenant un virus ? [O/N] )
synonyme de "jemenfoutisme" adapté au jargon informatique ;-)
[^] # Re: A la fin, il y a quand meme une certification !
Posté par nooky59 . Évalué à 3.
Il y a également des CLUF en console, quand tu installes kle J2SDK par exemple/
Personnelement, quand je vois la tartine gavante à lire, je ne lis pas.
Ca n'est pas l'idéal, surtout quand on est amateur de logiciel libre mais bon ainsi va la flemne et la rapidité de découverte d'un nouveau logiciel ;o)
[^] # Re: A la fin, il y a quand meme une certification !
Posté par Joris Dedieu (site web personnel) . Évalué à 6.
Il semble toutefois que Mandrake n'ait qu'une "petite" partie du boulot à accomplir.
Je cite le communiqué de Mandrake :
Selon les partenaires du consortium, les techniques de virtualisation et de partitionnement matériel seront au centre des systèmes d'exploitation de demain.
En ce domaine, Jaluna risque de faire de gros apport technique, puisque la virtualisation est son fond de commerce.
Jaluna est responsable du développement du système
Mandrake s'occuppera donc de ce qu'il sait faire : une distribution linux. je pense évidement qu'ils intégrerons des technologies telle que SElinux (ce qui ma fois est dans l'ordre des chose).
En tout cas une amélioration de Mandrake en terme de sécurité sera sans doute bénéfique à l'ensemble des logiciels libres. Mandrake n'ayant à ma connaissance jamais été ambiguë sur la disponibilité de ses sources.
Visiblement le consortium compte sur la communauté pour auditer et améliorer le code source. Si la communauté peut en retirer une solution de virtualisation viable, stable et performante, je pense qu'il y aura du monde au portillon. Toutefois, en ce domaine, toute demi-mesure avec la liberté serait sans doute fatale.
Je pense qu'il y a là, une réelle opportunité de plus pour une dynamique Européenne autour du libre. D'ailleurs, le communiqué ne manque pas de rappeler : Le domaine d'application de la solution de sécurité multi niveaux développée par le projet dépasse largement le cadre strictement militaire. Elle est destinée au marché industriel en général, des télécommunications et des systèmes d'entreprise. De grands acteurs industriels seront invités à s'associer au projet pour faire part de leurs besoins et interagir avec l'équipe de développement.
[^] # Re: A la fin, il y a quand meme une certification !
Posté par Nicolas Boulay (site web personnel) . Évalué à 5.
La distrib inclue déjà un kernel "sécurisé" avec grsec + un mode extrèment fermé par default (paranoïque, un très beau moyen de voir comment mettre en route un service). En gros, en msec 5, un utilisateur ne peut pas sortir de son home, on peut lui interdire les outils réseaux, etc...
"La première sécurité est la liberté"
[^] # Re: A la fin, il y a quand meme une certification !
Posté par nooky59 . Évalué à 4.
OpenBSD est très sûr mais c'est un BSD, pas un Linux.
Que tu prennes une Debian, une Fedora, une SuSE, une Slack ou une Mandrake, tu as tout un travail à faire pour vraiment blinder ta distribution.
Et en parlant de MAndrake, il faut signaler que msec est déjà un bon début. Si tu le passe en niveau 5, ta machine est déjà bien blindée, même si effectivement tu ne maîtrises pas les concepts sous-jacents.
Dans ce cadre, Mandrake est tout aussi adapté qu'une autre distribution majeure en tant que distribution sécurisée.
Je te concède qu'il faut voir la réactivité en terme de rapidité de corrections de failles graves par rapport à d'autres distributions.
Il est également à noter qu'une distribution russe dont je ne connais plus le nom mais qui est orientée bastion est sur une base de Mandrake.
[^] # Re: A la fin, il y a quand meme une certification !
Posté par ashram4 . Évalué à 5.
Le point ford de MDK, C'est le coté intuitif, l'interface graphique de la distrib...
bien d'après ma courte expérience des logiciels militaires je dirais que c'est déjà pas mal le coté intuitif. J'ai travaillé quelques mois à coté de personne qui s'occupaient du système de gestion régimentaire de l'armée de terre (SIR). Parmis les problèmes rencontrés lors des manoeuvres le problème de l'utilisation de l'environnement par les militaires était plus important que les problèmes technique (plantage, bug). Même s'il était reconnu que très peu de militaires qualifiés sur le système étaient présent lors des essais ça révèle quand même que l'aspect interface est crucial.
# Des certifications CC-EALx
Posté par dromadaire35 . Évalué à 8.
- EAL1 : functionally tested
- EAL2 : structurally tested
- EAL3 : methodically tested and checked
- EAL4 : methodically designed, tested, and reviewed
- EAL5 : semiformally designed and tested
- EAL6 : semiformally verified design and tested
- EAL7 : formally verified design and tested
Le passage au niveau EAL5 me semble significatif, puisqu'il introduit l'utilisation de méthodes semi-formelles.[^] # Re: Des certifications CC-EALx
Posté par Joris Dedieu (site web personnel) . Évalué à 7.
Si quelqu'un pouvait expliquer en détail, ça serait vraiment interessant.
Merci
[^] # Re: Des certifications CC-EALx
Posté par Fanf (site web personnel) . Évalué à 10.
Bon, ça c'est la théorie, en pratique la complexité est telle qu'on ne peut généralement pas appliquer une méthodologie pure de A à Z. On doit donc faire des consessions, mais globalement les logiciels créés ainsi ne contiennent presque pas de bug. Il faut aussi que la spécification initiale soit bonne, et c'est là aussi un gros chalenge.
En France, notre recherche est plutôt bien positionnée sur le domaine au niveau mondial, avec en particulier des outils : d'une part, la méthode B et son atelier[1], d'autre part l'assistant à la preuve Coq[2].
Pour ce qui est de la méthode B, c'est une méthode de spécification qui marche par pallier en ce basant sur la théorie des ensembles : on comence par modéliser grossièrement, en posant les propriétés qui doivent être vérifiées, puis on raffine, c'est à dire qu'on devient de plus en plus précis, en prouvant l'équivalence entre chaque niveau. Au final, après un certains nombre de pallier la spécification est tellement précise qu'elle peut être exporter dans un langage (Ada par exemple). Cette méthode a été utilisée par Matra pour construire le SI de météor, la ligne 14 automatique du métro parisien (qui n'a à ce jour jamais eu de problèmes informatique).
Pour ce qui est de Coq, c'est un assistant à la preuve, c'est à dire que c'est un logiciel qui permet de spécifier des propriétés puis de prouver qu'elles sont vrai das un contexte donné. Il se fonde sur un lambda-calcul amélioré, qu'on appelle le Calcul des Constructions Inductives : c'est une Lambda-calcul typé + constructeurs de types + types dépendants / polymorphisme + types inductifs. Avec ça, on dispose d'une expressivité consécante.
Avec Coq, on procéde donc à la spécification du logiciel et de ses propriétés que l'on prouve dans l'assistant. Une fois que les preuves sont faite, on peux réaliser l'extraction du logiciel prouvé. Ceci est quelque chose de très nouveau et Coq est le seul logiciel le proposant pour l'instant : à partir de la preuve, on génére automatiquement le code source du logiciel dans un langage cible (en général, OCaml). On obtient alors le logiciel et on a la preuve qu'il vérifie la spécification et ses propriétés. Bref, c'est beau. Aujourd'hui, Coq et l'extraction de programmes sont utilisés dans une grosse action[3] du CÉDRIC et de l'INRIA afin de certifier un compilateur pour C.
Bon, c'était un peu long, désolé...
[1] http://www.atelierb.societe.com/(...)
[2] http://coq.inria.fr/(...)
[3] http://www-sop.inria.fr/lemme/concert/(...)
[^] # Re: Des certifications CC-EALx
Posté par gael s. . Évalué à 2.
c'est mon prof d'ada à l'ecole qui disait : "quand ca y est, enfin, ca compile,
t'as pas besoin de tester, yaura pas de bug : c'est ca la difference
entre le C et l'ada"
bon ok il exagerait toujours un peu....
[^] # Re: Des certifications CC-EALx
Posté par Guillaume Knispel . Évalué à 2.
Pourquoi ca lui arrive (ou arrivait... ca fait longtemps que je suis plus allé à paris) de s'arreter pas en fasse des portes :p ?
[^] # Il bug le météore ?
Posté par theocrite (site web personnel) . Évalué à 1.
Maintenant si tu parles des quelques centimètres d'écart entre les portes du métro et celles de la stations par rapport à aux trois mètres que font les portes (à vue de nez), alors je dirais que tu es légèrement pointilleux.
Pour ceux qui ont du mal à se représenter : http://www.fersystem.com/portepaliere.jpg(...) (désolé, on ne voit pas bien, mais je n'ai pas trouvé mieux. On voit quand même le métro en vert et la "bulle" autour en verre/Metal)
¹ : Il est arrivé une fois en me rendant à gare de lyon en météore qu'un autre métro soit déjà stationné à la station. Le métro a gentillement freiné et a stationné derrière son ami transporteur. Ça a bien duré 20 minutes avant qu'il reparte.
It's not a bug, it's a feature...
[^] # Re: Des certifications CC-EALx
Posté par hermes42 . Évalué à 1.
Coq est généraliste mais il existe déjà des logiciels équivalents (commerciaux et non libres) dans des domaines plus spécialisés (je ne citerai que Scade+Prover).
[^] # Re: Des certifications CC-EALx
Posté par Matthieu Moy (site web personnel) . Évalué à 3.
PROVER, c'est un prouver automatique (c'est un moteur SAT). Le langage sous-jascent est donc forcément moins expressif. Coq, c'est tout le contraire: C'est un langage très puissant (logique d'ordre supérieur, un truc qui ressemble à CAML), mais il faut *tout* prouver à la main. En général, le premier exercice qu'on donne à un débutant en coq, c'est de prouver que 1 != 0, et il faut déjà un certain temps pour y arriver. A ma connaissance, le plus gros programme jamais prouvé en coq fait 20 000 lignes.
Enfin, en tous cas, si tu vas dire aux gens qui font SCADE (ou la version académique, Lustre) que c'est "équivalent" à coq, tu risques ne ne pas en ressortir vivant, et réciproquement ;-)
[^] # Re: Des certifications CC-EALx
Posté par hermes42 . Évalué à 1.
[^] # Re: Des certifications CC-EALx
Posté par fmaz fmaz . Évalué à 6.
Première méthode:
- T'y vas comme un barbare et tu codes.
- Tu obtiens un truc qui semble ressembler à un tri.
Deuxième méthode:
- Tu définis un algo de tri et tu prouve qu'il est correct;
- Tu codes ton algo en espérant que tu ne t'es pas planté dans tes indices.
Troisième méthode:
- Tu prends ton code et tu prouves formellement qu'il correspond à ton algo.
La deuxième méthode est prouvée semi-formellement.
[^] # Re: Des certifications CC-EALx
Posté par Guillaume Knispel . Évalué à 3.
Je préfère largement la méthode 4 :
tu prends un tri qui existe déjà depuis 30 ans et que 100 000 personnes ont relus :p (après faut trouver un moyen de savoir si 100 000 personnes l'ont bien relu ou non, mais c'est une autre question :))
[^] # Re: Des certifications CC-EALx
Posté par Foxy (site web personnel) . Évalué à 1.
C'est là où est le gros problème et que je ne comprend pas comment va faire Mandrake pour certifier le système à ce niveau.
D'après ce que je connais ces Critères Communs (de longues heures de rédaction de docs pour ma boite...), on ne peut certifier un OS à posteriori au niveau EAL5 car il faut qu'il ait été conçu avec des méthodes semi-formelles pour prouver sa sécurité.
Or le système Mandrake (kernel Linux) est déjà conçu et pas basé sur des preuves semi-formelles donc je ne vois pas comment ils pourraient atteindre ce niveau.
C'est d'ailleurs pour cela que la plupart des OS (dont Windows) atteignent seulement le niveau EAL4 (+ à la rigueur) car ils n'ont pas été conçu avec l'objectif d'atteindre le niveau EAL 5.
Le seul système EAL5 que je connaisse en France est le Fox de Thalès conçu pour les militaires.
[^] # Re: Des certifications CC-EALx
Posté par Pascal Terjan (site web personnel) . Évalué à 3.
[^] # Re: Des certifications CC-EALx
Posté par Foxy (site web personnel) . Évalué à 1.
j'avais bien compris que ce n'est pas l'ensemble du système Mandrake qui sera certifié (j'ai fait assez de CC pour ma boite pour savoir ce qu'est une "Cible de sécurité" CC et que ce n'est qu'un sous-ensemble "très réduit" d'un OS).
Mais développer un kernel basé sur Linux qui soit certifié EAL 5 me parait déjà une tâche très difficile à atteindre.
En tout cas, bon courage et je suivrais le projet de près.
# "mobiliser les ressources de la communauté du logiciel libre"
Posté par echant echant (site web personnel) . Évalué à 3.
[^] # Re: "mobiliser les ressources de la communauté du logiciel libre"
Posté par Joris Dedieu (site web personnel) . Évalué à 3.
il sagit de travailler pour l'armée gratuitement.
Tout les chercheurs, travaillent pour l'armée. Elle a un droit de regard absolue sur tout ce qui est publié. Elle peut très bien bloquer une publication et la classer secret défense. Sans tomber dans l'espionnite aiguë, tu peux te dire qu'un ?il discret surveille tout ce qui se passe dans les labos. C'est comme ça en France. Ce n'est évidement pas mieux ailleurs. Grothendieck a arrêté les Maths pour cette raison.
[^] # Re: "mobiliser les ressources de la communauté du logiciel libre"
Posté par echant echant (site web personnel) . Évalué à 0.
Là l'armée est le client, il devrait être assez facile de tracer les projets informatiques découlant de sa commande auprès de MandrakeSoft. J'aimerais bien que les bénévoles sachent qu'ils travaillent en grande partie pour l'armée française et que l'argent va dans la poche des possesseurs de MandrakeSoft.
Gageons que nous allons voir sortir une distribution "Madrake/secure", avec un appel de MandrakeSoft genre "Venez partager avec nous une expérience formidable de développement d'une nouvelle distribution ...".
[^] # Re: "mobiliser les ressources de la communauté du logiciel libre"
Posté par thecat . Évalué à 1.
Tu aurrait une URL sur ca ou sur ce qui à motivé son arret des maths ? (ca m'interresse pas mal perso ...)
[^] # Re: "mobiliser les ressources de la communauté du logiciel libre"
Posté par Joris Dedieu (site web personnel) . Évalué à 4.
Tu aurait une URL sur ça ou sur ce qui à motivé son arrêt des maths ? (ça m'interresse pas mal perso ...)
Quelques infos générales sur Grothendieck pour ceux que sa interesse :
http://www.bibmath.net/bios/index.php3?action=affiche&quoi=grot(...)
Sur sa fin, je n'ai pas d'URL. Je ne peux que raconter ce que je sais par ouïe dire. C'est à dire par mes parents (des matheux) qui l'ont connue sur la fin lorsqu'il est allé se perdre à la fac de Montpellier.
Grothendieck outre son génie, à toujours été malade de ses souffrances de guerre.
Ainsi il a toujours été engagé, voire enragé. A tel point que dans les années 70 il ne pouvait plus encadrer personne. Et même si les fac les plus prestigieuses l'enviaient, il a décidé de repartir à Montpellier (ville dans laquelle il avait fait une partie de ses études).
Cela correspond à son réel pétage de plomb (il faisait marcher ses étudiants pied nu). Puis peu après il a déclaré que si on ne lui garantissait pas , par changement de la loi que son travail ne servirait jamais au militaires, il arrêterai les maths. Il a arrêté.
Voilà c'est tout ce que je sais sur la question.
[^] # Re: "mobiliser les ressources de la communauté du logiciel libre"
Posté par renoo . Évalué à 2.
http://www.lacitoyennete.com/magazine/retro/grothendiecka.php(...) éclaire à ce sujet.
[^] # Re: "mobiliser les ressources de la communauté du logiciel libre"
Posté par patrick_g (site web personnel) . Évalué à 3.
en crypto peut-être ?
de toute façon une éventuelle découverte applicable en crypto et effectuée par Grothendiek aurait été publié et donc le monde entier aurait été au courant.
je crois plutot que ce brave homme est devenu un peu fou et parano et qu'il abandonné les maths au moment ou sa créativité extraordinaire a commencé à disparaitre.
j'avais lu qu'actuellement il est complètement à la masse (il croit que si la vitesse de la lumière n'est pas exactement égale à 300.000 km/s c'est un coup du diable).
[^] # Re: "mobiliser les ressources de la communauté du logiciel libre"
Posté par Yhar Gla . Évalué à 4.
source : http://www.20minutes.fr/journal/recherche/pop_article.php?ida=30570(...)
Extrait :
"Argument de poids dans le dossier de candidature : le nombre de bénévoles mobilisables. La région évoque les 600 000 lycéens et apprentis, mais aussi les 2,2 millions de licenciés en Ile-de-France."
On comprends mieux la vieille rengaine "l'important c'est de participer".
[^] # Re: "mobiliser les ressources de la communauté du logiciel libre"
Posté par syntaxerror . Évalué à 5.
Je me souviens que dans ma boite pour les jeux d'Albertville en 92 et les jeux
Méditerranéens en 93, plein de pigeons ont été incités à prendre des congés
pour aller jouer les bénévoles. Et ils n'ont même rien vu des jeux, occupés à faire la circulation dans les parkings...
[^] # Re: "mobiliser les ressources de la communauté du logiciel libre"
Posté par Yhar Gla . Évalué à 2.
> à prendre des congés pour aller jouer les bénévoles
Tu bosses dans une boîte liée au sport?
> Et ils n'ont même rien vu des jeux, occupés à faire la circulation dans les parkings...
Ah je pensais que les pigeons avaient au moins le droit d'assister à un quelconque éliminatoire de curling... Ils n'ont pas même eu une casquette ou un pin's officiel (r) (tm) (c) ?
[^] # Re: "mobiliser les ressources de la communauté du logiciel libre"
Posté par Le_Maudit Aime . Évalué à 3.
# 1 Million ça fait pas lourd quand on y pense !
Posté par xavier philippon . Évalué à 1.
Cela dit, que Mdk travaille pour l'armée française ne me perturbe pas outre mesure.
# And the winner is ...
Posté par itstimetogo . Évalué à -1.
Mandrake
Ça donne à Mandrake un quasi monopole sur tous les contrats publics en Europe. Normal, c'est la même chose de "l'autre côté".
Fanclub et contrats publics sont les deux mamelles de Mandrake. Espérons que l'argent sera investit dans autre chose que "supermount 2 : Le Retour".
# Mandrake n'est pas seul
Posté par jeff110 . Évalué à 2.
--> http://www.01net.com/article/251625.html(...)
L'article fait mention de plusieurs société, mais sans toutes les citer.
Il précise également que W2k aurait obtenu un niveau de certification 4 (mode Troll activé... ) alors que le monde GNU/Linux n'aurait pas depassé 3 et 2 pour Solaris8.
Le niveau de securité 5 n'aurait jamais était atteind.
[^] # Re: Mandrake n'est pas seul
Posté par Ayrton . Évalué à 1.
Je suis septique sur les avantages que MandrakeSoft peut tirer de cette news (hors avantage pécunier).
Linux n'a pas dépassé le niveau 3 mais Red Hat a un OS qui a le niveau pour l'armée américain (ce n'est pas EAL, c'est autre chose).
En 2005, ça va être la déferlante SELinux "out of the box".
Que va proposer ce projet de plus qu'une Red Hat ou SuSE SELinux ?
Probablement rien. Ceux qui auront investi 7 millions d'Euro apprécirons en voyant la même chose "sur étagère" à 1 000 ou 400 voire 0 $
[^] # Re: Mandrake n'est pas seul
Posté par Joris Dedieu (site web personnel) . Évalué à 5.
je crois qu'il ne faut pas oublier qu'on part ici sur quelque chose de totallement different, dans sa conception même.
Il est probable que cet OS integrera SElinux. Ceci dit sa caracteristique fondamentale semble surtout être la virtualisation. Ce qui me semble-t-il, pour du Linux serait une vrai nouveauté, certe déjà dans les starting blocs mais enfin encore virtuelle (je pense à UML qui est surtout destiné au débugage du noyau, je pense également à plusieurs journaux que j'ai lu ici).
Enfin la nouveauté principale réside dans le choix d'une methode semi-formelle, ce qui ne changera peut-être pas grand chose au résultat final, si ce n'est (si j'ai bien compris ce qui ce disait plus haut) : une absence de bugs mathematiquement prouvée. Ça aussi c'est nouveau.
l'article du Monde :
http://www.weblmi.com/news_store/2004_09_24_MandrakeSoft_partici_2/(...)
[^] # Re: Mandrake n'est pas seul
Posté par Ayrton . Évalué à 1.
SELinux est une surcouche du *modèle* de sécurité classique Unix.
Ce n'est pas "limité à". Vu la souplesse/puissance d'SELinux (très difficile à aborder d'ailleurs) j'ai du mal à imaginer que SELinux "limite" le niveau de sécurité.
Par contre, SELinux ne s'occupe pas d'authentification, pare-feu, etc... Il fixe les règles d'accès (une foi que tu es authentifié, etc).
> la virtualisation. Ce qui me semble-t-il, pour du Linux serait une vrai nouveauté
> je pense à UML qui est surtout destiné au débugage du noyau
La virtualisation est déjà beaucoup utilisé. Comme marche les mainframes à ton avis ?
> une absence de bugs mathematiquement prouvée. Ça aussi c'est nouveau.
S'ils y arrivent pour un système aussi complexe, alors chapeau bas.
Red Hat certifié pour l'armée américain :
http://www.redhat.com/solutions/industries/government/coe/(...)
[^] # Re: Mandrake n'est pas seul
Posté par tgl . Évalué à 4.
Ne nous emballons pas.
Autant que je me souvienne (mais je jurerais pas non plus et j'ai super la flemme de remettre le nez dans les CC), en EAL5, il n'y a pas encore de "preuve de l'absence de bug" (càd de vérification formelle du code). C'est au niveau du design que se situe l'utilisation de méthodes (semi-)formelles, et ce qui est démontré c'est que la description super détaillée du design de bas niveau colle bien avec celle super détaillée aussi de plus haut niveau, qui elle colle bien avec les spécifications fonctionnelles super détaillées aussi et avec le modèle formel de sécurité qu'on a décidé d'implémenter. En gros, on s'assure avec un très fort degré de confiance que tout ce qui est prévu est bien pensé et bien fichu.
Par là dessus, l'implémentation elle est soumise à des tests très systématiques, ce qui n'est possible que grâce à tous nos super-détails énumérés ci-dessus. À ce niveau, on parle de test (semi-)formel, parcequ'ils ne sont pas juste fait suivant l'inspiration du programmeur mais peuvent être vraiment dérivés méthodiquement de la spec de chaque composant de bas niveau.
Mais la vérification du code (ou sa génération à partir du modèle prouvé, comme en B ou en Coq), c'est plutôt aux niveaux EAL6 et 7 que ça se fait vraiment. Et là, on est pas près de rencontrer un système de ce niveau de complexité amha.
[^] # Re: Mandrake n'est pas seul
Posté par Benoît Sibaud (site web personnel) . Évalué à 4.
Huh ?
« Solaris 8 et IRIX 6.5.13 ont ainsi atteint le niveau 3. Tandis qu'AIX 5L, HP-UX 11i et Windows 2000 avec le service pack 3 sont, eux, crédités d'un EAL 4. Les systèmes d'exploitation issus de Linux atteignent des niveaux proches. Red Hat Enterprise Linux 3 est EAL 2, tandis que Suse Linux Enterprise Server V8 a obtenu l'EAL 3. »
[^] # Re: Mandrake n'est pas seul
Posté par jeff110 . Évalué à 2.
Merci de le faire remarquer.
# Foutaises !
Posté par TSelek . Évalué à -1.
- ne pas oublier le Protection Profile, le périmetre quoi. on ne certifie pas tout, par exemple dans le cas MS c'est uniquement le login local qui est EAL4, le reste de l'OS c'est la daube habituelle non certifiable (la blague a ses limites...)
- EAL5 dit introduction de méthodes semi-formelles, hum hum c'est pas vraiment compatible avec MDK (non, ce n'est pas un troll). en plus on considère que EAL4 est le dernier niveau que l'on peut passer après implémentation, faire de l'EAL5 sur de l'existant, no way !
donc EAL5, oui mais sur quoi au juste ? pourquoi on ne parle pas du PP ou de la security target ? sur Linux ? mwawawawa.... je ris jaune.
MDK vient de s'incruster dans un projet européen qui lui permettra de payer 2 ou 3 gars pendant 3 ou 4 ans, et puis plouf le super projet...
bah ça sera pas les premiers à bénéficier de ce genre de subventions cachées, très bien MDK, la microsoftisation continue...
[^] # Re: Foutaises !
Posté par Pascal Terjan (site web personnel) . Évalué à 4.
Il y aura un noyau sur, avec Linux qui tourne par dessus, comme le fait déjà Jaluna pour fournir du temps réél.
[^] # Re: Foutaises !
Posté par TSelek . Évalué à 1.
Pour avoir bossé sur du NF/FIPS/CC..., je sais pertinement que EAL5 n'est pas un objectif réalisable en si peu de temps, en partant de rien. Ici ça fait quelques années qu'on est sur des EAL5/6/7 et rien n'est encore sorti de la R&D pure...
D'expérience, je peux te dire que tout le monde sous-évalue la lourdeur des CC... et les EAL>4 sont plutôt dans le domaine expérimental que production.
D'ailleurs tu n'as toujours pas donné de PP en réf...
enfin bon, pourvu que je me trompe.
Suivre le flux des commentaires
Note : les commentaires appartiennent à celles et ceux qui les ont postés. Nous n’en sommes pas responsables.