Конколическое тестирование
Конколическое тестирование ( сочетание конкретного конкретному и символического исполнения , также известное как динамическое символическое выполнение ) — это гибридный проверки программного обеспечения метод , который выполняет символическое выполнение , классический метод, который рассматривает программные переменные как символические переменные по пути выполнения ( тестирования на определенных входных данных). . Символическое выполнение используется в сочетании с автоматизированным средством доказательства теорем или решателем ограничений, основанным на программировании логики ограничений, для генерации новых конкретных входных данных (тестовых примеров) с целью максимизации покрытия кода . Его основная задача — поиск ошибок в реальном программном обеспечении, а не демонстрация корректности программы.
Описание и обсуждение концепции были представлены в книге «DART: Направленное автоматизированное случайное тестирование» Патриса Годфруа, Нильса Кларлунда и Кошика Сена. [1] Статья «CUTE: Механизм модульного тестирования concolic для C», [2] Кошик Сен, Дарко Маринов и Гул Ага расширили эту идею на структуры данных и впервые ввели термин « конколическое тестирование» . Другой инструмент, названный EGT (переименованный в EXE, а затем улучшенный и переименованный в KLEE), основанный на аналогичных идеях, был независимо разработан Кристианом Кадаром и Доусоном Энглером в 2005 году и опубликован в 2005 и 2006 годах. [3] PathCrawler [4] [5] впервые предложил выполнять символическое выполнение по конкретному пути выполнения, но в отличие от concolic-тестирования PathCrawler не упрощает сложные символические ограничения с использованием конкретных значений. Эти инструменты (DART и CUTE, EXE) применяли конколическое тестирование к модульному тестированию программ на языке C , а конколическое тестирование изначально задумывалось как улучшение «белого ящика» по сравнению с устоявшимися методологиями случайного тестирования . Позже этот метод был распространен на тестирование многопоточных Java с помощью jCUTE. программ [6] и программы модульного тестирования из их исполняемых кодов (инструмент OSMOSE). [7] Оно также было объединено с нечетким тестированием и расширено для обнаружения уязвимостей безопасности в крупномасштабных двоичных файлах x86 компанией Microsoft Research . SAGE от [8] [9]
Конколический подход также применим для проверки моделей . В средстве проверки модели concolic средство проверки модели проходит состояния модели, представляющей проверяемое программное обеспечение, сохраняя при этом как конкретное состояние, так и символическое состояние. Символическое состояние используется для проверки свойств программного обеспечения, а конкретное состояние используется, чтобы избежать достижения недостижимого состояния. Одним из таких инструментов является ExpliSAT, разработанный Шэрон Барнер, Синди Эйснер, Зивом Глазбергом, Дэниелом Крёнингом и Ишаем Рабиновицем. [10]
Рождение конколик-теста
[ редактировать ]Реализация традиционного тестирования, основанного на символьном выполнении, требует реализации полноценного символьного интерпретатора языка программирования. Разработчики тестирования Concolic заметили, что реализации полноценного символьного выполнения можно избежать, если символическое выполнение можно совмещать с обычным выполнением программы посредством инструментирования . Эта идея упрощения реализации символического выполнения породила конколическое тестирование.
Разработка решателей SMT
[ редактировать ]Важной причиной роста популярности concolic-тестирования (и, в более общем плане, анализа программ, основанного на символическом выполнении) за десятилетие с момента его появления в 2005 году является резкое улучшение эффективности и выразительности SMT Solvers . Ключевые технические разработки, которые приводят к быстрому развитию решателей SMT, включают сочетание теорий, ленивое решение, DPLL(T) и огромные улучшения скорости решателей SAT . Решатели SMT, специально предназначенные для concolic-тестирования, включают Z3 , STP, Z3str2 и Boolector .
Пример
[ редактировать ]Рассмотрим следующий простой пример, написанный на C:
void f ( int x , int y ) { int z знак равно 2 * y ; если ( Икс == 100000 ) { если ( Икс < z ) { утверждать ( 0 ); /* ошибка */ } } } 
Простое случайное тестирование, в котором проверяются случайные значения x и y , потребует непрактично большого количества тестов для воспроизведения сбоя.
Мы начинаем с произвольного выбора x и y , например x = y = 1. В конкретном выполнении строка 2 устанавливает z равным 2, а тест в строке 3 завершается неудачно, поскольку 1 ≠ 100000. Одновременно символическое выполнение следует за тот же путь, но рассматривает x и y как символические переменные. Он присваивает z выражение 2 y и отмечает, что, поскольку тест в строке 3 не пройден, x ≠ 100000. Это неравенство называется условием пути и должно быть истинным для всех выполнения, следующих по тому же пути выполнения, что и текущее.
Поскольку мы хотим, чтобы при следующем запуске программа следовала по другому пути выполнения, мы берем последнее встретившееся условие пути, x ≠ 100000, и инвертируем его, получая x = 100000. Затем вызывается автоматизированное средство доказательства теорем, чтобы найти значения для входные переменные x и y заданы полным набором значений символических переменных и условий пути, созданных во время символьного выполнения. В этом случае действительным ответом средства доказательства теоремы может быть x = 100000, y = 0.
Запуск программы на этом входе позволяет ей достичь внутренней ветви в строке 4, которая не используется, поскольку 100000 ( x ) не меньше 0 ( z = 2 y ). Условия пути: x = 100000 и x ≥ z . Последнее отменяется, давая x < z . Затем средство доказательства теорем ищет x , y, удовлетворяющие условиям x = 100000, x < z и z = 2 y ; например, x = 100000, y = 50001. Этот ввод достигает ошибки.
Алгоритм
[ редактировать ]По сути, алгоритм конколик-тестирования работает следующим образом:
- Классифицируйте определенный набор переменных как входные переменные . Эти переменные будут рассматриваться как символические переменные во время символьного выполнения. Все остальные переменные будут рассматриваться как конкретные значения.
- Инструментируйте программу так, чтобы каждая операция, которая может повлиять на значение символической переменной или условие пути, записывалась в файл трассировки, а также любая возникающая ошибка.
- Для начала выберите произвольный вход.
- Выполните программу.
- Символически повторно выполнить программу на трассировке, создав набор символических ограничений (включая условия пути).
- Отмените последнее условие пути, которое еще не было отменено, чтобы перейти к новому пути выполнения. Если такого условия пути нет, алгоритм завершает работу.
- Вызовите автоматический решатель выполнимости для нового набора условий пути, чтобы сгенерировать новые входные данные. Если нет входных данных, удовлетворяющих ограничениям, вернитесь к шагу 6, чтобы попробовать следующий путь выполнения.
- Вернитесь к шагу 4.
Вышеописанная процедура имеет несколько осложнений:
- Алгоритм выполняет поиск в глубину по неявному дереву возможных путей выполнения. На практике программы могут иметь очень большие или бесконечные деревья путей — типичным примером является тестирование структур данных, которые имеют неограниченный размер или длину. Чтобы не тратить слишком много времени на одну небольшую область программы, поиск может быть ограничен по глубине (ограничен).
- Символьное выполнение и автоматизированные средства доказательства теорем имеют ограничения на классы ограничений, которые они могут представлять и решать. Например, средство доказательства теорем, основанное на линейной арифметике, не сможет справиться с условием нелинейного пути xy = 6. Каждый раз, когда возникают такие ограничения, символическое выполнение может заменить текущее конкретное значение одной из переменных, чтобы упростить задачу. Важной частью разработки системы тестирования concolic является выбор символического представления, достаточно точного для представления интересующих ограничений.
Коммерческий успех
[ редактировать ]Анализ и тестирование, основанные на символическом выполнении, в целом вызвали значительный интерес со стороны промышленности. [ нужна ссылка ] . Пожалуй, самым известным коммерческим инструментом, использующим динамическое символьное выполнение (также известное как concolic-тестирование), является инструмент SAGE от Microsoft. Инструменты KLEE и S2E (оба являются инструментами с открытым исходным кодом и используют решатель ограничений STP) широко используются во многих компаниях, включая Micro Focus Fortify, NVIDIA и IBM. [ нужна ссылка ] . Эти технологии все чаще используются многими охранными компаниями и хакерами для поиска уязвимостей безопасности.
Ограничения
[ редактировать ]Конколик-тест имеет ряд ограничений:
- Если программа демонстрирует недетерминированное поведение, она может следовать по пути, отличному от запланированного. Это может привести к прекращению поиска и плохому охвату.
- Даже в детерминированной программе ряд факторов может привести к плохому покрытию, включая неточные символические представления, неполное доказательство теорем и неспособность найти наиболее плодотворную часть большого или бесконечного дерева путей.
- Программы, которые тщательно перемешивают состояния своих переменных, например криптографические примитивы, генерируют очень большие символьные представления, которые невозможно решить на практике. Например, условие
if(sha256_hash(input) == 0x12345678) { ... }требует, чтобы средство доказательства теорем инвертировало SHA256 , что является открытой проблемой.
Инструменты
[ редактировать ]- pathcrawler-online.com — это ограниченная версия текущего инструмента PathCrawler, который общедоступен в качестве онлайн-сервера тестовых сценариев для оценочных и образовательных целей.
- jCUTE доступен в виде двоичного кода по лицензии Urbana-Champaign только для исследовательского использования для Java .
- CREST — это решение с открытым исходным кодом для C, которое заменило [11] CUTE ( модифицированная лицензия BSD ).
- KLEE — это решение с открытым исходным кодом, построенное на базе инфраструктуры LLVM ( лицензия UIUC ).
- CATG — это решение с открытым исходным кодом для Java ( лицензия BSD ).
- Jalangi — это инструмент concolic тестирования и символического выполнения с открытым исходным кодом для JavaScript. Jalangi поддерживает целые числа и строки.
- Microsoft Pex , разработанный в Microsoft Rise, общедоступен как мощный инструмент Microsoft Visual Studio 2010 для NET Framework .
- Triton — это библиотека совместного выполнения с открытым исходным кодом для двоичного кода.
- CutEr — это инструмент concolic-тестирования с открытым исходным кодом для функционального языка программирования Erlang.
Многие инструменты, особенно DART и SAGE, не были доступны широкой публике. Однако обратите внимание, что, например, SAGE «используется ежедневно» для внутреннего тестирования безопасности в Microsoft. [12]
Ссылки
[ редактировать ]- ^ Патрис Годфруа; Нильс Кларлунд; Кошик Сен (2005). «DART: Направленное автоматизированное выборочное тестирование» (PDF) . Материалы конференции ACM SIGPLAN 2005 года по проектированию и реализации языков программирования . Нью-Йорк, штат Нью-Йорк: ACM. стр. 213–223. ISSN 0362-1340 . Архивировано из оригинала (PDF) 29 августа 2008 г. Проверено 9 ноября 2009 г.
- ^ Кошик Сен; Дарко Маринов; Гуль Ага (2005). «CUTE: механизм модульного тестирования concolic для C» (PDF) . Материалы 10-й Европейской конференции по программной инженерии, проведенной совместно с 13-м международным симпозиумом ACM SIGSOFT по основам программной инженерии . Нью-Йорк, штат Нью-Йорк: ACM. стр. 263–272. ISBN 1-59593-014-0 . Архивировано из оригинала (PDF) 29 июня 2010 г. Проверено 9 ноября 2009 г.
- ^ Кристиан Кадар; Виджай Ганеш; Питер Павлоски; Дэвид Л. Дилл; Доусон Энглер (2006). «EXE: автоматическое создание входных данных о смерти» (PDF) . Материалы 13-й Международной конференции по компьютерной и коммуникационной безопасности (CCS 2006) . Александрия, Вирджиния, США: ACM.
- ^ Ники Уильямс; Бруно Марре; Патрисия Муи (2004). «Мгновенная генерация тестов K-Path для функций C». Материалы 19-й Международной конференции IEEE по автоматизированной разработке программного обеспечения (ASE 2004), 20–25 сентября 2004 г., Линц, Австрия . Компьютерное общество IEEE. стр. 290–293. ISBN 0-7695-2131-2 .
- ^ Ники Уильямс; Бруно Марре; Патрисия Муи; Мюриэл Роджер (2005). «PathCrawler: автоматическое создание тестов пути путем сочетания статического и динамического анализа». Надежные вычисления — EDCC-5, 5-я Европейская конференция по надежным вычислениям, Будапешт, Венгрия, 20–22 апреля 2005 г., Материалы . Спрингер. стр. 281–292. ISBN 3-540-25723-3 .
- ^ Кошик Сен; Гуль Ага (август 2006 г.). «CUTE и jCUTE: инструменты модульного тестирования Concolic и проверки моделей с явным путем» . Компьютерная проверка: 18-я Международная конференция, CAV 2006, Сиэтл, Вашингтон, США, 17–20 августа 2006 г., Материалы . Спрингер. стр. 419–423. ISBN 978-3-540-37406-0 . Архивировано из оригинала 29 июня 2010 г. Проверено 9 ноября 2009 г.
- ^ Себастьен Барден; Филипп Херрманн (апрель 2008 г.). «Структурное тестирование исполняемых файлов» (PDF) . Материалы 1-й Международной конференции IEEE по тестированию, верификации и валидации программного обеспечения (ICST 2008), Лиллехаммер, Норвегия . Компьютерное общество IEEE. стр. 22–31. ISBN 978-0-7695-3127-4 . ,
- ^ Патрис Годфруа; Майкл Ю. Левин; Дэвид Молнар (2007). Автоматизированное нечеткое тестирование Whitebox (PDF) (Технический отчет). Исследования Майкрософт. ТР-2007-58.
- ^ Патрис Годфруа (2007). «Выборочное тестирование безопасности: фаззинг черного ящика или белого ящика» (PDF) . Материалы 2-го международного семинара по выборочному тестированию, проведенного совместно с 22-й Международной конференцией IEEE/ACM по автоматизированной разработке программного обеспечения (ASE 2007) . Нью-Йорк, штат Нью-Йорк: ACM. п. 1. ISBN 978-1-59593-881-7 . Проверено 9 ноября 2009 г.
- ^ Шэрон Барнер, Синди Эйснер, Зив Глазберг, Дэниел Кронинг, Ишай Рабиновиц: ExpliSAT: Руководство по проверке программного обеспечения на основе SAT с явными состояниями. Хайфская контрольная конференция 2006: 138-154
- ^ "Программное обеспечение" .
- ^ Команда SAGE (2009). «Microsoft PowerPoint — SAGE в одном слайде» (PDF) . Исследования Майкрософт . Проверено 10 ноября 2009 г.