Cours MIT "Sécurité des systèmes informatiques". Conférence 10: Exécution symbolique, partie 1

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

Bonjour à tous, je suis Armando Solar-Lesam et aujourd'hui je donnerai une conférence sur la performance symbolique. Qui parmi les personnes présentes ici connaît ce terme ou en a entendu parler auparavant? Je veux juste avoir une idée de notre public. Commençons donc. J'ai laissé tomber mon ordinateur portable plusieurs fois, donc le chargement prend beaucoup de temps.



L'exécution symbolique est le cheval de bataille de l'analyse de programme moderne. C'est l'une des méthodes issues de la recherche et qui a ensuite commencé à être utilisée dans de nombreuses applications. Par exemple, aujourd'hui chez Microsoft, il existe un système appelé SAGE, qui fonctionne avec de nombreux logiciels Microsoft importants, allant de Power Point et se terminant par Windows lui-même, pour vraiment trouver des problèmes de sécurité et des vulnérabilités.

Il existe de nombreux projets académiques qui ont eu un impact important sur le monde réel, tels que la détection de bogues importants dans les logiciels open source à l'aide de l'exécution symbolique. Et la beauté de l'exécution symbolique en tant que technique est que, par rapport aux tests, elle vous donne la possibilité d'imaginer comment votre programme se comportera avec un ensemble potentiellement infini de données d'entrée possibles. Cela nous permet d'étudier des tableaux de données d'entrée, ce qui serait complètement impraticable et peu pratique à étudier, par exemple, par des tests aléatoires, même s'il y a un très grand nombre de testeurs. En revanche, par rapport aux méthodes d'analyse statique plus traditionnelles, elle présente l'avantage suivant. Lors de l'examen d'un problème, l'exécution symbolique peut créer une entrée et une trace, un chemin d'exécution qui peut être exécuté dans un programme réel et exécuter ce programme en fonction de cette entrée. Et après cela, nous pouvons identifier le vrai bogue et commencer à le corriger à l'aide des mécanismes de débogage traditionnels. Et cela est particulièrement précieux lorsque vous êtes dans un environnement de développement industriel où vous n'avez probablement pas le temps de vous occuper de chaque petit problème dans votre code.

Par exemple, vous voulez vraiment pouvoir distinguer les vrais problèmes des faux positifs. Comment ça marche?

Pour vraiment comprendre comment cela fonctionne, il est utile de commencer par une exécution normale. Si nous considérons l'exécution symbolique comme une généralisation d'une exécution traditionnelle et simple, il est logique de savoir à quoi elle ressemble. Par conséquent, je vais utiliser ce programme très simple comme illustration pour beaucoup de choses dont nous parlerons aujourd'hui.



Ici, nous avons un extrait d'un code très simple de plusieurs branches et la déclaration que si, dans certaines conditions, la valeur t <x, alors c'est une fausse déclaration. Nous voulons savoir si cette déclaration pourra jamais être soulevée. Est-ce possible? Y a-t-il une entrée qui fera échouer cette déclaration?

L'une des choses que je peux faire est de vérifier l'exécution de ce programme en utilisant des valeurs d'entrée spécifiques comme exemple. Supposons que nous utilisons une entrée pour laquelle X = 4 et Y = 4. La valeur de T est nulle, comme annoncé au début du programme.

Donc, avant d'arriver à une exécution normale, découvrons quel est le point important ici. Nous devons avoir une idée de l'état du programme, non? Que nous fassions une exécution normale ou que nous fassions une exécution symbolique, nous devons avoir un moyen de caractériser l'état du programme. Dans ce cas, il s'agit d'un programme si simple qu'il n'utilise pas le tas, n'utilise pas la pile et qu'il n'y a aucun appel de fonction ici.

Ainsi, l'état peut être entièrement caractérisé par ces trois variables, tout en sachant où je suis dans le programme. Par conséquent, si je commence l'exécution à partir de 4, 4 et 0 et que j'arrive à la fin de la branche, je vérifierai l'expression: 4 est supérieur à 4? Evidemment non.
Maintenant, je vais exécuter le programme à T = Y, c'est-à-dire que T n'est plus 0, mais a une valeur de 4. C'est l'état actuel de mon programme, et maintenant je peux évaluer cette branche.



Est-il vrai que T <X? Non. Nous avons esquivé la balle, la fausse déclaration n'a pas fonctionné. Il n'y a eu aucun problème dans cette exécution privée.

Mais cela ne nous dit rien sur une autre exécution. Nous savons qu'avec des valeurs X = 4 et Y = 4, le programme n'échouera pas. Mais cela ne nous dit rien sur ce qui se passera si les valeurs d'entrée sont 2 et 1.



