Cours MIT "Sécurité des systèmes informatiques". Conférence 11: Langage de programmation Ur / Web, partie 2

Institut de technologie du Massachusetts. Cours magistral # 6.858. "Sécurité des systèmes informatiques." Nikolai Zeldovich, James Mickens. 2014 année

Computer Systems Security est un cours sur le développement et la mise en œuvre de systèmes informatiques sécurisés. Les conférences couvrent les modèles de menace, les attaques qui compromettent la sécurité et les techniques de sécurité basées sur des travaux scientifiques récents. Les sujets incluent la sécurité du système d'exploitation (OS), les fonctionnalités, la gestion du flux d'informations, la sécurité des langues, les protocoles réseau, la sécurité matérielle et la sécurité des applications Web.

Cours 1: «Introduction: modèles de menace» Partie 1 / Partie 2 / Partie 3
Conférence 2: «Contrôle des attaques de pirates» Partie 1 / Partie 2 / Partie 3
Conférence 3: «Débordements de tampon: exploits et protection» Partie 1 / Partie 2 / Partie 3
Conférence 4: «Séparation des privilèges» Partie 1 / Partie 2 / Partie 3
Conférence 5: «D'où viennent les systèmes de sécurité?» Partie 1 / Partie 2
Conférence 6: «Opportunités» Partie 1 / Partie 2 / Partie 3
Conférence 7: «Native Client Sandbox» Partie 1 / Partie 2 / Partie 3
Conférence 8: «Modèle de sécurité réseau» Partie 1 / Partie 2 / Partie 3
Conférence 9: «Sécurité des applications Web», partie 1 / partie 2 / partie 3
Conférence 10: «Exécution symbolique» Partie 1 / Partie 2 / Partie 3
Conférence 11: «Ur / Web Programming Language» Partie 1 / Partie 2 / Partie 3

Un peu plus tard, je vous parlerai de fausses demandes intersites. Je pense que les notes de cours expliquent pourquoi les scripts crossite ne fonctionnent pas dans notre cas. La raison en est que chaque fois que vous créez un «morceau» de syntaxe, cet objet, cet arbre et les différentes parties de cet arbre ne sont pas uniquement des chaînes.



Vous ne pouvez pas accidentellement transformer une chaîne utilisateur en une arborescence de structure, cela ne se produit pas automatiquement, car il est difficile d'écrire un tel traducteur. Mais vous pouvez essayer d'écrire un traducteur pour Ur / Web. Je donnerai bientôt un exemple qui contribuera à réduire votre inquiétude à ce sujet. Je veux vous montrer en quoi cette syntaxe se transforme réellement dans le compilateur.

Il pourrait sembler que nous pourrions simplement ajouter des guillemets doubles autour du HTML afin que nous puissions ensuite revenir au monde normal. On peut se demander pourquoi il est si important de sauter les guillemets doubles, en plaçant XML à la place?

Vous pouvez me croire sur parole que c'est le code équivalent pour ce qu'il fait. Voici une balise de fonction en ligne qui crée le nœud d'arbre d'un document HTML. Ensuite, je place les arguments qui expriment le style CSS dans ce nœud. Rien ne se passe réellement ici, il existe donc de nombreuses façons de dire «Aucun», cela ne nécessite aucun attribut.

Ensuite, je mets la balise body, c'est une autre chose de la bibliothèque standard. Toutes les balises standard sont des fonctions de première classe dans la bibliothèque.



Ensuite, nous devons mettre le texte «Hello World» dans le corps, nous appelons donc la fonction cdata, où cdata est le mot XML pour les données de caractères ou simplement une constante de chaîne, et nous pouvons placer le texte ici. Cela devrait nous donner le même résultat qu'auparavant. Voyons voir si cela fonctionne.

Je reviens maintenant à la page. Nous voyons la même chose qu'avant, c'est donc la même chose que la fonction au début.



Ce n'est pas seulement la construction de lignes. Cela provoque une série d'opérations qui sont conçues de manière à ce qu'elles seules vous permettent de créer du code HTML valide, et elles ne pourront jamais interpréter implicitement la ligne comme du code au lieu de simplement placer le contenu qui devrait être là sur la page.



