Skip to main content
Top

2018 | OriginalPaper | Chapter

Verifying Rust Programs with SMACK

Authors : Marek Baranowski, Shaobo He, Zvonimir Rakamarić

Published in: Automated Technology for Verification and Analysis

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

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.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

  • über 102.000 Bücher
  • über 537 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Maschinenbau + Werkstoffe
  • Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 390 Zeitschriften

aus folgenden Fachgebieten:

  • Automobil + Motoren
  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Elektrotechnik + Elektronik
  • Energie + Nachhaltigkeit
  • Maschinenbau + Werkstoffe




 

Jetzt Wissensvorsprung sichern!

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

  • über 67.000 Bücher
  • über 340 Zeitschriften

aus folgenden Fachgebieten:

  • Bauwesen + Immobilien
  • Business IT + Informatik
  • Finance + Banking
  • Management + Führung
  • Marketing + Vertrieb
  • Versicherung + Risiko




Jetzt Wissensvorsprung sichern!

Literature
1.
go back to reference Balasubramanian, A., Baranowski, M.S., Burtsev, A., Panda, A., Rakamarić, Z., Ryzhyk, L., et al.: System programming in rust: beyond safety. In: HotOS (2017) Balasubramanian, A., Baranowski, M.S., Burtsev, A., Panda, A., Rakamarić, Z., Ryzhyk, L., et al.: System programming in rust: beyond safety. In: HotOS (2017)
2.
go back to reference 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) 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)
3.
go back to reference Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard: Version 2.0. In: SMT (2010) Barrett, C., Stump, A., Tinelli, C.: The SMT-LIB standard: Version 2.0. In: SMT (2010)
5.
go back to reference de Moura, L.M., Bjørner, N.: Z3: an efficient SMT solver. In: TACAS (2008) de Moura, L.M., Bjørner, N.: Z3: an efficient SMT solver. In: TACAS (2008)
6.
go back to reference Hahn, F.: Rust2Viper: building a static verifier for rust. Master’s thesis, ETH (2016) Hahn, F.: Rust2Viper: building a static verifier for rust. Master’s thesis, ETH (2016)
7.
go back to reference He, S., Rakamarić, Z.: Counterexample-guided bit-precision selection. In: APLAS (2017) He, S., Rakamarić, Z.: Counterexample-guided bit-precision selection. In: APLAS (2017)
8.
go back to reference Jung, R., Jourdan, J.-H., Krebbers, R., Dreyer, D.: RustBelt: securing the foundations of the Rust programming language. In: POPL (2017) Jung, R., Jourdan, J.-H., Krebbers, R., Dreyer, D.: RustBelt: securing the foundations of the Rust programming language. In: POPL (2017)
9.
go back to reference Lal, A., Qadeer, S., Lahiri, S.K.: A solver for reachability modulo theories. In: CAV (2012) Lal, A., Qadeer, S., Lahiri, S.K.: A solver for reachability modulo theories. In: CAV (2012)
10.
go back to reference Lattner, C., Adve, V.: LLVM: a compilation framework for lifelong program analysis & transformation. In: CGO (2004) Lattner, C., Adve, V.: LLVM: a compilation framework for lifelong program analysis & transformation. In: CGO (2004)
11.
go back to reference Rakamarić, Z., Emmi, M.: SMACK: decoupling source language details from verifier implementations. In: CAV (2014) Rakamarić, Z., Emmi, M.: SMACK: decoupling source language details from verifier implementations. In: CAV (2014)
14.
go back to reference Toman, J., Pernsteiner, S., Torlak, E.: CRUST: a bounded verifier for rust. In: ASE (2015) Toman, J., Pernsteiner, S., Torlak, E.: CRUST: a bounded verifier for rust. In: ASE (2015)
Metadata
Title
Verifying Rust Programs with SMACK
Authors
Marek Baranowski
Shaobo He
Zvonimir Rakamarić
Copyright Year
2018
DOI
https://doi.org/10.1007/978-3-030-01090-4_32

Premium Partner