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

Blanchette, Jasmin Christian (ed.) et al., Interactive theorem proving. 7th international conference, ITP 2016, Nancy, France, August 22–25, 2016. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 9807, 87-106 (2016).
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.
For the entire collection see [Zbl 1343.68004].


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] Jif: Java + information flow (2014). http://www.cs.cornell.edu/jif
[3] SPARK (2014). http://www.spark-2014.org · Zbl 1298.14052
[4] Caritas Anchor House (2016). http://caritasanchorhouse.org.uk/
[5] Bauereiß, T., Gritti, A.P., Popescu, A., Raimondi, F.: The CoSMed website (2016). https://cosmed.globalnoticeboard.com
[6] Bichhawat, A., Rajani, V., Garg, D., Hammer, C.: Information flow control in WebKit’s javascript bytecode. In: Abadi, M., Kremer, S. (eds.) POST 2014 (ETAPS 2014). LNCS, vol. 8414, pp. 159–178. Springer, Heidelberg (2014) · Zbl 06400651
[7] Chlipala, A.: Ur/Web: a simple model for programming the web. In: POPL, pp. 153–165 (2015)
[8] Chugh, R., Meister, J.A., Jhala, R., Lerner, S.: Staged information flow for javascript. In: PLDI, pp. 50–62 (2009)
[9] 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)
[10] de Amorim, A.A., Collins, N., DeHon, A., Demange, D., Hritcu, C., Pichardie, D., Pierce, B.C., Pollack, R., Tolmach, A.: A verified information-flow architecture. In: POPL, pp. 165–178 (2014) · Zbl 1284.68306
[11] Esparza, J., Lammich, P., Neumann, R., Nipkow, T., Schimpf, A., Smaus, J.-G.: A fully verified executable LTL model checker. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 463–478. Springer, Heidelberg (2013) · Zbl 06233053
[12] Fong, P.W.L., Anwar, M., Zhao, Z.: A privacy preservation model for facebook-style social network systems. In: Backes, M., Ning, P. (eds.) ESORICS 2009. LNCS, vol. 5789, pp. 303–320. Springer, Heidelberg (2009) · Zbl 05616815
[13] Goguen, J.A., Meseguer, J.: Unwinding and inference control. In: IEEE Symposium on Security and Privacy, pp. 75–87 (1984)
[14] 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)
[15] Haftmann, F., Nipkow, T.: Code generation via higher-order rewrite systems. In: Blume, M., Kobayashi, N., Vidal, G. (eds.) FLOPS 2010. LNCS, vol. 6009, pp. 103–117. Springer, Heidelberg (2010) · Zbl 1284.68131
[16] Hardin, D.S., Smith, E.W., Young, W.D.: A robust machine code proof framework for highly secure applications. In: Manolios, P., Wilding, M. (eds.) ACL2, pp. 11–20 (2006)
[17] Jang, D., Tatlock, Z., Lerner, S.: Establishing browser security guarantees through formal shim verification. In: USENIX Security, pp. 113–128 (2012)
[18] Kanav, S., Lammich, P., Popescu, A.: A conference management system with verified document confidentiality. In: Biere, A., Bloem, R. (eds.) CAV 2014. LNCS, vol. 8559, pp. 167–183. Springer, Heidelberg (2014) · Zbl 06349507
[19] 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(6), 107–115 (2010) · Zbl 05748249
[20] Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: a verified implementation of ML. In: POPL, pp. 179–192 (2014) · Zbl 1284.68405
[21] Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107–115 (2009) · Zbl 05747873
[22] Lochbihler, A.: Java and the java memory model – a unified, machine-checked formalisation. In: Seidl, H. (ed.) Programming Languages and Systems. LNCS, vol. 7211, pp. 497–517. Springer, Heidelberg (2012) · Zbl 1352.68034
[23] Mantel, H.: Information flow and noninterference. In: van Tilborg, H.C.A., Jajodia, S. (eds.) Encyclopedia of Cryptography and Security, 2nd edn, pp. 605–607. Springer, Heidelberg (2011)
[24] Moore, J.S., Lynch, T.W., Kaufmann, M.: A mechanically checked proof of the amd5 \[ {}_{\text{ k }} \] 86 \[ {}^{\text{ tm }} \] floating point division program. IEEE Trans. Comput. 47(9), 913–926 (1998)
[25] 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: Security and Privacy, pp. 415–429 (2013)
[26] Nipkow, T., Klein, G.: Concrete Semantics: With Isabelle/HOL. Springer, Heidelberg (2014) · Zbl 1410.68004
[27] Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002) · Zbl 0994.68131
[28] Pardo, R., Schneider, G.: A formal privacy policy framework for social networks. In: Giannakopoulou, D., Salaün, G. (eds.) SEFM 2014. LNCS, vol. 8702, pp. 378–392. Springer, Heidelberg (2014) · Zbl 06461673
[29] Sutherland, D.: A model of information. In: 9th National Security Conference, pp. 175–183 (1986)
[30] Yang, J., Yessenov, K., Solar-Lezama, A.: A language for automatically enforcing privacy policies. In: POPL, pp. 85–96 (2012) · Zbl 06481239
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.