C# static analysis framework

The paper describes static analysis techniques that are used for defect detection in C# programs. The goal of proposed analysis approaches is to catch more defects within an acceptable amount of time. Although the paper contains a description of full analysis cycle, it mainly focuses on special aspects that distinguish C# analysis approaches from well-known Java and C++ techniques. The paper illustrates methods that allow taking into account C# specialties of all analysis stages: call graph and control flow graph construction, data flow analysis, context- and path-sensitive interprocedural analysis. We propose an adaptation of symbolic execution methods inspired by Bounded Model Checking and Saturn Software Analysis Project. The paper also explains the organization of memory model, which is suitable for both a precise intraprocedural analysis and a creation of compact function-bound conditions used for interprocedural analysis. Special attention is paid to optimization of condition size and simplicity during a path sensitive-analysis. The conditions produced by a path-sensitive analysis are supposed to be solved by modern SMT solvers like Microsoft Z3 Prover. Different approaches to external functions modeling are covered. All proposed approaches are implemented in the SharpChecker static analysis tool and, as evaluated on several open source C# projects of varying size (1K - 1.35M lines of code), display good results and scalability.

static analysis, null pointer dereference, path-sensitive analysis, context-sensitive analysis, function summary, bug detection, Roslyn, C#

1. TIOBE Index [HTML] http://www.tiobe.com/tiobe_index

2. LINQ (Language-Integrated Query): Microsoft Developer Network [HTML] https://msdn.microsoft.com/ru-ru/library/bb397926.aspx

3. V.P. Ivannikov, A.A. Belevantsev, A.E. Borodin, V.N. Ignatiev, D.M. Zhurikhin, A.I. Avetisyan, M.I. Leonov. Staticheskij analizator Svace dlja poiska defektov v ishodnom kode programm (Static analyzer Svace for finding of defects in program source code). Trudy ISP RАN [Proceedings of ISP RAS], volume 26 (issue 1), 2014,. pp. 231-250 (in Russian). DOI: 10.15514/ISPRAS-2014-26(1)-7

4. Coverity: Software Testing and Static Analysis Tools [HTML] http://www.coverity.com/

5. Klocwork: Source Code Analysis Tools for Security & Reliability [HTML] http://www.klocwork.com/

6. SonarLint [HTML] http://www.sonarlint.org/

7. PVS-Studio for C/C++/C# [HTML] http://www.viva64.com/

8. SharpChecker [HTML] http://sharpchecker.ispras.ru/ru/

9. Visual Studio - Microsoft Developer Tools [HTML] https://www.visualstudio.com/ru-ru/visual-studio-homepage-vs.aspx

10. Roslyn.NET Compiler Platform [HTML] https://github.com/dotnet/roslyn

11. Alfred V. Aho , Monica S. Lam , Ravi Sethi , Jeffrey D. Ullman, Compilers: Principles, Techniques, and Tools (2nd Edition), Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 2006

12. Vijay Sundaresan, Laurie Hendren, Chrislain Razafimahefa, Raja Vallée-Rai, Patrick Lam, Etienne Gagnon, and Charles Godin. Practical virtual method call resolution for Java. 2000. In Proceedings of the 15th ACM SIGPLAN conference on Object-oriented programming, systems, languages, and applications (OOPSLA '00). ACM, New York, NY, USA, pp. 264-280. doi: 10.1145/353171.353189

13. Falke Stephan, Merz Florian, Sinz Carsten. LLBMC: Improved Bounded Model Checking of C Programs Using LLVM. 2010. Tools and Algorithms for the Construction and Analysis of Systems, pp. 623-626. doi: 10.1007/978-3-642-36742-7_48

14. V. Koshelev, I. Dudina, V. Ignatyev, A. Borzilov. Chuvstvitel'nyj k putjam poisk defektov v programmah na jazyke C# na primere razymenovanija nulevogo ukazatelja (Path-sensitive bug detection analysis of C# program illustrated by null pointer dereference). Trudy ISP RАN [Proceedings of ISP RAS], volume 27 (issue 5), 2015, pp. 59-86 (in Russian). DOI: 10.15514/ISPRAS-2015-27(5)-5

15. H. R. Andersen, An Introduction to Binary Decision Diagrams, 1997, Lecture notes [PDF] http://www.cs.utexas.edu/~isil/cs389L/bdd.pdf

16. K. L. McMillan, Interpolants from Z3 proofs, 2011. Formal Methods in Computer-Aided Design (FMCAD), pp. 19-27.

17. [17]. ECMA-335 Standard [PDF] http://www.ecma-international.org/publications/files/ECMA-ST/ECMA-335.pdf

18. Mono.Cecil http://www.mono-project.com/docs/tools+libraries/libraries/Mono.Cecil/

19. Windows API: Microsoft Developer Network [HTML] https://msdn.microsoft.com/en-us/library/cc433218

20. NET Framework Class Library: Microsoft Developer Network [HTML] https://msdn.microsoft.com/en-us/library/mt472912(v=vs.110).aspx