MCHyper

A hardware model checker for hyperproperties

See also https://finkbeiner.groups.cispa.de/tools/mchyper/.

Introduction

Hyperproperties specify relations between multiple system executions and thereby generalize trace properties. HyperLTL is a temporal logic capable of expressing hyperproperties. It is an extension of the linear-time temporal logic (LTL) with quantification over trace variables. With HyperLTL, we can formalize many interesting hyperproperties including information-flow policies and symmetry requirements.

With MCHyper, it is possible to model check hardware circuits against these hyperproperties. To do this, MCHyper builds on the standard verification techniques from hardware model checking by using the hardware model checking tool ABC as its backend.

Online Interface and Tutorial

Try MCHyper without installation directly in our online interface and check out the tutorial.

Installation

1. Install and build the dependencies:
   • GHC (tested with versions 7.8.3, 8.4.4, and 8.10.1)
   • Additional Haskell dependencies: the parsec compiler framework, packages hashable and MissingH. Install using cabal update; cabal install parsec hashable MissingH. Make sure that ghc finds the dependencies when compiling.
   • Python (tested with version 2.7)
   • Aiger tools (version 1.9.4): Compile using ./configure; make in the directory aiger/.
   • ABC model checker (version 1.01): Compile using make. If necessary, install the readline package and a g++ compiler using, e.g., sudo apt-get install libreadline-dev build-essential.
2. Clone this repository: git clone https://github.com/reactive-systems/MCHyper.git
3. Compile MCHyper: cd src; ghc Main.hs; cd ..
4. Update the paths in the Python script mchyper.py pointing to the mchyper binary, the Aiger tools and to ABC. (E.g. abc_bin = os.path.dirname(sys.argv[0]) + '/../abc/abc')
5. Try MCHyper by running ./mchyper.py -f "Forall (AP \"select<0>\" 0)" case-studies/quantifier-alternation_2019/bakery/good_bakery.atom.nondet2.aag -pdr -cex.

The last step should output:

Hyper Hyper!
ABC is running (use '-v 1' to see output of ABC)

Counterexample found. Safety violation.
Writing counterexample to: tmp.cex.

If you obtain Error: Tool did not provide a model. make sure you are using unix line endigs.

Please note that this tool is in a prototype stage. Thus, there may be bugs in the implementation. If you find one, please contact Norine Coenen.

Usage

The main inputs of MCHyper are the system to check (as an Aiger circuit) and the formula that should be checked. You can run MCHyper on your own inputs or execute our case studies:

• The alternation-free case studies [FRS15] provide formulas.txt files containing the MCHyper calls that should be executed.
• The quantifier-alternation case studies [CFST19] provide shell scripts that run the respective experiments. More information on the software doping case study can be found in the corresponding paper [DBBFH17].
• The A-HyperLTL case studies [BCBFS21] provide shell scripts as well running the respective experiments.

To use MCHyper, execute the Python script and give formula, system circuit, strategy circuit (if necessary) and further options as arguments. The formula (following option -f) needs to be fully parenthesized, the operators are Forall, Exists, X (Next), Until, G, F, Neg, And, Or, Eq, Implies (amongst others, the full list of operators can be found in src/Logic.hs) and an atomic proposition ap is given as AP "ap" i, where i is the index of the quantifier it belongs to. A path to the system Aiger file is given without any preceding option. If a strategy circuit is provided, the path to this file is given after the option -s. Further options are -v followed by a number indicating the level of verbosity and options that should be used to call the backend tool ABC. Use -h or --help to print information on the usage of MCHyper.

The online interface also allows a more readable input format for the formula and using Verilog as input format for the system. Here, Yosys is used to obtain the corresponding Aiger circuit from the Verilog description.

Contributors

• Markus N. Rabe - Initial version handling the alternation-free fragment
• Norine Coenen - Extension to one quantifier alternation
• Norine Coenen and Jan Baumeister - Case study for A-HyperLTL

Publications

• [FRS15]: Algorithms for Model Checking HyperLTL and HyperCTL*, CAV 2015, Bernd Finkbeiner, Markus N. Rabe, Cesar Sanchez
• [CFST19]: Verifying Hyperliveness, CAV 2019, Norine Coenen, Bernd Finkbeiner, Cesar Sanchez, Leander Tentrup
• [BCBFS21]: A Temporal Logic for Asynchronous Hyperproperties, CAV 2021, Jan Baumeister, Norine Coenen, Borzoo Bonakdarpour, Bernd Finkbeiner, Cesar Sanchez

Some Other Related Publications

• [DFKRS12]: Model Checking Information Flow in Reactive Systems, VMCAI 2012, Rayna Dimitrova, Bernd Finkbeiner, Mate Kovacs, Markus N. Rabe, Helmut Seidl
• [CFKMRS14]: Temporal Logics for Hyperproperties, POST 2014, Michael Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K. Micinski, Markus N. Rabe, Cesar Sanchez
• [FR14]: The Linear-Hyper-Branching Spectrum of Temporal Logics, Information Technology 2014, Bernd Finkbeiner and Markus N. Rabe
• [DBBFH17]: Is your Software on Dope?, ESOP 2017, Pedro R. D'Argenio, Gilles Barthe, Sebastian Biewer, Bernd Finkbeiner, Holger Hermanns