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)

[Alexandre Dulaunoy]

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 ;-)]

Tiens,  c'est  marrant, je  ne  croyais pas  trouver  des  fans de  la
formalisation dans cette liste ;-)  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]. Cette approche de
formalisation fonctionne  aussi pour  les protocoles de  sécurité avec
notre  ami CSP.  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.

- 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...)

- La formalisation  c'est bien mais  sans plus. Le plus  marrant c'est
  les modèles  des attaquants comme  si on avait  un modèle :  le plus
  beau, le plus méchant, le plus rigolo, ....

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,

adulau

[1] J'essaye (mais c'est  difficile ((vraiment)(très) difficile) de ne
pas parler Lisp).

>
> PS: Il y a un troll caché dans ce message, saurez vous le découvrir ?
>
>

[Bien entendu, la validité de  ce courrier est uniquement du 1er avril
au 1er avril]

-- 
** Alexandre Dulaunoy (adulau) **** http://www.foo.be/ **** 0x44E6CBCD
**/ "To  disable the  Internet to  save EMI  and Disney  is  the moral
**/ equivalent of burning down the library of Alexandria to ensure the
**/ livelihood of monastic scribes." Jon Ippolito.