Исследование свойств алгоритма слайсинга предиката пути
https://doi.org/10.15514/ISPRAS-2022-34(3)-1
Аннотация
Безопасный цикл разработки ПО (SDL) применяется для повышения надежности и защищенности программного обеспечения. В жизненный цикл программы добавляются этапы для проверки свойств ее безопасности. Среди прочего повсеместно применяется фаззинг-тестирование, которое позволяет обнаруживать аварийные завершения и зависания анализируемого кода. Гибридный подход, совмещающий в себе фаззинг и динамическую символьную интерпретацию, показал еще большую эффективность, чем классический фаззинг. Более того, символьная интерпретация позволяет добавлять дополнительные проверки, называемые предикатами безопасности, которые ищут ошибки работы с памятью и неопределенное поведение. Данная статья исследует свойства и характеристики алгоритма слайсинга предиката пути, который позволяет устранять избыточные ограничения из предиката пути без потери точности. В статье доказывается, что алгоритм конечен и не теряет решений. Более того, производится оценка асимптотической сложности алгоритма.
Ключевые слова
динамическая символьная интерпретация,
DSE,
предикат пути,
слайсинг,
устранение избыточных ограничений,
анализ бинарного кода
При поддержке: Работа поддержана грантом РФФИ № 20-07-00921 A
Об авторе
Алексей Вадимович ВИШНЯКОВ
https://vishnya.xyz/
Институт системного программирования им. В.П. Иванникова РАН
Россия
Институт системного программирования им. В.П. Иванникова РАН
Россия
Младший научный сотрудник отдела компиляторных технологий в ИСП РАН, закончил бакалавриат и магистратуру ВМК МГУ
Список литературы
1. M. Howard and S. Lipner. The security development lifecycle. SDL: A Process for Developing Demonstrably More Secure Software. Microsoft Press, Redmond, 2006, 348 p.
2. ISO/IEC 15408-3:2008: Information Technology – Security Techniques –Evaluation Criteria for It Security – Part 3: Security Assurance Components. ISO Geneva, Switzerland, 2008.
3. ГОСТ Р 56939-2016: Защита информации. Разработка безопасного программного обеспечения. Общие требования. Национальный стандарт Российской Федерации, 2016 / GOST R 56939-2016: Information Protection. Secure Software Development. General Requirements, National Standard of Russian Federation, 2016 (in Russian).
4. K. Serebryany. Continuous Fuzzing with libFuzzer and AddressSanitizer. In Proc. of the the 2016 IEEE Cybersecurity Development (SecDev), 2016, p. 157.
5. A. Fioraldi, D. Maier et al. AFL++: combining incremental steps of fuzzing research. In Proc. of the 14th USENIX Workshop on Offensive Technologies (WOOT 20), 2020, 12 p.
6. I. Yun, S. Lee et al. QSYM: a practical concolic execution engine tailored for hybrid fuzzing. In Proc. of the 27th USENIX Security Symposium, 2018, pp. 745-761.
7. S. Poeplau and A. Francillon. Symbolic execution with SymCC: don’t interpret, compile! In Proc. of the 9th USENIX Security Symposium (USENIX Security 20), 2020, pp. 181-198.
8. S. Poeplau and A. Francillon. SymQEMU: compilation-based symbolic execution for binaries. In Proc. of the 2021 Network and Distributed System Security Symposium, 2021, 18 p.
9. L. Borzacchiello, E. Coppa, and C. Demetrescu. FUZZOLIC: mixing fuzzing and concolic execution. Computers & Security, vol. 108, 2021, article no. 102368.
10. E. J. Schwartz, T. Avgerinos, and D. Brumley. All you ever wanted to know about dynamic taint analysis and forward symbolic execution (but might have been afraid to ask). In Proc. of the 2010 IEEE Symposium on Security and Privacy, 2010, pp. 317-331.
11. R. Baldoni, E. Coppa et al. A survey of symbolic execution techniques. ACM Computing Surveys, vol. 51, issue 3, 2018, article no. 50, pp. 1-39.
12. A. Vishnyakov, V. Logunova et al. Symbolic security predicates: hunt program weaknesses. In Proc. of the 2021 Ivannikov ISPRAS Open Conference (ISPRAS), 2021, pp. 76-85.
13. A. Vishnyakov, A. Fedotov et al. Sydr: cutting edge dynamic symbolic execution. In Proc. of the 2020 Ivannikov ISPRAS Open Conference (ISPRAS), 2020, pp. 46-54.
14. C. Cadar, D. Dunbar, and D. R. Engler. KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In Proc. of the 8th USENIX Conference on Operating Systems Design and Implementation, pp. 209-224, 2008.
Рецензия
Для цитирования:
ВИШНЯКОВ А.В. Исследование свойств алгоритма слайсинга предиката пути. Труды Института системного программирования РАН. 2022;34(3):7-12. https://doi.org/10.15514/ISPRAS-2022-34(3)-1
For citation:
VISHNYAKOV A.V. Analyzing properties of path predicate slicing algorithm. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2022;34(3):7-12. (In Russ.) https://doi.org/10.15514/ISPRAS-2022-34(3)-1
Послать статью по эл. почте 