Инфраструктура статического анализа программ на языке C#
Автор: Кошелев В.К., Игнатьев В.Н., Борзилов А.И.
Журнал: Труды Института системного программирования РАН @trudy-isp-ran
Статья в выпуске: 1 т.28, 2016 года.
Бесплатный доступ
В работе рассмотрены различные аспекты статического анализа программ на языке C# с целью обнаружения максимального количества ошибок за минимально приемлемое время. Описан полный цикл статического анализа программного обеспечения, при этом основное внимание уделяется особенностям, возникающим при анализе языка C#. Рассмотрены методы, позволяющие учитывать популярные возможности языка на всех уровнях анализа: построение графа вызовов и графа потока управления, проведение анализа потоков данных и чувствительного к контексту и путям межпроцедурного анализа. Предлагается метод символьного исполнения, основанный на таких работах, как Bounded Model Checking и Saturn Software Analysis Project. В статье описана организация модели памяти, позволяющая как проводить точный внутрипроцедурный анализ, так и создавать компактные представления для привязанных к функциям условий, используемые при межпроцедурном анализе. Особое внимание уделяется теме оптимизации возникающих на этапе чувствительного к путям анализа условий. Условия необходимо оптимизировать как по размеру, поскольку при межпроцедурном чувствительном к путям анализе необходимо сохранять большое количество условий для каждой проанализированной функции, так и по сложности, поскольку время анализа ограничено. Решение условий производится при помощи современных SMT-решателей, таких как Microsoft Z3 Prover. В статье также рассмотрены различные подходы к моделированию поведения библиотечных функций: при помощи резюме в виде набора признаком или в виде упрощенных реализаций на языке C#. Все приведённые решения реализованы в инструменте статического анализа SharpChecker и протестированы на наборе проектов различного объема (от 1.5 тыс. до 1.35 млн. строк кода) с открытым исходным кодом.
Статический анализ, использование нулевого указателя, чувствительность к путям, чувствительность к контексту, резюме функции, поиск дефектов
Короткий адрес: https://sciup.org/14916323
IDR: 14916323 | DOI: 10.15514/ISPRAS-2016-28(1)-2
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.
Список литературы Инфраструктура статического анализа программ на языке C#
- TIOBE Index http://www.tiobe.com/tiobe_index
- LINQ (Language-Integrated Query): Microsoft Developer Network https://msdn.microsoft.com/ru-ru/library/bb397926.aspx
- 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 , volume 26 (issue 1), 2014,. pp. 231-250 DOI: 10.15514/ISPRAS-2014-26(1)-7
- Coverity: Software Testing and Static Analysis Tools http://www.coverity.com/
- Klocwork: Source Code Analysis Tools for Security & Reliability http://www.klocwork.com/
- SonarLint http://www.sonarlint.org/
- PVS-Studio for C/C++/C# http://www.viva64.com/
- SharpChecker http://sharpchecker.ispras.ru/ru/
- Visual Studio -Microsoft Developer Tools https://www.visualstudio.com/ru-ru/visual-studio-homepage-vs.aspx
- Roslyn.NET Compiler Platform https://github.com/dotnet/roslyn
- 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
- 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
- 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
- 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 , volume 27 (issue 5), 2015, pp. 59-86 DOI: 10.15514/ISPRAS-2015-27(5)-5
- H. R. Andersen, An Introduction to Binary Decision Diagrams, 1997, Lecture notes http://www.cs.utexas.edu/~isil/cs389L/bdd.pdf
- K. L. McMillan, Interpolants from Z3 proofs, 2011. Formal Methods in Computer-Aided Design (FMCAD), pp. 19-27.
- ECMA-335 Standard http://www.ecma-international.org/publications/files/ECMA-ST/ECMA-335.pdf
- Mono.Cecil http://www.mono-project.com/docs/tools+libraries/libraries/Mono.Cecil/
- Windows API: Microsoft Developer Network https://msdn.microsoft.com/en-us/library/cc433218
- NET Framework Class Library: Microsoft Developer Network https://msdn.microsoft.com/en-us/library/mt472912(v=vs.110).aspx
