Обнаружение ошибок взаимоисключающей блокировки в программах на языке С# при помощи методов статического анализа

В статье рассматриваются алгоритмы статического анализа, которые направлены на поиск трех типов ошибок, связанных с понятием синхронизирующего монитора: переопределение переменной взаимоисключающей блокировки внутри критической секции; использование переменной некорректного типа при входе в монитор; блокировка с задействованием объекта, имеющего методы, которые используют для блокировки ссылку на экземпляр (this). Разработанные алгоритмы опираются на технологию символьного исполнения и опираются на межпроцедурный анализ с применением резюме функций, что обеспечивает масштабируемость, чувствительность к полям, контексту, потоку управления. Полученные методы реализованы в инфраструктуре статического анализатора SharpChecker, использующего элементы компиляторной платформы Roslyn, в виде трёх детекторов. С их помощью при тестировании на проектах с открытым кодом найдено 23 ошибки и получена доля верных срабатываний в 88.5%, в то время как потребление времени каждым детектором составляет от 0.1 до 0.7% от общего времени работы анализатора. Ошибки, для поиска которых были разработаны данные детекторы, сложно обнаружить другими способами, помимо статического анализа, из-за того, что они тесно связаны с понятием многопоточности. При этом находить их необходимо: всего один подобный дефект может привести к нестабильности работы программы и даже сделать её уязвимой для злоумышленников.