Search Results

Documents authored by Ayoun, Sacha-Élie

Document
DOI: 10.4230/LIPIcs.ECOOP.2025.5
Compositional Bug Detection for Internally Unsafe Libraries: A Logical Approach to Type Unsoundness

Authors: Pedro Carrott, Sacha-Élie Ayoun, and Azalea Raad

Published in: LIPIcs, Volume 333, 39th European Conference on Object-Oriented Programming (ECOOP 2025)

Abstract
Rust is a modern programming language marrying the best of language design by offering fine-grained control over system resources (thus enabling efficient implementations), while simultaneously ensuring memory safety and data-race freedom. However, ensuring type safety in internally unsafe libraries remains an important and non-trivial challenge, where unsafe features enable low-level control but can introduce undefined behaviour (UB). Existing works on reasoning about unsafe code either use verification techniques to show correctness (i.e. safety, useful only when the unsafe code is indeed correct), or use bug detection techniques to show incorrectness (i.e. unsafety) but fail to do so automatically (to avoid developer burden), compositionally (to support libraries without a main function), soundly (without false positives) and generally (rather than applying to specific patterns). We close this gap by developing RUXt, a fully automatic, compositional bug detection technique for detecting UB in internally unsafe Rust libraries with a formal inadequacy theorem (formalised and proven in Rocq) providing a no-false-positives guarantee. RUXt leverages the Rust type system to under-approximate the set of safe values for user-defined types and detect safety violations without requiring manual annotations by the user. By encoding well-typed values in Rust as separation logic assertions, RUXt enables compositional reasoning about types to refute unsound type signatures and detect UB. The inadequacy theorem of RUXt ensures that each UB detected by RUXt in an internally unsafe library is a true safety violation that can be triggered by a safe program, i.e. one that solely interacts with the safe API of the library. To this end, when RUXt identifies a UB, it additionally produces a safe program witnessing the UB. In addition, we develop a prototype implementation in OCaml that can analyse programs written in a small model of Rust, and apply it to several case studies, showcasing its ability to detect true safety violations.
Cite as

