Хабрахабр

[Перевод] Курс MIT «Безопасность компьютерных систем». Лекция 10: «Символьное выполнение», часть 1

Массачусетский Технологический институт. Курс лекций #6.858. «Безопасность компьютерных систем». Николай Зельдович, Джеймс Микенс. 2014 год

Computer Systems Security — это курс о разработке и внедрении защищенных компьютерных систем. Лекции охватывают модели угроз, атаки, которые ставят под угрозу безопасность, и методы обеспечения безопасности на основе последних научных работ. Темы включают в себя безопасность операционной системы (ОС), возможности, управление потоками информации, языковую безопасность, сетевые протоколы, аппаратную защиту и безопасность в веб-приложениях.

Лекция 1: «Вступление: модели угроз» Часть 1 / Часть 2 / Часть 3
Лекция 2: «Контроль хакерских атак» Часть 1 / Часть 2 / Часть 3
Лекция 3: «Переполнение буфера: эксплойты и защита» Часть 1 / Часть 2 / Часть 3
Лекция 4: «Разделение привилегий» Часть 1 / Часть 2 / Часть 3
Лекция 5: «Откуда берутся ошибки систем безопасности» Часть 1 / Часть 2
Лекция 6: «Возможности» Часть 1 / Часть 2 / Часть 3
Лекция 7: «Песочница Native Client» Часть 1 / Часть 2 / Часть 3
Лекция 8: «Модель сетевой безопасности» Часть 1 / Часть 2 / Часть 3
Лекция 9: «Безопасность Web-приложений» Часть 1 / Часть 2 / Часть 3
Лекция 10: «Символьное выполнение» Часть 1 / Часть 2 / Часть 3

Кто из присутствующих здесь знаком с этим термином или слышали об этом раньше? Доброе утро всем, я Армандо Солар-Лесама и сегодня я прочитаю лекцию о символьном выполнении. Итак, начнём. Я просто хочу составить представление о нашей аудитории. Я несколько раз ронял свой ноутбук, поэтому он долго загружается.

Это один из методов, который вырос из исследований и затем стал использоваться во множестве приложений. Символьное выполнение является рабочей лошадкой современного анализа программ. Например, на сегодня в Microsoft есть система под названием SAGE, которая работает с большим количеством важного программного обеспечения Microsoft, начиная от Power Point и заканчивая самой Windows, чтобы реально находить проблемы безопасности и уязвимости.

И красота символьного выполнения как техники заключается в том, что по сравнению с тестированием, это дает вам возможность представить, как ваша программа будет себя вести с потенциально бесконечным набором возможных входных данных. Есть много академических проектов, которые оказали большое влияние на реальный мир, например, на обнаружение важных ошибок в программном обеспечении с открытым исходным кодом, с помощью символьного выполнения. С другой стороны, по сравнению с более традиционными методами статического анализа оно имеет следующее преимущество. Это позволяет исследовать массивы входных данных, которые было бы совершенно нецелесообразно и непрактично исследовать, скажем, случайным тестированием даже при наличии очень большого количества тестеров. И после этого мы можете выявить реальный баг и приступить к его исправлению, используя традиционные механизмы отладки. При исследовании проблемы символьное выполнение может создать входные данные и трассировку, путь выполнения, которые можно запустить в реальной программе и выполнить эту программу на основе этих входных данных. И это особенно ценно, когда вы находитесь в промышленной среде разработки, где у вас, вероятно, нет времени, чтобы заботиться о каждой маленькой проблеме в вашем коде.

Как же это работает? Например, вы действительно хотите быть в состоянии отличить реальные проблемы от ложных срабатываний.

Если мы думаем о символьном выполнении как об обобщении традиционного, простого исполнения, имеет смысл знать, как это выглядит. Чтобы действительно понять, как это работает, полезно начать с обычного выполнения. Поэтому я собираюсь использовать эту очень простую программу в качестве иллюстрации для многих вещей, о которых мы сегодня поговорим.

