Marre des argumentaires s?curit?s (et techniques) pour le LL was Re: [Linux-bruxelles] bug de s?curit?: kernel 2.4.25-ovh (marre de linux)
Nicolas =?unknown-8bit?Q?=C3=89vrard?=
nicoe at altern.org
Jeu 1 Avr 15:45:11 CEST 2004
* Alexandre Dulaunoy [13:57 01/04/04 CEST]:
>On Thu, 1 Apr 2004, Nicolas [unknown-8bit] ?^Ivrard wrote:
>
>> * Alexandre Dulaunoy [10:20 01/04/04 CEST]:
>>
>> >C'est impossible (enfin presque[1]) d'avoir du logiciel sans bugs ou
>> >sans failles de s?curit?. Le logiciel (par essence) est bourr?
>> >d'erreurs visibles ou non.
>>
>> Notons qu'il y a des th?ories math?matique qui permettent de prouver
>> qu'un logiciel est juste et donc sans bug. C'est d'ailleurs une des
>> applications du lambda-calcul. Il est donc tout ? fait possible d'avoir
>> des logiciels sans bug, il faut "juste" passer beaucoup de temps ?
>> prouver que le logiciel l'est. Certains langages simplifient cette t?che
>> mais ils sont assez peu r?pandu.
>
>[On s'?loigne de la dichotomie logiciel libre / logiciel propri?taire
>- s?curit? mais bon nous sommes le 1er avril ;-)]
C'est un peu comme un vendredi qui tomberai plus tôt.
>Tiens, c'est marrant, je ne croyais pas trouver des fans de la
>formalisation dans cette liste ;-)
Bah, quand on aime le scheme on se doit de savoir d'où viennent tout ces
lambda qui trainent partout. Et en plus on en parle dans les cours qu'il
faut bien étudier ... Ce que j'en ai retenu se résume en ces quelques
points:
- le lambda calcul a la même expressivité que la machine de Turing
- c'est un concept amusant
- mais c'est chiant comme jamais, jouer avec dans un esprit
mathématique pourquoi pas mais c'est trop long. J'ai des souvenirs
de preuve de programme triviaux trop longues.
Comme on le voit, ça date un peu ...
>Il est vrai que le Lambda Calculus est une approche de formalisation
>pour d?crire la d?finition d'une fonction math?matique et ces petits
>corollaires[1].
Petits corollaires qui sont à mon avis (pas très objectif) assez grands.
Les langages fonctionnels sont assez souvent mal vus mais c'est plus à
cause d'une paresse des étudiants qui les apprenent qu'à cause de leurs
hypothétiques défauts.
Je veux pour preuve le prédicat "do" introduit dans le scheme.
L'immense majorité des personnes qui l'ont étudié avec moi l'ont utilisé
sans vergogne dès qu'ils en ont eu l'occasion, malgrè le fait que c'est:
- visiblement contraire au principe de la programmation
fonctionnelle
- inutile puisque la tail-recursion est plus efficace.
>Cette approche de formalisation fonctionne aussi pour
>les protocoles de s?curit? avec notre ami CSP.
Mmm, j'ai vu les ingés jouer avec ... mais je ne l'ai jamais approché
moi-même. C'est un tord.
>Cela r?alise des mod?les parfaits dans un domaine neutre ou cadr?
>avec pas ou tr?s peu d'int?ractions entre d'autres mod?les parfaits.
>Mais il y a plusieurs point qui sont n?glig?s (mais aussi tr?s
>amusants) :
>
>- La qualit? d'un gateau n'est pas uniquement pas la qualit? du sucre
> utilis?. Prendre un sous-ensemble, le rendre parfait ne change rien
> par rapport ? un cuisinier qui laisse le gateau trop longtemps dans
> le four.
Évidemment mais une fois que l'on sait que le gateau est parfait, on
sait déjà que ce n'est plus là qu'il faut chercher.
Mauvais cuisinier ? Changer cuisinier !
>- Certaines th?ories de formalisation essayent de mettre le pied (ou
> les pieds) dans l'impl?mentation. Par exemple, on place le syst?me
> d?crit dans une machine virtuelle qui aussi respecte le
> formalisme. On vous dit, pas de probl?mes. Si on imagine le plat
> pour le gateau (ou m?me le four) mais qu'une inondation arrive dans
> la cuisine alors ce n'est plus de la faute de la formalisation. (Il
> existe un bel exemple d'une machine XXXX[1] pour un algorithme
> cryptographique mais qui prenait l'entropie au-del? de la machine
> virtuelle sans contr?le...)
J'aimerai vraiment avoir cette XXXXm juste pour voir une fois. Je me
demande si les gains qu'elles apportent à la programmation en XXXX sont
si conséquent que ça.
>Ce 1er avril, on peut tenter de d?gager une r?gle "La s?curit? d'un
>syst?me d?pend du milieu o? il est plong?".
>Je savais que ce jeudi sera une mauvaise journ?e,
Mais non, il fait beau dehors !
>[1] J'essaye (mais c'est difficile ((vraiment)(tr?s) difficile) de ne
>pas parler Lisp).
:)
De toute façon tout le monde parle Lisp (surtout s'il est allemand).
Relisons Chomsky (sa linguistique et aussi ses trucs politiques) qui
montre que finallement "recurser"[1] c'est peut-être plus humain que ce
que l'on croit.
[1] : Quelqu'un se rappelle qui a dit "To iterate is human, to recurse,
divine".
--
(°> Nicolas Évrard
/ ) Liège - Belgique
^^
Plus d'informations sur la liste de diffusion Linux-bruxelles