Making security type systems less ad hoc

Article

Nipkow, T. and Popescu, A. 2014. Making security type systems less ad hoc. Information Technology. 56 (6), pp. 267-272. https://doi.org/10.1515/itit-2014-1060
TypeArticle
TitleMaking security type systems less ad hoc
AuthorsNipkow, T. and Popescu, A.
Abstract

We present a uniform, top-down design method for security type systems applied to a parallel while-language. The method takes the following route: from a notion of end-to-end security via a collection of stronger notions of anytime security targeting compositionality to a matching collection of type-system-like syntactic criteria. This method has emerged by distilling and unifying security type system results from the literature while formalizing them in a proof assistant. Unlike in our previous papers on this topic, here we focus entirely on high-level ideas
instead of technical proof details.

Research GroupFoundations of Computing group
PublisherDe Gruyter
JournalInformation Technology
ISSN1611-2776
Publication dates
PrintDec 2014
Publication process dates
Deposited23 Apr 2015
Accepted17 Oct 2014
Output statusPublished
Accepted author manuscript
Additional information

Published Online: 2014-11-30. The final publication is available at www.degruyter.com

Digital Object Identifier (DOI)https://doi.org/10.1515/itit-2014-1060
LanguageEnglish
Permalink -

https://repository.mdx.ac.uk/item/85122

Log in to edit

Download files

Accepted author manuscript
lessAdHoc.pdf

  • 88
    total views
  • 23
    total downloads
  • 5
    views this month
  • 2
    downloads this month

Export as

Related outputs