Maintenant, je vais essayer de faire quelque chose de moins compliqué, ce qui pourrait potentiellement être un problème. Décidons que nous sommes vraiment heureux de voir le monde, nous mettons donc en évidence le mot "bonjour" en gras et le compilons à nouveau.



Vous voyez ce qui s'est passé sur la page - le mot n'est pas devenu gras car le compilateur montre comment le texte est interprété au lieu du balisage. Il s'agit d'une représentation de la syntaxe HTML en tant que fonction qui construit la syntaxe sans les conventions de codage habituelles qui y sont intégrées. Cette fonction interprète tout comme vous vouliez écrire, sans penser à vous-même.

Ainsi, l'implémentation de cdata fait ce qui est communément appelé échapper ou "échapper". Mais le programmeur n'a pas besoin de savoir qu'il existe une telle chose que de s'échapper. Vous pouvez le considérer comme un ensemble de fonctions pratiques pour créer une arborescence d'objets qui décrit la page.

J'entends que vous voulez voir le code HTML généré ici. D'accord, ce ne sera pas la chose la plus excitante. J'essaierai de l'agrandir sur l'écran, mais ensuite il ne rentre pas sur une seule ligne.



Étudiant: Étant donné que vous utilisez XHTML, pourriez-vous simplement utiliser le chemin d'accès aux données de caractères cdata au lieu de le faire manuellement?

Professeur: Je suppose, mais cela nécessiterait plus de XML de ma part que ceux que j'ai. Il y avait une autre bonne question sur les URL JavaScript. Si nous autorisons les URL JavaScript, nous créons une porte dérobée pour interpréter automatiquement les chaînes comme des programmes au moment de l'exécution. Et cela cause toutes sortes de problèmes.

Essayons de l'éviter. Je reviens tout d'abord à la version raccourcie et fais quelques lignes à l'intérieur du corps. Et mettons un lien qui va essayer de faire quelque chose de approprié. Ici, nous laissons de la place aux messages d'erreur.



Ensuite, exécutez le compilateur et voyez comment cela fonctionne.



URL non valide, puis entrée JavaScript et la phrase «passé pour bénir» ou «bénédiction passée». Bless est intégré à la fonction, qui est le contrôleur d'accès qui résout l'URL. Par défaut, les URL ne sont pas autorisées, donc bien sûr cette option n'est pas autorisée. En général, c'est une mauvaise idée d'écrire votre propre stratégie d'URL afin de pouvoir créer des valeurs qui représentent des URL JavaScript. Parce qu'alors toutes sortes de garanties seront nécessaires, car ces adresses peuvent être invalides.

Pour rendre un peu plus clair comment cela fonctionne, permettez-moi de décomposer ce code dans une fonction distincte qui appelle l'éditeur de liens qui accepte l'URL. Ainsi, une URL est un type, pas une chaîne. Il s'agit du type qui désigne l'URL, ce qui est explicitement autorisé par la stratégie de votre application.

J'utilise des accolades, comme dans certains cadres de modèles HTML populaires, pour indiquer l'insertion de code du langage hôte à l'intérieur du HTML que nous créons. Et tout cela se fait de telle sorte que le type soit vérifié statiquement. Le système vérifiera donc: "oui, c'est l'endroit auquel appartient l'URL, et il dit que c'est vraiment une URL, donc tout va bien."



Et puis je peux explicitement organiser l'appel de bénédiction en disant: "appelons simplement la fonction de l'éditeur de liens ici sur la base des résultats de la" bénédiction "de cette URL." Après cela, nous devrions obtenir le même message d'erreur qu'auparavant.



Malheureusement, je ne peux pas l'exécuter pour vous et attendre qu'il échoue, mais je peux dire qu'il échouera certainement, car j'ai intentionnellement fait une erreur de compilation. Cette URL ne sera pas acceptée par la politique d'URL.

Si j'ai raté cet appel béni, ce serait une erreur plus grave au moment de la compilation, car vous avez la chaîne et la bonne URL, et elles sont de types différents.



Rendons-le plus intéressant. Je vais ouvrir un fichier de configuration pour cette démo. C'est assez court, du moins si vous regardez n'importe quel cadre d'application Web Java. Ils ont ces fichiers XML géants pour la configuration, donc tout va beaucoup mieux avec nous.



Nous pouvons ajouter une règle qui stipule que tout sur Wikipédia est autorisé, puis mettre l'URL de Wikipédia dans le corps.