Pedro Carrott, Sacha-Élie Ayoun, and Azalea Raad. Compositional Bug Detection for Internally Unsafe Libraries: A Logical Approach to Type Unsoundness. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 5:1-5:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{carrott_et_al:LIPIcs.ECOOP.2025.5,
  author =	{Carrott, Pedro and Ayoun, Sacha-\'{E}lie and Raad, Azalea},
  title =	{{Compositional Bug Detection for Internally Unsafe Libraries: A Logical Approach to Type Unsoundness}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{5:1--5:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-373-7},
  ISSN =	{1868-8969},
  year =	{2025},
  volume =	{333},
  editor =	{Aldrich, Jonathan and Silva, Alexandra},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2025.5},
  URN =		{urn:nbn:de:0030-drops-232988},
  doi =		{10.4230/LIPIcs.ECOOP.2025.5},
  annote =	{Keywords: Rust, bug detection, static analysis, program logics, under-approximation}
}
Document
Artifact
DOI: 10.4230/DARTS.11.2.9
Compositional Bug Detection for Internally Unsafe Libraries: A Logical Approach to Type Unsoundness (Artifact)

Authors: Pedro Carrott, Sacha-Élie Ayoun, and Azalea Raad

Published in: DARTS, Volume 11, Issue 2, Special Issue of the 39th European Conference on Object-Oriented Programming (ECOOP 2025)

Abstract
This artifact is a companion to the paper "Compositional Bug Detection for Internally Unsafe Libraries: A Logical Approach to Type Unsoundness". It contains the Rocq formalisation of the RISL program logic, the RUXtBelt semantic model and the inadequacy theorem of RUXt. It also contains the OCaml prototype for RUXt, along with the case studies discussed in the paper.
Cite as

Pedro Carrott, Sacha-Élie Ayoun, and Azalea Raad. Compositional Bug Detection for Internally Unsafe Libraries: A Logical Approach to Type Unsoundness (Artifact). In Special Issue of the 39th European Conference on Object-Oriented Programming (ECOOP 2025). Dagstuhl Artifacts Series (DARTS), Volume 11, Issue 2, pp. 9:1-9:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@Article{carrott_et_al:DARTS.11.2.9,
  author =	{Carrott, Pedro and Ayoun, Sacha-\'{E}lie and Raad, Azalea},
  title =	{{Compositional Bug Detection for Internally Unsafe Libraries: A Logical Approach to Type Unsoundness (Artifact)}},
  pages =	{9:1--9:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2025},
  volume =	{11},
  number =	{2},
  editor =	{Carrott, Pedro and Ayoun, Sacha-\'{E}lie and Raad, Azalea},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.11.2.9},
  URN =		{urn:nbn:de:0030-drops-233529},
  doi =		{10.4230/DARTS.11.2.9},
  annote =	{Keywords: Rust, bug detection, static analysis, program logics, under-approximation}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2024.25
Compositional Symbolic Execution for Correctness and Incorrectness Reasoning

Authors: Andreas Lööw, Daniele Nantes-Sobrinho, Sacha-Élie Ayoun, Caroline Cronjäger, Petar Maksimović, and Philippa Gardner

Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)

Abstract
The introduction of separation logic has led to the development of symbolic execution techniques and tools that are (functionally) compositional with function specifications that can be used in broader calling contexts. Many of the compositional symbolic execution tools developed in academia and industry have been grounded on a formal foundation, but either the function specifications are not validated with respect to the underlying separation logic of the theory, or there is a large gulf between the theory and the implementation of the tool. We introduce a formal compositional symbolic execution engine which creates and uses function specifications from an underlying separation logic and provides a sound theoretical foundation for, and indeed was partially inspired by, the Gillian symbolic execution platform. This is achieved by providing an axiomatic interface which describes the properties of the consume and produce operations used in the engine to update compositionally the symbolic state, for example when calling function specifications. This consume-produce technique is used by VeriFast, Viper, and Gillian, but has not been previously characterised independently of the tool. As part of our result, we give consume and produce operations inspired by the Gillian implementation that satisfy the properties described by our axiomatic interface. A surprising property is that our engine semantics provides a common foundation for both correctness and incorrectness reasoning, with the difference in the underlying engine only amounting to the choice to use satisfiability or validity. We use this property to extend the Gillian platform, which previously only supported correctness reasoning, with incorrectness reasoning and automatic true bug-finding using incorrectness bi-abduction. We evaluate our new Gillian platform by using the Gillian instantiation to C. This instantiation is the first tool grounded on a common formal compositional symbolic execution engine to support both correctness and incorrectness reasoning.
Cite as

Andreas Lööw, Daniele Nantes-Sobrinho, Sacha-Élie Ayoun, Caroline Cronjäger, Petar Maksimović, and Philippa Gardner. Compositional Symbolic Execution for Correctness and Incorrectness Reasoning. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 25:1-25:28, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{loow_et_al:LIPIcs.ECOOP.2024.25,
  author =	{L\"{o}\"{o}w, Andreas and Nantes-Sobrinho, Daniele and Ayoun, Sacha-\'{E}lie and Cronj\"{a}ger, Caroline and Maksimovi\'{c}, Petar and Gardner, Philippa},
  title =	{{Compositional Symbolic Execution for Correctness and Incorrectness Reasoning}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{25:1--25:28},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-341-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{313},
  editor =	{Aldrich, Jonathan and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2024.25},
  URN =		{urn:nbn:de:0030-drops-208741},
  doi =		{10.4230/LIPIcs.ECOOP.2024.25},
  annote =	{Keywords: separation logic, incorrectness logic, symbolic execution, bi-abduction}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2024.26
Matching Plans for Frame Inference in Compositional Reasoning

Authors: Andreas Lööw, Daniele Nantes-Sobrinho, Sacha-Élie Ayoun, Petar Maksimović, and Philippa Gardner

Published in: LIPIcs, Volume 313, 38th European Conference on Object-Oriented Programming (ECOOP 2024)

Abstract
The use of function specifications to reason about function calls and the manipulation of user-defined predicates are two essential ingredients of modern compositional verification tools based on separation logic. To execute these operations successfully, these tools must be able to solve the frame inference problem, that is, to understand which parts of the state are relevant for the operation at hand. We introduce matching plans, a concept that is used in the Gillian verification platform to automate frame inference efficiently. We extract matching plans and their automation machinery from the Gillian implementation and present them in a tool-agnostic way, making the Gillian approach available to the broader verification community as a verification-tool design pattern.
Cite as

Andreas Lööw, Daniele Nantes-Sobrinho, Sacha-Élie Ayoun, Petar Maksimović, and Philippa Gardner. Matching Plans for Frame Inference in Compositional Reasoning. In 38th European Conference on Object-Oriented Programming (ECOOP 2024). Leibniz International Proceedings in Informatics (LIPIcs), Volume 313, pp. 26:1-26:20, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@InProceedings{loow_et_al:LIPIcs.ECOOP.2024.26,
  author =	{L\"{o}\"{o}w, Andreas and Nantes-Sobrinho, Daniele and Ayoun, Sacha-\'{E}lie and Maksimovi\'{c}, Petar and Gardner, Philippa},
  title =	{{Matching Plans for Frame Inference in Compositional Reasoning}},
  booktitle =	{38th European Conference on Object-Oriented Programming (ECOOP 2024)},
  pages =	{26:1--26:20},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-341-6},
  ISSN =	{1868-8969},
  year =	{2024},
  volume =	{313},
  editor =	{Aldrich, Jonathan and Salvaneschi, Guido},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2024.26},
  URN =		{urn:nbn:de:0030-drops-208751},
  doi =		{10.4230/LIPIcs.ECOOP.2024.26},
  annote =	{Keywords: Compositional reasoning, separation logic, frame inference}
}
Document
Artifact
DOI: 10.4230/DARTS.10.2.13
Compositional Symbolic Execution for Correctness and Incorrectness Reasoning (Artifact)

Authors: Andreas Lööw, Daniele Nantes-Sobrinho, Sacha-Élie Ayoun, Caroline Cronjäger, Nat Karmios, Petar Maksimović, and Philippa Gardner

Published in: DARTS, Volume 10, Issue 2, Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024)

Abstract
This artifact is a companion to the paper "Compositional Symbolic Execution for Correctness and Incorrectness Reasoning". It contains the source code of the Gillian compositional symbolic execution (CSE) platform, in which we added the incorrectness reasoning capabilities, and the benchmarks used in the evaluation of the paper. It also contains a Haskell demonstrator CSE engine that directly implements the CSE engine inference rules presented in the paper.
Cite as

Andreas Lööw, Daniele Nantes-Sobrinho, Sacha-Élie Ayoun, Caroline Cronjäger, Nat Karmios, Petar Maksimović, and Philippa Gardner. Compositional Symbolic Execution for Correctness and Incorrectness Reasoning (Artifact). In Special Issue of the 38th European Conference on Object-Oriented Programming (ECOOP 2024). Dagstuhl Artifacts Series (DARTS), Volume 10, Issue 2, pp. 13:1-13:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2024)

Copy BibTex To Clipboard

@Article{loow_et_al:DARTS.10.2.13,
  author =	{L\"{o}\"{o}w, Andreas and Nantes-Sobrinho, Daniele and Ayoun, Sacha-\'{E}lie and Cronj\"{a}ger, Caroline and Karmios, Nat and Maksimovi\'{c}, Petar and Gardner, Philippa},
  title =	{{Compositional Symbolic Execution for Correctness and Incorrectness Reasoning (Artifact)}},
  pages =	{13:1--13:2},
  journal =	{Dagstuhl Artifacts Series},
  ISBN =	{978-3-95977-342-3},
  ISSN =	{2509-8195},
  year =	{2024},
  volume =	{10},
  number =	{2},
  editor =	{L\"{o}\"{o}w, Andreas and Nantes-Sobrinho, Daniele and Ayoun, Sacha-\'{E}lie and Cronj\"{a}ger, Caroline and Karmios, Nat and Maksimovi\'{c}, Petar and Gardner, Philippa},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.10.2.13},
  URN =		{urn:nbn:de:0030-drops-209110},
  doi =		{10.4230/DARTS.10.2.13},
  annote =	{Keywords: separation logic, incorrectness logic, symbolic execution, bi-abduction}
}
Any Issues?
X

Feedback on the Current Page

CAPTCHA

Thanks for your feedback!

Feedback submitted to Dagstuhl Publishing

Could not send message

Please try again later or send an E-mail
© 2023-2026 Schloss Dagstuhl – LZI GmbH Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact