Detection of erroneous usage of synchronization monitor in С# via static analysis

The paper describes static analysis algorithms aimed at finding three types of errors related to the concept of a synchronizing monitor: redefinition of a variable of mutually exclusive locking inside a critical section; use of an incorrect variable type when entering the monitor; blocking involving an object that has methods that use a reference to an instance (this) to lock. Developed algorithms rely on symbolic execution technology and involve interprocedural analysis via summary of functions, which ensures scalability, field-, context-, and flow-sensivity. Proposed methods were implemented in the infrastructure of a static analyzer in the form of three separate detectors. Testing on the set of open source projects revealed 23 errors and the true positive ratio of 88.5% was obtained, while the time consumption only made up from 0.1 to 0.7% of the total analysis time. The errors that these detectors were designed to find are difficult to detect by testing or dynamic analysis because of their multithreading nature. At the same time, it is necessary to find them: just one such defect can lead to incorrectness of the program and even make it vulnerable to intruders.

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.