Maintenant, allez à la page et cliquez sur Veuillez cliquer.



Voici ce que nous avons obtenu: adresse Wikipedia introuvable.



Donc, l'idée principale est d'avoir un type abstrait d'URL, comme vous pourriez avoir un type abstrait de table de hachage qui encode les variations de ce à quoi ressemble la table de hachage et empêche le code d'entrer dans le tableau de table de hachage. Nous pouvons faire de même pour l'URL. En utilisant cette fonction de bénédiction, le système s'assure que chaque valeur de ce type passe un contrôle approprié à un moment donné.

Par exemple, avec cette politique, nous savons que nous n'aurons jamais d'URL JavaScript, vous pouvez donc en toute sécurité prendre la valeur de l'URL et l'utiliser comme lien. Cela ne cassera pas les abstractions de base de la langue.

Etudiant: est- il possible d'utiliser du JavaScript "pur" en l'insérant dans la chaîne du corps?

Professeur: oui et non. Au lieu de JavaScript, vous intégrez du code Ur / Web qui effectue une sorte de tâche. Maintenant, je vais taper la commande:

return <xml><body onload = {alert “LOADED”}> 

Et vous verrez ce qui s'est passé - l'interprète a placé une fenêtre sur l'écran avec l'inscription «Loaded» - «Loaded».



Essayer d'interpréter le code JavaScript sous forme de chaîne comme un programme serait un désastre. Vous voyez, nous pouvons mettre du code dans le même langage de programmation que celui avec lequel vous travaillez, déjà limité par ces accolades. Et puis il est automatiquement compilé en JavaScript pour s'exécuter côté client.

Je note que les versions plus récentes des navigateurs peuvent éviter les erreurs d'interprétation des caractères, mais certains navigateurs plus anciens sont capables de semer la confusion. Dans tous les cas, tous les éléments de caractère seront interprétés comme UTF-8 s'ils entrent dans le document. S'il y a un problème avec un codage différent, ce codage ne doit pas être appliqué ici.

Étudiant: le compilateur vérifie si la chaîne contient une URL valide. Mais si vous calculez une chaîne au moment de l'exécution, bénit-elle au moment de l'exécution si une chaîne donnée est valide ou non?

Professeur: créons un formulaire pour tester cette déclaration et placez-le ici. Nous entrons notre URL dans la zone de texte URL, puis insérons le bouton soumettre et soumettre.



Lorsque vous cliquez dessus, la fonction de l'éditeur de liens sera appelée en écrivant une valeur pour chaque champ du formulaire. Dans ce cas, il n'y a qu'un seul champ appelé "URL", donc l'éditeur de liens traitera l'entrée contenant l'URL comme un type de chaîne. Et puis nous essayons de lui appliquer la fonction bénir et de voir si cela fonctionne.



Vous voyez un exemple de messages d'erreur lorsque vous tapez le mauvais type d'URL, une de ces choses qui n'auront aucun sens si vous n'êtes pas familier avec Haskell. J'ai oublié d'insérer la fonction de retour ici. Au moins maintenant, cela ressemble plus à un programme Java. Et j'ai aussi oublié de dire que maintenant c'est une page complète. Par conséquent, nous ne pouvons pas utiliser la balise a tant que nous ne sommes pas dans la balise body.



Maintenant, lancez le compilateur, allez sur notre page, cliquez sur le bouton Veuillez cliquer, entrez une adresse inexistante inexistante.



Ensuite, nous cliquons sur Soumettre la requête - "Envoyer une demande" et nous obtenons un message d'erreur - l'adresse de ce type n'est pas résolue.



Si nous saisissons l'URL correcte comme indiqué sur l'écran suivant, puis cliquez sur Soumettre la requête, aucun message d'erreur n'apparaîtra.



Je pense que la réponse à votre question a été longue et pas trop excitante.

Étudiant: existe-t-il des conditions plus strictes pour les URL en plus de l'interdiction d'utiliser JavaScript?
Professeur: Actuellement, les restrictions plus strictes ne sont que des constantes et des préfixes. Mais vous pouvez également créer vos propres règles d'interdiction, et elles fonctionneront dans l'ordre dans lequel vous les écrivez.