Мы хотим узнать, может ли это утверждение когда-либо быть вызвано. Здесь у нас имеется отрывок очень простого кода из нескольких ветвей и утверждение, что если при некотором условии значение t < х, то это ложное утверждение. Существуют ли какие-то входные данные, которые сделают так, чтобы это утверждение провалилось? Это возможно?

Предположим, что мы используем входные данные, при которых X= 4 и Y = 4. Одна из вещей, которую я могу сделать – это проверить выполнение данной программы на примере конкретных значений входных данных. Величина T равно нулю, как это объявлено в начале программы.

Нам нужно иметь какое-то представление о состоянии программы, верно? Итак, прежде чем мы перейдем к нормальному исполнению, давайте выясним, в чём здесь заключается важный момент? В данном случае это такая простая программа, что она не использует кучу, не использует стек и здесь нет никаких вызовов функций. Делаем ли мы нормальное выполнение или делаем ли мы символьное выполнение, нам нужно иметь какой-то способ охарактеризовать состояние программы.

Поэтому, если я начну выполнение с 4, 4 и 0 и доберусь до конца ветви, то проверю выражение: 4 больше 4? Таким образом, состояние может быть полностью охарактеризовано этими тремя переменными вместе со знанием того, в каком месте программы я нахожусь. Таково нынешнее состояние моей программы, и теперь я могу оценить эту ветвь. Очевидно, что нет.
Теперь я собираюсь выполнить программу при T = Y, то есть T больше не равно 0, а имеет значение, равное 4.

Нет. Правильно ли, что T < X? Не было никаких проблем в этом частном выполнении. Мы увернулись от пули, утверждение false не сработало.

Мы знаем, что при значениях X=4 и Y=4 программа не подведет. Но это ничего не говорит нам ни о каком другом выполнении. Но это ничего не говорит нам о том, что произойдёт, если входными значениями буду 2 и 1.

На этот раз мы видим, что T = X, и после выполнения этой строки T примет значение, равное 2. При таких значениях входных данных выполнение пойдёт по другому пути. Возникнет ли при таких входных данных ошибка утверждения? Есть ли какие-либо проблемы в этом выполнении?

Так, если T равно 2 и Х равно 2, то T никак не меньше Х. Что ж, давайте посмотрим. Верно? Похоже, мы снова увернулись от пули. Но на самом деле это ничего не говорит нам о любых других значениях input. Итак, здесь у нас есть два конкретных входных значения, при которых программа работает без ошибок.

Мы хотим иметь возможность на самом деле рассуждать о поведении программы при использовании очень большого набора данных, в некоторых случаях – бесконечного множества возможных значений input. Итак, идея символьного выполнения состоит в том, что мы хотим выйти за рамки исполнения программы при одном наборе входных данных. Основная идея этого заключена в следующем.

Но теперь вместо конкретных значений для X и Y у меня будет символьное значение, просто переменная. Для такой программы, как эта, её состояние определяется значением этих трех различных переменных: X, Y и T и знанием того, в каком месте программы в данный момент я нахожусь. Это означает, что состояние моей программы больше не характеризуется сопоставлением имен переменных конкретным значениям. Переменная, которая позволяет мне дать имя этому значению, которое пользователь использует в качестве input. Теперь это сопоставление имен переменных этим символьным значениям.

В этом случае формула для Х равна Х и формула для Y равна просто Y, а для T она на самом деле равна значению 0. Символьное значение можно рассматривать как формулу. Значение T после первого утверждения будет равно 0. Мы знаем, что для каждого входного значения не важно, что именно вы делаете.

Мы добрались до этой ветви, которая говорит, что если X больше Y, мы пойдем в одном направлении. Вот где теперь становится интересно. Если X меньше или равно Y, мы пойдем в другом направлении.

