Zobrazeno 1 - 10
of 66
pro vyhledávání: '"Dominique Devriese"'
Autor:
Andreas Nuyts, Dominique Devriese
Publikováno v:
Logical Methods in Computer Science, Vol Volume 20, Issue 2 (2024)
Presheaf models of dependent type theory have been successfully applied to model HoTT, parametricity, and directed, guarded and nominal type theory. There has been considerable interest in internalizing aspects of these presheaf models, either to mak
Externí odkaz:
https://doaj.org/article/7f03116fcc054e20904dc0c1cb3e015d
Publikováno v:
Logical Methods in Computer Science, Vol Volume 13, Issue 4 (2017)
A compiler is fully-abstract if the compilation from source language programs to target language programs reflects and preserves behavioural equivalence. Such compilers have important security benefits, as they limit the power of an attacker interact
Externí odkaz:
https://doaj.org/article/b6d5f939f0c6412da1f7ebbd1eab4cdd
Publikováno v:
Proceedings of the ACM on Programming Languages. 6:194-224
Verifying soundness of symbolic execution-based program verifiers is a significant challenge. This is especially true if the resulting tool needs to be usable outside of the proof assistant, in which case we cannot rely on shallowly embedded assertio
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::7a72754e5e09e0caa10d795429dd8478
https://doi.org/10.1145/3547628
https://doi.org/10.1145/3547628
Publikováno v:
Proceedings of the ACM on Programming Languages. 6:1-28
Graduality and parametricity have proven to be extremely challenging notions to bring together. Intuitively, enforcing parametricity gradually requires possibly sealing values in order to detect violations of uniform behavior. Toro et al. (2019) argu
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::80cafbe138d2d8e362f8f3f864b715ea
https://doi.org/10.1145/3527314
https://doi.org/10.1145/3527314
Many variants of type theory extend a basic theory with additional primitives or properties like univalence, guarded recursion or parametricity, to enable constructions or proofs that would be harder or impossible to do in the original theory. Howeve
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::4d0a506baa9be51d25e98dd90f6dd4bf
http://arxiv.org/abs/2207.00843
http://arxiv.org/abs/2207.00843
Publikováno v:
Jacobs, K, Devriese, D & Timany, A 2022, ' Purity of an ST monad : Full abstraction by semantically typed back-translation ', Proceedings of the ACM on Programming Languages, vol. 6, no. OOPSLA1, 82 . https://doi.org/10.1145/3527326
In 1995, Launchbury and Peyton Jones extended Haskell with an ST monad that allows the programmer to use higher-order mutable state. They informally argued that these state computations were safely encapsulated, and as such, that the rich reasoning p
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::d8f1ffa0096e51d84fcf589c1bb481bb
https://pure.au.dk/portal/da/publications/purity-of-an-st-monad(c6018dd0-f704-4ec7-866f-384123bf2982).html
https://pure.au.dk/portal/da/publications/purity-of-an-st-monad(c6018dd0-f704-4ec7-866f-384123bf2982).html
The formal calculus System F models the essence of polymorphism and abstract data types, features that exist in many programming languages. The calculus’ core property is parametricity: a theorem expressing the language’s abstractions and validat
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::167007fbcce73f179a5bbf8f53339fa5
https://hdl.handle.net/11572/362402
https://hdl.handle.net/11572/362402
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
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
https://lirias.kuleuven.be/handle/20.500.12942/705681
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
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
https://biblio.vub.ac.be/vubir/(c96b23ca-0972-4fec-ae4c-c9b7dd8db4ad).html
Separation logic is a powerful program logic for the static modular verification of imperative programs. However, dynamic checking of separation logic contracts on the boundaries between verified and untrusted modules is hard because it requires one
Externí odkaz:
https://explore.openaire.eu/search/publication?articleId=doi_dedup___::9bcb9dbeed1c87380679db839a610831
https://biblio.vub.ac.be/vubir/linear-capabilities-for-fully-abstract-compilation-of-separationlogicverified-code(04d41a64-4b64-4dc5-b6e9-100d85a81bcf).html
https://biblio.vub.ac.be/vubir/linear-capabilities-for-fully-abstract-compilation-of-separationlogicverified-code(04d41a64-4b64-4dc5-b6e9-100d85a81bcf).html