Reseña: From operational models to information theory; side channels in pGCL with Isabelle
Se ha publicado un artículo de razonamiento formalizado en Isabelle titulado From operational models to information theory; side channels in pGCL with Isabelle.
Su autor es David Cock (del Software Systems Research Group, NICTA).
Su resumen es
In this paper, we formally derive the probabilistic security predicate (expectation) for a guessing attack against a system with side-channel leakage, modelled in pGCL. Our principal theoretical contribution is to link the process-oriented view, where attacker and system execute particular model programs, and the information-theoretic view, where the attacker solves an optimal-decoding problem, viewing the system as a noisy channel. Our practical contribution is to illustrate the selection of probabilistic loop invariants to verify such security properties, and the demonstration of a mechanical proof linking traditionally distinct domains.
El trabajo se presentó ayer en el ITP 2014 (5th Conference on Interactive Theorem Proving).
El código de las correspondientes teorías en Isabelle/HOL se encuentra aquí.