Etudiant: il s'avère que si vous adhérez à l'interdiction de JavaScript, mais mettez un saut de ligne au milieu du mot "JavaScript", le compilateur peut interpréter cela ...

Professeur: oui, ce serait dommage. C'est pourquoi il est bon de s'en tenir à l'approche de la liste blanche au lieu d'utiliser l'approche de la liste noire. Vous souhaitez probablement que toutes les règles commencent par un protocole spécifique, tel que HTTP, et n'autorisent que ce qui convient à votre suite de protocoles approuvée. Je recommande de faire exactement cela.

Étudiant: pour de nombreux sites, vous pouvez autoriser les utilisateurs à échanger des liens, auquel cas vous devez autoriser les liens partout.

Professeur: vous pouvez autoriser les liens si vous souhaitez que vos utilisateurs partagent des liens JavaScript ou, je ne sais pas, des liens flash ou tout ce qui y est autorisé. Vous voyez, vous pouvez créer une «liste blanche» de tous les HTTP, HTTPS, URL et ainsi assurer le fonctionnement sûr de la plupart des sites. Cette approche n'est que légèrement plus faible que d'autoriser uniquement des URL spécifiques. Mais au moins, vous pouvez éliminer complètement la possibilité d'exécution automatique d'une chaîne en tant que programme.

Permettez-moi de vous donner un exemple de résumé, qui est un exemple d'un système de salon de discussion simple présenté dans la base de données. L'utilisateur peut cliquer sur le lien pour accéder à la salle puis envoyer un message. Il s'agit de la première de plusieurs options de circuit.



Tout d'abord, je noterai que je vais recompiler cela. Et puis comme par magie, toutes les tables de base de données déclarées seront ajoutées à la base de données, et nous pouvons commencer à utiliser l'application. Mais nous devons d'abord ajouter quelques salles de chat. Ouvrons donc notre interface à la base de données de démonstration et insérons les valeurs «un» et «deux» dans la salle de table.



Maintenant, ils sont apparus ici.



Maintenant, nous entrons dans la première salle de discussion et pouvons nous amuser toute la journée en envoyant des lignes de texte, par exemple, une telle première ligne. Il sera plus intéressant d'essayer d'envoyer du HTML, et il sera immédiatement traité. Ceci est un exemple des principales fonctionnalités du programme.



Encore une fois, nous allons rapidement voir comment cela fonctionne, nous avons donc ces deux tables SQL - table room et table message, qui sont simplement déclarées dans cette première classe à l'intérieur du langage de programmation. Et nous donnons un diagramme de chaque table. Et puis, lorsque nous essayons d'accéder à ces tables, le compilateur s'assure qu'elles sont accessibles conformément à un schéma de typage prometteur.



Ainsi, nous avons un tableau des chambres, où chaque chambre est un enregistrement composé d'un identifiant ID, qui est un entier, et d'un titre, qui est une chaîne. C'est le type de vue dans lequel nous avons simplement créé des enregistrements. Je viens de créer quelques salles dans la console SQL. Nous avons également une notification que chaque message appartient à une salle particulière, l'heure à laquelle il a été créé et le texte qui est le contenu du message.
Permettez-moi maintenant de passer rapidement à la fonction principale.



Nous exécutons une requête SQL - vous voyez un exemple de syntaxe SQL intégrée à Ur / Web. Je ne veux pas entrer dans les appels de fonction via cette extension depuis la bibliothèque standard. Ce sera assez verbeux, il suffit de rappeler mes mots sur le fait que la bibliothèque standard a des méthodes pour appeler des fonctions qui sont des moyens valides pour construire une requête SQL.

Et ces fonctions ont des types qui en font des demandes d'impression pour vous, et ne garantissent pas seulement que la syntaxe est valide. Ce code itère simplement sur toutes les lignes issues de cette requête et génère des parties du code HTML pour chacune d'elles.

En particulier, nous allons mettre le résultat de la requête dans le champ Titre et le convertir en HTML avec une notation qui comprend des accolades. Les crochets indiquent en outre que ce n'est pas encore un vrai morceau de HTML, mais veuillez le convertir pour moi de manière standard. Nous pouvons donc faire avec des chaînes et des entiers et toutes les données d'autres types.

Étudiant: s'il contenait du HTML malveillant ou autre, serait-il filtré?

