Verified & fast probabilistic verification: Stepwise refinement of probabilistic model checking into an IEEE 754 floating-point implementation

Probabilistic systems exist everywhere. In wireless communication, that are all around us, there is a certain probability that a message gets lost. Furthermore, in leader election protocols, randomness may be used to resolve conflicts. It may be used to model biological processes in your cells as well as security protocols for your payments. Due to their probabilistic nature, these systems are difficult to get right, while their correctness may be crucial. For example, communication protocols that are not robust against random interactions may potentially cause harmful situations. We use probabilistic model checking to check the robustness of these systems.

In probabilistic model checking, the user provides a model and a specification for the system that they want to verify. The former is typically captured as a Markov decision process. A probabilistic model checker computes the probability that the system satisfies the specification. We use model checkers because of their strong theoretical foundations; their core algorithms are supported by formal guarantees. This means that we can trust that the output is correct.

However, (probabilistic) model checkers typically consist of huge code bases, making it difficult to determine whether the implementation actually corresponds to the algorithm whose correctness was proven. Moreover, most of these correctness proofs are pen-and-paper style. This may cause mistakes in proofs resulting in bugs. To solve this, one may formalise the model checking algorithms in a theorem prover. The theorem prover is a computer program that systematically checks every step in a proof against the basic axioms. Several theorem provers also support code generation from those formalisations, yielding correct-by-construction implementations against a specification. This solves the problem of how to determine whether an implementation corresponds to the algorithm it implements. However, correct implementations of real arithmetic, which correctness proofs for probabilistic model checking algorithms typically employ, need a representation that supports infinite precision. These representations tend to be inefficient in practice. Therefore, unverified implementations are often done using IEEE 754 floating-point arithmetic, which has finite precision, but is implemented with dedicated operations in most modern consumer hardware. On the one hand, this makes operation with floating-point numbers fast. On the other hand, this may introduce rounding errors in the computations, breaking the formal guarantees of the algorithm. Correct-by-construction implementations and the corresponding proofs, therefore, need to take this implementation detail into account.

In this work, we use the Isabelle/HOL theorem prover to formalise a pipeline of algorithms for probabilistic model checking from preprocessing to analysis. We employ the Isabelle refinement framework (IRF) to refine these algorithms down to verified code that performs on par with existing unverified implementations. To this end, we extend the IRF with support for refinement to IEEE 754 floating-point computations. We employ a safe rounding approach: By consistently rounding a variable either up or down, we obtain a bound on the real value that it refines. By performing a computation that provides a lower and upper bound of a value, we can determine a posteriori how “good” these bounds are.
To achieve a fully verified pipeline for a probabilistic model checker, we formalise a strongly connected components algorithm, a maximal end components algorithm and a reduction algorithm. These are graph algorithms that can be refined using standard functionality of the IRF. These algorithms are also necessary precomputations for interval iteration, which computes a lower bound and an upper bound to the probability of interest: reachability probabilities, i.e. given a model and a starting state, what is the probability that a run of this program reaches a target state. We provide a correctness proof for interval iteration using real arithmetic. Then, we use the safe rounding argument to refine those real numbers to IEEE 754 floating-point numbers. This allows us to do a relatively straightforward correctness proof for interval iteration on real numbers, and substitute them with floating-point numbers while preserving some of the interesting correctness properties.