Verifying document confidentiality of a conference management system

Se ha publicado un artículo de verificación formal con Isabelle/HOL titulado Verifying document confidentiality of a conference management system.

Sus autores son Sudeep Kanav, Peter Lammich y Andrei Popescu (de la Universidad Técnica de Munich).

Su resumen es

We present a case study in verified security for realistic systems: the implementation of a conference management system, whose functional kernel is faithfully represented in the Isabelle theorem prover, where we specify and verify confidentiality properties. The various theoretical and practical challenges posed by this development led to some novel security model and verification method that we hope is reusable for other multi-user document management systems.