Professeur: oui, ce serait le cas. Dans Ur / Web, vous pouvez simplement le considérer comme la construction d'un arbre. Il s'agit d'un nœud qui représente du texte. De toute évidence, le texte ne peut rien faire.

Etudiant: donc si cet en-tête était sous le contrôle de l'utilisateur et que quelqu'un discutait avec le titre Alert, ne serait-ce pas JavaScript?

Professeur: il ne sera pas automatiquement interprété comme JavaScript, HTML ou autre. Il sera perçu par le programme comme du texte brut.

Revenons donc à notre image d'écran. Nous avons ce titre Titre, encadrons-le avec des balises. Et au lieu de href, la manière habituelle de lier en HTML, nous utilisons l'attribut link, qui est une sorte de pseudo-attribut ur / web qui prend comme argument non l'URL, mais surtout les expressions Ur / Web. Le fait est que lorsque vous cliquez sur ce lien, cette expression est lancée pour créer une nouvelle page qui doit être affichée.
Dans ce cas, nous appelons la fonction chat, qui est définie ici sur l'écran suivant, c'est ce que c'est.



Je n'entrerai pas dans les détails. Mais nous avons encore quelques requêtes SQL utilisant diverses fonctions de bibliothèque standard pour différentes façons d'utiliser les résultats demandés.

Nous générons cette page HTML et disons que vous êtes dans un chat avec un tel titre, nous avons un formulaire où l'utilisateur peut saisir du texte. C'est le formulaire que j'ai utilisé pour montrer comment le programme fonctionnait il y a quelques minutes. Le bouton d'envoi du formulaire a cet attribut Add contenant say, qui est le nom de la fonction Ur / Web. Par conséquent, lorsque nous soumettons le formulaire, nous appelons cette fonction.

L'exécution de quelques SQL supplémentaires insère de nouvelles lignes dans la table. Nous sautons automatiquement de l'ID de la salle de conversation aux champs de texte qui sont venus ici du formulaire, et ils sont automatiquement masqués selon les besoins. Mais là encore, dans Ur / Web, vous n'avez pas besoin de penser à "échapper" à la fonction de cette façon. Parce que c'est juste la syntaxe pour construire un arbre, pas pour une chaîne. Ainsi, il n'y a aucun moyen que des choses étranges puissent arriver à l'analyse que vous n'attendez pas de la façon choisie d'interpréter la syntaxe.

Ainsi, le fait que nous ayons un widget sous cette forme sous la forme d'une interface graphique et qu'il s'agit d'un champ de texte, le compilateur conclut que l'enregistrement résultant du remplissage du formulaire de zone de texte doit avoir un élément appelé «texte» de type chaîne . Cet encodage du formulaire et les règles de saisie ne sont pas intégrés dans le langage, mais sont issus de la bibliothèque Ur express, qui contrôle réellement ces formulaires, déterminant les types de fonctions valides.
Si vous n'avez plus de questions sur cette partie du programme, je passe à l'étape suivante. Je vais utiliser un moyen pour forcer l'encapsulation de différentes parties d'une application qui prend en charge Ur / Web et qui prend rarement en charge d'autres langues. Je vais prendre cette pièce. Je vais prendre quelques définitions et les mettre dans un module qui encapsule certaines d'entre elles comme privées. En particulier, les tables de la base de données seront privées, donc personne ne pourra y accéder directement.

Vous ne pouvez y accéder qu'en utilisant l'ensemble des méthodes que nous proposons. Une méthode s'exécute à l'intérieur d'une transaction et crée une liste d'enregistrements avec des champs d'ID et de titre pour les salles de discussion disponibles.

Ensuite, nous étendons simplement cette opération de chat. Et la seule chose que j'ai faite ici a été d'entrer un nom pour l'ID de concept - ID de type. Donc je ne dis pas seulement que l'ID est un entier, je dis que c'est un nouveau type.



La seule façon dont le monde extérieur peut contacter le chat est d'obtenir une liste de toutes les salles, et la seule façon que le monde extérieur puisse l'utiliser est d'appeler la fonction de chat. Disons qu'il s'agit d'un type abstrait de table de hachage à l'intérieur de la classe de table de hachage, où des détails sont stockés qui expliquent ce que sont les ID et comment ils sont produits en interne, étant privés de ce module, et le code client qui appelle ce module ne doit pas les utiliser.