Что нам о них известно? Мы знаем что-нибудь об X и Y? Получается, что информация, которую мы о них знаем, недостаточна для того, чтобы сказать, в каком направлении может идти эта ветка. По крайней мере, мы знаем их тип, мы знаем, что они будут варьироваться в интервале от min int до max int, но это все, что мы о них знаем. Попробуйте высказать самое дикое предположение. Она может идти в любом направлении
Существует много вещей, которые мы можем сделать, но что мы можем сделать в данный момент?

Аудитория: мы можем проследить выполнение программы по обеим ветвям.

Подбросить монетку, и в зависимости от того, как она упадёт, выбрать ту или иную ветвь. Профессор: да, мы можем проследить выполнение по обеим ветвям.

Допустим, мы начнём с этой ветки – T=X. Итак, если мы хотим следовать за обеими ветвями, мы должны следовать сначала за одной, а затем за другой, верно? Мы не знаем, каково это значение, но у нас есть для него имя — это скрипт X. Мы знаем, что если доберёмся до этого места, то T будет иметь то же значение, что и X.

Значение T будет равно чему-то другому, так? Если мы возьмем противоположную ветвь, что тогда произойдет? В этой ветви значением T будет символьное значение Y.

Может быть, это Х, может быть это Y. Так что означает это значение T, когда мы дойдем до этой точки в программе? Назовём его t0. Мы не знаем точно, какое именно это значение, но почему бы нам не дать ему имя? В каких случаях t0 будет равно X? И что мы знаем о t0?

Поэтому у нас есть значение, которое мы определили, назовём его t0, и у него есть эти логические свойства. По существу, мы знаем, что если X больше Y, то переменная равна X, а если X меньше или равно Y, то переменная равна Y.

Что же мы здесь сделали? Итак, в данной точке программы у нас есть имя для значения T, это t0. Теперь значение T равно t0, и мы хотим знать, возможно ли, чтобы t0 было бы меньше, чем Х? Мы взяли обе ветви оператора if, а затем вычислили символьное значение, посмотрев, при каких условиях будет выполняться одна ветвь программы, а при каких – другая.
Теперь дело доходит до того, что мы должны спросить, может ли T быть меньше Х. Вспомните первую ветвь, которую мы рассмотрели — мы задавали вопрос об X и Y и ничего о них не знали, кроме того, что они имели тип int.

Мы знаем, что в отдельных случаях он будет равен Х, а в некоторых случаях он будет равен Y. Но имея t0, мы действительно много о нём знаем. Итак, мы можем сказать, возможно ли, что t0 меньше, чем Х, зная, что t0 удовлетворяет всем этим условиям? Так что теперь это дает нам набор уравнений, которые мы можем решить. И если Х больше Y, то t0 равно Х, а если Х меньше или равно Y, это означает, что t0 = Y. Таким образом, можно выразить это как ограничение, показывающее, возможно ли, чтобы t0 было меньше, чем Х.

Если оно имеет решение, если можно найти значение t0, значение Х и значение Y, которые удовлетворяют этому уравнению, тогда мы узнаем эти значения, и когда введём их в программу, то при выполнении она пойдёт по этой ветви if t < x и «взорвется», когда попадет в assert false. Итак, у нас есть уравнение.

Мы выполнили программу, но вместо того, чтобы сопоставить имена переменных конкретным значениям, мы придали этим именам переменных символьные значения. Так что мы здесь cделали? И в этом случае наши другие имена переменных – это скрипт X, скрипт Y, t0, и кроме того, у нас есть набор уравнений, которые показывают, как эти значения связаны. По сути, дали им другие имена переменных. У нас есть уравнение, которое говорит нам, как t0 связан с X и Y в этом случае.

Взглянем на уравнение — можно ли взять эту ветвь или нет? Решение этого уравнения позволяет ответить на вопрос, может ли эта ветвь исполняться или нет. Похоже, что нет, потому что мы ищем случаи, где t0 меньше, чем Х, но если в первом условии t0 = X, то выражение t0 < X будет неправдой.

