{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,9]],"date-time":"2024-09-09T06:17:31Z","timestamp":1725862651438},"publisher-location":"Cham","reference-count":30,"publisher":"Springer International Publishing","isbn-type":[{"type":"print","value":"9783319431437"},{"type":"electronic","value":"9783319431444"}],"license":[{"start":{"date-parts":[[2016,1,1]],"date-time":"2016-01-01T00:00:00Z","timestamp":1451606400000},"content-version":"unspecified","delay-in-days":0,"URL":"http:\/\/www.springer.com\/tdm"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2016]]},"DOI":"10.1007\/978-3-319-43144-4_6","type":"book-chapter","created":{"date-parts":[[2016,8,6]],"date-time":"2016-08-06T04:24:16Z","timestamp":1470457456000},"page":"87-106","source":"Crossref","is-referenced-by-count":5,"title":["CoSMed: A Confidentiality-Verified Social Media Platform"],"prefix":"10.1007","author":[{"given":"Thomas","family":"Bauerei\u00df","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Armando","family":"Pesenti Gritti","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Andrei","family":"Popescu","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Franco","family":"Raimondi","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","published-online":{"date-parts":[[2016,8,7]]},"reference":[{"key":"6_CR1","unstructured":"OWASP top ten project. www.owasp.org\/index.php\/Top10#OWASP_Top_10_for_2013"},{"key":"6_CR2","unstructured":"Jif: Java + information flow (2014). http:\/\/www.cs.cornell.edu\/jif"},{"key":"6_CR3","unstructured":"SPARK (2014). http:\/\/www.spark-2014.org"},{"key":"6_CR4","unstructured":"Caritas Anchor House (2016). http:\/\/caritasanchorhouse.org.uk\/"},{"key":"6_CR5","unstructured":"Bauerei\u00df, T., Gritti, A.P., Popescu, A., Raimondi, F.: The CoSMed website (2016). https:\/\/cosmed.globalnoticeboard.com"},{"key":"6_CR6","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"159","DOI":"10.1007\/978-3-642-54792-8_9","volume-title":"Principles of Security and Trust","author":"A Bichhawat","year":"2014","unstructured":"Bichhawat, A., Rajani, V., Garg, D., Hammer, C.: Information flow control in WebKit\u2019s javascript bytecode. In: Abadi, M., Kremer, S. (eds.) POST 2014 (ETAPS 2014). LNCS, vol. 8414, pp. 159\u2013178. Springer, Heidelberg (2014)"},{"key":"6_CR7","doi-asserted-by":"crossref","unstructured":"Chlipala, A.: Ur\/Web: a simple model for programming the web. In: POPL, pp. 153\u2013165 (2015)","DOI":"10.1145\/2775051.2677004"},{"key":"6_CR8","doi-asserted-by":"crossref","unstructured":"Chugh, R., Meister, J.A., Jhala, R., Lerner, S.: Staged information flow for javascript. In: PLDI, pp. 50\u201362 (2009)","DOI":"10.1145\/1542476.1542483"},{"key":"6_CR9","doi-asserted-by":"crossref","unstructured":"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\u2013234 (2013)","DOI":"10.1145\/2508859.2516702"},{"key":"6_CR10","doi-asserted-by":"crossref","unstructured":"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\u2013178 (2014)","DOI":"10.1145\/2535838.2535839"},{"key":"6_CR11","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"463","DOI":"10.1007\/978-3-642-39799-8_31","volume-title":"Computer Aided Verification","author":"J Esparza","year":"2013","unstructured":"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\u2013478. Springer, Heidelberg (2013)"},{"key":"6_CR12","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"303","DOI":"10.1007\/978-3-642-04444-1_19","volume-title":"Computer Security \u2013 ESORICS 2009","author":"PWL Fong","year":"2009","unstructured":"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\u2013320. Springer, Heidelberg (2009)"},{"key":"6_CR13","doi-asserted-by":"crossref","unstructured":"Goguen, J.A., Meseguer, J.: Unwinding and inference control. In: IEEE Symposium on Security and Privacy, pp. 75\u201387 (1984)","DOI":"10.1109\/SP.1984.10019"},{"key":"6_CR14","doi-asserted-by":"crossref","unstructured":"Groef, W.D., Devriese, D., Nikiforakis, N., Piessens, F.: FlowFox: a web browser with flexible and precise information flow control. In: CCS, pp. 748\u2013759 (2012)","DOI":"10.1145\/2382196.2382275"},{"key":"6_CR15","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"103","DOI":"10.1007\/978-3-642-12251-4_9","volume-title":"Functional and Logic Programming","author":"F Haftmann","year":"2010","unstructured":"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\u2013117. Springer, Heidelberg (2010)"},{"key":"6_CR16","doi-asserted-by":"crossref","unstructured":"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\u201320 (2006)","DOI":"10.1145\/1217975.1217978"},{"key":"6_CR17","unstructured":"Jang, D., Tatlock, Z., Lerner, S.: Establishing browser security guarantees through formal shim verification. In: USENIX Security, pp. 113\u2013128 (2012)"},{"key":"6_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"167","DOI":"10.1007\/978-3-319-08867-9_11","volume-title":"Computer Aided Verification","author":"S Kanav","year":"2014","unstructured":"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\u2013183. Springer, Heidelberg (2014)"},{"issue":"6","key":"6_CR19","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1145\/1743546.1743574","volume":"53","author":"G Klein","year":"2010","unstructured":"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\u2013115 (2010)","journal-title":"Commun. ACM"},{"key":"6_CR20","doi-asserted-by":"crossref","unstructured":"Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: a verified implementation of ML. In: POPL, pp. 179\u2013192 (2014)","DOI":"10.1145\/2535838.2535841"},{"issue":"7","key":"6_CR21","doi-asserted-by":"crossref","first-page":"107","DOI":"10.1145\/1538788.1538814","volume":"52","author":"X Leroy","year":"2009","unstructured":"Leroy, X.: Formal verification of a realistic compiler. Commun. ACM 52(7), 107\u2013115 (2009)","journal-title":"Commun. ACM"},{"key":"6_CR22","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"497","DOI":"10.1007\/978-3-642-28869-2_25","volume-title":"Programming Languages and Systems","author":"A Lochbihler","year":"2012","unstructured":"Lochbihler, A.: Java and the java memory model \u2014 a unified, machine-checked formalisation. In: Seidl, H. (ed.) Programming Languages and Systems. LNCS, vol. 7211, pp. 497\u2013517. Springer, Heidelberg (2012)"},{"key":"6_CR23","doi-asserted-by":"crossref","first-page":"605","DOI":"10.1007\/978-1-4419-5906-5_874","volume-title":"Encyclopedia of Cryptography and Security","author":"H Mantel","year":"2011","unstructured":"Mantel, H.: Information flow and noninterference. In: van Tilborg, H.C.A., Jajodia, S. (eds.) Encyclopedia of Cryptography and Security, 2nd edn, pp. 605\u2013607. Springer, Heidelberg (2011)","edition":"2"},{"issue":"9","key":"6_CR24","doi-asserted-by":"crossref","first-page":"913","DOI":"10.1109\/12.713311","volume":"47","author":"JS Moore","year":"1998","unstructured":"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\u2013926 (1998)","journal-title":"IEEE Trans. Comput."},{"key":"6_CR25","doi-asserted-by":"crossref","unstructured":"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\u2013429 (2013)","DOI":"10.1109\/SP.2013.35"},{"key":"6_CR26","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-319-10542-0","volume-title":"Concrete Semantics: With Isabelle\/HOL","author":"T Nipkow","year":"2014","unstructured":"Nipkow, T., Klein, G.: Concrete Semantics: With Isabelle\/HOL. Springer, Heidelberg (2014)"},{"key":"6_CR27","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","DOI":"10.1007\/3-540-45949-9","volume-title":"Isabelle\/HOL: A Proof Assistant for Higher-Order Logic","author":"T Nipkow","year":"2002","unstructured":"Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle\/HOL: A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002)"},{"key":"6_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"crossref","first-page":"378","DOI":"10.1007\/978-3-319-10431-7_30","volume-title":"Software Engineering and Formal Methods","author":"R Pardo","year":"2014","unstructured":"Pardo, R., Schneider, G.: A formal privacy policy framework for social networks. In: Giannakopoulou, D., Sala\u00fcn, G. (eds.) SEFM 2014. LNCS, vol. 8702, pp. 378\u2013392. Springer, Heidelberg (2014)"},{"key":"6_CR29","unstructured":"Sutherland, D.: A model of information. In: 9th National Security Conference, pp. 175\u2013183 (1986)"},{"key":"6_CR30","doi-asserted-by":"crossref","unstructured":"Yang, J., Yessenov, K., Solar-Lezama, A.: A language for automatically enforcing privacy policies. In: POPL, pp. 85\u201396 (2012)","DOI":"10.1145\/2103656.2103669"}],"container-title":["Lecture Notes in Computer Science","Interactive Theorem Proving"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-319-43144-4_6","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2020,9,24]],"date-time":"2020-09-24T21:50:31Z","timestamp":1600984231000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-319-43144-4_6"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016]]},"ISBN":["9783319431437","9783319431444"],"references-count":30,"URL":"https:\/\/doi.org\/10.1007\/978-3-319-43144-4_6","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2016]]}}}