Verified symbolic execution with Kripke specification monads (and no meta-programming)

Autor: Steven Keuchel, Sander Huyghebaert, Georgy Lukyanov, Dominique Devriese

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

Modular, Fully-abstract Compilation by Approximate Back-translation

Autor: Dominique Devriese, Marco Patrignani, Frank Piessens, Steven Keuchel

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

Purity of an ST monad:Full abstraction by semantically typed back-translation

Autor: Koen Jacobs, Amin Timany, Dominique Devriese

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

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

Linear capabilities for fully abstract compilation of separation-logic-verified code

Autor: Dominique Devriese, Thomas Van Strydonck, Frank Piessens

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