CoSMed: a confidentiality-verified social media platform
Conference paper
Bauereiß, T., Pesenti Gritti, A., Popescu, A. and Raimondi, F. 2018. CoSMed: a confidentiality-verified social media platform. Interactive Theorem Proving - 7th International Conference, ITP 2016, Nancy, France, August 22-25, 2016, Proceedings. Nancy, France 22 - 27 Aug 2016 Springer. https://doi.org/10.1007/s10817-017-9443-3
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-De- ducibility (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 declas- sification 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. We also show that, from a theoretical viewpoint, the removal of triggers from the notion of BD Security does not restrict its expressiveness. |
Research Group | Foundations of Computing group |
Conference | Interactive Theorem Proving - 7th International Conference, ITP 2016, Nancy, France, August 22-25, 2016, Proceedings |
Proceedings Title | Journal of Automated Reasoning |
ISSN | 0168-7433 |
Electronic | 1573-0670 |
Publisher | Springer |
Publication dates | |
Online | 02 Dec 2017 |
30 Jun 2018 | |
Publication process dates | |
Deposited | 19 Jan 2018 |
Submitted | 19 Mar 2017 |
Accepted | 24 Nov 2017 |
Output status | Published |
Accepted author manuscript | |
Copyright Statement | This is a post-peer-review, pre-copyedit version of an article published in Journal of Automated Reasoning. The final authenticated version is available online at: http://dx.doi.org/10.1007/s10817-017-9443-3 |
Additional information | Special Issue: Milestones in Interactive Theorem Proving |
Digital Object Identifier (DOI) | https://doi.org/10.1007/s10817-017-9443-3 |
Language | English |
Book title | Interactive Theorem Proving (ITP) 2016 |
https://repository.mdx.ac.uk/item/87683
Download files
67
total views11
total downloads1
views this month0
downloads this month