CoSMed: a confidentiality-verified social media platform

DOI10.1007/978-3-319-43144-4_6zbMATH Open1451.68167OpenAlexW3016501173MaRDI QIDQ2829248FDOQ2829248

Authors: Thomas Bauereiß, Armando Pesenti Gritti, Andrei Popescu 

Publication date: 27 October 2016

Published in: Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL: https://eprints.mdx.ac.uk/22094/1/CoSMedITP2016.pdf

Recommendations

• CoSMed: a confidentiality-verified social media platform
• A verified information-flow architecture
• A proof system for information flow security
• Programming Languages and Systems
• A certificate infrastructure for machine-checked proofs of conditional information flow

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Cites Work

• A note on spark varieties
• A verified information-flow architecture
• CakeML
• Code generation via higher-order rewrite systems
• Concrete semantics. With Isabelle/HOL
• Isabelle/HOL. A proof assistant for higher-order logic
• Java and the Java memory model -- a unified, machine-checked formalisation
• Ur/Web

Cited In (2)

• CoCon: a conference management system with formally verified document confidentiality
• CoSMed: a confidentiality-verified social media platform

Uses Software

• Isabelle/HOL
• CakeML
• seL4
• Jif
• CoSMed
• Ur/Web
• CAVA LTL Modelchecker
• FlowFox

This page was built for publication: CoSMed: a confidentiality-verified social media platform

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2829248)