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

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

Cited In (1)

• 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)