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

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

1. Microsoft Docs: .NET API browser: System.Threading: Monitor Class. Available at: https://docs.microsoft.com/en-us/dotnet/api/system.threading.monitor, accessed: 29.07.22.

2. Microsoft Docs: .NET API browser: System.Threading: ReaderWriterLock Class. Available at: https://docs.microsoft.com/en-us/dotnet/api/system.threading.readerwriterlock, accessed: 01.08.22.

3. Microsoft Docs: .NET API browser: System.Threading: ReaderWriterLockSlim Class. Available at: https://docs.microsoft.com/en-us/dotnet/api/system.threading.readerwriterlockslim, accessed: 01.08.22.

4. Microsoft Docs: .NET API browser: C# Keywords: Statement Keywords (C# Reference): lock statement. Available at: https://docs.microsoft.com/en-us/dotnet/csharp/language-reference/statements/lock, accessed: 03.08.22.

5. The .NET Compiler Platform (“Roslyn”). Available at: https://github.com/dotnet/Roslyn, accessed: 29.07.22

6. Кошелев В.К. Межпроцедурный статический анализ для поиска ошибок в исходном коде программ на языке C. Диссертация на соискание учёной степени кандидата физико-математических наук, Москва, ИСП РАН, 2017 г., 104 стр. / Koshelev V.K. Interprocedural static analysis for finding errors in the source code of C programs. Thesis for the degree of candidate of physical and mathematical sciences, Moscow, ISP RAS, 2017, 104 p. (in Russian).

7. Кошелев В.К., Игнатьев В.Н., Борзилов А.И. Инфраструктура статического анализа программ на языке C#. Труды ИСП РАН, том 28, вып. 1, 2016 г., стр. 21-40 / Koshelev V.K., Ignatyev V.N., Borzilov A.I. C# static analysis framework. Trudy ISP RAN/Proc. ISP RAS, vol. 28, issue 1, 2016, pp. 21-40 (in Russian). DOI: 10.15514/ISPRAS-2016-28(1)-2.

8. OpenSimulator. Available at: http://opensimulator.org, accessed: 23.10.2021.

9. WCell: World of Warcraft emulator written in C#/.NET 4.0, with design and extensibility in mind. Available at: https://github.com/WCell/WCell, accessed at 15.08.2022.

10. Welcome to the Lucene.NET website! | Apache Lucene.NET 4.8.0. Available at: https://lucenenet.apache.org, accessed: 23.10.2021.

11. Белеванцев А.А. Многоуровневый статический анализ исходного кода для обеспечения качества программ. Диссертация на соискание учёной степени доктора физико-математических наук, Москва, ИСП РАН, 2017 г., 229 стр. / Belevantsev A.A. Multi-level static analysis of the source code to ensure the quality of programs. Thesis for the degree of Doctor of Physical and Mathematical Sciences, Moscow, ISP RAS, 2017, 229 p. (in Russian).

12. Иванников В.П., Белеванцев А.А. и др. Статический анализатор Svace для поиска дефектов в исходном коде программ. Труды ИСП РАН, том 26, вып. 1, 2014 г., стр. 231-250 / Ivannikov V.P., Belevantsev A.A. et al. Static analyzer Svace for finding of defects in program source code. Trudy ISP RAN/Proc. ISP RAS, vol. 26, issue 1, 2014, pp. 231-240 (in Russian). DOI: 10.15514/ISPRAS-2014-26(1)-7.

13. Calcagno C., Distefano D. Infer: An automatic program verifier for memory safety of C programs. Lecture Notes in Computer Science, vol. 6617, 2011, pp. 459-465

14. Calcagno C., Distefano D. et al. Moving fast with software verification. Lecture Notes in Computer Science, vol. 9058, 2015, pp. 3-11.

15. Liu B., Liu P. et al. When threads meet events: efficient and precise static race detection with origins. In Proc. of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, 2021, pp. 725-739.

16. Kremenek T. Finding software bugs with the clang static analyzer. Available at: https://llvm.org/devmtg/2008-08/Kremenek_StaticAnalyzer.pdf, accessed: 23.10.2021.

17. Campbell G.A., Papapetrou P.P. SonarQube in action. Manning, 2013, 392 p.

18. Synopsys Software Security | Software Integrity Group, Available at: http://www.coverity.com, accessed: 13.09.2022.