Advertisement

Symbiotic 5: Boosted Instrumentation

(Competition Contribution)
  • Marek Chalupa
  • Martina Vitovská
  • Jan Strejček
Open Access
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10806)

Abstract

The fifth version of Symbiotic significantly improves instrumentation capabilities that the tool uses to participate in the category MemSafety. It leverages an extended pointer analysis re-designed for instrumenting programs with memory safety errors, and staged instrumentation reducing the number of inserted function calls that track or check the memory state. Apart from various bugfixes, we have ported Symbiotic (including the external symbolic executor Klee) to llvm 3.9 and improved the generation of violation witnesses by providing values of some variables.

1 Verification Approach

The basic approach of Symbiotic remains unchanged [7]: it uses instrumentation to reduce checking of specific properties (e.g. no-overflow or memory safety) to checking reachability of error locations. Then we apply slicing which removes the code that has no influence on reachability of these locations. Finally, we symbolically execute the sliced code using Klee  [1] to refute or confirm that an error location is reachable.

For many years, our attention has been focused mainly on slicing [2, 6, 8]. Only in 2016, we implemented a configurable instrumentation that enabled Symbiotic to check memory safety or, in general, any safety property. Consequently, Symbiotic  4 [4] participated for the first time in the category MemSafety where it won the bronze medal.

The instrumentation used in Symbiotic  4 to check memory safety inserts calls to functions that track every block of allocated memory and calls to functions that check validity of dereferences using the tracked information. A check is not inserted if a static pointer analysis guarantees that the dereferenced pointer points to a memory block that was allocated before. Later we have recognized a flaw of this optimization: a standard pointer analysis ignores memory deallocations and, hence, it can tell that a pointer can point to memory blocks allocated by specific program lines, but it does not tell whether these memory blocks are still allocated. As a result, Symbiotic  4 sometimes does not insert a check even if the dereference may be invalid and thus it may miss some bugs.

In Symbiotic  5, we have fixed and significantly boosted the instrumentation part. First, we have extended the above mentioned pointer analysis such that it takes into account deallocations as well. Second, the instrumentation now works in two stages. The first stage inserts the checks where extended pointer analysis cannot guarantee the dereference safety. Moreover, compared to Symbiotic  4, we use simpler checks if possible. For example, if a pointer analysis says that a given pointer points into a known fixed-size memory block, we just insert a check that the pointer’s offset is within the size of the block (without searching the tracked information about the block). The second stage inserts calls to memory tracking functions only to allocations of the memory blocks that can be accessed by some dereference instrumented in the first stage. Hence, we track only the information that may be possibly used in the checks.
Fig. 1.

Quantile plot of running times of the three considered configurations of Symbiotic  5. On the x-axis are the benchmarks sorted according to the corresponding running times and on the logarithmic y-axis are the times.

To evaluate the boosted instrumentation, we run the following three configurations of Symbiotic on 393 benchmarks of the SV-COMP 2017 meta category MemSafety and of the category MemSafety-TerminCrafted:
  • basic uses instrumentation without any pointer analysis,

  • ePTA uses extended pointer analysis (i.e. it is a fixed version of the instrumentation in Symbiotic  4),

  • staged uses extended pointer analysis and staged instrumentation.

Figure 1 clearly shows that the performance improvement brought by the extended pointer analysis itself is negligible compared to the performance improvement delivered by the extended pointer analysis in combination with staged instrumentation. For a precise description of the boosted instrumentation, experimental setup and results, we refer to [3].

Symbiotic  5 also changed the approach to error witness generation. Symbiotic  4 describes an errorneous run by a sequence of passed program locations. The sequence is often very long and it turned out to be too restrictive for witness checkers. Symbiotic  5 provides only the starting and target locations of the run and return values of some __VERIFIER_nondet* calls. More precisely, we provide return values of calls in main and such that they are called just once in the run. The witnesses are now more often confirmed by witness checkers.

2 Software Architecture

All components of Symbiotic are built on top of llvm  3.9 [9]. We use the clang compiler to compile the analyzed sources into llvm bitcode. Symbiotic consists of scripts written in Python that distribute work to three basic modules, all written in C++:

 
Instrumentation module.

This module inserts function calls to instructions according to a given configuration in JSON. The instrumented functions are implemented in C and compiled to llvm automatically by Symbiotic before the instrumentation process. We use this configurable instrumentation for instrumenting the memory safety property only. For instrumenting the no-overflow property, we use clang’s sanitizer as it works sufficiently well in this case.

Slicing module.

This module implements an interprocedural version of the slicing algorithm based on dependence graphs [5] altogether with analyses that are needed to compute dependencies between instructions, i.e. pointer analyses (including the extended pointer analysis as described in Sect. 1 that is used by the instrumentation) and analyses of reaching definitions.

Verification backend.

For deciding reachability of error locations, we currently use our clone of the open-source symbolic executor Klee  [1], that was ported to llvm  3.9 and modified to support error witness generation.

 

