No panic! Verification of Rust programs by symbolic execution

Marcus Lindner, Jorge Aparicius, Per Lindgren
[doi] [Google Scholar] [DBLP] [Citeseer]
Read: 12 May 2020

2018 IEEE 16th International Conference on Industrial Informatics (INDIN)
Volume
Pages 108-114
July 2018
Topic(s): tools verification
Note(s): Rust language, symbolic execution, extended static checking, contract driven development, modular verification, KLEE verifier
Papers: lindner:indin:2019

This paper describes the cargo-Rust that allows the KLEE verifier to be used to verify Rust programs. KLEE is a symbolic execution tool so using it to verify code leads to a path explosion problem. The solution taken in this paper is to use a contract driven development approach to enable modular verification. This reduces the path explosion problem to only involve the number of paths per function instead of the number of paths through the entire program.

Two related approaches that are mentioned are the KLEE Rust crate and the Symbolic Execution Engine for Rust (SEER).

  • Verification of safety functions implemented in Rust: A symbolic execution based approach [lindner:indin:2019]