Илья Захаров, ИСП РАН.
Доклад посвящен применению инструментов статической верификации для поиска нефункциональных ошибок в исходном коде системного программного обеспечения. В докладе будет представлен метод модульной статической верификации с интерактивным пошаговым уточнением и его реализация в системе статической верификации Klever. О результатах практического применения я расскажу на примере поиска ошибок в модулях и подсистемах ядра Linux и приведу результаты первых экспериментов по верификации другого системного программного обеспечения.
Введение
Ошибки и уязвимости в системном программном обеспечении могут привести к серьезным убыткам и даже человеческим жертвам. Существует множество методов поиска ошибок и уязвимостей, применяемых при разработке, приемке и сертификации системного программного обеспечения, такие как экспертиза, тестирование и динамический анализ, статический анализ, формальные методы. В то же время ни один из существующих подходов к обеспечению корректности ПО не гарантирует отсутствия ошибок, поэтому чтобы снизить риск допустить ошибку или уязвимость в конечном программном продукте, используется весь доступный арсенал методов и инструментов в зависимости от важности системы и доступных ресурсов на ее верификацию.
Статическая верификация
Статическая верификация является одним из направлений поиска ошибок в исходном коде программы без ее реального выполнения. В отличие от традиционных методов статического анализа программ инструменты статической верификации ставят своей целью доказательство корректности программ при заданных условиях и поиск всех нарушений нефункциональных требований заданного вида на конечных путях выполнения программы. Инструменты статической верификации строят модель программы по ее исходному коду автоматически, корректность которой проверяется при помощи формальных методов. Для верификации модели используются алгоритмы, такие как, например, уточнение абстракции по контр-примеру [1] и ограничиваемая проверка моделей [2]. Построение модели и доказательство корректности всегда выполняется автоматически, что отличает данное направление верификации программ от дедуктивной верификации. Инструменты статической верификации разрабатывает как академическое сообщество, так и коммерческие компании. К академическим разработкам можно отнести CPAchecker [3] и CBMC [4]. Коммерческими разработками являются Q от Microsoft [5][6] и Varvel от NEC [7] соответственно.
Применение инструментов статической верификации является достаточно трудоемким. Инструменты статической верификации не способны проверять проекты, размер которых более нескольких десятков тысяч строк кода. Поэтому на практике код программы разбивается на фрагменты, верифицируемые отдельно друг от друга. При верификации требуется предварительная инструментация исходного кода для проверки определенных требований к программе или моделирование тех частей программы, исходный код которых недоступен. Для автоматизации процесса подготовки кода к верификации, запуска инструментов, а также анализа результатов применяются системы статической верификации. Примерами подобных систем являются: система статической верификации драйверов операционной системы Windows SDV [8], система верификации модулей ядра Linux LDV Tools [9], система для верификации встраиваемого ПО DC2 [10].
Предлагаемый метод
В данном докладе будет представлен метод модульной статической верификации с интерактивным пошаговым уточнением системного программного обеспечения на языке Си. В процессе верификации выполняется инкрементальное уточнение результатов на основе анализа сообщений о найденных ошибках и информации о достижимости разных участков верифицируемого кода. На каждом шаге процесс уточнения предполагает выбор фрагментов программы, разработку спецификаций моделей окружения и подбор оптимальных конфигурационных параметров инструментов статической верификации. Значительная часть времени при верификации ПО тратится именно на моделирование окружения верифицируемого фрагмента программы. И ключевой особенностью предлагаемого метода является подход к моделированию окружения. Модель окружения предлагается генерировать на основе спецификаций, разрабатываемых вручную, и результатах анализа исходного кода. Спецификации моделей окружения представляют собой описание моделируемого интерфейса и сценариев взаимодействия окружения с целевой программой на языках предметной области. Генерация модели выполняется несколькими генераторами, результаты работы которых компонуются в финальную модель в промежуточном представлении. Затем, модель транслируется на язык Си с учетом проверяемого требования, выбранного инструмента статической верификации и конфигурационных параметров, заданных пользователем.
Реализация метода и практическое применение
Предлагаемый метод реализован в системе статической верификации Klever1. Данная система предоставляет средства для формализации требований, моделирования окружения, интеграции новых инструментов статической верификации, запуска инструментов локально, в распределенной вычислительной среде и облачной инфраструктуре. Инструменты анализа результатов верификации Klever позволяют хранить данные в виде, позволяющем легко воспроизводить, сравнивать, переносить и анализировать результаты. Система предоставляет существенно больший набор возможностей для верификации, чем существующие аналоги, упомянутые выше.
В докладе я расскажу об опыте поиска ошибок модулях ядра Linux и подсистемах самого ядра. Кроме того, будут представлены первые результаты экспериментов по верификации других программ при помощи данной системы статической верификации.
1 - Klever является проектом с открытым исходным кодом: https://forge.ispras.ru/projects/klever?jump=welcome
Список литературы
[1] Clarke E., Grumberg O., Jha S. et al. Counterexample-guided Abstraction Refinement for Symbolic Model Checking // J. ACM. 2003. Vol. 50, no. 5. P. 752–794. URL: http://doi.acm.org/10.1145/876638.876643.
[2] Biere A., Cimatti A., Clarke E. M. et al. Bounded model checking // Advances in Computers. 2003. Vol. 58. P. 117– 148. URL: http://dx.doi.org/10.1016/S0065-2458(03)58003-2.
[3] Beyer D., Keremoglu M. E. CPAchecker: A Tool for Configurable Software Verification // Proceedings of the 23rd International Conference on Computer Aided Verification. Berlin, Heidelberg: Springer, 2011. P. 184–190. URL: http://dl.acm.org/citation.cfm?id=2032305.2032321.
[4] Clarke E., Kroening D., Lerda F. A Tool for Checking ANSI-C Programs // Proceedings of the 10th International Conference on Tools and Algorithms for the Construction and Analysis of Systems / Ed. by K. Jensen, A. Podelski. Berlin, Heidelberg: Springer, 2004. P. 168–176. URL: http://dx.doi.org/10.1007/978-3-540-24730-2_15.
[5] Ball T., Bounimova E., Kumar R., Levin V. SLAM2: Static Driver Verific ation with Under 4% False Alarms // Proceedings of the 2010 Conference on Formal Methods in Computer-Aided Design. Austin, TX: FMCAD Inc, 2010. P. 35–42. URL: http://dl.acm.org/citation.cfm?id=1998496.1998508.
[6] Lal A., Qadeer S. Powering the Static Driver Verifier Using Corral // Proceedings of the 22nd ACM SIGSOFT International Symposium on Foundations of Software Engineering. New York, NY, USA: ACM, 2014. P. 202–212. URL: http://doi.acm.org/10.1145/2635868.2635894.
[7] Ivančić F., Balakrishnan G., Gupta A. et al. Scalable and scope-bounded software verification in Varvel // Automated Software Engineering. 2015. — Dec. Vol. 22, no. 4. P. 517–559. URL: https://doi.org/10.1007/s10515-014-0164-0.
[8] Ball T., Levin V., Rajamani S. K. A Decade of Software Model Checking with SLAM // Commun. ACM. 2011. — jul. Vol. 54, no. 7. P. 68–76. URL: http://doi.acm.org/10.1145/1965724.1965743.
[9] Zakharov I. S., Mandrykin M. U., Mutilin V. S. et al. Configurable toolset for static verification of operating systems kernel modules // Programming and Computer Software. 2015. — Jan. Vol. 41, no. 1. P. 49–64. URL: http://dx.doi.org/10.1134/S0361768815010065.
[10] Ivancic F., Balakrishnan G., Gupta A. et al. Scalable and Scope-bounded Software Verification in Varvel // Automated Software Engg. 2015. — dec. Vol. 22, no. 4. P. 517–559. URL: http://dx.doi.org/10.1007/s10515-014-0164-0.
