×

CoCon: a conference management system with formally verified document confidentiality. (English) Zbl 07356975

Summary: We present a case study in formally verified security for realistic systems: the information flow security verification of the functional kernel of a web application, the CoCon conference management system. We use the Isabelle theorem prover to specify and verify fine-grained confidentiality properties, as well as complementary safety and “traceback” properties. The challenges posed by this development in terms of expressiveness have led to bounded-deducibility security, a novel security model and verification method generally applicable to systems describable as input/output automata.

MSC:

68V15 Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.)
PDF BibTeX XML Cite
Full Text: DOI

References:

[1] Arapinis, M., Bursuc, S., Ryan, M.: Privacy supporting cloud computing: confichair, a case study. In: POST, pp. 89-108 (2012)
[2] Askarov, A., Chong, S.: Learning is change in knowledge: knowledge-based security for dynamic policies. In: CSF, pp. 308-322 (2012)
[3] Askarov, A.; Myers, AC, Attacker control and impact for confidentiality and integrity, Log. Methods Comput. Sci. (2011) · Zbl 1237.68055
[4] Askarov, A., Sabelfeld, A.: Gradual release: unifying declassification, encryption and key release policies. In: IEEE Symposium on Security and Privacy, pp. 207-221 (2007)
[5] Askarov, A., Sabelfeld, A.: Tight enforcement of information-release policies for dynamic languages. In: CSF, pp. 43-59 (2009)
[6] Bauereiß, T., Pesenti Gritti, A., Popescu, A., Raimondi, F.: CoSMeDis: a distributed social media platform with formally verified confidentiality guarantees. In: IEEE Symposium on Security and Privacy, pp. 729-748 (2017) · Zbl 1451.68168
[7] Bauereiß, T.; Pesenti Gritti, A.; Popescu, A.; Raimondi, F., CoSMed: a confidentiality-verified social media platform, J. Autom. Reason., 61, 1-4, 113-139 (2018) · Zbl 1451.68168
[8] Bell, E.D., La Padula, J.L.: Secure computer system: unified exposition and multics interpretation, 1975. Technical Report MTR-2997, MITRE, Bedford, MA
[9] Bichhawat, A., Rajani, V., Garg, D., Hammer, C.: Information flow control in WebKit’s JavaScript bytecode. In: POST, pp. 159-178 (2014)
[10] Blanchet, B., Abadi, M., Fournet, C.: Automated verification of selected equivalences for security protocols. In: LICS, pp. 331-340 (2005) · Zbl 1135.68007
[11] Blanchette, JC; Merz, S., Interactive Theorem Proving: 7th International Conference, ITP 2016, Nancy, France, August 22-25, 2016, Proceedings (2016), Berlin: Springer, Berlin · Zbl 1343.68004
[12] Broberg, N.; van Delft, B.; Sands, D., Paragon: practical programming with information flow control, J. Comput. Secur., 25, 4-5, 323-365 (2017)
[13] Chlipala, A.: Ur/Web: a simple model for programming the web. In: POPL, pp. 153-165 (2015)
[14] Chugh, R., Meister, J.A., Jhala, R., Lerner, S.: Staged information flow for Javascript. In: PLDI, pp. 50-62 (2009)
[15] Clarkson, M.R., Finkbeiner, B., Koleini, M., Micinski, K.K., Rabe, M.N., Sánchez, C.: Temporal logics for hyperproperties. In: POST, pp. 265-284 (2014)
[16] Cohen, E.S.: Information transmission in computational systems. In: SOSP, pp. 133-139 (1977)
[17] 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)
[18] de Amorim, AA; Collins, N.; DeHon, A.; Demange, D.; Hritcu, C.; Pichardie, D.; Pierce, BC; Pollack, R.; Tolmach, A., A verified information-flow architecture, J. Comput. Secur., 24, 6, 689-734 (2016)
[19] de Nivelle, H., Automated Reasoning with Analytic Tableaux and Related Methods—24th International Conference, TABLEAUX 2015, Wrocław, Poland, September 21-24, 2015. Proceedings (2015), Berlin: Springer, Berlin · Zbl 1325.68016
[20] Dimitrova, R., Finkbeiner, B., Kovács, M., Rabe, M.N., Seidl, H.: Model checking information flow in reactive systems. In: VMCAI, pp. 169-185 (2012) · Zbl 1326.68182
[21] 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)
[22] Finkbeiner, B., Rabe, M.N., Sánchez, C.: Algorithms for model checking hyperltl and hyperctl \(^*\). In: CAV, pp. 30-48 · Zbl 1381.68161
[23] Focardi, R., Gorrieri, R.: Classification of security properties (part I: information flow). In: FOSAD, pp. 331-396 (2000) · Zbl 1007.68508
[24] Giffin, DB; Levy, A.; Stefan, D.; Terei, D.; Mazières, D.; Mitchell, JC; Russo, A., Hails: protecting data privacy in untrusted web applications, J. Comput. Secur., 25, 4-5, 427-461 (2017)
[25] Goguen, J.A., Meseguer, J.: Security policies and security models. In: IEEE Symposium on Security and Privacy, pp. 11-20 (1982)
[26] Goguen, J.A., Meseguer, J.: Unwinding and inference control. In: IEEE Symposium on Security and Privacy, pp. 75-87 (1984)
[27] Gollmann, D., Computer Security (2005), New York: Wiley, New York
[28] Greiner, S., Grahl, D.: Non-interference with what-declassification in component-based systems. In: CSF, pp. 253-267. IEEE Computer Society (2016)
[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: Fournet, C., Hicks, M.W., Viganò, L. (eds.) IEEE 28th Computer Security Foundations Symposium, CSF 2015, Verona, Italy, 13-17 July 2015, pp. 107-121. IEEE (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] Halpern, JY; O’Neill, KR, Secrecy in multiagent systems, ACM Trans. Inf. Syst. Secur., 12, 1, 1-47 (2008)
[34] 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)
[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: USENIX, pp. 165-181 (2014)
[36] Hou, P., Lammich, P., Popescu, A.: This paper’s website. http://andreipopescu.uk/papers/CoConExtended.html
[37] Jang, D., Tatlock, Z., Lerner, S.: Establishing browser security guarantees through formal shim verification. In: USENIX Security, pp. 113-128 (2012)
[38] Jif: Java + information flow, 2014. http://www.cs.cornell.edu/jif
[39] Kanav, S., Lammich, P., Popescu, A.: A conference management system with verified document confidentiality. In: CAV, pp. 167-183 (2014)
[40] 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)
[41] Kozyri, E., Arden, O., Myers, A.C., Schneider, F.B.: JRIF: reactive information flow control for java. In: Foundations of Security, Protocols, and Equational Reasoning—Essays Dedicated to Catherine A. Meadows, pp. 70-88 (2019) · Zbl 07176723
[42] Kumar, R., Myreen, M.O., Norrish, M., Owens, S.: CakeML: a verified implementation of ML. In: POPL, pp. 179-192 (2014) · Zbl 1284.68405
[43] Lampson, BW, Protection, Oper. Syst. Rev., 8, 1, 18-24 (1974)
[44] Leroy, X., Formal verification of a realistic compiler, Commun. ACM, 52, 7, 107-115 (2009)
[45] Liu, J.; Arden, O.; George, MD; Myers, AC, Fabric: building open distributed systems securely by construction, J. Comput. Secur., 25, 4-5, 367-426 (2017)
[46] Lochbihler, A.: Java and the Java memory model—a unified, machine-checked formalisation. In: ESOP, pp. 497-517 (2012) · Zbl 1352.68034
[47] Mantel, H.: Information flow control and applications—bridging a gap. In: FME, pp. 153-172 (2001) · Zbl 0977.68681
[48] Mantel, H.: A uniform framework for the formal specification and verification of information flow security. Ph.D. thesis, University of Saarbrücken (2003)
[49] Mantel, H.: Information flow and noninterference. In: Encyclopedia of Cryptography and Security (2nd Ed.), pp. 605-607 (2011)
[50] McCullough, D.: Specifications for multi-level security and a hook-up property. In: IEEE Symposium on Security and Privacy (1987)
[51] McLean, J.: A general theory of composition for trace sets closed under selective interleaving functions. In: Proceedings of the IEEE Symposium on Security and Privacy, pp. 79-93 (1994)
[52] McLean, J.: Security models. In: Encyclopedia of Software Engineering (1994)
[53] Mehta, A., Elnikety, E., Harvey, K., Garg, D., Druschel, P.: Qapla: policy compliance for database-backed systems. In: USENIX Security, pp. 1463-1479 (2017)
[54] Milner, R., Communication and Concurrency (1989), Upper Saddle River: Prentice Hall, Upper Saddle River · Zbl 0683.68008
[55] Moore, JS; Lynch, TW; Kaufmann, M., A mechanically checked proof of the amd \(5{}_{\text{k}}86{}^{\text{ tm }}\) floating point division program, IEEE Trans. Comput., 47, 9, 913-926 (1998) · Zbl 1392.68051
[56] 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)
[57] Murray, T.C., Matichuk, D., Brassil, M., Gammie, P., Klein, G.: Noninterference for operating system kernels. In: CPP, pp. 126-142 (2012) · Zbl 1383.68021
[58] Murray, TC; Sabelfeld, A.; Bauer, L., Special issue on verified information flow security, J. Comput. Secur., 25, 4-5, 319-321 (2017)
[59] Murray, T.C., Sison, R., Engelhardt, K.: COVERN: a logic for compositional verification of information flow control. In: EuroS&P, pp. 16-30. IEEE (2018)
[60] Nipkow, T.; Klein, G., Concrete Semantics: With Isabelle/HOL (2014), Berlin: Springer, Berlin · Zbl 1410.68004
[61] Nipkow, T.; Paulson, LC; Wenzel, M., Isabelle/HOL: A Proof Assistant for Higher-Order Logic (2002), Berlin: Springer, Berlin · Zbl 0994.68131
[62] O’Halloran, C.: A calculus of information flow. In: ESORICS, pp. 147-159 (1990)
[63] Popek, GJ; Farber, DA, A model for verification of data security in operating systems, Commun. ACM, 21, 9, 737-749 (1978) · Zbl 0399.68036
[64] Rabe, M.N., Lammich, P., Popescu, A.: A shallow embedding of hyperctl. Archive of Formal Proofs, 2014 (2014)
[65] Reliably Secure software systems (RS3): priority program of the German research foundation (DFG), (2019). https://www.spp-rs3.de
[66] Ronald Fagin, YM; Halpern, JY; Vardi, M., Reasoning About Knowledge (2003), Cambridge: MIT Press, Cambridge · Zbl 0839.68095
[67] Rushby, J.: Noninterference, transitivity, and channel-control security policies. Technical report, Dec (1992)
[68] Ryan, P.Y.A.: Mathematical models of computer security. In: FOSAD, pp. 1-62 (2000) · Zbl 1007.68129
[69] Sabelfeld, A.; Myers, AC, Language-based information-flow security, IEEE J. Sel. Areas Commun., 21, 1, 5-19 (2003)
[70] Sabelfeld, A., Myers, A.C.: A model for delimited information release. In: ISSS, pp. 174-191 (2003)
[71] Sabelfeld, A.; Sands, D., Declassification: dimensions and principles, J. Comput. Secur., 17, 5, 517-548 (2009)
[72] Sangiorgi, D., On the bisimulation proof method, Math. Struct. Comput. Sci., 8, 5, 447-479 (1998) · Zbl 0916.68057
[73] SPARK, 2014. http://www.spark-2014.org
[74] Sutherland, D.: A model of information. In: 9th National Security Conference, pp. 175-183 (1986)
[75] The Redis System. https://redis.io, 2019
[76] The EasyChair conference system, 2014. http://easychair.org
[77] The HotCRP conference management system, 2014. http://read.seas.harvard.edu/ kohler/hotcrp
[78] The Scalatra Web Framework, 2019. http://scalatra.org/
[79] Wimmer, S., Lammich, P.: Verified model checking of timed automata. In: TACAS, pp. 61-78 (2018) · Zbl 1423.68294
[80] Xiao, Z.; Kathiresshan, N.; Xiao, Y., A survey of accountability in computer networks and distributed systems, Secur. Commun. Netw., 9, 4, 290-315 (2016)
[81] Yang, J., Yessenov, K., Solar-Lezama, A.: A language for automatically enforcing privacy policies. In: POPL, pp. 85-96 (2012)
[82] Zdancewic, S., Myers, A.C.: Robust declassification. In: CSFW, pp. 15-23 (2001)
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.