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