Formalization of a Time-Parametric Type System In Isabelle/HOL


Programs which are secure under a naive information flow criterion
may still leak data through indirect channels. Of particular importance
are timing side channels, which were repeatedly used in recent years
to break cryptographic protocols. Already in 2000, Agat described a
While-language in which programs are typeable only if they do not have
timing leaks. The system is agnostic on the specifics of the timing
model, i.e., the type system is sound for many different models of
how long it takes to execute program fragments.
 
This talk reports on an ongoing formalization of Agat's language and
type system in Isabelle/HOL. It highlights and resolved some ambiguities
in Agat's paper and presents some successful Isabelle proofs. Finally,
the question of how to effectively use the parametricity of the type
system is discussed. In the future, the type system and Agat's soundness
proof of it shall be formalized.