Статический поиск ошибок повторной блокировки семафора
https://doi.org/10.15514/ISPRAS-2014-26(3)-5
Аннотация
В статье описывается алгоритм статического поиска ошибки повторной блокировки семафоров, позволяющий выдавать предупреждения с низким уровнем ложных срабатываний. Поиск ошибок рассмотрен для абстрактной библиотеки, включающей функции блокировки семафора, разблокировки семафора и условной блокировки семафора. Определено множество регулярных языков, моделирующих блокировки и разблокировки при конкретном исполнении программы. Определён домен, аппроксимирующий множество регулярных языков. Алгоритм реализован в терминах анализа потока данных. При анализе элементы домена используются в качестве свойств потока данных. Алгоритм описан для программы с одним семафором и без алиасов. В этом случае каждое выданное предупреждение должно соответствовать ошибке при конкретном выполнении. Алгоритм реализован в системе статического анализа Svace, разрабатываемой в Институте системного программирования Российской академии наук. Svace осуществляет анализ алиасов и сопоставление формальных и фактических параметров при вызове функции. Благодаря этому можно применять алгоритм поиска повторных блокировок для программы, содержащей только один семафор, а вся остальная работа будет выполнена системой Svace. Алгоритм поиска повтороных блокировок реализованный в Svace может выдавать некоторое количество ложных срабатываний, т. к. Svace выполняет неконсервативный анализ.
Ключевые слова
Список литературы
1. POSIX.1-2008, Technical Corrigendum 1, XSH/TC1-2008/0464 [121]
2. Cousot, P., & Cousot, R. (1992). Abstract interpretation and application to logic programs. The Journal of Logic Programming, 13(2), 103-179.
3. В.С. Несов. Автоматическое обнаружение дефектов при помощи межпроцедурного статического анализа исходного кода. Материалы XI Международной конференции «РусКрипто’2009».
4. А. Аветисян, А. Белеванцев, А. Бородин, В. Несов. Использование статического анализа для поиска уязвимостей и критических ошибок в исходном коде программ. Труды ИСП РАН, 2011, том 21.
5. Иванников, В. П., Белеванцев, А. А., Бородин, А. Е., Игнатьев, В. Н., Журихин, Д. М., Аветисян А.И., Леонов, М. И. Статический анализатор Svace для поиска дефектов в исходном коде программ. Труды Института системного программирования РАН, 2014, 26(1), с. 231-250, doi: 10.15514/ISPRAS-2014-26(1)-7.
6. POSIX.1-2008, Technical Corrigendum 1, XSH/TC1-2008/0464 [121]
7. Cousot, P., & Cousot, R. (1992). Abstract interpretation and application to logic programs. The Journal of Logic Programming, 13(2), 103-179.
8. Nesov V. S. Automatically Finding Bugs in Open Source Programs. Proceedings of the Third International Workshop on Foundations and Techniques for Open Source Software Certification (OpenCert 2009).
9. Avetisyan A.I., Belevantsev A.A., Borodin A.E., Nesov V. S. Ispol'zovanie staticheskogo analiza dlya poiska uyazvimostej i kriticheskikh oshibok v iskhodnom kode programm [Using static analysis to find vulnerabilities and critical errors in the source code of programs]. Trudy ISP RАN [The Proceedings of ISP RAS], 2011, vol 21 (in Russian).
10. Ivannikov V.P., Belevantsev A.A., Borodin A.E., Ignatyev V.N., Zhurikhin D.M., Avetisyan A.I., Leonov M.I. Staticheskij analizator Svace dlya poiska defektov v iskhodnom kode programm [Svace: static analyzer for detecting of defects in program source code]. Trudy ISP RАN [The Proceedings of ISP RAS], 2014, vol 26(1), pp. 231-250 (in Russian), doi: 10.15514/ISPRAS-2014-26(1)-7.
Рецензия
Для цитирования:
Бородин А.Е. Статический поиск ошибок повторной блокировки семафора. Труды Института системного программирования РАН. 2014;26(3):103-112. https://doi.org/10.15514/ISPRAS-2014-26(3)-5
For citation:
Borodin A. Static detection of error of double locking of mutex. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2014;26(3):103-112. (In Russ.) https://doi.org/10.15514/ISPRAS-2014-26(3)-5
Послать статью по эл. почте 