Before and after slicing, we optimize the code using available llvm’s optimizations. The rest of bitcode transformations that we use and whose nature is mostly technical (e.g. replacement of calls inserted by clang’s sanitizer to __VERIFIER_error calls) are implemented as llvm passes. All the components that transform bitcode take a bitcode as an input and give a valid bitcode as an output. This makes Symbiotic highly modular: any part (module) can be easily replaced or used as a stand-alone tool.

3 Strengths and Weaknesses

The main strength of the approach is its universality and modularity. The instrumentation can reduce any safety property to reachability checks and therefore no special monitors need to be incorporated into the verification backend. Indeed, any tool that can decide reachability of error locations can be plugged-in.

The main disadvantage of the current configuration is that symbolic execution does not satisfactory handle programs with unbounded loops. Moreover, Klee cannot generate invariants for loops.

4 Tool Setup and Configuration

  • Download: https://github.com/staticafi/symbiotic/releases/download/5.0.1/symbiotic-5.0.1.zip.

  • Installation: Unpack the archive.

  • Participation Statement: Symbiotic  5 participates in all categories.

  • Execution: Run \(\texttt {bin/symbiotic\;OPTS\;{<}source{>}}\), where available OPTS include:
    • –prp=file, which sets the property specification file to use,

    • –witness=file, which sets the output file for the witness,

    • –32, which sets the 32-bit environment,

    • –help, which shows the full list of possible options.

5 Software Project and Contributors

Symbiotic  5 has been developed by M. Chalupa and M. Vitovská under supervision of J. Strejček. The tool and its components are available under Apache-2.0 and MIT Licenses. The project is hosted by the Faculty of Informatics, Masaryk University. llvm and Klee are also available under open-source licenses. The project web page is: https://github.com/staticafi/symbiotic.

References

  1. 1.
    Cadar, C., Dunbar, D., Engler, D.: KLEE: unassisted and automatic generation of high-coverage tests for complex systems programs. In: OSDI, pp. 209–224. USENIX Association (2008)Google Scholar
  2. 2.
    Chalupa, M., Jonáš, M., Slaby, J., Strejček, J., Vitovská, M.: Symbiotic 3: new slicer and error-witness generation - (competition contribution). In: Chechik, M., Raskin, J.-F. (eds.) TACAS 2016. LNCS, vol. 9636, pp. 946–949. Springer, Heidelberg (2016).  https://doi.org/10.1007/978-3-662-49674-9_67CrossRefGoogle Scholar
  3. 3.
    Chalupa, M., Strejček, J., Vitovská, M.: Joint forces for memory safety checking. Submitted to SPIN 2018Google Scholar
  4. 4.
    Chalupa, M., Vitovská, M., Jonáš, M., Slaby, J., Strejček, J.: Symbiotic 4: beyond reachability - (competition contribution). In: Legay, A., Margaria, T. (eds.) TACAS 2017. LNCS, vol. 10206, pp. 385–389. Springer, Heidelberg (2017).  https://doi.org/10.1007/978-3-662-54580-5_28CrossRefGoogle Scholar
  5. 5.
    Ferrante, J., Ottenstein, K.J., Warren, J.D.: The program dependence graph and its use in optimization. In: Paul, M., Robinet, B. (eds.) Programming 1984. LNCS, vol. 167, pp. 125–132. Springer, Heidelberg (1984).  https://doi.org/10.1007/3-540-12925-1_33CrossRefGoogle Scholar
  6. 6.
    Slaby, J., Strejček, J.: Symbiotic 2: more precise slicing (competition contribution). In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 415–417. Springer, Heidelberg (2014).  https://doi.org/10.1007/978-3-642-54862-8_34CrossRefGoogle Scholar
  7. 7.
    Slabý, J., Strejček, J., Trtík, M.: Checking properties described by state machines: on synergy of instrumentation, slicing, and symbolic execution. In: Stoelinga, M., Pinger, R. (eds.) FMICS 2012. LNCS, vol. 7437, pp. 207–221. Springer, Heidelberg (2012).  https://doi.org/10.1007/978-3-642-32469-7_14CrossRefGoogle Scholar
  8. 8.
    Slaby, J., Strejček, J., Trtík, M.: Symbiotic: synergy of instrumentation, slicing, and symbolic execution (competition contribution). In: Piterman, N., Smolka, S.A. (eds.) TACAS 2013. LNCS, vol. 7795, pp. 630–632. Springer, Heidelberg (2013).  https://doi.org/10.1007/978-3-642-36742-7_50CrossRefGoogle Scholar
  9. 9.

Copyright information

© The Author(s) 2018

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 book are included in the book's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the book'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.

Authors and Affiliations

  • Marek Chalupa
    • 1
  • Martina Vitovská
    • 1
  • Jan Strejček
    • 1
  1. 1.Masaryk UniversityBrnoCzech Republic

Personalised recommendations