Extending DIVINE with Symbolic Verification Using SMT
- 3.6k Downloads
DIVINE is an LLVM-based verification tool focusing on analysis of real-world C and C++ programs. Such programs often interact with their environment, for example via inputs from users or network. When these programs are analyzed, it is desirable that the verification tool can deal with inputs symbolically and analyze runs for all inputs. In DIVINE, it is now possible to deal with input data via symbolic computation instrumented into the original program at the level of LLVM bitcode. Such an instrumented program maintains symbolic values internally and operates directly on them. Instrumentation allows us to enhance the tool with support for symbolic data without substantial modifications of the tool itself. Namely, this competition contribution uses SMT formulae for representation of input data.
1 Verification Approach and Software Architecture
DIVINE is an explicit-state model checker primarily designed to detect bugs in multithreaded programs . Testing of multithreaded programs is a known hard problem because of nondeterminism in the execution caused by thread interleavings. To deal with control flow nondeterminism, DIVINE exhaustively explores all relevant executions of the multithreaded program. Unfortunately, this explicit approach fails to deal with data nondeterminism caused by communication with the environment. In order to verify a program with inputs, DIVINE would need to examine all the possible inputs of the program. This would cause enormous state-space explosion and would be unmanageable in reasonable time and space.
In order to maintain efficiency we do not transform the entire program, but only the parts that might come into contact with symbolic values. As shown in Fig. 2, the program is analyzed starting from input points, and all downstream operations are augmented (s_add, s_eq), but concrete computation remains unchanged (fun). The transformed program uses a special operation called lift, which takes a concrete value and returns a symbolic one. The result of lifting * represents an arbitrary input value.
2 Strengths and Weaknesses
In comparison to bounded model checkers, DIVINE ’s strength is sound verification – it explores a whole state-space and uses formulae in bitvector theory to precisely represent symbolic values. However DIVINE produced a few wrong results in the competition, these should not be possible in theory and likely stem from implementation errors in the verification tool.
Our compilation-based approach has allowed us to increase modularity of the tool. It is easy to change the representation of symbolic values, the verification algorithm and even the entire verifier while preserving the transformation. Another upside is that the implementation of symbolic operations is subject to checks performed by the verifier.
On the other hand, the current implementation is only a proof of concept. Our primary goal was to show that a compilation-based approach may compete with interpretation-based approaches even though it increases the size of the verified program and therefore possibly also verification complexity. Currently, the transformation can only handle scalar values, hence verification of programs with symbolic memory is not yet possible.
3 Tool Setup and Configuration
The verifier archive can be found on the SV-COMP 2019 page2 under the name DIVINE-SMT. In case the binary distribution does not work on your system, we also provide a source distribution and build instructions at https://divine.fi.muni.cz/2019/sv-comp-smt.
It is usually sufficient to run divine as follows: divine check --symbolic --svcomp TESTCASE.c. This command runs DIVINE with the SMT-based representation of symbolic data described in this paper and with SV-COMP-specific instrumentation.
For SV-COMP benchmarks, additional settings are handled by the divine-svc wrapper.3 The only option used for DIVINE-SMT is --32 for 32 bit categories. The wrapper sets DIVINE options based on the property file and the benchmark. In particular, it enables symbolic mode if any nondetermism is found, sequential mode if no threads are found, and it sets which errors should be reported based on the property file. It also generates witness files. More details can be found on the aforementioned distribution page.
DIVINE participates in all categories, but it can only produce non-unknown results for the error reachability and memory safety categories.
4 Software Project and Contributors
The project home page is https://divine.fi.muni.cz. Many people have contributed to DIVINE, including Petr Ročkai, Henrich Lauko and Vladimír Štill. DIVINE is open source software distributed under the ISC license.
Given a symbolic value x and a branch with condition x < 5, the condition can be both true and false. The program makes a nondeterministic choice and extends the path condition with \(x < 5\) or \(x \ge 5\) respectively.
To be found in the main directory of the binary archive, or in the tools directory of the source distribution. Usage: divine-svc DIVINE_BINARY PROP_FILE [OPTIONS] TESTCASE.c.
- 1.Beyer, D.: Automatic verification of c and java programs: Sv-comp 2019. In: Beyer, D., Huisman, M., Kordon, F., Steen, B. (eds.) TACAS 2019, Part III. LNCS, vol. 11429, pp. 133–155. Springer, Cham (2019)Google Scholar
- 2.Cadar, C., Dunbar, D., Engler, D.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: Operating Systems Design and Implementation, pp. 209–224. USENIX Association (2008)Google Scholar
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.