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.
Cite
CITATION STYLE
Bauereiß, T., Gritti, A. P., Popescu, A., & Raimondi, F. (2016). CoSMed: A confidentiality-verified social media platform. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 9807 LNCS, pp. 87–106). Springer Verlag. https://doi.org/10.1007/978-3-319-43144-4_6
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