CoCon: A conference management system with formally verified document confidentiality
Popescu, A., Lammich, P. and Hou, P. 2021. CoCon: A conference management system with formally verified document confidentiality. Journal of Automated Reasoning. 65 (2), pp. 321-356. https://doi.org/10.1007/s10817-020-09566-9
A formally verified abstract account of Gödel's incompleteness theorems
Popescu, A. and Traytel, D. 2019. A formally verified abstract account of Gödel's incompleteness theorems. Fontaine, P. (ed.) CADE 27 - 27th International Conference on Automated Deduction. Natel, Brazil 27 - 30 Aug 2019 Springer. pp. 442-461 https://doi.org/10.1007/978-3-030-29436-6_26
Bindings as bounded natural functors
Blanchette, J., Gheri, L., Popescu, A. and Traytel, D. 2019. Bindings as bounded natural functors. 46th ACM SIGPLAN Symposium on Principles of Programming Languages (POPL 2019). Hotel Cascais Miragem, Cascais, Portugal 13 - 19 Jan 2019 Association for Computing Machinery (ACM). https://doi.org/10.1145/3290335
A formalized general theory of syntax with bindings
Gheri, L. and Popescu, A. 2017. A formalized general theory of syntax with bindings. 8th International Conference Interactive Theorem Proving. Brasilia, Brazil 26 - 29 Sep 2017 Cham Springer International Publishing. pp. 241-261 https://doi.org/10.1007/978-3-319-66107-0_16
Foundational (co)datatypes and (co)recursion for higher-order logic
Biendarra, J., Blanchette, J., Bouzy, A., Desharnais, M., Fleury, M., Hölzl, J., Kunčar, O., Lochbihler, A., Meier, F., Panny, L., Popescu, A., Sternagel, C., Thiemann, R. and Traytel, D. 2017. Foundational (co)datatypes and (co)recursion for higher-order logic. 11th International Symposium on Frontiers of Combining Systems, FroCoS 2017. Brasilia, Brazil 27 - 29 Sep 2017 Cham Springer International Publishing. pp. 3-21 https://doi.org/10.1007/978-3-319-66167-4_1
Safety and conservativity of definitions in HOL and Isabelle/HOL
Kunčar, O. and Popescu, A. 2018. Safety and conservativity of definitions in HOL and Isabelle/HOL. Proceedings of the ACM on Programming Languages. 2, pp. 1-26. https://doi.org/10.1145/3158112
CoSMed: a confidentiality-verified social media platform
Bauereiß, T., Pesenti Gritti, A., Popescu, A. and Raimondi, F. 2018. CoSMed: a confidentiality-verified social media platform. Journal of Automated Reasoning. 61 (1-4), pp. 113-119. https://doi.org/10.1007/s10817-017-9443-3
A formalized general theory of syntax with bindings
Gheri, L. and Popescu, A. 2017. A formalized general theory of syntax with bindings. 8th International Conference Interactive Theorem Proving (ITP). Brasília, Brazil 26 - 29 Sep 2017 Springer. pp. 241-261 https://doi.org/10.1007/978-3-319-66107-0_16
Foundational nonuniform (co)datatypes for higher-order logic
Blanchette, J., Meier, F., Popescu, A. and Traytel, D. 2017. Foundational nonuniform (co)datatypes for higher-order logic. 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). Reykjavik, Iceland 20 - 23 Jun 2017 IEEE. https://doi.org/10.1109/LICS.2017.8005071
Soundness and completeness proofs by coinductive methods
Blanchette, J., Popescu, A. and Traytel, D. 2017. Soundness and completeness proofs by coinductive methods. Journal of Automated Reasoning. 58 (1), pp. 149-179. https://doi.org/10.1007/s10817-016-9391-3
Friends with benefits: implementing corecursion in foundational proof assistants
Blanchette, J., Bouzy, A., Lochbihler, A., Popescu, A. and Traytel, D. 2017. Friends with benefits: implementing corecursion in foundational proof assistants. 26th European Symposium on Programming, ESOP 2017. Uppsala, Sweden 22 - 29 Apr 2017 Springer. https://doi.org/10.1007/978-3-662-54434-1_5
From types to sets by local type definitions in higher-order logic
Kunčar, O. and Popescu, A. 2016. From types to sets by local type definitions in higher-order logic. ITP 2016: 7th International Conference on Interactive Theorem Proving. Nancy, France 22 - 25 Aug 2016 Springer. https://doi.org/10.1007/978-3-319-43144-4_13
Comprehending Isabelle/HOL's consistency
Kunčar, O. and Popescu, A. 2017. Comprehending Isabelle/HOL's consistency. Yang, H. (ed.) ESOP 2017: 26th European Symposium on Programming (ESOP). Uppsala, Sweden 22 - 29 Apr 2017 Berlin, Heidelberg Springer. https://doi.org/10.1007/978-3-662-54434-1_27
CoSMeDis: a distributed social media platform with formally verified confidentiality guarantees
Bauereiß, T., Pesenti Gritti, A., Popescu, A. and Raimondi, F. 2017. CoSMeDis: a distributed social media platform with formally verified confidentiality guarantees. 38th IEEE Symposium on Security and Privacy. San Jose, CA, USA 22 - 26 May 2017 Institute of Electrical and Electronics Engineers (IEEE). pp. 729-748 https://doi.org/10.1109/SP.2017.24
Encoding monomorphic and polymorphic types
Blanchette, J., Böhme, S., Popescu, A. and Smallbone, N. 2017. Encoding monomorphic and polymorphic types. Logical Methods in Computer Science. 12 (4). https://doi.org/10.2168/LMCS-12(4:13)2016
CoSMed: a confidentiality-verified social media platform
Bauereiß, T., Pesenti Gritti, A., Popescu, A. and Raimondi, F. 2016. CoSMed: a confidentiality-verified social media platform. Blanchette, J.C. and Merz, S. (ed.) ITP 2016: 7th International Conference on Interactive Theorem Proving. Nancy, France 22 - 25 Aug 2016 Springer. pp. 87-106 https://doi.org/10.1007/978-3-319-43144-4_6
A consistent foundation for Isabelle/HOL
Kunčar, O. and Popescu, A. 2015. A consistent foundation for Isabelle/HOL. 6th conference on Interactive Theorem Proving (ITP). Nanjing, China 24 - 27 Aug 2015 Springer. pp. 234-252 https://doi.org/10.1007/978-3-319-22102-1_16
Weak bisimilarity coalgebraically
Popescu, A. 2009. Weak bisimilarity coalgebraically. Algebra and Coalgebra in Computer Science, Third International Conference, CALCO 2009. Udine, Italy 07 - 10 Sep 2009 Springer. pp. 157-172
A semantic approach to interpolation
Popescu, A., Şerbănuţă, T. and Roşu, G. 2009. A semantic approach to interpolation. Theoretical Computer Science. 410 (12-13), pp. 1109-1128. https://doi.org/10.1016/j.tcs.2008.09.038
Incremental pattern-based coinduction for process algebra and its Isabelle formalization
Popescu, A. and Gunter, E. 2010. Incremental pattern-based coinduction for process algebra and its Isabelle formalization. Foundations of Software Science and Computation Structures (FOSSACS). Paphos, Cyprus 20 - 28 Mar 2010 Springer. pp. 109-127
More SPASS with Isabelle: superposition with hard sorts and configurable simplification
Blanchette, J., Popescu, A., Wand, D. and Weidenbach, C. 2012. More SPASS with Isabelle: superposition with hard sorts and configurable simplification. Interactive Theorem Proving (ITP), Third International Conference. Princeton, New Jersey, US 13 - 15 Aug 2012 Springer. pp. 345-360
Proving concurrent noninterference
Popescu, A., Hölzl, J. and Nipkow, T. 2012. Proving concurrent noninterference. 2nd International Conference on Certified Programs and Proofs (CPP 2012). Kyoto, Japan 13 - 15 Dec 2012 Springer. pp. 109-125
Formal verification of language-based concurrent noninterference
Popescu, A., Hölzl, J. and Nipkow, T. 2013. Formal verification of language-based concurrent noninterference. Journal of Formalized Reasoning. 6 (1), pp. 1-30. https://doi.org/10.6092/issn.1972-5787/3690
Noninterfering schedulers: when possibilistic noninterference implies probabilistic noninterference
Popescu, A., Hölzl, J. and Nipkow, T. 2013. Noninterfering schedulers: when possibilistic noninterference implies probabilistic noninterference. 5th Conference on Algebra and Coalgebra in Computer Science (CALCO). Warsaw, Poland 03 - 06 Sep 2013 Springer. pp. 236-252
Mechanizing the metatheory of sledgehammer
Blanchette, J. and Popescu, A. 2013. Mechanizing the metatheory of sledgehammer. 9th International Symposium on Frontiers of Combining Systems (FroCoS 2013). Nancy, France 18 - 20 Sep 2013 Springer. pp. 245-260
Formalizing probabilistic noninterference
Popescu, A., Hölzl, J. and Nipkow, T. 2013. Formalizing probabilistic noninterference. 3rd International Conference on Certified Programs and Proofs (CPP 2013). Melbourne, VIC, Australia 11 - 13 Dec 2013 Springer International Publishing. pp. 259-275
Nonfree datatypes in Isabelle/HOL: animating a many-sorted metatheory
Schropp, A. and Popescu, A. 2013. Nonfree datatypes in Isabelle/HOL: animating a many-sorted metatheory. Certified Programs and Proofs (CPP). Melbourne, Australia 11 - 13 Dec 2013 Springer. pp. 114-130 https://doi.org/10.1007/978-3-319-03545-1_8
Witnessing (co)datatypes
Blanchette, J., Popescu, A. and Traytel, D. 2015. Witnessing (co)datatypes. 24th European Symposium on Programming (ESOP 2015). London, UK 11 - 18 Apr 2015 Springer. pp. 359-382
A conference management system with verified document confidentiality
Kanav, S., Lammich, P. and Popescu, A. 2014. A conference management system with verified document confidentiality. Biere, A. and Bloem, R. (ed.) 26th International Conference on Computer Aided Verification (CAV) 2014. Vienna, Austria 18 - 24 Jul 2014 Springer. pp. 167-183 https://doi.org/10.1007/978-3-319-08867-9_11
Unified classical logic completeness: a coinductive pearl
Blanchette, J., Popescu, A. and Traytel, D. 2014. Unified classical logic completeness: a coinductive pearl. 7th International Joint Conference on Automated Reasoning (IJCAR). Vienna, Austria 19 - 22 Jul 2014 Springer International Publishing. pp. 46-60
Strong normalization for System F by HOAS on top of FOAS
Popescu, A., Gunter, E. and Osborn, C. 2010. Strong normalization for System F by HOAS on top of FOAS. 25th Annual IEEE Symposium on Logic in Computer Science (LICS). Edinburgh, United Kingdom 11 - 14 Jul 2010 Institute of Electrical and Electronics Engineers. pp. 31-40
Recursion principles for syntax with bindings and substitution
Popescu, A. and Gunter, E. 2011. Recursion principles for syntax with bindings and substitution. The 16th ACM SIGPLAN International Conference on Functional Programming. Tokyo 19 - 21 Sep 2011 Association for Computing Machinery (ACM). pp. 346-358
Foundational, compositional (co)datatypes for higher-order logic: category theory applied to theorem proving
Traytel, D., Popescu, A. and Blanchette, J. 2012. Foundational, compositional (co)datatypes for higher-order logic: category theory applied to theorem proving. 27th Annual IEEE Symposium on Logic in Computer Science (LICS). Dubrovnik, Croatia 25 - 28 Jun 2012 Institute of Electrical and Electronics Engineers (IEEE). pp. 596-605 https://doi.org/10.1109/LICS.2012.75
Truly modular (co)datatypes for Isabelle/HOL
Blanchette, J., Hölzl, J., Lochbihler, A., Panny, L., Popescu, A. and Traytel, D. 2014. Truly modular (co)datatypes for Isabelle/HOL. 5th International Conference on Interactive Theorem Proving (ITP). Vienna, Austria 14 - 17 Jul 2014 Springer International Publishing. pp. 93-110
Cardinals in Isabelle/HOL
Blanchette, J., Popescu, A. and Taytel, D. 2014. Cardinals in Isabelle/HOL. 5th International Conference on Interactive Theorem Proving. Vienna, Austria 14 - 17 Jul 2014 Springer. pp. 111-127
Term-generic logic
Popescu, A. and Roşu, G. 2015. Term-generic logic. Theoretical Computer Science. 577, pp. 1-24. https://doi.org/10.1016/j.tcs.2015.01.047
Foundational extensible corecursion: a proof assistant perspective
Blanchette, J., Popescu, A. and Traytel, D. 2015. Foundational extensible corecursion: a proof assistant perspective. 20th ACM SIGPLAN International Conference on Functional Programming (ICFP). Vancouver, Canada 31 Aug - 02 Sep 2015 Association for Computing Machinery (ACM). pp. 192-204 https://doi.org/10.1145/2784731.2784732
Encoding monomorphic and polymorphic types
Blanchette, J., Böhme, S., Popescu, A. and Smallbone, N. 2013. Encoding monomorphic and polymorphic types. 19th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS). Rome 16 - 24 Mar 2013 Springer. pp. 493-507