Il est impossible de prouver une propriété en faisant de l'analyse statique pour la bonne et simple raison qu'il est impossible pour un programme de vérifier tous les cas. C'est un truc que tu vois dans les 20 premières minutes d'un cours sur l'analyse statique. La seule solution pour prouver le bon fonctionnement d'un programme en un temps raisonnable, c'est de générer des tonnes de faux négatifs. Ça revient à demander à un compilateur de générer des patterns de code. Pourquoi pas, mais c'est documenté? Quid de la vitesse d'exécution?
Un exemple, tu peux vérifier que les appels systèmes sont bien les bons et appelés seulement avec une adresse immédiate (miam le cassage de programmes existants).
Mais au final, c'est quoi un appel système dans un OS comme ça? Ça existe pas, c'est plus un espèce de gros tas qui prétend être tenu en place par de l'analyse statique de tous les cotés.
2) Si tu crois que C# se limite a débordements de tampons c'est que tu n'as rien compris a C# et encore moins a Singularity.
Ensuite si tu es assez naif pour croire que les problemes de gestion de tampon se reglent avec une API quelconque c'est que tu n'as rien compris a la programmation...
Si tu veux vraiment éviter les buffers overflows, il faut contrôler la création de buffers puis tous les accès subséquents. La seule façon crédible de faire ça et vérifier à l'exécution et la seule façon de vérifier et de faire des processeurs qui soient au courant de la taille de ton "buffer".
Ça a déjà été "fait": http://www.cc.gatech.edu/~idoud/documents/TAINTTC.pdf
Maintenant explique moi comment fait .net pour empêcher les buffers overflow alors? C'est de la programmation orientée objet, et une vérification à la compilation à moins que .net interprète ton code.
Et je me répète, mais y'a pas que les processus qui font des accès mémoire, le matériel aussi. Et le matériel peut être programmé pour faire un accès mémoire qui va modifier les bits que tu veux au bon endroit même si la page mémoire est marquée comme ro (et oui).
3) De nouveau, tu n'as rien compris, un gestionnaire de paquets depot/app store n'a rien a voir avec la problematique en jeu, ces manifestes c'est pas une histoire de dependance ou securite sur le paquet lui-meme
Mais oui, je comprend rien, regarde plutôt ça:
Singularity’s third unique architectural feature, called "manifest-based programs," represents another shift in orientation. Traditionally, operating systems have had no "knowledge" of a program’s composition, its purpose, or the resources it uses. Presented with a set of bits, the operating system would simply run them. Singularity, with its emphasis on overall system dependability, takes a different approach to ensure that a new program won’t "break" the programs already on board.
Comment ils font? 2 choix, soit le manifest décrit le fonctionnement du programme de façon formelle de façon à ce que le kernel puisse voir si c'est normal ou pas.
Soit le manifest ne contient que des informations de plus haut niveau qui permettent à l'OS de choisir de l'exécuter ou pas.
Dans le 2ème cas, le kernel devrait vérifier que le manifest soit pas bidonné, donc, il faut utiliser l'analyseur statique pour vérifier le code.
J'aime l'idée du manifest qui indique les besoins d'un programme, c'est une très bonne chose. Mais c'est pas au kernel de vérifier ça! C'est à un dépôt de vérifier ça puis de livrer les applications à l'utilisateur signées par le dépôt.
Alors, c'est qui qui a rien compris?
Quand à l'arrogance, je te retourne le compliment. Pourquoi la recherche sur la sécurité mémoire ne s'est pas arrêtée lors de l'arrivée de .net et C#? Oh, mais que je suis bête, c'est simplement parce que C# ne résout rien...
De toute façon, C# ne peut être meilleur que la virtualisation ... qui n'est pas de la sécurité.
Je le répète, je suis à l'aise avec ce sujet car j'ai fais mon mémoire de master sur la gestion d'accès aux pages mémoires, j'ai étudié la sécurité durant 3 ans (spécialité mobilité et virtualisation) et je débute dans l'écriture de driver (je bosse sur Nouveau, le driver libre nvidia). Tu fais quoi toi pour me traiter d'incapable?
Et puis si encore j'étais le seul: http://www.ok-labs.com/blog/entry/about-security-singularity-vs-l4-part-2/ Et j'ai passé 10s sur google pour le trouver.
Je ne traite pas Microsoft d'idiots, juste de personnes qui pensent avec le porte monnaie. Dire qu'ils travaillent sur un OS sécurisé, c'est dire on essaye de faire mieux, ça rassure et donc, ça rapporte à plus ou moins long terme.
[^] # Re: Bonne interview
Posté par Martin Peres (site web personnel) . En réponse à la dépêche Linus Torvalds : l’interview anniversaire des 20 ans du noyau. Évalué à 1.
Il est impossible de prouver une propriété en faisant de l'analyse statique pour la bonne et simple raison qu'il est impossible pour un programme de vérifier tous les cas. C'est un truc que tu vois dans les 20 premières minutes d'un cours sur l'analyse statique. La seule solution pour prouver le bon fonctionnement d'un programme en un temps raisonnable, c'est de générer des tonnes de faux négatifs. Ça revient à demander à un compilateur de générer des patterns de code. Pourquoi pas, mais c'est documenté? Quid de la vitesse d'exécution?
Un exemple, tu peux vérifier que les appels systèmes sont bien les bons et appelés seulement avec une adresse immédiate (miam le cassage de programmes existants).
Mais au final, c'est quoi un appel système dans un OS comme ça? Ça existe pas, c'est plus un espèce de gros tas qui prétend être tenu en place par de l'analyse statique de tous les cotés.
Tu lis vraiment ce que tu veux lire. C'est le seul intérêt de C# citée dans http://research.microsoft.com/en-us/news/features/singularity.aspx . Je m'arrête donc là.
Si tu veux vraiment éviter les buffers overflows, il faut contrôler la création de buffers puis tous les accès subséquents. La seule façon crédible de faire ça et vérifier à l'exécution et la seule façon de vérifier et de faire des processeurs qui soient au courant de la taille de ton "buffer".
Ça a déjà été "fait": http://www.cc.gatech.edu/~idoud/documents/TAINTTC.pdf
Maintenant explique moi comment fait .net pour empêcher les buffers overflow alors? C'est de la programmation orientée objet, et une vérification à la compilation à moins que .net interprète ton code.
Et je me répète, mais y'a pas que les processus qui font des accès mémoire, le matériel aussi. Et le matériel peut être programmé pour faire un accès mémoire qui va modifier les bits que tu veux au bon endroit même si la page mémoire est marquée comme ro (et oui).
Mais oui, je comprend rien, regarde plutôt ça:
Comment ils font? 2 choix, soit le manifest décrit le fonctionnement du programme de façon formelle de façon à ce que le kernel puisse voir si c'est normal ou pas.
Soit le manifest ne contient que des informations de plus haut niveau qui permettent à l'OS de choisir de l'exécuter ou pas.
Dans le 2ème cas, le kernel devrait vérifier que le manifest soit pas bidonné, donc, il faut utiliser l'analyseur statique pour vérifier le code.
J'aime l'idée du manifest qui indique les besoins d'un programme, c'est une très bonne chose. Mais c'est pas au kernel de vérifier ça! C'est à un dépôt de vérifier ça puis de livrer les applications à l'utilisateur signées par le dépôt.
Alors, c'est qui qui a rien compris?
Quand à l'arrogance, je te retourne le compliment. Pourquoi la recherche sur la sécurité mémoire ne s'est pas arrêtée lors de l'arrivée de .net et C#? Oh, mais que je suis bête, c'est simplement parce que C# ne résout rien...
De toute façon, C# ne peut être meilleur que la virtualisation ... qui n'est pas de la sécurité.
Je le répète, je suis à l'aise avec ce sujet car j'ai fais mon mémoire de master sur la gestion d'accès aux pages mémoires, j'ai étudié la sécurité durant 3 ans (spécialité mobilité et virtualisation) et je débute dans l'écriture de driver (je bosse sur Nouveau, le driver libre nvidia). Tu fais quoi toi pour me traiter d'incapable?
Et puis si encore j'étais le seul: http://www.ok-labs.com/blog/entry/about-security-singularity-vs-l4-part-2/ Et j'ai passé 10s sur google pour le trouver.
Je ne traite pas Microsoft d'idiots, juste de personnes qui pensent avec le porte monnaie. Dire qu'ils travaillent sur un OS sécurisé, c'est dire on essaye de faire mieux, ça rassure et donc, ça rapporte à plus ou moins long terme.