Массачусетский Институт Технологий.
Курс лекций №6.858. «Безопасность компьютерных систем».
Николай Зельдович, Джеймс Микенс.
2014 год Безопасность компьютерных систем — это курс, посвященный проектированию и внедрению безопасных компьютерных систем.
Лекции охватывают модели угроз, атаки, ставящие под угрозу безопасность, а также методы обеспечения безопасности, основанные на последних научных работах.
Темы включают безопасность операционной системы (ОС), возможности, управление информационными потоками, языковую безопасность, сетевые протоколы, аппаратную безопасность и безопасность веб-приложений.
Лекция 1: «Введение: модели угроз» Часть 1 / Часть 2 / Часть 3 Лекция 2: «Контроль хакерских атак» Часть 1 / Часть 2 / Часть 3 Лекция 3: «Переполнение буфера: эксплойты и защита» Часть 1 / Часть 2 / Часть 3 Лекция 4: «Разделение привилегий» Часть 1 / Часть 2 / Часть 3 Лекция 5: «Откуда берутся ошибки системы безопасности» Часть 1 / Часть 2 Лекция 6: «Возможности» Часть 1 / Часть 2 / Часть 3 Лекция 7: «Нативная клиентская песочница» Часть 1 / Часть 2 / Часть 3 Лекция 8: «Модель сетевой безопасности» Часть 1 / Часть 2 / Часть 3 Лекция 9: «Безопасность веб-приложений» Часть 1 / Часть 2 / Часть 3 Лекция 10: Символическое исполнение Часть 1 / Часть 2 / Часть 3 Теперь, пройдя по ветке вниз, мы видим выражение t = y. Поскольку мы рассматриваем один путь за раз, нам не обязательно вводить новую переменную для t. Мы можем просто сказать, что поскольку t = y, то t больше не равно 0. Продолжаем двигаться вниз и доходим до точки, где натыкаемся на другую ветку.
Какое новое предположение мы должны сделать, чтобы идти дальше по этому пути? Это предположение, что т < y.
Что такое т? Если мы посмотрим на правую ветвь, мы увидим, что t = y. А в нашей таблице T=y и Y=y. Из этого логически следует, что наше ограничение имеет вид y < y, which cannot be the case. 
Так что у нас все было в порядке, пока мы не дошли до этого момента.
< y. Until we get to the false statement, all our inequalities must be correct. But this does not work, because when performing tasks on the right branch, we have a logical inconsistency. У нас есть то, что часто называют условием пути.
Это условие должно быть истинным, чтобы программа могла следовать по этому пути.
Но мы знаем, что это условие не может быть выполнено, поэтому программа не может пойти по этому пути.
Итак, этот путь теперь полностью устранен, и мы знаем, что по этому правильному пути идти нельзя.
А как насчет другого способа? Попробуем пройти левую ветку по другому пути.
Каковы будут условия этого пути? Опять же, наше символическое состояние начинается с t = 0, а X и Y равны переменным x и y. 
Как теперь выглядит ограничение пути в этом случае? Обозначим левую ветвь как True, а правую — как False, а затем рассмотрим значение t = x. В результате логической обработки условий t = x, x > y и t < y, we obtain that we simultaneously have the fact that x > у и х < y. 
Совершенно очевидно, что такое условие пути является неудовлетворительным.
Мы не можем иметь x, который одновременно больше и меньше y. Не существует присваивания X, удовлетворяющего обоим ограничениям.
Это говорит нам о том, что другой путь также неудовлетворителен.
Получается, что на данный момент мы исследовали все возможные пути в программе, которые могли бы привести нас к этому состоянию.
Мы действительно можем установить и проверить, что не существует никакого возможного пути, который привел бы нас к ложному утверждению.
Аудитория: Этот пример показал, что вы изучили ход программы по всем возможным ветвям.
Но одно из преимуществ символического выполнения состоит в том, что нам не нужно исследовать все возможные экспоненциальные пути.
Так как же нам избежать этого в этом примере? Профессор: Это очень хороший вопрос.
Здесь вы делаете компромисс между символическим исполнением и тем, насколько конкретным вы хотите быть.
Таким образом, в этом случае мы не используем символическое выполнение так часто, как в первый раз, когда мы смотрели на выполнение программы по обеим ветвям одновременно.
Но благодаря этому наши ограничения стали очень и очень простыми.
Отдельные ограничения «один путь за другим» очень просты, но вам придется делать это снова и снова, исследуя все существующие ветки и экспоненциально все возможные пути.
Существует экспоненциально много путей, но для каждого пути в целом существует также экспоненциально большой набор входных данных, которые могут идти по этому пути.
Так что это уже дает вам большое преимущество, потому что вместо того, чтобы пробовать все возможные входные данные, вы пробуете все возможные пути.
Но можете ли вы сделать что-нибудь лучше? Это одна из областей, где было проведено много экспериментов с символическим выполнением, например, с одновременным выполнением нескольких путей.
В материалах лекций вы познакомились с эвристикой и набором стратегий, которые экспериментаторы использовали, чтобы сделать поиск более удобным.
Например, они исследуют один путь за другим, но не делают это полностью вслепую.
Они проверяют условия пути после каждого сделанного шага.
Предположим, что здесь в нашей программе вместо «ложного» оператора будет сложное дерево программ, граф потока управления.
Вам не нужно ждать, пока вы дойдете до самого конца, чтобы убедиться, что путь осуществим.
В тот момент, когда вы достигнете состояния t < y, you already know that this path is unsatisfactory and you will never go in this direction. Therefore, cutting off incorrect branches at the beginning of the program reduces the amount of empirical work. Intelligent path exploration prevents the possibility of program failure later on. A lot of practical tools in use today first start with random testing to get an initial set of paths, after which they start exploring paths in the neighborhood. They consider the many possible executions of the program along each branch, wondering what happens along those paths. Это особенно полезно, если у нас есть хороший набор тестов.
Вы запускаете тест и обнаруживаете, что этот фрагмент кода не выполняется.
Итак, вы можете выбрать путь, наиболее близкий к реализации кода, и спросить, можете ли вы изменить этот путь, чтобы идти в нужном вам направлении? 
Но в тот момент, когда вы пытаетесь пройти все пути одновременно, начинаются ограничения, которые становится сложно решить.
Итак, вы можете выполнять одну функцию за раз и исследовать все пути в функции вместе.
Если вы попытаетесь создавать большие блоки, вы, как правило, сможете исследовать все возможные пути.
Самое важное заключается в том, что для каждой ветви вы проверяете свои ограничения и устанавливаете, может ли эта ветвь действительно идти в обе стороны.
Если она не может пойти обоими путями, вы сэкономите время и силы, не идя в том направлении, куда она идти не может. Кроме того, я не помню конкретных стратегий, которые они используют для поиска путей, которые с большей вероятностью дадут очень хороший результат. Но обрезать неправильные ветки на начальном этапе очень важно.
До сих пор мы в основном говорили об игрушечном коде, целочисленных переменных, ветвях и очень простых вещах.
Но что происходит, когда у вас более сложная программа? В частности, что происходит, когда у вас есть программа, включающая кучу? 
Исторически сложилось так, что «куча» была проклятием любого анализа программ, потому что чистые и элегантные вещи времен Фортрана полностью разрушались, когда вы пытались запустить их с программами, написанными на C, где вы распределяли память слева и справа.
Вот вам и перекрытия и вся та ерунда, которая возникает при запуске программы с выделенной памятью и арифметикой указателей.
Это одна из областей, где символическое выполнение обладает замечательной способностью рассуждать о программах.
Итак, как мы это сделаем? Давайте на мгновение забудем о ветках и потоке управления.
У нас есть простая программа.
Он выделяет часть памяти, сбрасывает ее и получает новый указатель y из указателя x. Затем он что-то записывает в y и проверяет, равно ли значение, хранящееся в указателе y, значению, хранящемуся в указателе x? Основываясь на базовых знаниях C, вы можете видеть, что эта проверка не удалась, поскольку x установлен в ноль, а y=25, поэтому x указывает на другое местоположение.
Пока что у нас все хорошо.
То, как мы будем моделировать кучу, и то, как куча моделируется в большинстве систем, заключается в использовании представления кучи на языке C, где это просто гигантская база адресов, гигантский массив, в котором вы можете разместить свои данные.
Это означает, что мы можем думать о нашей программе как об очень большом глобальном наборе данных, который будет называться MEM. Это массив, который по сути будет сопоставлять адреса со значениями.
Адрес — это всего лишь 64-битное значение.
Что произойдет после того, как вы прочитаете что-нибудь с этого адреса? Это зависит от того, как вы моделируете память.
Если вы смоделируете это на уровне байта, вы получите байт. Если вы смоделируете это на уровне слова, вы получите слово.
В зависимости от типа ошибок, которые вас интересуют, и от того, заботитесь ли вы о распределении памяти или нет, вы будете моделировать ее немного по-другому, но обычно память — это просто массив от адреса до значения.
Таким образом, адрес представляет собой просто целое число.
В некотором смысле не имеет значения, что C думает об адресе, это просто целое 64-битное или 32-битное число, в зависимости от вашей машины.
Это просто значение, которое индексируется в эту память.
И то, что вы можете поместить в память, вы можете прочитать из этой памяти.
Таким образом, такие вещи, как арифметика указателей, просто становятся целочисленной арифметикой.
На практике здесь нет особых сложностей, поскольку в C арифметика указателей знает типы указателей, и они будут увеличиваться пропорционально размеру.
В результате мы получим следующую строку:
у = х + 10; размер(целое) 
Но что действительно важно, так это то, что происходит, когда вы записываете в память и читаете из памяти.
Основываясь на указателе, что y нужно записать в 25, я беру массив памяти и индексирую его с помощью y. И я записываю 25 в эту ячейку памяти.
Затем я перехожу к оператору MEM[y] = = MEM[x], считываю значение из ячейки y в памяти, считываю значение из ячейки x в памяти и сравниваю их друг с другом.
Вот как я проверяю, совпадают они или нет. Это очень простое предположение, позволяющее перейти от программы, использующей кучу, к программе, использующей этот гигантский глобальный массив, представляющий память.
Это означает, что теперь, когда вы говорите о программах, управляющих кучей, вам фактически не нужно говорить о программах, управляющих кучей.
Вы будете в порядке, если сможете говорить о массивах, а не о кучах.
Вот еще один простой вопрос.
А как насчет функции malloc? Вы можете просто использовать реализацию malloc на языке C, отслеживать все выделенные страницы, отслеживать все, что было освобождено, просто иметь свободный список, и этого достаточно.
Оказывается, для многих целей и для многих типов ошибок не обязательно, чтобы malloc был сложным.
Фактически, вы можете перейти от malloc, который выглядит так: x= malloc(sizeof(int)*100), к malloc, который выглядит так: ПОС = 1 Int malloc(int n){ рв = ПОС ПОС+=n; } Это просто говорит: «Я собираюсь сохранить счетчик следующего свободного места в памяти, и всякий раз, когда кто-то запрашивает адрес, я даю ему это местоположение и увеличиваю эту позицию, а затем возвращаю rv».
Это полностью игнорирует то, что такое malloc в традиционном смысле.
Освобождения памяти в этом случае не происходит. Функция просто продолжает двигаться всё дальше и дальше по памяти, и всё, без всякого освобождения.
Его также не волнует, что существуют области памяти, в которые не следует производить запись, поскольку существуют специальные адреса, имеющие особое значение и зарезервированные для операционной системы.
Он не моделирует ничего, что затрудняло бы написание malloc, а только на определенном уровне абстракции, когда вы пытаетесь рассуждать о каком-то сложном коде, манипулирующем указателями.
При этом вас не заботит освобождение памяти, но вас волнует, будет ли программа, например, писать за пределами некоторого буфера, и в этом случае эта функция malloc может быть весьма хороша.
И это на самом деле происходит очень и очень часто, когда вы выполняете символическое выполнение реального кода.
Очень важным шагом является моделирование функций вашей библиотеки.
То, как вы моделируете библиотечные функции, окажет огромное влияние на производительность и масштабируемость анализа, но также повлияет на точность.
Так что, если у вас есть такая «игрушечная» модель malloc, она будет очень быстрой, но в ней будут возникать определенные виды ошибок, которые вы не сможете заметить.
Например, в этой модели я полностью игнорирую распределение, поэтому могу получить ошибку, если кто-то получит доступ к нераспределенному пространству.
Так что в реальной жизни я никогда не буду использовать эту модель malloc Микки Мауса.
Так что это всегда баланс между аналитической точностью и эффективностью.
И чем сложнее становятся модели стандартных функций, таких как malloc, тем менее масштабируемым оказывается их анализ.
Но для некоторых классов ошибок вам понадобятся эти простые модели.
Поэтому большое значение имеют различные библиотеки на языке Си, которые нужны для того, чтобы понять, что же на самом деле делает программа.
Таким образом, мы уменьшили проблему рассуждений о куче, рассуждая о программе с массивами, но я еще не рассказал вам, как рассуждать о программе с массивами.
Оказывается, большинство решателей SMT поддерживают теорию массивов.
Идея состоит в том, что если a — это какой-то массив, то существует некоторая запись, которая позволяет вам взять этот массив и создать новый массив, в котором местоположение i обновляется до значения e. Ясно?
Итак, если у меня есть массив a, и я выполняю эту операцию обновления, а затем пытаюсь прочитать значение k, это означает, что значение k будет равно значению k в массиве a, если k отличается от i, и оно будет быть равным е.
если k равно i. Обновление массива означает взятие старого массива и обновление его новым массивом.
Хорошо, если у вас есть формула, основанная на теории массивов, поэтому я начал с нулевого массива, который состоит только из нулей.
Затем я записываю 5 в ячейку i и 7 в ячейку j, после чего читаю из k и проверяю, равно оно 5 или нет. Затем это можно расширить, используя определение чего-то, в котором говорится, например: «если k равно i и k равно y, причем k отличается от j, тогда да, оно будет равно 5, в противном случае оно будет равно 5».
не быть равным 5".
И на практике решатели SMT не просто расширяют это до набора логических формул, они используют эту стратегию перемещения вперед и назад между решателем SAT и механизмом, который может рассуждать о теории массивов для выполнения работы.
Важно то, что, полагаясь на эту теорию массивов и используя ту же стратегию, которую мы использовали для генерации формул для целых чисел, мы действительно можем генерировать формулы, включающие логику массива, обновления массива, оси массива, итерацию массива.
И пока вы корректируете свой путь, эти формулы очень легко сгенерировать.
Если вы не исправляете свои пути, а хотите создать формулу, которая будет соответствовать программе по всем путям, то это тоже относительно просто.
Единственное, вам придется иметь дело с особым видом циклов.
Словари и карты также очень легко моделировать с помощью неопределенных функций.
На самом деле сама теория массивов — это всего лишь частный случай неопределенной функции.
С помощью таких функций можно делать и более сложные вещи.
Современный решатель SMT имеет встроенную поддержку рассуждений о множествах и операций с множествами, что может быть очень полезно, если вы рассуждаете о программе, которая включает в себя вычисление множеств.
При разработке одного из этих инструментов очень важен этап моделирования.
И речь идет не только о том, как вы моделируете сложные функции программного обеспечения в соответствии с вашими теориями, например, о преобразовании кучи в массивы.
Это также вопрос того, какие теории и решатели вы используете.
Существует большое количество теорий и решателей с различными соотношениями, для которых необходимо найти разумный компромисс между эффективностью и стоимостью.
Большинство практических инструментов придерживаются теории битовых векторов и при необходимости могут использовать теорию массивов для моделирования кучи.
В целом практические инструменты стараются избегать более сложных теорий, таких как теория множеств.
Это связано с тем, что в некоторых случаях они имеют тенденцию быть менее масштабируемыми, если только вы не имеете дело с программой, для запуска которой фактически требуются именно такие инструменты.
Аудитория: Помимо изучения символического исполнения, на чем разработчики сосредотачивают свое внимание? Профессор: Еще одна очень активная область исследований — приложения и поиск моделей программного обеспечения, которые позволят выявлять новые типы ошибок.
Например, Николай, Франц и Си Ван в прошлогодних лекциях обсуждали использование символьного выполнения для программ, которые невозможно оптимизировать с помощью компилятора.
Речь шла о проверках безопасности, которые можно было оптимизировать без компилятора.
Так что это сильно отличается от вопроса, пойдет ли программа по этому пути или нет. Но есть этап моделирования, который позволяет вам перейти от концептуального вопроса высокого уровня о том, есть ли в вашей программе код, который можно скомпилировать, к алгоритму, основанному на символьном выполнении, который может легко определить, может ли программа следовать по определенному пути.
и возможен ли этот конкретный путь.
Оказывается, приложения — это большая область, расширяющаяся до новых классов ошибок, до новых возможностей разных языков программирования.
Например, одна из вещей, которую до сих пор довольно сложно моделировать с помощью символьного выполнения, — это языки очень высокого уровня, такие как JavaScript или Python, где имеется множество очень динамичных языковых функций.
Но в то же время практически любую программу можно адаптировать для символьного исполнения, и это, безусловно, очень хорошо.
Пару лет назад мы использовали символическое выполнение для выявления ошибок в задачах программирования на Python. Итак, при символическом выполнении часть проблемы заключается в том, что ваше символическое состояние не позволяет вам просто сказать: «Хорошо, я выполню эту инструкцию, а затем эту инструкцию, а затем эту инструкцию».
Нет никакой последовательности.
Например, несколько лет назад мы рассматривали очень маленькие, но очень важные фрагменты кода, которые содержали соответствующую структуру данных в операционной системе, или разблокированную структуру данных, или моделировали взаимодействие между потоками.
По сути, каждый раз, когда существует переменная, которую можно перезаписать каким-либо другим значением, вы просто заменяете ее значение новым символьным значением и создаете ограничения, которые применяются к этим символьным значениям и к символьным значениям в других потоках.
Это даже использовалось, чтобы говорить о таких вещах, как отсутствие границ памяти, с очень небольшим увеличением сложности.
Условно говоря, то, что вы больше не можете сделать в масштабе Microsoft Word, вы можете сделать в масштабе, например, параллельной структуры данных.
Были и другие работы в контексте параллелизма, например, можно ли использовать символическое выполнение для восстановления неправильного чередования на основе знания того, как вела себя программа при этом.
Это открывает множество возможностей, поскольку позволяет вам задавать конкретные вопросы о пути программы.
Символическое выполнение позволяет задать вопрос, какие значения должны иметь эти вещи, чтобы программа что-то сделала или чтобы что-то произошло.
Это очень мощная функция, и на ее основе было протестировано множество приложений.
Но это достаточно новая технология, как и технология анализа выполнения программ.
Доступна полная версия курса Здесь .
Спасибо, что остаетесь с нами.
Вам нравятся наши статьи? Хотите увидеть больше интересных материалов? Поддержите нас, разместив заказ или порекомендовав друзьям, Скидка 30% для пользователей Хабра на уникальный аналог серверов начального уровня, который мы придумали для вас: Вся правда о VPS (KVM) E5-2650 v4 (6 Cores) 10GB DDR4 240GB SSD 1Gbps от 20$ или как правильно расшарить сервер? (доступны варианты с RAID1 и RAID10, до 24 ядер и до 40 ГБ DDR4).
VPS (KVM) E5-2650 v4 (6 ядер) 10 ГБ DDR4 240 ГБ SSD 1 Гбит/с бесплатно до декабря при оплате на срок от шести месяцев и более вы можете заказать здесь .
Dell R730xd в 2 раза дешевле? Только здесь 2 x Intel Dodeca-Core Xeon E5-2650v4 128 ГБ DDR4 6x480 ГБ SSD 1 Гбит/с 100 ТВ от 249 долларов США в Нидерландах и США! Прочтите об этом Как построить корпоративную инфраструктуру класса, используя серверы Dell R730xd E5-2650 v4 стоимостью 9000 евро за копейки? Теги: #информационная безопасность #программирование #ИТ-инфраструктура #Анализ и проектирование систем #SMT #Символическое исполнение #Символическое исполнение #Символическое исполнение #Теория массивов TOA #Теория массивов TOA #Теория неинтерпретируемых функций #Теория неинтерпретируемых функций #Решатели SAT #Решатели SAT
-
Обзор Asus Eeepc 1201Ha
19 Oct, 24 -
Я, Пират (Главы 3–5)
19 Oct, 24 -
Работа С Сенсорным Экраном На Arduino Due
19 Oct, 24 -
В Один Из Последних Июльских Вечеров...
19 Oct, 24
