Search Results

Documents authored by Carrott, Pedro

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}
}
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