MCHyper – A Model Checker for Hyperproperties

Copyright © 2015 Markus N. Rabe, Saarland University

Introduction

Model checking has become a critical technique in the EDA industry. Since the early days of model checking, the algorithms have improved a lot and are now able to handle substantial hardware designs. Today, various complementary verification techniques are available, including binary decision diagrams (BDDs), SAT-based bounded model checking (BMC), interpolation, and Aaron Bradley’s IC3.

Temporal logics, like LTL, CTL, and CTL*, have proven to be flexible specification languages for various application areas and their verification is well understood. However, a class of system properties with ever growing importance turned our to be inherently not expressible in standard temporal logics. One example are properties that specify how information spreads (flows) in a system, so called information-flow properties. Information-flow is typically specified as the comparison of multiple executions of the system.

Recent extensions to temporal logics alleviate this shortcoming. HyperLTL and HyperCTL* introduce quantifiers that extend the quantification of CTL* by path variables. MCHyper is a model checker for the alternation-free fragments of HyperLTL and HyperCTL* that builds on the standard verification techniques from hardware model checking. Thereby, MCHyper enables the verification of hardware designs for intricate information-flow properties. HyperLTL and HyperCTL* also include properties from other application domains. The case studies that are provided with this tool include the analysis of symmetries among the processes in a mutual exclusion protocol, and the distance of code words of error resistant codes.

Install MCHyper using Homebrew

  1. Tap reactive systems repository: $ brew tap reactive-systems/react
  2. Install MCHyper from source: $ brew install mchyper

Install MCHyper Manually

Dependencies:

  1. Compile MCHyper via $ ghc mchypertool/Main.hs -imchypertool -o mchyper. The implementation uses the ‘parsec’ compiler framework and the packets ‘hashable’ and ‘MissingH’. You can fetch them via the Haskell build system ‘cabal’, which typically comes with the GHC distribution: run $ cabal update; cabal install parsec hashable MissingH (this may take a while).
  1. Compile the Aiger tools in the directory aiger/: $ ./configure; make
  1. Compile ABC via make (this may take a while). Depending on your system, you may need to install the ‘readline’ package and a g++ compiler. In Ubuntu you can use the following command: $ sudo apt-get install libreadline-dev build-essential
  1. Update the path to the mchyper-binary, the Aiger tools and to ABC in the Python script mc.py.
  1. You are ready to use MCHyper! Try the following command:
./mchyper.py -f "Exists (AP \"c\" 0)" testmodels/halfadder.aag -pdr -cex

Note that this tool is in a prototype stage. Thus, there may be bugs in the implementation. If you find one, please contact the author.

Download

License

The prototype is free for use in academic context. For all other purposes, including integration into other tools, please contact the author Markus N. Rabe.

Related Publications

[FRS15] Algorithms for Model Checking HyperLTL and HyperCTL*.
with Bernd Finkbeiner and César Sánchez.
Accepted at CAV 2015.
Implementation
[FR14] The Linear-Hyper-Branching Spectrum of Temporal Logics
Bernd Finkbeiner and Markus N. Rabe
Information Technology 2014
[CFKMRS14] Temporal Logics for Hyperproperties
Michael Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K. Micinski, Markus N. Rabe, and César Sánchez
POST 2014
Implementation
Full version available at arxiv
[DFKRS12] Model Checking Information Flow in Reactive Systems
Rayna Dimitrova, Bernd Finkbeiner, Máté Kovács, Markus N. Rabe, and Helmut Seidl
VMCAI 2012
Won the RS3 Best Paper Award! (Best among 27 papers of the RS3 project.)

Hyper

Contact

Markus N. Rabe