Таким образом, это означает, что когда X > Y, то этого не может произойти, потому что t0 = X и оно не может одновременно быть равным и меньшим X.

Может ли t0 быть меньше X в этом случае? А что произойдёт, если t0 = Y?

Так что если t0 будет меньше X, тогда оно будет также меньше Y. Нет, определенно не может, потому что мы знаем, что X < Y. И поэтому, опять же, это условие не может быть удовлетворено. Но мы знаем, что в этом случае t0 = Y. Итак, мы имеем здесь уравнение, которое не имеет решения, при этом не важно, какие значения вы включаете в это уравнение.

Вы не можете решить его, и это говорит нам, что независимо от того, какие входные данные Х и Y мы передадим программе, она не будет спускаться по ветке if t < x.

На практике мы знаем, что машинные int ведут себя не совсем так, как математические int. Теперь обратите внимание, что, создавая здесь этот аргумент, я в основном намекал на вашу интуицию о целых числах, о математических целых числах. Есть случаи, когда законы, применяемые к математическим целочисленным типам данных, не применимы для программных int.

Это 32-разрядные целые числа, используемые машиной. Поэтому мы должны быть очень осторожны, когда решаем эти уравнения, потому что нужно помнить, что это не те целые числа, о которых нам рассказывали в начальной школе. И есть много случаев ошибок, которые возникли, потому что программисты думали о своем коде с точки зрения математических целых чисел, не понимая, что есть такие вещи, как переполнения, которые могут вызвать разное поведение программы для математических входных данных.

Я провожу вас через процесс, показывая, как это сделать вручную, но это отнюдь не алгоритм. Другое дело, что я описал здесь чисто интуитивный аргумент. И решить ее можно механическим способом, что позволяет сделать это не просто для программы в 10 строк, а для миллионов программ. Красота этой идеи символического исполнения, однако, заключается в том, что она может быть закодирована в алгоритм. И данные рассуждения можно масштабировать и распространить на очень большие программы. Это позволяет использовать те же интуитивные рассуждения, которые мы использовали в данном случае, и говорить о том, что происходит, когда мы выполняем эту программу с разными значениями input.

Аудитория: что, если программа не поддерживает ввод определённого типа переменных?

Допустим, у нас есть та же самая программа, но вместо t = x у нас будет t = (x-1). Профессор: это очень хороший вопрос! Тогда интуитивно мы можем представить, что теперь эта программа может «взорваться», не так ли?

Что же случится с такой программой? Потому что когда программа пойдет по этому пути, t действительно будет меньше x. Чему будет равно t0, когда x больше y? Как будет выглядеть наше символьное состояние? Теперь программа может потерпеть неудачу, и вы идёте к разработчику и говорите ему: «эй, эта функция может взорваться, когда x больше y»! Исправим строки в наших уравнениях в соответствии с другим значением, когда t = (x-1).

Я просто написал так по неким историческим соображениям, так что не беспокойтесь, я бы об этом и не вспомнил, если бы вы мне не рассказали». Разработчик смотрит на это и говорит: «о, я забыл сказать вам — фактически эта функция никогда не будет вызываться с параметрами, где x больше y.

Допустим, у нас есть предположение, что x будет меньше или равно y.

Функция обещает что-то сделать, но только, если значение удовлетворяет этому предположению. Это предварительное условие или соглашение для нашей функции. Я обещаю, что ошибки не будет только в том случае, когда это предположение будет выполнено». Но если оно не удовлетворено, функция говорит: «мне все равно, что произойдет.

По существу у нас есть набор ограничений, которые говорят нам, осуществима ли эта ветвь. Итак, как мы закодируем это ограничение, когда решаем уравнения? И помимо имеющихся ограничений, мы должны также убедиться, что предварительное условие, или предположение, выполняется.

