Journal : Qu'est-ce qu'un langage sécurisé ?
Posté par Nicolas Boulay () le 11 novembre 2007
0
Je me pose une question méta physique ce soir.Qu'est-ce qu'un langage sécurisé ?
En général, lorsque l'on voit ce terme, Java n'est pas loin. Mais il est plus souvent question de JVM que du langage lui-même.
La jvm controle le champ d'execution d'un programme pour empécher d'aller faire des choses non autorisé : accéder directement à certaine fonctions, injecter du code, executer du code non prévus en injectant des paramètres, accéder à des IOs interdite, accéder directement à la mémoire, etc...
Mais du point de vue du Langage ? J'imagine qu'il doit absolument pouvoir éviter les horreurs du C comme les buffers overflow. Mais est-ce que tous langages avec allocation automatique de mémoire serait protégés ?
La plus part des attaques du C sont basé sur ce problème : le retour dans la libc, l'injection de code dans la pile, etc... Par contre, les bug de printf avec "%n", est plus un problème de non controle de paramètres par le C.
On peut aussi bannir les pointeurs qui permètent de casser la ségmentation des données (au profit des références).
On peut aussi ajouter toutes les fonctionnalités qui empèchent les bugs et assurent plus facilement que le code soit correct.
Mais est-ce suffisant ? Y'a t -il d'autres paramètres à prendre en compte ?
> Lire le journal (85 commentaires, moyenne: 2,7).
Vous avez demandé le commentaire #883590.
Run by 
Cette page a été générée par Templeet en 0.05s (dont 0.0051 de SQL).
Cette page est peut-être conforme xhtml 1.0.
Information sur le site.
Faire un don !
Les langages sécurisés ca existe !
Le langage le plus sécurisé que je connaisse c'est Coq [1]. Je cite :
"Coq est un système de manipulation de preuves mathématiques formelles; une preuve réalisée avec Coq est mécaniquement vérifiée par la machine"
" Coq intègre aussi [...] un mécanisme d'extraction [qui] permet d'engendrer automatiquement des programmes certifiés en Objective Caml, Haskell ou Scheme à partir de preuves de leurs spécifications."
Niveau sécurité c'est béton, vôtre programme fait exactement ce qu'il est censé faire, vous l'avez prouvé.
Si vous trouvez cette approche trop violente, vous pouvez regarder du coté de Conqoction [2]. Concoqtion est une extention de MetaOCaml qui est elle même une extension d'Objective Caml. Elle permet d'avoir un système de type très riche appelé types indexées. Par exemple vous pouvez indexer le type des listes par le nombre d'élements dans une liste, ainsi vous pouvez spécifier une fonction sur des listes non vides, des listes qui ont un nombre pair d'élements, ect ...
La vérification des types est fait par inférence autant que possible et par des preuves que vous pouvez faire en Coq.
Il est certes plus complexe de programmer dans ces langages que de pisser du code en priant pour que ca ne merde pas mais la sécurité est bien souvent à ce prix.
[1] http://coq.inria.fr/coq-fra.html
[2] http://www.metaocaml.org/concoqtion/
[^]Re: Les langages sécurisés ca existe !
Ouais, enfin des types indexés, ca se fait à la main avec des "types phantomes"... (du moins dans le cas que tu cites)
J'utilise ça même assez souvent, tant en Haskell qu'en Caml...
J'aime la liberté.
J'aime BSD.
[^]Re: Les langages sécurisés ca existe !
Pas du tout, et même pas dans le cas que je cite. Un type de liste indexé par un entier n'est pas un type liste indexé par le type entier (int) mais par des valeurs de type entier. C'est a dire que la liste vide est de type "('a,0) list" et que le constructeur "::" est de type "'a -> ('a,n) list -> ('a, (n+1)) list". Et oui le "n" est bien une *avleur* entière qui dit que la liste est de taile "n".
Ceci est impossible à faire en OCaml ou Haskell, c'est bien pour ca que des gens développent Concoqtion, Cayenne, Epigram, Twelf, etc .... Si c'était si trvial je pense pas que tant de gens se ferait chier pour rien.