Теоретические границы символьного исполнения и конколического тестирования
«Почему техники автоматической проверки программ не могут гарантировать, что код безопасен, даже в теории — и какие границы существуют у символьного исполнения и конколического тестирования». Говоря о безопасности программного обеспечения, часто возникает соблазн доверить проверку кода автоматизированным инструментам.
Внешние зависимости и недетерминизм.** Символьный анализ эффективно работает с чистой, самодостаточной логикой программы.
Работающий подход лежит в комбинировании: использование конколического тестирования для глубокого, но неполного исследования, статического анализа для поиска шаблонных ошибок, динамического фаззинга для проверки устойчивости и, наконец, экспертного аудита для тех самых сложных случаев на стыке логики, памяти и внешнего мира, куда автоматика заглянуть не может. Безопасность остаётся задачей, где глубокая автоматизация не исключает, а требует внимания человека.
