Module monster::engine::rarity_simulation

Rarity Simulation

This module contains an implementation of rarity simulation, as descibed in the paper “Using Speculation for Sequential Equivalence Checking” by Brayton et. al.

Rarity simulation is a “guided random simulation” using heuristics to determine interesting states and which aims to reduce the time required to find bugs in a target application. Instead of symbolically pursuing all control branches and recording constraints, it concretely executes a fixed number of states. On each iteration, rarity simulation advances each state by a fixed amount of instruction cycles and records statistics which values were encountered over the entire execution state. Furthermore, at the end of the iteration, it uses the recorded statistics to determine the rarity of each state and only pursues a subset of rarest states, all other states are discarded and new states are copied from the remaining states or created to reach the number of states. Rarity simulation interations are repeated until a bug in any state is encountered or a specific amount of iterations have been completed.

To archive divergent states, the target application shall issue word-granularity read() system calls to receive random input values. Rarity simulation stores a list of subsequent inputs that were provided to the application. In case a state caused a bug, it is able to provide a list of inputs which provoke the bug.

The amount of iterations/cycles and the amount of states allows for a fine-grained control for finding bugs in depth or in breadth, respectively.

Modules

defaults

Structs

Executor
RarityBugInfo
RaritySimulation
RaritySimulationOptions
State	The state information of a running target

Enums

MeanType	Strategy for mean calculation
RaritySimulationError
Value

Type Definitions

RaritySimulationBug