CoSMeDis: A Distributed Social Media Platform with Formally Verified Confidentiality Guarantees
CoSMeDis: A Distributed Social Media Platform with Formally Verified Confidentiality Guarantees
复制标题
CoSMeDis：具有正式验证的保密保证的分布式社交媒体平台
DOI：
10.1109/sp.2017.24
复制
发表时间：
2017
期刊：
影响因子：
--
通讯作者：
Bauereiss T
中科院分区：
文献类型：
--
作者：
Bauereiss T
我们介绍了分布式社交媒体平台 CoSMeDis 的设计、实现和信息流验证。该系统由任意数量的通信节点组成，可部署在互联网上的不同位置。其注册用户可以发布内容并建立节点内和节点间的友谊，用于规范对帖子的访问控制。系统内核已在证明助手Isabelle/HOL中进行了验证，并自动提取为Scala代码。我们形式化了一个框架，用于在分布式系统中组成一类信息流安全保证，适用于输入/输出自动机。我们将此框架实例化为 CoSMeDis 信息源的机密属性：帖子、好友请求和好友状态。
We present the design, implementation and information flow verification of CoSMeDis, a distributed social media platform. The system consists of an arbitrary number of communicating nodes, deployable at different locations over the Internet. Its registered users can post content and establish intra-node and inter-node friendships, used to regulate access control over the posts. The system's kernel has been verified in the proof assistant Isabelle/HOL and automatically extracted as Scala code. We formalized a framework for composing a class of information flow security guarantees in a distributed system, applicable to input/output automata. We instantiated this framework to confidentiality properties for CoSMeDis's sources of information: posts, friendship requests, and friendship status.
登录
查看更多内容
影子知道：顺序程序的细化和安全性
DOI：
10.1016/j.scico.2007.09.003
发表时间：
2009
期刊：
Sci. Comput. Program.
影响因子：
--
作者：
Carroll Morgan
通讯作者：
Carroll Morgan
论安全系统的构成
DOI：
10.1109/secpri.2002.1004364
发表时间：
2002
期刊：
Proceedings 2002 IEEE Symposium on Security and Privacy
影响因子：
--
作者：
H. Mantel
通讯作者：
H. Mantel
DOI：
10.1007/978-3-319-08867-9_11
发表时间：
2014
期刊：
18th IEEE Computer Security Foundations Workshop (CSFW'05)
影响因子：
--
作者：
Sudeep Kanav;P. Lammich;A. Popescu
通讯作者：
A. Popescu
经过验证的信息流架构
DOI：
10.1145/2535838.2535839
发表时间：
2014
期刊：
Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages
影响因子：
--
作者：
Arthur Azevedo de Amorim;Nathan Collins;A. DeHon;Delphine Demange;Cătălin Hriţcu;David Pichardie;B. Pierce;R. Pollack;A. Tolmach
通讯作者：
A. Tolmach
DOI：
--
发表时间：
--
期刊：
影响因子：
--
作者：
Daniel Grahl;Simon Greiner
通讯作者：
Simon Greiner