Avec ces valeurs d'entrée, l'exécution ira différemment. Cette fois, nous voyons que T = X, et après avoir exécuté cette ligne, T prendra une valeur égale à 2. Y a-t-il des problèmes dans cette exécution? Y aura-t-il une erreur d'assertion avec une telle entrée?

Voyons voir. Donc, si T est 2 et X est 2, alors T n'est pas moins que X. Il semble que nous ayons de nouveau esquivé la balle. Non? Nous avons donc ici deux valeurs d'entrée spécifiques auxquelles le programme fonctionne sans erreur. Mais en réalité, il ne nous dit rien sur les autres valeurs d'entrée.

Ainsi, l'idée de l'exécution symbolique est que nous voulons aller au-delà de l'exécution d'un programme avec un seul ensemble de données d'entrée. Nous voulons pouvoir parler réellement du comportement du programme lors de l'utilisation d'un très grand ensemble de données, dans certains cas, d'un nombre infini de valeurs d'entrée possibles. L'idée principale de ceci est la suivante.



Pour un programme comme celui-ci, son état est déterminé par la valeur de ces trois variables différentes: X, Y et T, et sachant où je suis en ce moment dans le programme. Mais maintenant, au lieu des valeurs spécifiques pour X et Y, j'aurai une valeur symbolique, juste une variable. Une variable qui me permet de nommer cette valeur, que l'utilisateur utilise comme entrée. Cela signifie que l'état de mon programme n'est plus caractérisé par la correspondance des noms de variables avec des valeurs spécifiques. Il s'agit maintenant d'un mappage de noms de variables avec ces valeurs symboliques.

La valeur symbolique peut être considérée comme une formule. Dans ce cas, la formule pour X est égale à X et la formule pour Y est simplement Y, et pour T elle est en fait égale à 0. Nous savons que pour chaque valeur d'entrée, peu importe ce que vous faites. La valeur de T après la première instruction sera 0.

C'est là que ça devient intéressant maintenant. Nous sommes arrivés à cette branche, qui dit que si X est supérieur à Y, nous irons dans une direction. Si X est inférieur ou égal à Y, nous irons dans l'autre sens.

Savons-nous quelque chose sur X et Y? Que savons-nous d'eux? Au moins, nous connaissons leur type, nous savons qu'ils varieront de min int à max int, mais c'est tout ce que nous savons à leur sujet. Il s'avère que les informations que nous connaissons à leur sujet ne suffisent pas à dire dans quelle direction cette branche peut aller. Elle peut aller dans n'importe quelle direction
Il y a beaucoup de choses que nous pouvons faire, mais que pouvons-nous faire pour le moment? Essayez de faire la supposition la plus folle.



Public: nous pouvons suivre l'exécution du programme sur les deux branches.

Professeur: oui, nous pouvons suivre les progrès sur les deux branches. Lancez une pièce et, selon la façon dont elle tombe, choisissez l'une ou l'autre branche.

Donc, si nous voulons suivre les deux branches, nous devons d'abord suivre l'une puis l'autre, non? Supposons que nous commençons par cette branche - T = X. Nous savons que si nous arrivons à cet endroit, T aura la même signification que X. Nous ne savons pas quelle est cette valeur, mais nous avons un nom pour cela - c'est le script X.



Si nous prenons la branche opposée, que se passera-t-il? La valeur de T sera égale à autre chose, non? Dans cette branche, la valeur de T sera la valeur symbolique de Y.



Alors, que signifie cette valeur T lorsque nous arrivons à ce point du programme? Peut-être que c'est X, peut-être que c'est Y. Nous ne savons pas exactement quelle est cette valeur, mais pourquoi ne lui donnons-nous pas un nom? Appelez-le t ₀ . Et que savons-nous de t ₀ ? Dans quels cas t ₀ sera égal à X?

Essentiellement, nous savons que si X est supérieur à Y, alors la variable est égale à X, et si X est inférieure ou égale à Y, alors la variable est égale à Y. Par conséquent, nous avons une valeur que nous avons définie, appelons-la t ₀ , et elle les a propriétés logiques.



Donc, à ce stade du programme, nous avons un nom pour la valeur de T, c'est t ₀ . Qu'avons-nous fait ici? Nous avons pris les deux branches de l'instruction if, puis calculé la valeur symbolique, en voyant dans quelles conditions une branche du programme serait exécutée et dans quelles autres.
Maintenant, il s'agit de demander si T peut être inférieur à X. Maintenant, la valeur de T est t ₀ , et nous voulons savoir s'il est possible que t ₀ soit inférieur à X? Rappelez-vous la première branche que nous avons examinée - nous avons posé une question sur X et Y et nous ne savions rien à leur sujet, sauf qu'ils étaient de type int.

