Modular verification of op-based CRDTs in separation logic

Autor: Abel Nieto, Léon Gondelman, Alban Reynaud, Amin Timany, Lars Birkedal

Publikováno v: Nieto, A, Gondelman, L, Reynaud, A, Timany, A & Birkedal, L 2022, ' Modular verification of op-based CRDTs in separation logic ', Proceedings of the ACM on Programming Languages, vol. 6, no. OOPSLA2, pp. 1788-1816 . https://doi.org/10.1145/3563351

Operation-based Conflict-free Replicated Data Types (op-based CRDTs) are a family of distributed data structures where all operations are designed to commute, so that replica states eventually converge. Additionally, op-based CRDTs require that opera

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::ef5da70bb01c15f8ca9a0c53126085a6
https://doi.org/10.1145/3563351

Mechanized logical relations for termination-insensitive noninterference

Autor: Amin Timany, Simon Oddershede Gregersen, Johan Bay, Lars Birkedal

Publikováno v: Gregersen, S O, Bay, J, Timany, A & Birkedal, L 2021, ' Mechanized logical relations for termination-insensitive noninterference ', Proceedings of the ACM on Programming Languages, vol. 5, no. POPL, 10 . https://doi.org/10.1145/3434291

We present an expressive information-flow control type system with recursive types, existential types, label polymorphism, and impredicative type polymorphism for a higher-order programming language with higher-order state. We give a novel semantic m

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::6ee9a55f1f685ae93dcd4f0a43698110
https://doi.org/10.1145/3434291

Proving full-system security properties under multiple attacker models on capability machines

Autor: Thomas Van Strydonck, Aina Linn Georges, Armael Gueneau, Alix Trieu, Amin Timany, Frank Piessens, Lars Birkedal, Dominique Devriese

Publikováno v: Strydonck, T V, Georges, A L, Guéneau, A, Trieu, A, Timany, A, Piessens, F, Birkedal, L & Devriese, D 2022, Proving full-system security properties under multiple attacker models on capability machines . in Proceedings-2022 IEEE 35th Computer Security Foundations Symposium, CSF 2022 . IEEE, pp. 80-95, 35th IEEE Computer Security Foundations Symposium, CSF 2022, Haifa, Israel, 07/08/2022 . https://doi.org/10.1109/CSF54842.2022.9919645
CSF 2022-35th IEEE Computer Security Foundations Symposium
CSF 2022-35th IEEE Computer Security Foundations Symposium, Aug 2022, Haifa, Israel

Assembly-level protection mechanisms (virtual mem-ory, trusted execution environments, virtualization) make it possible to guarantee security properties of a full system in the presence of arbitrary attacker provided code. However, they typically onl

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::4d075c0ccc829a4572a4bc1f1525ea0a
https://lirias.kuleuven.be/handle/20.500.12942/705681

Cap’ ou pas cap’ ?

Autor: Aïna Linn Georges, Armaël Guéneau, Thomas Van Strydonck, Amin Timany, Alix Trieu, Dominique Devriese, Lars Birkedal

Publikováno v: Georges, A L, Guéneau, A, Van Strydonck, T, Timany, A, Trieu, A, Devriese, D & Birkedal, L 2021, Cap’ ou pas cap’ ?: Preuve de programmes pour une machine à capacités en présence de code inconnu . i Journées Francophones des Langages Applicatifs 2021 . Institut de Recherche en Informatique Fondamentale, Journées Francophones des Langages Applicatifs 2021, 07/04/2021 . < https://researchportal.vub.be/en/publications/cap-ou-pas-cap-preuve-de-programmes-pour-une-machine-%C3%A0-capacit%C3%A9s->
Aarhus University

Une machine à capacités est un type de microprocesseur permettant une séparation des permissions précise grâce à l’utilisation de capacités, mots machine porteurs d’une certaine autorité. Dans cet article, nous présentons une méthode pe

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=dedup_wf_001::71c592db4ae94c8e161299186a7b67db
https://biblio.vub.ac.be/vubir/(c96b23ca-0972-4fec-ae4c-c9b7dd8db4ad).html

Fully abstract from static to gradual

Autor: Dominique Devriese, Amin Timany, Koen Jacobs

Publikováno v: Jacobs, K, Timany, A & Devriese, D 2021, ' Fully abstract from static to gradual ', Proceedings of the ACM on Programming Languages, vol. 5, no. POPL, 7 . https://doi.org/10.1145/3434288

What is a good gradual language? Siek et al. have previously proposed the refined criteria, a set of formal ideas that characterize a range of guarantees typically expected from a gradual language. While these go a long way, they are mostly focused o

Externí odkaz: https://explore.openaire.eu/search/publication?articleId=doi_dedup___::d83bdee71ab6e1bb1fb7cece294eb54a
https://lirias.kuleuven.be/handle/123456789/679843