Verifying Probabilistic Correctness in Isabelle with pGCL
This paper presents a formalization of pGCL in Isabelle/HOL. Using a shallow embedding, the authors demonstrate close integration with existing automation support. They demonstrate the facility with which the model can be extended to incorporate existing results, including those of the L4.verified project. They motivate the applicability of the formalism to the mechanical verification of probabilistic security properties, including the effectiveness of side-channel countermeasures in real systems. They present a new formalization of the pGCL programming logic within Isabelle/HOL. The motivation for this paper is the desire for formal, mechanized verification of probabilistic security properties (in particular, bounds on side-channel vulnerability) for real systems.