Можно увидеть, что это ограничение Х ≤ Y представляет собой разницу межу случаем, когда это ограничение выполняется, и случаем, когда оно не выполняется. Спрашивается, могу ли я найти x и y, которые удовлетворяют всем этим ограничениям и одновременно обладают требуемыми свойствами?

Желательно знать, что имел ввиду программист при написании этой функции. Это очень важный вопрос при работе с анализом, особенно когда вы хотите это сделать одновременно на уровне отдельных функций. Потому что если вы не имеете представления об этих предположениях, вы могли бы подумать, что есть некоторые входные данные, при которых программа потерпит неудачу.

Существуют два аспекта этой проблемы. Как же сделать это механическим способом? Аспект номер один — как вы на самом деле придумали эти формулы?

Но как создавать эти формулы механическим способом? В данном случае интуитивно понятно, как мы пришли к этим формулам, мы просто составили их вручную.

Можно ли на самом деле решить эти формулы, которые описывают, происходит сбой вашей программы или нет?
Начнем со второго вопроса. И второй аспект — как вы решаете эти формулы после того, как они у вас появились? Создавая программы, вы заботитесь о массивах, о функциях и в итоге получаете гигантские формулы. Мы можем уменьшить нашу проблему с этими формулами, которые включают целочисленные рассуждения и битовые векторы. Можно ли решить их механическим способом?

В частности, существует очень важный класс решателей, называемый SMT, или «решатель выполнимости модульных теорий». Множество технологий, о которых мы говорим сегодня, являются практическими инструментами, имеющими отношение к огромным достижениям в разработке решателей для логических вопросов. SMT- решатель — это задача разрешимости логических формул с учётом теорий, лежащих в их основе.

Многие люди утверждают, что это название не является особо хорошим, но оно закрепилось как наиболее часто используемое.

Второй случай означает, что в этой формуле невозможно использовать значения переменных, удовлетворяющие требованиям установленных вами ограничений. SMT-решатель является алгоритмом, благодаря которому данная логическая формула на выходе даст вам один из двух вариантов: либо она удовлетворяет своему назначению, либо не удовлетворяет.

Большую часть проблем, которые должны решать SMT, представляют NP-полные задачи, то есть задачи с ответом «да» или «нет».
Можем ли мы иметь систему, которая опирается в качестве своего основного строительного блока на решение NP-полных задач? На практике это звучит немного страшно и немного магически. Дело в том, что у многих SMT – решателей есть ещё и третий возможный ответ: «Я не знаю». Или нам нужно еще что-нибудь, что работает на практике?

Они в состоянии дать вам гарантию, что этот набор ограничений является неудовлетворительным или полностью удовлетворяет своему назначению, то есть они дают вам вполне точный ответ. И поэтому часть красоты этих решателей заключается в том, что, даже решая очень большие и сложные практические проблемы, они способны на большее, чем просто ответить: «я не знаю».

27:30 мин

Лекция 10: «Символьное выполнение», часть 2 Курс MIT «Безопасность компьютерных систем».

Полная версия курса доступна здесь.

Вам нравятся наши статьи? Спасибо, что остаётесь с нами. Поддержите нас оформив заказ или порекомендовав знакомым, 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 Cores) 10GB DDR4 240GB SSD 1Gbps до декабря бесплатно при оплате на срок от полугода, заказать можно тут.

класса c применением серверов Dell R730xd Е5-2650 v4 стоимостью 9000 евро за копейки? Dell R730xd в 2 раза дешевле? Только у нас 2 х Intel Dodeca-Core Xeon E5-2650v4 128GB DDR4 6x480GB SSD 1Gbps 100 ТВ от $249 в Нидерландах и США! Читайте о том Как построить инфраструктуру корп.

Показать больше

Похожие публикации

Добавить комментарий

Ваш адрес email не будет опубликован. Обязательные поля помечены *

Кнопка «Наверх»