Predicate extension of symbolic memory graphs for analysis of memory safety correctness
https://doi.org/10.15514/ISPRAS-2019-31(6)-1
Abstract
Safety-critical systems require additional effort to comply with specifications. One of the required specification is correct memory usage. The article describes an efficient method for static verification against memory safety errors as a combination of Symbolic Memory Graphs and predicate abstraction on symbolic values used in graph. In this article, we introduce an extension of Symbolic Memory Graphs. In addition to symbolic values, the graph stores predicates over symbolic values, which allow to track the relationship between symbolic values in the graph. We also expand existing vertex types to support arbitrary abstract regions, which allow us to represent such dynamic data structures as lists and trees. One of the types of abstract regions is also the ODM region, which presents a special kind of on-demand memory that occurs when analyzing incomplete programs. For this memory, the size and structure of the contents are not known in advance, but it is believed that such memory can be operated safely. The method is implemented in CPAchecker tool. Practical usage is demonstrated on Linux kernel modules. The practical contribution of our work is to reduce false error messages by constructing more accurate abstractions using predicates over symbolic values.
Supporting agencies: The research was supported by RFBR grant 18-01-00426.
About the Authors
Anton Aleksandrovich Vasiliev
Ivannikov Institute for System Programming of the Russian Academy of Sciences
Russian Federation
Intern researcher, PhD student of ISP RAS
Russian Federation
Intern researcher, PhD student of ISP RAS
Vadim Sergeevich Mutilin
Ivannikov Institute for System Programming of the Russian Academy of Sciences
Russian Federation
PhD in physical and mathematical sciences, Senior Researcher
Russian Federation
PhD in physical and mathematical sciences, Senior Researcher
References
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.
Review
For citations:
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
Email this article 