CoSMed: a confidentiality-verified social media platform. (English) Zbl 1451.68168

Summary: 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 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.


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


[1] OWASP top ten project. www.owasp.org/index.php/Top10#OWASP_Top_10_for_2013
[2] The CoSMed Homepage. http://andreipopescu.uk/CoSMed.html
[3] The CoSMeDis Homepage. http://andreipopescu.uk/CoSMeDis.html
[4] Jif: Java\(+\) information flow. http://www.cs.cornell.edu/jif (2014)
[5] SPARK. http://www.spark-2014.org (2014)
[6] Caritas Anchor House. http://caritasanchorhouse.org.uk/ (2016)
[7] The diaspora\(^*\) project. https://diasporafoundation.org/ (2016)
[8] Arapinis, M., Bursuc, S., Ryan, M.: Privacy supporting cloud computing: ConfiChair, a case study. In: POST, pp. 89-108 (2012)
[9] Barthe, G., Grégoire, B., Béguelin, S.Z.: Formal certification of code-based cryptographic proofs. In: POPL, pp. 90-101 (2009) · Zbl 1315.68081
[10] Bauereiß, T., Gritti, A.P., Popescu, A., Raimondi, F.: CoSMed: a confidentiality-verified conference management system. In: ITP (2016) · Zbl 1451.68167
[11] Bauereiß, T., Pesenti Gritti, A., Popescu, A., Raimondi, F.: CoSMeDis: A distributed social media platform with formally verified confidentiality guarantees. In: IEEE Security and Privacy, pp. 729-748 (2017) · Zbl 1451.68167
[12] Bichhawat, A., Rajani, V., Garg, D., Hammer, C.: Information flow control in WebKit’s JavaScript bytecode. In: POST, pp. 159-178 (2014)
[13] Blanchet, B., Abadi, M., Fournet, C.: Automated verification of selected equivalences for security protocols. In: LICS, pp. 331-340 (2005) · Zbl 1135.68007
[14] Blanchette, JC; Böhme, S; Fleury, M; Smolka, SJ; Steckermeier, A, Semi-intelligible isar proofs from machine-generated proofs, J. Autom. Reason., 56, 155-200, (2016) · Zbl 1356.68178
[15] Blanchette, J.C., Böhme, S., Popescu, A., Smallbone, N.: Encoding monomorphic and polymorphic types. Log. Methods Comput. Sci. 12(4) (2016). https://doi.org/10.2168/LMCS-12(4:13)2016 · Zbl 1445.68327
[16] Blanchette, J.C., Hölzl, J., Lochbihler, A., Panny, L., Popescu, A., Traytel, D.: Truly modular (co)datatypes for Isabelle/HOL. In: ITP, pp. 93-110 (2014) · Zbl 1416.68151
[17] Blanchette, J.C., Merz, S. (eds.): Interactive theorem proving. In: Proceedings on 7th International Conference of ITP 2016, Nancy, France, vol. 9807, 22-25 Aug 2016 (2016)
[18] Broberg, N; Delft, B; Sands, D, Paragon—practical programming with information flow control, J. Comput. Secur., 25, 323-365, (2017) · Zbl 06385653
[19] Chlipala, A.: Ur/Web: a simple model for programming the web. In: POPL, pp. 153-165 (2015)
[20] Chong, S; Meyden, RVD, Using architecture to reason about information security, ACM Trans. Inf. Syst. Secur., 18, 8:1-8:30, (2015)
[21] Chugh, R., Meister, J.A., Jhala, R., Lerner, S.: Staged information flow for JavaScript. In: PLDI, pp. 50-62 (2009)
[22] Dam, M., Guanciale, R., Khakpour, N., Nemati, H., Schwarz, O.: Formal verification of information flow security for a simple ARM-based separation kernel. In: CCS, pp. 223-234 (2013)
[23] de Amorim, A.A., Collins, N., DeHon, A., Demange, D., Hriţcu, C., Pichardie, D., Pierce, B.C., Pollack, R., Tolmach, A.: A verified information-flow architecture. In: POPL, pp. 165-178 (2014) · Zbl 1284.68306
[24] de Nivelle, H. (ed.): Automated reasoning with analytic tableaux and related methods. In: Proceedings on 24th International Conference of TABLEAUX 2015, Wrocław, Poland, vol. 9323, 21-24 Sept 2015 (2015) · Zbl 1325.68016
[25] Esparza, J., Lammich, P., Neumann, R., Nipkow, T., Schimpf, A., Smaus, J.: A fully verified executable LTL model checker. In: CAV, pp. 463-478 (2013)
[26] Finkbeiner, B., Rabe, M.N., Sánchez, C.: Algorithms for model checking HyperLTL and HyperCTL\({\hat{}}\)*. In: CAV, pp. 30-48 · Zbl 1381.68161
[27] Fong, P.W.L., Anwar, M.M., Zhao, Z.: A privacy preservation model for Facebook-style social network systems. In: ESORICS, pp. 303-320 (2009) · Zbl 1284.68131
[28] Goguen, J.A., Meseguer, J.: Unwinding and inference control. In: IEEE Symposium on Security and Privacy, pp. 75-87 (1984)
[29] Groef, W.D., Devriese, D., Nikiforakis, N., Piessens, F.: FlowFox: a web browser with flexible and precise information flow control. In: CCS, pp. 748-759 (2012)
[30] Guttman, J.D., Rowe, P.D.: A cut principle for information flow. In: CSF, pp. 107-121 (2015)
[31] Haftmann, F.: Code generation from specifications in higher-order logic. Ph.D. thesis, Technische Universität München (2009)
[32] Haftmann, F; Nipkow, T, Code generation via higher-order rewrite systems, FLOPS, 2010, 103-117, (2010) · Zbl 1284.68131
[33] Haftmann, F., Wenzel, M.: Constructive type classes in Isabelle. In: TYPES, pp. 160-174 (2006) · Zbl 1178.68529
[34] Hardin, D.S., Smith, E.W., Young, W.D.: A robust machine code proof framework for highly secure applications. In: ACL2, pp. 11-20 (2006)
[35] Hawblitzel, C., Howell, J., Lorch, J.R., Narayan, A., Parno, B., Zhang, D., Zill, B.: Ironclad apps: end-to-end security via automated full-system verification. In: OSDI ’14, pp. 165-181 (2014)
[36] Jang, D., Tatlock, Z., Lerner, S.: Establishing browser security guarantees through formal shim verification. In: USENIX Security, pp. 113-128 (2012)
[37] Kammüller, F., Wenzel, M., Paulson, L.C.: Locales—a sectioning concept for Isabelle. In: TPHOLs’99, pp. 149-166 (1999)
[38] Kanav, S., Lammich, P., Popescu, A.: A conference management system with verified document confidentiality. In: CAV, pp. 167-183 (2014)
[39] Klein, G; Andronick, J; Elphinstone, K; Heiser, G; Cock, D; Derrin, P; Elkaduwe, D; Engelhardt, K; Kolanski, R; Norrish, M; Sewell, T; Tuch, H; Winwood, S, Sel4: formal verification of an operating-system kernel, Commun. ACM, 53, 107-115, (2010)
[40] Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: a verified implementation of ML. In: POPL, pp. 179-192 (2014) · Zbl 1284.68405
[41] Leroy, X, Formal verification of a realistic compiler, Commun. ACM, 52, 107-115, (2009)
[42] Lochbihler, A.: Java and the Java memory model—a unified, machine-checked formalisation. In: ESOP, pp. 497-517 (2012) · Zbl 1352.68034
[43] Mantel, H.: Possibilistic definitions of security—an assembly kit. In: CSFW, pp. 185-199 (2000)
[44] Mantel, H.: Information flow and noninterference. In: Encyclopedia of Cryptography and Security, 2nd edn., pp. 605-607 (2011) · Zbl 1356.68178
[45] Moore, JS; Lynch, TW; Kaufmann, M, A mechanically checked proof of the amd5\({}_{\text{k}}86{}^{\text{ tm }}\) floating point division program, IEEE Trans. Comput., 47, 913-926, (1998) · Zbl 1392.68051
[46] Murray, T.C., Matichuk, D., Brassil, M., Gammie, P., Bourke, T., Seefried, S., Lewis, C., Gao, X., Klein, G.: seL4: from general purpose to a proof of information flow enforcement. In: IEEE Security and Privacy, pp. 415-429 (2013)
[47] Naumowicz, A., Korniłowicz, A.: A brief overview of Mizar. In: TPHOLs, pp. 67-72 (2009) · Zbl 1252.68262
[48] Nipkow, T.: Programming and proving in Isabelle/HOL. https://isabelle.in.tum.de/dist/Isabelle2016-1/doc/prog-prove.pdf (2017)
[49] Nipkow, T., Klein, G.: Concrete Semantics: With Isabelle/HOL. Springer, Berlin (2014) · Zbl 1410.68004
[50] Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Berlin (2002) · Zbl 0994.68131
[51] Pardo, R., Schneider, G.: A formal privacy policy framework for social networks. In: SEFM, pp. 378-392 (2014)
[52] Paulson, L.C., Blanchette, J.C.: Three years of experience with Sledgehammer, a practical link between automatic and interactive theorem provers. In: IWIL (2010)
[53] Sabelfeld, A; Sands, D, Declassification: dimensions and principles, J. Comput. Secur., 17, 517-548, (2009)
[54] Sutherland, D.: A model of information. In: 9th National Security Conference, pp. 175-183 (1986)
[55] Wenzel, M.: Isar—a generic interpretative approach to readable formal proof documents. In: TPHOLs, pp. 167-184 (1999)
[56] Yang, J., Yessenov, K., Solar-Lezama, A.: A language for automatically enforcing privacy policies. In: POPL, pp. 85-96 (2012)
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.