Анализ корректности работы с памятью с использованием расширения теории символьных графов предикатами над символьными значениями
https://doi.org/10.15514/ISPRAS-2019-31(6)-1
Аннотация
В работе мы рассмотрим подход статической верификации исходного кода программы на предмет корректной работы с памятью. Метод основывается на использовании символьных графов для представлении памяти программы. В работе представлено расширение символьных графов памяти, позволяющее использовать предикаты над символьными значениями для повышения точности анализа. Предикаты позволяют отсекать недостижимые пути, уменьшая количество ложных сообщений об ошибках, а также находить новые ошибки за счет добавления новых проверок на символьных значениях. Метод реализован на основе инструмента CPAchecker. Практическая полезность продемонстрирована на драйверах ядра операционной системы Linux.
Ключевые слова
символьные графы памяти,
верификация,
модель памяти,
предикатные абстракции,
динамические структуры данных
При поддержке: Работа поддержана грантом РФФИ 18-01-00426
Об авторах
Антон Александрович Васильев
Институт системного программирования им. В.П.Иванникова РАН
Россия
Стажер-исследователь, аспирант ИСП РАН
Россия
Стажер-исследователь, аспирант ИСП РАН
Вадим Сергеевич Мутилин
Институт системного программирования им. В.П.Иванникова РАН
Россия
Кандидат физико-математических наук, старший научный сотрудник
Россия
Кандидат физико-математических наук, старший научный сотрудник
Список литературы
1. Klein G., Elphinstone K. et al. sel4: Formal verification of an os kernel. In Proc. of the ACM SIGOPS 22nd Symposium on Operating Systems Principles, 2009, pp. 207–220.
2. Stewart G., Beringer L., Cuellar S., Appel A.W. Compositional compcert. In Proc. of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2005, pp. 275–287.
3. Beyer D., Keremoglu M.E.: CPAchecker: A tool for configurable software verification. Lecture Notes in Computer Science, vol. 6806, 2011, pp. 184-190.
4. Donaldson A.F., Haller L., Kroening D., R ̈ummer P. Software verification using k-induction. Lecture Notes in Computer Science, vol. 6887, 2011, pp. 351-368.
5. Clarke E., Grumberg O., Jha S., Lu Y., Veith H. Counterexample-guided abstraction refinement. Lecture Notes in Computer Science, vol. 1855, 2000, pp. 154–169.
6. Beyer D., Keremoglu, M.E., Wendler, P. Predicate abstraction with adjustable-block encoding. In Proc. of the 10th International Conference on Formal Methods in Computer-Aided Design, 2010, pp. 189–197.
7. Beyer D., Henzinger T., Theoduloz G. Program analysis with dynamic precision adjustment. In Proc. of the 23rd IEEE/ACM International Conference on Automated Software Engineering, 2008. pp. 29–38.
8. Beyer D., Löwe S. Explicit-state software model checking based on CEGAR and interpolation. Lecture Notes in Computer Science, vol. 7793, 2013, pp. 146–162.
9. Biere A., Cimatti A., Clarke E.M., Zhu Y. Symbolic model checking without bdds. Lecture Notes in Computer Science, vol. 1579, 1999, pp. 193–207.
10. Graf S., Saidi H. Construction of abstract state graphs with PVS. Lecture Notes in Computer Science, vol. 1254, 1997, pp. 72–83.
11. Andrianov P., Friedberger K., Mandrykin M., Mutilin V., Volkov A. CPA-BAM-BnB: Block-abstraction memoization and region-based memory models for predicate abstractions. Lecture Notes in Computer Science, vol. 10206, 2017, pp. 355–359.
12. Yang H., Lee O., Berdine J., Calcagno C., Cook B., Distefano D., O’Hearn P. Scalable shape analysis for systems code. Lecture Notes in Computer Science, vol. 5123, 2008, pp. 385–398.
13. Volkov A., Mandrykin M. Predicate Abstractions Memory Modeling Method with Separation into Disjoint Regions. Trudy ISP RAN/Proc. ISP RAS, vol. 29, issue 4, 2017, pp. 203-216. DOI: 10.15514/ISPRAS-2017-29(4)-13.
14. Beyer D., Henzinger T., Jhala R., Majumdar R. The software model checker BLAST. International Journal on Software Tools for Technology Transfer, vol. 9, issue 5-6, 2007, 505–525.
15. Shved P., Mandrykin M., Mutilin V. Predicate analysis with BLAST 2.7. Lecture Notes in Computer Science, vol. 7214, 2012, pp. 525–527.
16. Ball T., Bounimova E., Kumar R., Levin V. SLAM2: Static driver verification with under 4% false alarms. In Proc. Of the 10th International Conference on Formal Methods in Computer-Aided Design, 2010. pp. 35–42.
17. Sagiv M., Reps T.W., Wilhelm R. Parametric shape analysis via 3-valued logic. ACM Transactions on Programming Languages and Systems, vol. 24, issue 3, 2002, pp. 217–298.
18. Beyer D., Henzinger T.A., Théoduloz G. Lazy shape analysis. Lecture Notes in Computer Science, vol. 4144, 2006, pp. 532–546.
19. Reynolds J.C. Separation logic: A logic for shared mutable data structures. In Proc. of the 17th Annual IEEE Symposium on Logic in Computer Science, 2002, pp. 55–74.
20. Berdine J., Cook B., Ishtiaq S. Slayer Memory safety for systems-level code. Lecture Notes in Computer Science, vol. 6806, 2011, pp. 178-183.
21. Jacobs B., Smans J., Piessens F. A quick tour of the verifast program verifier. Lecture Notes in Computer Science, vol. 6461, 2010, pp. 304–311.
22. Volkov A., Mandrykin M. Predicate Abstractions Memory Modeling Method with Separation into Disjoint Regions. Trudy ISP RAN/Proc. ISP RAS, vol. 29, issue 4, 2017, pp. 203-216. DOI: 10.15514/ISPRAS-2017-29(4)-13.
23. Calcagno C., Distefano D. et al. Moving fast with software verification. Lecture Notes in Computer Science, vol. 9058, 2015, pp. 3-11.
24. Beyer D. Automatic verification of C and Java Programs: SV-COMP 2019. Lecture Notes in Computer Science, vol. 11429, 2019, pp. 133–155.
25. Dudka K., Peringer P., Vojnar T.: Byte-precise verification of low-level list manipulation. Lecture Notes in Computer Science, vol. 7935, 2013, pp. 215–237.
26. Vasilyev A.A. Static verification for memory safety of Linux kernel drivers. Trudy ISP RAN/Proc. ISP RAS, vol. 30, issue 6, 2018. pp. 143-160. DOI: 10.15514/ISPRAS-2018-30(6)-8.
27. Novikov E., Zakharov I. Towards automated static verification of GNU C programs. Lecture Notes in Computer Science, vol. 10742, 2018, pp. 402–416.
Рецензия
Для цитирования:
Васильев А.А., Мутилин В.С. Анализ корректности работы с памятью с использованием расширения теории символьных графов предикатами над символьными значениями. Труды Института системного программирования РАН. 2019;31(6):7-20. https://doi.org/10.15514/ISPRAS-2019-31(6)-1
For citation:
Vasiliev A.A., Mutilin V.S. Predicate extension of symbolic memory graphs for analysis of memory safety correctness. Proceedings of the Institute for System Programming of the RAS (Proceedings of ISP RAS). 2019;31(6):7-20. (In Russ.) https://doi.org/10.15514/ISPRAS-2019-31(6)-1
Послать статью по эл. почте 