Использование зависимостей для повышения точности статического анализа программ
Аннотация
Статья посвящена разработке методов анализа зависимостей с целью повышения точности статического анализа. Рассмотрены причины, ведущие к снижению точности абстрактной интерпретации при обнаружении дефектов в программном коде. На различных примерах показана необходимость выявления и интерпретации зависимостей между программными объектами в ходе анализа. Приведена классификация зависимостей по различным признакам. Показана необходимость совокупного рассмотрения хранимых значений и зависимостей. Описан порядок выявления зависимостей при интерпретации присваиваний. Предложен метод интерпретации зависимостей на основе логического вывода, базирующегося на известных правилах логики и арифметики. Некоторые из разработанных методов реализованы в средстве обнаружения дефектов Digitek Aegis, показано значительное увеличение точности анализа.
Ключевые слова
статический анализ,
абстрактная интерпретация,
анализ зависимостей,
обнаружение программных дефектов
MSC2020: 004.415.5+004.416.2
Об авторах
Михаил Игоревич Глухих
Санкт-Петербургский государственный политехнический университет
Россия
Россия
Владимир Михайлович Ицыксон
Санкт-Петербургский государственный политехнический университет
Россия
Россия
Вадим Александрович Цесько
Санкт-Петербургский государственный политехнический университет
Россия
Россия
Список литературы
1. Zhivich M., Cunningham R. The Real Cost of Software Errors. IEEE Security & Privacy // IEEE Computer Society. 2009. Vol. 7, № 2.
2. Nielson F., Nielson N., Hankin C. Principles of Program Analysis. Corr. 2nd printing. Springer, 2005. XXI. 452 p.
3. Cousot P. Abstract Interpretation. ACM Computing Surveys (CSUR) // ACM, New York, 1996. Vol. 28, Issue 2. P. 324-328.
4. Jones N., Nielson F. Abstract Interpretation: A Semantic-based Tool for Program Analysis. Handbook of logic in computer science (vol. 4): semantic modeling. Oxford: Oxford University Press, 1995. P. 527-636.
5. Несов В. С., Маликов О. Р. Использование информации о линейных зависимостях для обнаружения уязвимостей в исходном коде программ // Труды ИСП РАН. 2006. №9. С. 51-57.
6. Cousot P., Halbwachs N. Automatic discovery of linear restraints among variables of a program // Proceedings of the 5th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages (POPL '78). ACM, New York, 1978. P. 8496.
7. Code Analysis for C/C++ Overview, Microsoft Corporation. <http://msdn.microsoft.com/en-us/library/d3bbz7tz.aspx>
8. Frama-C Software Analyzers. <http://frama-c.com>
9. Splint home page. <http://www.splint.org>
10. Fortify Software. <http://www.fortify.com>
11. Ицыксон В.М., Моисеев М. Ю., Цесько В. А., Карпенко А. В. Исследование систем автоматизации обнаружения дефектов в исходном коде программного обеспечения // Научно-технические ведомости СПбГПУ. Информатика. Телекоммуникации. Управление. 2008. №5(65). C. 119-127.
12. Schwartzbach M. Lecture Notes on Static Analysis. Aarhus, 2000. 58 p.
13. Aegis - a defect detection system. <http://www.digiteklabs.ru/aegis>
14. Ицыксон В. М., Моисеев М. Ю., Цесько В. А., Захаров А. В., Ахин М.Х. Алгоритм интервального анализа для обнаружения дефектов в исходном коде программ // Информационные и управляющие системы. 2009. №2 (39). C. 3441.
15. Ицыксон В. М., Моисеев М. Ю., Ахин М.Х., Захаров А. В., Цесько В. А. Алгоритмы анализа указателей для обнаружения дефектов в исходном коде // Системное программирование. 2009. C. 5-30.
16. Bush W., Pincus J., Sielaff D. A static analyzer for finding dynamic programming errors // Software: Practice and Experience. Vol. 30, iss. 7 (June 2000). John Wiley & Sons, Inc. NY, USA. P. 775-802.
17. Wang A., Fei H., Gu M., Song X. Verifying Java Programs By Theorem Prover HOL // Proceedings of the 30th Annual International Computer Software and Applications Conference. Vol. 01. IEEE Computer Society Washington DC, USA 2006. P. 139-142.
18. HOL 4 Kananaskis 6. <http://hol.sourceforge.net>
19. WHY - a software verification platform. <http://why.lri.fr>
20. Steensgaard B. Points-to analysis in almost linear time // Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages. New York, USA, 1996. P. 32-41.
21. Avots D., Dalton M., Livshits V., Lam M. Improving software security with a C pointer analysis // Proceedings of the 27th international conference on Software engineering. New York, USA, 2005. P. 332-341.
22. VCC. <http://vcc.codeplex.com>
23. Z3. <http://research.microsoft.com/en-us/um/redmond/projects/z3>
24. SMT-LIB. <http://www.smtlib.org>
Для цитирования:
Глухих М.И., Ицыксон В.М., Цесько В.А. Использование зависимостей для повышения точности статического анализа программ. Моделирование и анализ информационных систем. 2011;18(4):68-79.
For citation:
Glukhikh M.I., Itsykson V.M., Tsesko V.A. The Use of Dependencies for Improving the Precision of Program Static Analysis. Modeling and Analysis of Information Systems. 2011;18(4):68-79. (In Russ.)
Просмотров: 236
Послать статью по эл. почте 