3 Search Results for "Rezk, Tamara"

Document
DOI: 10.4230/LIPIcs.ECOOP.2025.14
IsaBIL: A Framework for Verifying (In)correctness of Binaries in Isabelle/HOL

Authors: Matt Griffin, Brijesh Dongol, and Azalea Raad

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

Abstract
This paper presents IsaBIL, a binary analysis framework in Isabelle/HOL that is based on the widely used Binary Analysis Platform (BAP). Specifically, in IsaBIL, we formalise BAP’s intermediate language, called BIL and integrate it with Hoare logic (to enable proofs of correctness) as well as incorrectness logic (to enable proofs of incorrectness). IsaBIL inherits the full flexibility of BAP, allowing us to verify binaries for a wide range of languages (C, C++, Rust), toolchains (LLVM, Ghidra) and target architectures (x86, RISC-V), and can also be used when the source code for a binary is unavailable. To make verification tractable, we develop a number of big-step rules that combine BIL’s existing small-step rules at different levels of abstraction to support reuse. We develop high-level reasoning rules for RISC-V instructions (our main target architecture) to further optimise verification. Additionally, we develop Isabelle proof tactics that exploit common patterns in C binaries for RISC-V to discharge large numbers of proof goals (often in the 100s) automatically. IsaBIL includes an Isabelle/ML based parser for BIL programs, allowing one to automatically generate the associated Isabelle/HOL program locale from a BAP output. Taken together, IsaBIL provides a highly flexible proof environment for program binaries. As examples, we prove correctness of key examples from the Joint Strike Fighter coding standards and the MITRE database.
Cite as

Matt Griffin, Brijesh Dongol, and Azalea Raad. IsaBIL: A Framework for Verifying (In)correctness of Binaries in Isabelle/HOL. In 39th European Conference on Object-Oriented Programming (ECOOP 2025). Leibniz International Proceedings in Informatics (LIPIcs), Volume 333, pp. 14:1-14:30, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2025)

Copy BibTex To Clipboard

@InProceedings{griffin_et_al:LIPIcs.ECOOP.2025.14,
  author =	{Griffin, Matt and Dongol, Brijesh and Raad, Azalea},
  title =	{{IsaBIL: A Framework for Verifying (In)correctness of Binaries in Isabelle/HOL}},
  booktitle =	{39th European Conference on Object-Oriented Programming (ECOOP 2025)},
  pages =	{14:1--14:30},
  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.14},
  URN =		{urn:nbn:de:0030-drops-233070},
  doi =		{10.4230/LIPIcs.ECOOP.2025.14},
  annote =	{Keywords: Binary Analysis Platform, Isabelle/HOL, Hoare Logic, Incorrectness Logic}
}
Document
DOI: 10.4230/DARTS.3.2.9
Type Abstraction for Relaxed Noninterference (Artifact)

Authors: Raimil Cruz, Tamara Rezk, Bernard Serpette, and Éric Tanter

Published in: DARTS, Volume 3, Issue 2, Special Issue of the 31st European Conference on Object-Oriented Programming (ECOOP 2017)

Abstract
This artifact is a web interpreter for the ObSec language defined in the companion paper. ObSec is a simple object-oriented language that supports type-based declassification. Type-base declassification exploits the familiar notion of type abstraction to support expressive declassification policies in a simple and expressive manner.
Cite as

Raimil Cruz, Tamara Rezk, Bernard Serpette, and Éric Tanter. Type Abstraction for Relaxed Noninterference (Artifact). In Special Issue of the 31st European Conference on Object-Oriented Programming (ECOOP 2017). Dagstuhl Artifacts Series (DARTS), Volume 3, Issue 2, pp. 9:1-9:2, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@Article{cruz_et_al:DARTS.3.2.9,
  author =	{Cruz, Raimil and Rezk, Tamara and Serpette, Bernard and Tanter, \'{E}ric},
  title =	{{Type Abstraction for Relaxed Noninterference (Artifact)}},
  pages =	{9:1--9:2},
  journal =	{Dagstuhl Artifacts Series},
  ISSN =	{2509-8195},
  year =	{2017},
  volume =	{3},
  number =	{2},
  editor =	{Cruz, Raimil and Rezk, Tamara and Serpette, Bernard and Tanter, \'{E}ric},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/DARTS.3.2.9},
  URN =		{urn:nbn:de:0030-drops-72902},
  doi =		{10.4230/DARTS.3.2.9},
  annote =	{Keywords: type abstraction, relaxed noninterference, information flow control}
}
Document
DOI: 10.4230/LIPIcs.ECOOP.2017.7
Type Abstraction for Relaxed Noninterference

Authors: Raimil Cruz, Tamara Rezk, Bernard Serpette, and Éric Tanter

Published in: LIPIcs, Volume 74, 31st European Conference on Object-Oriented Programming (ECOOP 2017)

Abstract
Information-flow security typing statically prevents confidential information to leak to public channels. The fundamental information flow property, known as noninterference, states that a public observer cannot learn anything from private data. As attractive as it is from a theoretical viewpoint, noninterference is impractical: real systems need to intentionally declassify some information, selectively. Among the different information flow approaches to declassification, a particularly expressive approach was proposed by Li and Zdancewic, enforcing a notion of relaxed noninterference by allowing programmers to specify declassification policies that capture the intended manner in which public information can be computed from private data. This paper shows how we can exploit the familiar notion of type abstraction to support expressive declassification policies in a simpler, yet more expressive manner. In particular, the type-based approach to declassification---which we develop in an object-oriented setting---addresses several issues and challenges with respect to prior work, including a simple notion of label ordering based on subtyping, support for recursive declassification policies, and a local, modular reasoning principle for relaxed noninterference. This work paves the way for integrating declassification policies in practical security-typed languages.
Cite as

Raimil Cruz, Tamara Rezk, Bernard Serpette, and Éric Tanter. Type Abstraction for Relaxed Noninterference. In 31st European Conference on Object-Oriented Programming (ECOOP 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 74, pp. 7:1-7:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)

Copy BibTex To Clipboard

@InProceedings{cruz_et_al:LIPIcs.ECOOP.2017.7,
  author =	{Cruz, Raimil and Rezk, Tamara and Serpette, Bernard and Tanter, \'{E}ric},
  title =	{{Type Abstraction for Relaxed Noninterference}},
  booktitle =	{31st European Conference on Object-Oriented Programming (ECOOP 2017)},
  pages =	{7:1--7:27},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-035-4},
  ISSN =	{1868-8969},
  year =	{2017},
  volume =	{74},
  editor =	{M\"{u}ller, Peter},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ECOOP.2017.7},
  URN =		{urn:nbn:de:0030-drops-72688},
  doi =		{10.4230/LIPIcs.ECOOP.2017.7},
  annote =	{Keywords: type abstraction, relaxed noninterference, information flow control}
}
  • Refine by Type
  • 3 Document/PDF
  • 1 Document/HTML

  • Refine by Publication Year
  • 1 2025
  • 2 2017

  • Refine by Author
  • 2 Cruz, Raimil
  • 2 Rezk, Tamara
  • 2 Serpette, Bernard
  • 2 Tanter, Éric
  • 1 Dongol, Brijesh
  • Show More...

  • Refine by Series/Journal
  • 2 LIPIcs
  • 1 DARTS

  • Refine by Classification
  • 1 Theory of computation → Program reasoning

  • Refine by Keyword
  • 2 information flow control
  • 2 relaxed noninterference
  • 2 type abstraction
  • 1 Binary Analysis Platform
  • 1 Hoare Logic
  • Show More...

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