A Conference Management System with Verified Document Confidentiality
Authors: Sudeep Kanav, Peter Lammich and Andrei Popescu
Paper Information
| Title: | A Conference Management System with Verified Document Confidentiality |
| Authors: | Sudeep Kanav, Peter Lammich and Andrei Popescu |
| Proceedings: | CAV 2014 LNCS Proceedings |
| Editors: | Armin Biere, Swen Jacobs and Roderick Bloem |
| Keywords: | information-flow security, confidentiality, declassification, unwinding relation, theorem proving, program synthesis, conference management system |
| Abstract: | ABSTRACT. 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 a novel security model and verification method generally applicable to systems describable as input-output automata. |
| Pages: | 17 |
| Talk: | Jul 19 15:30 |
| Paper: |  |