Maintenant, je vais transférer toute cette syntaxe vers le bas et la placer dans le module, afin que par défaut, elle ne soit pas exposée au reste du code. Ensuite, j'implémente cette méthode de chambres. Nous avons déjà la possibilité d'organiser un chat. Mais nous pouvons implémenter les salles d'une manière plus simple en utilisant une autre fonction de bibliothèque standard pour interpréter la demande sous la forme actuelle.
Disons simplement tout sélectionner dans la liste des chambres, triées par nom. Comme d'habitude, cette requête est pour nous un type de données validé. Et le système détermine: "OK, cette expression va générer une liste d'enregistrements qui correspondent au type déclaré dans la signature de ce module." Alors maintenant, en dehors de ce module, aucun autre code ne peut mentionner une table de salle ou une table de messages.



Ainsi, au moins du point de vue de cette application, nous pouvons lui appliquer l'invariance requise. Nous pouvons même cacher des secrets à l'intérieur du module afin qu'il n'y ait aucun problème de sécurité si une autre partie du code peut les obtenir.

Étudiant: un autre morceau de code pourrait-il également implémenter cette méthode de salle?

Professeur: Ce serait un tableau complètement différent. En fait, nous pouvons le faire en insérant un tel fragment de 4 lignes dans un autre module.



Ensuite, nous pouvons faire ce que nous voulons avec ce tableau. Je vais le compiler, peut-être dans 30 secondes, et nous verrons ce qui se passe. Mais en réalité, c'est une table différente, comme si vous aviez le même nom privé, mais pour deux classes Java différentes.

Donc, vous supposez qu'à l'intérieur de ce module, il existe un type abstrait appelé salle, qui contient l'identifiant ID et le titre. Ce n'est pas correct. Le chat accepte les paramètres de la salle en entrée. Lorsque nous appelons la fonction de chat, elle sera appelée via l'URL. L'ID et le titre sont transmis en dehors de la représentation de l'URL qui appelle la fonction. Nous avons seulement besoin de l'ID pour implémenter cette fonction. Ainsi, lorsque nous appelons la fonction, nous appelons en fait l'URL.
Ce serait un gaspillage en termes d'utilisation de l'espace et aurait l'air grossier pour l'utilisateur si l'en-tête était passé comme argument supplémentaire lors de l'appel du chat via l'URL. Est-ce que cela a du sens? Regardons la barre d'URL sur cette diapositive.



L'identifiant de la chaîne que nous suivons est automatiquement sérialisé en URL à la fin de la ligne. Et si nous transmettions un enregistrement contenant l'ID et le titre du titre, ce titre serait également sérialisé, ce qui est au moins un peu illogique.

54:10

Cours MIT "Sécurité des systèmes informatiques". Conférence 11: Langage de programmation Ur / Web, partie 3


La version complète du cours est disponible ici .

Merci de rester avec nous. Aimez-vous nos articles? Vous voulez voir des matériaux plus intéressants? Soutenez-nous en passant une commande ou en le recommandant à vos amis, une réduction de 30% pour les utilisateurs Habr sur un analogue unique de serveurs d'entrée de gamme que nous avons inventés pour vous: Toute la vérité sur VPS (KVM) E5-2650 v4 (6 cœurs) 10 Go DDR4 240 Go SSD 1 Gbps à partir de 20 $ ou comment diviser le serveur? (les options sont disponibles avec RAID1 et RAID10, jusqu'à 24 cœurs et jusqu'à 40 Go de DDR4).

VPS (KVM) E5-2650 v4 (6 cœurs) 10 Go DDR4 240 Go SSD 1 Gbit / s jusqu'en décembre gratuitement en payant pour une période de six mois, vous pouvez commander ici .

Dell R730xd 2 fois moins cher? Nous avons seulement 2 x Intel Dodeca-Core Xeon E5-2650v4 128 Go DDR4 6x480 Go SSD 1 Gbps 100 TV à partir de 249 $ aux Pays-Bas et aux États-Unis! Pour en savoir plus sur la création d'un bâtiment d'infrastructure. classe utilisant des serveurs Dell R730xd E5-2650 v4 coûtant 9 000 euros pour un sou?