20.04.2015: BLAST 2.7.3 на SV-COMP'2015
BLAST 2.7.3 был представлен на четвертых международных соревнованиях по верификации программ, которые прошли в рамках конференции TACAS 2015 в Лондоне, Великобритания. В этом году BLAST выиграл золото в категории DeviceDrivers64.
BLAST - это классический инструмент статической верификации программ, основанный на предикатных абстракциях и методе CEGAR. Он поддерживается ИСП РАН и активно используется в проекте Linux Driver Verification (LDV).
В этом году в рамках проекта LDV для соревнований SV-COMP-2015 был подготовлен новый набор задач верификации с использованием более сложных спецификаций правил корректности. Набор включает следующие пакеты:
- ldv-linux-3.12-rc1 - различные задачи из ядра Linux версии 3.12-rc1 (включая правило 144_2a, требующее аккуратного отслеживания указателей)
- ldv-linux-3.16-rc1 - различные задачи из ядра Linux версии 3.16-rc1 (включая правило 205_9a, требующее аккуратной обработки массивов, и правило 43_2a, требующее поддержки битового представления чисел)
- ldv-validator-v0.6 - набор задач, нацеленных на поиск реальных ошибок в ядре Linux, изначально обнаруженных при эксплуатации ядра и исправленных в стабильных версиях ядра Linux.
Как можно видеть из результатов, инструменты статической верификации не работают хорошо на новом наборе, выдавая много ложных предупреждений, пропуская ошибки и выдавая вердикт неизвестно (unknown). В таблице ниже представлены результаты на новом наборе для трех лидирующих инструментов верификации в категории DeviceDrivers64: BLAST, Seahorn и CPAchecker.
| ldv-linux-3.12-rc1 (pointer tracking) |
BLAST 2.7.3 | CPAchecker 1.3.10-svcomp15 | Seahorn |
| Всего задач | 40 | ||
| Корректных результатов | 25 | 11 | 25 |
| Упущенных ошибок | 0 | 0 | 0 |
| Ложных предупреждений | 2 | 1 | 0 |
| ldv-linux-3.16-rc1 (arrays) |
BLAST 2.7.3 | CPAchecker 1.3.10-svcomp15 | Seahorn |
| Всего задач | 65 | ||
| Корректных результатов | 33 | 19 | 14 |
| Упущенных ошибок | 7 | 2 | 8 |
| Ложных предупреждений | 3 | 4 | 1 |
| ldv-linux-3.16-rc1 (bitvector) |
BLAST 2.7.3 | CPAchecker 1.3.10-svcomp15 | Seahorn |
| Всего задач | 94 | ||
| Корректных результатов | 73 | 56 | 70 |
| Упущенных ошибок | 0 | 1 | 2 |
| Ложных предупреждений | 0 | 0 | 0 |
| ldv-validator-v0.6 (real bugs) |
BLAST 2.7.3 | CPAchecker 1.3.10-svcomp15 | Seahorn |
| Всего задач | 22 | ||
| Корректных результатов | 16 | 13 | 12 |
| Упущенных ошибок | 0 | 0 | 0 |
| Ложных предупреждений | 0 | 0 | 0 |
В следующем году мы надеемся увидеть прогресс в этом направлении, так что мы сможем верифицировать ядро Linux на предмет выполнения более сложных спецификаций правил.
Мы приветствуем введение нового требования в правилах соревнований SV-COMP, обязывающего выдавать для каждого вердикта UNSAFE трассу ошибки в Общем формате трассы подтверждения ошибки (Common Error Witness Trace). Это позволяет нам визуализировать и анализировать результаты любого инструмента статической верификации, участвующего в соревнованиях. Например, мы провели экперименты с новым инструментом Seahorn и смогли успешно проанализировать выдаваемые им трассы ошибок. Это существенный шаг вперед по сравнению с предыдущими соревнованиями, в которых большинство инструментов были непригодны для нас без дополнительных усилий!
Однако, еще остаются направления для улучшения правил соревнований, связанных с подтверждением трасс ошибок. В первую очередь результаты соревнований показывают, что остается довольно много превышений лимита по времени для проверки подтверждений ошибок. Это означает, что инструменты верификации штрафуют за невозможность инструмента проверки подтверждений достаточно быстро проверить подтверждение ошибки. В соответствии с духом соревнований инструменты верификации должны извлекать выгоду из нахождения сложных трасс ошибок, тогда как сейчас она ограничивается возможностями инструментов проверки подтверждений. Для борьбы с данной проблемой мы предлагаем увеличить лимиты проверки подверждений. В тоже время, когда трасса подтверждения недостаточна точна и инструмент проверки подтверждения не знает куда идти дальше, зачастую он начинает угадывать недостающие части трассы, повторно обходя протранство состояний. Так как мы не хотим, чтобы инструмент проверки подтверждений повторял верификацию, то можно было бы ограничить время, затрачиваемое инструментом непосредственно на такие ситуации.
