Show simple item record

dc.contributor.authorBauereiss, Thomasen
dc.contributor.authorPesenti Gritti, Armandoen
dc.contributor.authorPopescu, Andreien
dc.contributor.authorRaimondi, Francoen
dc.date.accessioned2018-02-09T09:48:01Z
dc.date.available2018-02-09T09:48:01Z
dc.date.issued2018-06en
dc.identifier.issn0168-7433
dc.identifier.urihttps://www.repository.cam.ac.uk/handle/1810/271844
dc.description.abstractThis 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. We also show that, from a theoretical viewpoint, the removal of triggers from the notion of BD Security does not restrict its expressiveness.
dc.languageenen
dc.publisherSpringer Nature
dc.titleCoSMed: A Confidentiality-Verified Social Media Platformen
dc.typeArticle
prism.endingPage139
prism.issueIdentifier1-4en
prism.publicationDate2018en
prism.publicationNameJournal of Automated Reasoningen
prism.startingPage113
prism.volume61en
dc.identifier.doi10.17863/CAM.18851
dcterms.dateAccepted2017-11-16en
rioxxterms.versionofrecord10.1007/s10817-017-9443-3en
rioxxterms.versionAM*
rioxxterms.licenseref.urihttp://www.rioxx.net/licenses/all-rights-reserveden
rioxxterms.licenseref.startdate2018-06en
dc.contributor.orcidPopescu, Andrei [0000-0001-8747-0619]
dc.identifier.eissn1573-0670
rioxxterms.typeJournal Article/Reviewen
pubs.funder-project-idEPSRC (EP/K008528/1)
cam.issuedOnline2017-12-02en
rioxxterms.freetoread.startdate2018-12-02


Files in this item

Thumbnail

This item appears in the following Collection(s)

Show simple item record