Mais ayant t ₀ , nous en savons vraiment beaucoup à ce sujet. Nous savons que dans certains cas, il sera égal à X, et dans certains cas, il sera égal à Y. Alors maintenant, il nous donne un ensemble d'équations que nous pouvons résoudre. Donc, on peut dire s'il est possible que t _{0 soit} inférieur à X, sachant que t ₀ remplit toutes ces conditions? Ainsi, nous pouvons exprimer cela comme une restriction, montrant s'il est possible que t ₀ soit inférieur à X. Et si X est supérieur à Y, alors t ₀ est égal à X, et si X est inférieur ou égal à Y, cela signifie que t ₀ = Y.



Nous avons donc une équation. S'il a une solution, s'il est possible de trouver la valeur de t ₀ , la valeur de X et la valeur de Y qui satisfont cette équation, alors nous reconnaissons ces valeurs, et quand nous les entrons dans le programme, alors lorsqu'elles sont exécutées, elle ira le long de cette branche si t <x et " va exploser ”quand il tombera dans affirmer faux.

Alors qu'avons-nous fait ici? Nous avons exécuté le programme, mais au lieu de mapper les noms de variables à des valeurs spécifiques, nous avons donné à ces noms de variables des valeurs symboliques. En fait, ils leur ont donné d'autres noms de variables. Et dans ce cas, nos autres noms de variables sont le script X, le script Y, t ₀ , et en plus, nous avons un ensemble d'équations qui montrent comment ces valeurs sont liées. Nous avons une équation qui nous dit comment t ₀ est lié à X et Y dans ce cas.

La solution de cette équation nous permet de répondre à la question de savoir si cette branche peut être exécutée ou non. Jetez un œil à l'équation - est-il possible de prendre cette branche ou non? Il semble que non, car nous recherchons des cas où t _{0 est} inférieur à X, mais si dans la première condition t ₀ = X, alors l'expression t ₀ <X ne sera pas vraie.

Ainsi, cela signifie que lorsque X> Y, cela ne peut pas se produire, car t ₀ = X et il ne peut pas être égal ou inférieur à X en même temps.

Mais que se passe-t-il si t ₀ = Y? T ₀ peut-il être inférieur à X dans ce cas?

Non, cela ne peut certainement pas, car nous savons que X <Y. Donc, si t ₀ est inférieur à X, il sera également inférieur à Y. Mais nous savons que dans ce cas t ₀ = Y. Et donc, encore une fois , cette condition ne peut pas être remplie. Donc, ici, nous avons une équation qui n'a pas de solution, et peu importe les valeurs que vous incluez dans cette équation.

Vous ne pouvez pas le résoudre, et cela nous dit que peu importe les entrées X et Y que nous transmettons au programme, il ne descendra pas la branche si t <x.

Maintenant, remarquez qu'en créant cet argument ici, j'ai essentiellement fait allusion à votre intuition sur les entiers, sur les entiers mathématiques. En pratique, nous savons que les nombres machine ne se comportent pas exactement comme les nombres mathématiques. Il existe des cas où les lois appliquées aux types de données entiers mathématiques ne s'appliquent pas aux entiers programmatiques.

Par conséquent, nous devons être très prudents lors de la résolution de ces équations, car nous devons nous rappeler que ce ne sont pas les nombres entiers dont on nous a parlé à l'école primaire. Ce sont les entiers 32 bits utilisés par la machine. Et il y a de nombreux cas d'erreurs qui se sont produites parce que les programmeurs ont pensé leur code en termes d'entiers mathématiques, sans se rendre compte qu'il y a des choses comme les débordements qui peuvent provoquer un comportement de programme différent pour l'entrée mathématique.

Une autre chose que j'ai décrite ici est un argument purement intuitif. Je vais vous guider à travers le processus, montrant comment le faire manuellement, mais ce n'est en aucun cas un algorithme. La beauté de cette idée d'exécution symbolique, cependant, est qu'elle peut être codée dans un algorithme. Et vous pouvez le résoudre mécaniquement, ce qui vous permet de le faire non seulement pour un programme de 10 lignes, mais pour des millions de programmes. Cela nous permet d'utiliser le même raisonnement intuitif que nous avons utilisé dans ce cas et de parler de ce qui se passe lorsque nous exécutons ce programme avec différentes valeurs d'entrée. Et ces considérations peuvent être étendues et étendues à de très gros programmes.



