В информатике , символическое исполнение (также символическая оценка или symbex ) является средством анализа программы , чтобы определить , какие входы вызывают каждую часть программы выполнения . Интерпретатор следует программе, предполагая символические значения для входов , а не получение фактических входов в качестве нормального выполнения программы будет. Таким образом, он приходит к выражениям в терминах этих символов для выражений и переменных в программе и к ограничениям в терминах этих символов для возможных результатов каждой условной ветви. Наконец, возможные входы, запускающие ветвление, могут быть определены путем решения ограничений.
В области символьного моделирования та же концепция применяется к аппаратным средствам. Символическое вычисление применяет эту концепцию к анализу математических выражений.
Пример
Рассмотрим приведенную ниже программу, которая считывает значение и дает сбой, если на входе 6.
int f () { ... у = читать (); г = у * 2 ; if ( z == 12 ) { fail (); } else { printf ( "ОК" ); }}
Во время нормального выполнения («конкретное» выполнение) программа считывает конкретное входное значение (например, 5) и присваивает его y
. Затем выполнение продолжится с умножением и условной ветвью, которая будет оценивать как ложь и печатать OK
.
Во время символьного выполнения программа считывает символьное значение (например, λ
) и присваивает его y
. Программа будет затем приступить к умножению и правопреемника λ * 2
к z
. Достигнув if
утверждения, он будет оценивать λ * 2 == 12
. На этом этапе программы λ
может принимать любое значение, и поэтому символьное выполнение может продолжаться по обеим ветвям путем «разветвления» двух путей. Каждому пути назначается копия состояния программы в инструкции ветвления, а также ограничение пути. В этом примере ограничение пути предназначено λ * 2 == 12
для then
ветви и λ * 2 != 12
для else
ветви. Оба пути могут быть символически выполнены независимо. Когда пути завершаются (например, в результате выполнения fail()
или простого выхода), символьное выполнение вычисляет конкретное значение для λ
путем решения накопленных ограничений пути для каждого пути. Эти конкретные значения можно рассматривать как конкретные тестовые примеры, которые могут, например, помочь разработчикам воспроизводить ошибки. В этом примере решатель ограничений определит, что для достижения fail()
оператора λ
необходимо равное 6.
Ограничения
Путь взрыва
Символьное выполнение всех возможных программных путей не масштабируется до больших программ. Число возможных путей в программе растет экспоненциально с увеличением размера программы и даже может быть бесконечным в случае программ с неограниченными итерациями цикла. [1] В решениях проблемы взрыва пути обычно используются либо эвристики для поиска путей для увеличения покрытия кода, [2] сокращение времени выполнения за счет распараллеливания независимых путей [3], либо путем слияния аналогичных путей. [4]
Программно-зависимая эффективность
Символьное выполнение используется для рассуждений о последовательном пути к программе, что является преимуществом по сравнению с рассуждениями о программном вводе-вводе, которые используются в других парадигмах тестирования (например, динамический анализ программы ). Однако, если несколько входов проходят один и тот же путь через программу, можно получить небольшую экономию при тестировании каждого из входов по отдельности.
Псевдонимы памяти
Символьное выполнение сложнее, когда к одной и той же области памяти можно получить доступ через разные имена ( псевдонимы ). Псевдонимы не всегда распознаются статически, поэтому механизм символьного выполнения не может распознать, что изменение значения одной переменной также изменяет другую. [5]
Массивы
Поскольку массив представляет собой набор из множества различных значений, символьные исполнители должны либо обрабатывать весь массив как одно значение, либо обрабатывать каждый элемент массива как отдельное местоположение. Проблема с обработкой каждого элемента массива по отдельности заключается в том, что ссылка, такая как «A [i]», может быть указана только динамически, когда значение для i имеет конкретное значение. [5]
Взаимодействие с окружающей средой
Программы взаимодействуют со своей средой, выполняя системные вызовы , получая сигналы и т. Д. Проблемы согласованности могут возникнуть, когда выполнение достигает компонентов, которые не находятся под контролем инструмента символьного выполнения (например, ядра или библиотек). Рассмотрим следующий пример:
int main (){ ФАЙЛ * fp = fopen ( "doc.txt" ); ... if ( условие ) { fputs ( "некоторые данные" , fp ); } else { fputs ( "некоторые другие данные" , fp ); } ... данные = fgets (..., fp );}
Эта программа открывает файл и, в зависимости от некоторого условия, записывает в него данные различного типа. Затем он позже считывает записанные данные. Теоретически при символьном выполнении будут развиваться два пути в строке 5, и каждый путь оттуда будет иметь свою собственную копию файла. Таким образом, оператор в строке 11 будет возвращать данные, которые согласуются со значением «condition» в строке 5. На практике файловые операции реализованы как системные вызовы в ядре и находятся вне контроля инструмента символьного выполнения. Основные подходы к решению этой проблемы:
Выполнение обращений к среде напрямую. Преимущество такого подхода в том, что он прост в реализации. Недостатком является то, что побочные эффекты таких вызовов разрушают все состояния, управляемые механизмом символьного выполнения. В приведенном выше примере инструкция в строке 11 вернет «некоторые другие данные» или «некоторые другие данные» в зависимости от последовательного порядка состояний.
Моделирование окружающей среды. В этом случае движок инструментирует системные вызовы с помощью модели, моделирующей их эффекты и сохраняющей все побочные эффекты в хранилище для каждого состояния. Преимущество состоит в том, что можно получить правильные результаты при символическом выполнении программ, взаимодействующих с окружающей средой. Недостатком является необходимость реализации и поддержки множества потенциально сложных моделей системных вызовов. Такие инструменты, как KLEE, [6] Cloud9 и Otter [7], используют этот подход, реализуя модели для операций файловой системы, сокетов, IPC и т. Д.
Разветвляется состояние всей системы. Инструменты символьного выполнения, основанные на виртуальных машинах, решают проблему среды, разветвляя все состояние виртуальной машины. Например, в S2E [8] каждое состояние является независимым моментальным снимком виртуальной машины, который может выполняться отдельно. Такой подход устраняет необходимость в написании и сопровождении сложных моделей и позволяет символьно выполнять практически любую двоичную программу. Однако у него более высокие накладные расходы на использование памяти (снимки виртуальной машины могут быть большими).
Инструменты
Инструмент | Цель | URL | Кто-нибудь может его использовать / Открытый исходный код / Загружаемый |
---|---|---|---|
сердитый | на основе libVEX (поддержка x86, x86-64, ARM, AARCH64, MIPS, MIPS64, PPC, PPC64 и Java) | http://angr.io/ | да |
BE-PUM | x86 | https://github.com/NMHai/BE-PUM | да |
BINSEC | x86, ARM, RISC-V (32 бит) | http://binsec.github.io | да |
тигель | LLVM, JVM и т. Д. | https://github.com/GaloisInc/crucible | да |
Разоблачать | JavaScript | https://github.com/ExpoSEJS/ExpoSE | да |
FuzzBALL | VineIL / Родной | http://bitblaze.cs.berkeley.edu/fuzzball.html | да |
Джаланги2 | JavaScript | https://github.com/Samsung/jalangi2 | да |
janala2 | Ява | https://github.com/ksen007/janala2 | да |
JaVerT | JavaScript | https://www.doc.ic.ac.uk/~pg/publications/FragosoSantos2019JaVerT.pdf | да |
JBSE | Ява | https://github.com/pietrobraione/jbse | да |
jCUTE | Ява | https://github.com/osl/jcute | да |
JPF | Ява | http://babelfish.arc.nasa.gov/trac/jpf | да |
Ключ | Ява | http://www.key-project.org/ | да |
летающий змей | LLVM | http://www.cs.ubc.ca/labs/isd/Projects/Kite/ | да |
KLEE | LLVM | https://klee.github.io/ | да |
Кудзу | JavaScript | http://webblaze.cs.berkeley.edu/2010/kudzu/kudzu.pdf | нет |
MPro | Виртуальная машина Ethereum (EVM) / Собственная | https://sites.google.com/view/smartcontract-analysis/home | да |
Мантикора | x86-64, ARMv7, виртуальная машина Ethereum (EVM) / собственная | https://github.com/trailofbits/manticore/ | да |
Погром | Двоичный | http://forallsecure.com | нет |
Мифрил-Классик | Виртуальная машина Ethereum (EVM) / Собственная | https://github.com/ConsenSys/mythril-classic | да |
Выдра | C | https://bitbucket.org/khooyp/otter/overview | да |
Ойенте-НГ | Виртуальная машина Ethereum (EVM) / Собственная | http://www.comp.ita.br/labsca/waiaf/papers/RafaelShigemura_paper_16.pdf | нет |
Pathgrind [9] | Родной 32-битный на основе Valgrind | https://github.com/codelion/pathgrind | да |
Pex | .NET Framework | http://research.microsoft.com/en-us/projects/pex/ | нет |
пысымему | x86-64 / Собственный | https://github.com/feliam/pysymemu/ | да |
Розетка | Диалект ракетки | https://emina.github.io/rosette/ | да |
Рубикс | Рубин | http://www.cs.umd.edu/~avik/papers/ssarorwa.pdf | нет |
S2E | x86, x86-64, ARM / User и двоичные файлы режима ядра | http://s2e.systems/ | да |
Символьный Навигатор (SPF) | Байт-код Java | https://github.com/SymbolicPathFinder | да |
SymDroid | Байт-код Dalvik | http://www.cs.umd.edu/~jfoster/papers/symdroid.pdf | нет |
SymJS | JavaScript | http://www.cs.utah.edu/~ligd/publications/SymJS-FSE14.pdf | нет |
Тритон | x86 и x86-64 | https://triton.quarkslab.com | да |
Verifast | C, Java | https://people.cs.kuleuven.be/~bart.jacobs/verifast | да |
Ранние версии инструментов
- EXE [10] - это более ранняя версия KLEE. Бумагу EXE можно найти здесь .
История
Концепция символического исполнения была введена академически с описаниями: системы Select [11] системы EFFIGY, [12] системы DISSECT [13] и системы Кларка. [14] См. Библиографию других опубликованных технических статей по символической казни.
Смотрите также
- Абстрактная интерпретация
- Символьное моделирование
- Символьное вычисление
- Конколическое тестирование
- График потока управления
- Динамическая перекомпиляция
Рекомендации
- ^ Ананд, Saswat; Патрис Годфройд; Николай Тильманн (2008). «Композиционное символическое исполнение по требованию». Инструменты и алгоритмы построения и анализа систем . Конспект лекций по информатике. 4963 . С. 367–381. DOI : 10.1007 / 978-3-540-78800-3_28 . ISBN 978-3-540-78799-0.
- ^ Ма, Кин-Кенг; Кху Йит Панг; Джеффри С. Фостер; Майкл Хикс (2011). «Направленное символическое исполнение» . Материалы 18-й Международной конференции по статистическому анализу . С. 95–111. ISBN 9783642237010. Проверено 3 апреля 2013 .
- ^ Staats, Мэтт; Корина Пасаряну (2010). «Параллельное символьное выполнение для генерации структурных тестов». Материалы 19-го Международного симпозиума по тестированию и анализу программного обеспечения . С. 183–194. DOI : 10.1145 / 1831708.1831732 . ISBN 9781605588230. S2CID 9898522 .
- ^ Кузнецов, Владимир; Киндер, Йоханнес; Букур, Стефан; Кандеа, Джордж (2012-01-01). «Эффективное слияние состояний в символическом исполнении». Труды 33-й конференции ACM SIGPLAN по проектированию и реализации языков программирования . Нью-Йорк, Нью-Йорк, США: ACM. С. 193–204. CiteSeerX 10.1.1.348.823 . DOI : 10.1145 / 2254064.2254088 . ISBN 978-1-4503-1205-9. S2CID 135107 .
- ^ а б ДеМилло, Рич; Оффатт, Джефф (1991-09-01). «Автоматическая генерация тестовых данных на основе ограничений». IEEE Transactions по разработке программного обеспечения . 17 (9): 900–910. DOI : 10.1109 / 32.92910 .
- ^ Кадар, Кристиан; Данбар, Дэниел; Энглер, Доусон (01.01.2008). "KLEE: Автоматическое и автоматическое создание тестов с высоким уровнем покрытия для сложных системных программ" . Труды 8-й конференции USENIX по проектированию и внедрению операционных систем . OSDI'08: 209–224.
- ^ Терпи, Джонатан; Рейснер, Эльнатан; Фостер, Джеффри; Хикс, Майкл. «MultiOtter: многопроцессное символьное исполнение» (PDF) .
- ^ Чипунов, Виталий; Кузнецов, Владимир; Кандеа, Джордж (2012-02-01). «Платформа S2E: дизайн, реализация и приложения». ACM Trans. Comput. Syst . 30 (1): 2: 1-2: 49. DOI : 10.1145 / 2110356.2110358 . ISSN 0734-2071 . S2CID 16905399 .
- ^ Шарма, Асанкхая (2014). «Использование неопределенного поведения для эффективного символьного исполнения». ICSE Companion 2014: Материалы 36-й Международной конференции по разработке программного обеспечения . С. 727–729. DOI : 10.1145 / 2591062.2594450 . ISBN 9781450327688. S2CID 10092664 .
- ^ Кадар, Кристиан; Ганеш, Виджай; Павловский, Питер М .; Dill, David L .; Энглер, Доусон Р. (2008). «EXE: автоматическое создание входов смерти». ACM Trans. Инф. Syst. Secur . 12 : 10: 1–10: 38. DOI : 10.1145 / 1455518.1455522 . S2CID 10905673 .
- ^ Роберт С. Бойер и Бернард Элспас и Карл Н. Левитт SELECT - формальная система для тестирования и отладки программ путем символического выполнения, Труды Международной конференции по надежному программному обеспечению, 1975, стр. 234-245, Лос-Анджелес, Калифорния
- ^ Джеймс К. Кинг, Символическое исполнение и тестирование программы, Коммуникации ACM, том 19, номер 7, 1976, 385-394
- ^ Уильям Э. Хауден, Эксперименты с системой символической оценки, Труды, Национальная компьютерная конференция, 1976.
- ^ Лори А. Кларк, Система тестирования программ, ACM 76: Proceedings of the Annual Conference, 1976, стр. 488-491, Хьюстон, Техас, США
Внешние ссылки
- Символическое выполнение для поиска ошибок
- Презентация символического исполнения и тестирования программного обеспечения в НАСА в Эймсе
- Символическое выполнение для тестирования программного обеспечения на практике - предварительная оценка