CoSMed: a confidentiality-verified social media platform
Conference paper
Bauereiß, T., Pesenti Gritti, A., Popescu, A. and Raimondi, F. 2016. CoSMed: a confidentiality-verified social media platform. ITP 2016: 7th International Conference on Interactive Theorem Proving. Nancy, France 22 - 25 Aug 2016 Springer. pp. 87-106 https://doi.org/10.1007/978-3-319-43144-4_6
Type | Conference paper |
---|---|
Title | CoSMed: a confidentiality-verified social media platform |
Authors | Bauereiß, T., Pesenti Gritti, A., Popescu, A. and Raimondi, F. |
Abstract | This paper describes progress with our agenda of formal verification of information-flow security for realistic systems. We present CoSMed, a social media platform with verified document confidentiality. The system’s kernel is implemented and verified in the proof assistant Isabelle/HOL. For verification, we employ the framework of Bounded-Deducibility (BD) Security, previously introduced for the conference system CoCon. CoSMed is a second major case study in this framework. For CoSMed, the static topology of declassification bounds and triggers that characterized previous instances of BD security has to give way to a dynamic integration of the triggers as part of the bounds |
Research Group | Foundations of Computing group |
Conference | ITP 2016: 7th International Conference on Interactive Theorem Proving |
Page range | 87-106 |
ISSN | 0302-9743 |
ISBN | |
Hardcover | 9783319431437 |
Publisher | Springer |
Publication dates | |
Online | 07 Aug 2016 |
Publication process dates | |
Deposited | 19 Jun 2017 |
Accepted | 01 May 2016 |
Output status | Published |
Accepted author manuscript | |
Copyright Statement | The final publication is available at Springer |
Additional information | Published as: Bauereiß T., Pesenti Gritti A., Popescu A., Raimondi F. (2016) CoSMed: A Confidentiality-Verified Social Media Platform. In: Blanchette J., Merz S. (eds) Interactive Theorem Proving. ITP 2016. Lecture Notes in Computer Science, vol 9807. Springer, Cham |
Digital Object Identifier (DOI) | https://doi.org/10.1007/978-3-319-43144-4_6 |
Language | English |
Book title | Interactive Theorem Proving. ITP 2016. Lecture Notes in Computer Science, vol 9807 |
https://repository.mdx.ac.uk/item/870v7
Download files
46
total views12
total downloads1
views this month1
downloads this month