Public: que se passe-t-il si le programme ne prend pas en charge la saisie d'un certain type de variable?

Professeur: c'est une très bonne question! Supposons que nous ayons le même programme, mais au lieu de t = x, nous aurons t = (x-1). Ensuite, intuitivement, nous pouvons imaginer que maintenant ce programme peut «exploser», non?



Parce que quand le programme va dans ce sens, t sera vraiment inférieur à x. Qu'adviendra-t-il d'un tel programme? À quoi ressemblera notre état symbolique? Que sera t ₀ lorsque x est supérieur à y? Nous corrigeons les lignes de nos équations en fonction d'une autre valeur lorsque t = (x-1). Maintenant, le programme peut échouer, et vous allez voir le développeur et lui dites: "hé, cette fonction peut exploser lorsque x est supérieur à y"!

Le développeur regarde cela et dit: «Oh, j'ai oublié de vous dire - en fait, cette fonction ne sera jamais appelée avec des paramètres, où x est supérieur à y. "Je viens de l'écrire pour des raisons historiques, alors ne vous inquiétez pas, je ne m'en souviendrais pas si vous ne m'aviez pas dit."

Supposons que nous supposions que x sera inférieur ou égal à y.



Il s'agit d'une condition préalable ou d'un accord pour notre fonction. La fonction promet de faire quelque chose, mais seulement si la valeur satisfait cette hypothèse. Mais s'il n'est pas satisfait, la fonction dit: "Je me fiche de ce qui se passe. Je promets qu'il n'y aura pas d'erreur uniquement si cette hypothèse est remplie. "

Alors, comment codons-nous cette contrainte lorsque nous résolvons les équations? Essentiellement, nous avons un ensemble de contraintes qui nous indiquent si cette branche est faisable. Et en plus des limitations, nous devons également nous assurer que la condition préalable, ou l'hypothèse, est satisfaite.

La question est, puis-je trouver x et y qui satisfont à toutes ces restrictions et possèdent en même temps les propriétés requises? Vous pouvez voir que cette restriction X ≤ Y représente la différence entre le cas où cette restriction est remplie et le cas où elle n'est pas respectée.

Il s'agit d'un problème très important lorsque vous travaillez avec l'analyse, en particulier lorsque vous souhaitez le faire simultanément au niveau des fonctions individuelles. Il est conseillé de savoir ce que le programmeur avait en tête lors de l'écriture de cette fonction. Parce que si vous n'avez aucune idée de ces hypothèses, vous pourriez penser qu'il y a une entrée que le programme échouera.

Comment faire cela de manière mécanique? Ce problème comporte deux aspects. Aspect numéro un - comment avez-vous trouvé ces formules?

Dans ce cas, il est intuitivement clair comment nous sommes arrivés à ces formules, nous les avons simplement composées manuellement. Mais comment créer ces formules mécaniquement?

Et le deuxième aspect - comment résolvez-vous ces formules après les avoir? Est-il possible de résoudre réellement ces formules qui décrivent si votre programme plante ou non?
Commençons par la deuxième question. Nous pouvons réduire notre problème avec ces formules, qui incluent le raisonnement entier et les vecteurs de bits. Lorsque vous créez des programmes, vous vous occupez des tableaux, des fonctions et, par conséquent, vous obtenez des formules géantes. Est-il possible de les résoudre mécaniquement?



De nombreuses technologies dont nous parlons aujourd'hui sont des outils pratiques liés aux formidables avancées dans le développement de solveurs pour des questions logiques. En particulier, il existe une classe très importante de solveurs, appelée SMT, ou «solveur de solvabilité des théories modulaires». Le solveur SMT est la solvabilité des formules logiques en tenant compte des théories qui les sous-tendent.

Beaucoup de gens affirment que ce nom n'est pas particulièrement bon, mais il a été considéré comme le plus couramment utilisé.

SMT-solveur est un algorithme grâce auquel cette formule logique à la sortie vous donnera l'une des deux options: soit il remplit son objectif, soit il ne satisfait pas. , , .

. , SMT, NP- , «» «».
, NP- ? -, ? , SMT – : « ».



, , , , : « ». , , .

27:30

MIT « ». 10: « », 2


La version complète du cours est disponible ici .

, . ? ? , 30% entry-level , : VPS (KVM) E5-2650 v4 (6 Cores) 10GB DDR4 240GB SSD 1Gbps $20 ? ( RAID1 RAID10, 24 40GB 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 ? 2 Intel Dodeca-Core Xeon E5-2650v4 128GB DDR4 6x480GB SSD 1Gbps 100 $249 ! . c Dell R730xd 5-2650 v4 9000 ?