CoSMed: A Confidentiality-Verified Social Media Platform
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
- PDF / 541,159 Bytes
- 20 Pages / 439.37 x 666.142 pts Page_size
- 11 Downloads / 228 Views
German Research Center for Artificial Intelligence (DFKI), Bremen, Germany [email protected] 2 School of Science and Technology, Middlesex University, London, UK 3 Global NoticeBoard, London, UK 4 Institute of Mathematics Simion Stoilow of the Romanian Academy, Bucharest, Romania
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 BoundedDeducibility (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.
1
Introduction
Web-based systems are pervasive in our daily activities. Examples include enterprise systems, social networks, e-commerce sites and cloud services. Such systems pose notable challenges regarding confidentiality [1]. Recently, we have started a line of work aimed at addressing information flow security problems of realistic web-based systems by interactive theorem proving—using our favorite proof assistant, Isabelle/HOL [26,27]. We have introduced a security notion that allows a very fine-grained specification of what an attacker can observe about the system, and what information is to be kept confidential and in which situations. In our case studies, we assume the observers to be users of the system, and our goal is to verify that, by interacting with the system, the observers cannot learn more about confidential information than what we have specified. As a first case study, we have developed CoCon [18], a conference system (` a la EasyChair) verified for confidentiality. We have verified a comprehensive list of confidentiality properties, systematically covering the relevant sources of information from CoCon’s application logic [18, Sect. 4.5]. For example, besides authors, only PC members are allowed to learn about the content of submitted papers, and nothing beyond the last submitted version before the deadline. c Springer International Publishing Switzerland 2016 J.C. Blanchette and S. Merz (Eds.): ITP 2016, LNCS 9807, pp. 87–106, 2016. DOI: 10.1007/978-3-319-43144-4 6
88
T. Bauereiß et al.
This paper introduces a second major end product of this line of work: CoSMed, a confidentiality-verified social media platform. CoSMed allows users to register and post information, and to restrict access to this information based on friendship relationships established between users. Architecturally, CoSMed is an I/O automaton formalized in Isabelle, exported as Scala code, and wrapped in a web application (Sect. 2). For CoCon, we had proved that information only flows from the stored documents to the users in a suitably role-triggered and bounded fashi
Data Loading...
