Инфраструктура статического анализа программ на языке C#

В работе рассмотрены различные аспекты статического анализа программ на языке C# с целью обнаружения максимального количества ошибок за минимально приемлемое время. Описан полный цикл статического анализа программного обеспечения, при этом основное внимание уделяется особенностям, возникающим при анализе языка C#. Рассмотрены методы, позволяющие учитывать популярные возможности языка на всех уровнях анализа: построение графа вызовов и графа потока управления, проведение анализа потоков данных и чувствительного к контексту и путям межпроцедурного анализа. Предлагается метод символьного исполнения, основанный на таких работах, как Bounded Model Checking и Saturn Software Analysis Project. В статье описана организация модели памяти, позволяющая как проводить точный внутрипроцедурный анализ, так и создавать компактные представления для привязанных к функциям условий, используемые при межпроцедурном анализе. Особое внимание уделяется теме оптимизации возникающих на этапе чувствительного к путям анализа условий. Условия необходимо оптимизировать как по размеру, поскольку при межпроцедурном чувствительном к путям анализе необходимо сохранять большое количество условий для каждой проанализированной функции, так и по сложности, поскольку время анализа ограничено. Решение условий производится при помощи современных SMT-решателей, таких как Microsoft Z3 Prover. В статье также рассмотрены различные подходы к моделированию поведения библиотечных функций: при помощи резюме в виде набора признаком или в виде упрощенных реализаций на языке C#. Все приведённые решения реализованы в инструменте статического анализа SharpChecker и протестированы на наборе проектов различного объема (от 1.5 тыс. до 1.35 млн. строк кода) с открытым исходным кодом.

Статический анализ, использование нулевого указателя, чувствительность к путям, чувствительность к контексту, резюме функции, поиск дефектов, 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. В.П. Иванников А.А. Белеванцев А.Е. Бородин В.Н. Игнатьев Д.М. Журихин А.И. Аветисян М.И. Леонов. Статический анализатор Svace для поиска дефектов в исходном коде программ. Труды Института системного программирования РАН, том. 26 (выпуск 1), 2014 г., стр. 231–250. 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. Ахо А.В., Лам М.С., Сети Р., Ульман Д.Д. Компиляторы. Принципы, технологии и инструментарий: пер. с англ. / под ред. И.В. Красикова. М.: ООО «И.Д. Вильямс», 2008. 1184 с.

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. В.К. Кошелев И.А. Дудина В.Н. Игнатьев А.И. Борзилов Чувствительный к путям поиск дефектов в программах на языке C# на примере разыменования нулевого указателя. Труды Института системного программирования РАН, том. 27 (выпуск 5), 2015.г., стр.. 59–86. 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. Описание стандарта ECMA-335 [PDF]

18. http://www.ecma-international.org/publications/files/ECMA-ST/ECMA-335.pdf

19. Веб-сайт библиотеки Mono.Cecil

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

21. Описание Windows API в Microsoft Developer Network [HTML] https://msdn.microsoft.com/en-us/library/cc433218

22. Веб-сайт Библиотека классов .NET Framework в Microsoft Developer Network [HTML] https://msdn.microsoft.com/ru-ru/library/mt472912(v=vs.110).aspx