Использование зависимостей для повышения точности статического анализа программ

Михаил Игоревич Глухих; Владимир Михайлович Ицыксон; Вадим Александрович Цесько

doi:undefined

Использование зависимостей для повышения точности статического анализа программ

Михаил Игоревич Глухих, Владимир Михайлович Ицыксон, Вадим Александрович Цесько

Полный текст:

Аннотация

Статья посвящена разработке методов анализа зависимостей с целью повышения точности статического анализа. Рассмотрены причины, ведущие к снижению точности абстрактной интерпретации при обнаружении дефектов в программном коде. На различных примерах показана необходимость выявления и интерпретации зависимостей между программными объектами в ходе анализа. Приведена классификация зависимостей по различным признакам. Показана необходимость совокупного рассмотрения хранимых значений и зависимостей. Описан порядок выявления зависимостей при интерпретации присваиваний. Предложен метод интерпретации зависимостей на основе логического вывода, базирующегося на известных правилах логики и арифметики. Некоторые из разработанных методов реализованы в средстве обнаружения дефектов Digitek Aegis, показано значительное увеличение точности анализа.

Ключ. слова

статический анализ, абстрактная интерпретация, анализ зависимостей, обнаружение программных дефектов,

УДК: 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.)

Обратные ссылки

Обратные ссылки не определены.

Контент доступен под лицензией Creative Commons Attribution 4.0 License.

ISSN 1818-1015 (Print)
ISSN 2313-5417 (Online)

Логин
Пароль