Verifying Probabilistic Correctness in Isabelle with pGCL
David Cock (NICTA, School of Computer Science, Engineering,, University of New South Wales)
TL;DR
This paper formalizes probabilistic Guarded Command Language (pGCL) within Isabelle/HOL, enabling rigorous verification of probabilistic security properties and integration with existing verified systems, thus advancing formal methods for security analysis.
Contribution
It introduces a shallow embedding of pGCL in Isabelle/HOL, facilitating extension and application to probabilistic security verification.
Findings
Successful formalization of pGCL in Isabelle/HOL
Demonstrated integration with existing verification projects
Applied to verify probabilistic security properties
Abstract
This paper presents a formalisation of pGCL in Isabelle/HOL. Using a shallow embedding, we demonstrate close integration with existing automation support. We demonstrate the facility with which the model can be extended to incorporate existing results, including those of the L4.verified project. We motivate the applicability of the formalism to the mechanical verification of probabilistic security properties, including the effectiveness of side-channel countermeasures in real systems.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.