PV4 ⊧ MCHyperproves given properties on a given circuit

Hardware model checker for hyperproperties

Application domain/field

• Model checking
• Information-flow
• Hyperproperties

Type of tool

Model checker

Expected input

• Circuit description
• HyperLTL formula

Format:

• Circuit: Verilog module or AIGER circuit
• HyperLTL formula: EAHyper or MCHyper (own) format

Expected output

It will either report that the property is proven, or it will provide a counterexample. You can also inspect the generated circuit. The user can also choose to get more verbose output.

Internals

MCHyper is a model checker for synchronous HyperLTL properties. It can handle up to one quantifier alternation. HyperLTL allows the user to specify temporal properties that relate multiple computation traces, also called hyperproperties. Therefore, the user can check a.o. information-flow properties and noninterference between two traces. It uses ABC as the backend for checking the reachability of a violation. If given a Verilog system as input, it will be converted into an Aiger circuit using Yosys.