Advertisement

Verifying Rust Programs with SMACK

  • Marek BaranowskiEmail author
  • Shaobo He
  • Zvonimir Rakamarić
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 11138)

Abstract

Rust is an emerging systems programming language with guaranteed memory safety and modern language features that has been extensively adopted to build safety-critical software. However, there is currently a lack of automated software verifiers for Rust. In this work, we present our experience extending the SMACK verifier to enable its usage on Rust programs. We evaluate SMACK on a set of Rust programs to demonstrate a wide spectrum of language features it supports.

References

  1. 1.
    Balasubramanian, A., Baranowski, M.S., Burtsev, A., Panda, A., Rakamarić, Z., Ryzhyk, L., et al.: System programming in rust: beyond safety. In: HotOS (2017)Google Scholar
  2. 2.
    Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., Leino, K.R.M.: Boogie: a modular reusable verifier for object-oriented programs. In: FMCO (2005)Google Scholar
  3. 3.
    Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard: Version 2.0. In: SMT (2010)Google Scholar
  4. 4.
    Cross-platform Rust rewrite of the GNU coreutils. https://github.com/uutils/coreutils
  5. 5.
    de Moura, L.M., Bjørner, N.: Z3: an efficient SMT solver. In: TACAS (2008)Google Scholar
  6. 6.
    Hahn, F.: Rust2Viper: building a static verifier for rust. Master’s thesis, ETH (2016)Google Scholar
  7. 7.
    He, S., Rakamarić, Z.: Counterexample-guided bit-precision selection. In: APLAS (2017)Google Scholar
  8. 8.
    Jung, R., Jourdan, J.-H., Krebbers, R., Dreyer, D.: RustBelt: securing the foundations of the Rust programming language. In: POPL (2017)Google Scholar
  9. 9.
    Lal, A., Qadeer, S., Lahiri, S.K.: A solver for reachability modulo theories. In: CAV (2012)Google Scholar
  10. 10.
    Lattner, C., Adve, V.: LLVM: a compilation framework for lifelong program analysis & transformation. In: CGO (2004)Google Scholar
  11. 11.
    Rakamarić, Z., Emmi, M.: SMACK: decoupling source language details from verifier implementations. In: CAV (2014)Google Scholar
  12. 12.
    The Rust programming language. https://www.rust-lang.org
  13. 13.
    SMACK software verifier and verification toolchain. http://smackers.github.io
  14. 14.
    Toman, J., Pernsteiner, S., Torlak, E.: CRUST: a bounded verifier for rust. In: ASE (2015)Google Scholar

Copyright information

© Springer Nature Switzerland AG 2018

Authors and Affiliations

  • Marek Baranowski
    • 1
    Email author
  • Shaobo He
    • 1
  • Zvonimir Rakamarić
    • 1
  1. 1.School of ComputingUniversity of UtahSalt Lake CityUSA

Personalised recommendations