---
OA_place: publisher
OA_type: hybrid
PlanS_conform: '1'
_id: '21041'
abstract:
- lang: eng
text: "It is common for programmers to assemble their programs from a combination
of trusted and untrusted components. In this context, a trusted program component
is said to be robustly safe if it behaves safely when linked against arbitrary
untrusted code. Prior work has shown how various encapsulation mechanisms (in
both high- and low-level languages) can be used to protect code so that it is
robustly safe, but none of the existing work has explored how robust safety can
be achieved in a patently unsafe language like C.\r\nIn this paper, we show how
to bring robust safety to a simple yet representative C-like language we call
Rec. Although Rec (like C) is inherently ”dangerous” and thus not robustly safe,
we can ”save” Rec programs via compilation to Cap, a CHERI-like capability machine.
To formalize the benefits of such a hardening compiler, we develop Reckon, a separation
logic for verifying robust safety of Rec programs. Reckon is not sound under Rec’s
unsafe, C-like semantics, but it is sound when Rec programs are hardened via compilation
and linked against untrusted code running on Cap. As a crucial step in proving
soundness of Reckon, we introduce a novel technique of semantic back-translation,
which we formalize by building on the DimSum framework for multi-language semantics.
All our results are mechanized in the Rocq prover."
article_processing_charge: Yes (via OA deal)
article_type: original
author:
- first_name: Niklas
full_name: Mück, Niklas
last_name: Mück
- first_name: Aïna Linn
full_name: Georges, Aïna Linn
last_name: Georges
- first_name: Derek
full_name: Dreyer, Derek
last_name: Dreyer
- first_name: Deepak
full_name: Garg, Deepak
last_name: Garg
- first_name: Michael Joachim
full_name: Sammler, Michael Joachim
id: 510d3901-2a03-11ee-914d-d9ae9011f0a7
last_name: Sammler
citation:
ama: 'Mück N, Georges AL, Dreyer D, Garg D, Sammler MJ. Endangered by the language
but saved by the compiler: Robust safety via semantic back-translation. Proceedings
of the ACM on Programming Languages. 2026;10:1153-1182. doi:10.1145/3776682'
apa: 'Mück, N., Georges, A. L., Dreyer, D., Garg, D., & Sammler, M. J. (2026).
Endangered by the language but saved by the compiler: Robust safety via semantic
back-translation. Proceedings of the ACM on Programming Languages. Association
for Computing Machinery. https://doi.org/10.1145/3776682'
chicago: 'Mück, Niklas, Aïna Linn Georges, Derek Dreyer, Deepak Garg, and Michael
Joachim Sammler. “Endangered by the Language but Saved by the Compiler: Robust
Safety via Semantic Back-Translation.” Proceedings of the ACM on Programming
Languages. Association for Computing Machinery, 2026. https://doi.org/10.1145/3776682.'
ieee: 'N. Mück, A. L. Georges, D. Dreyer, D. Garg, and M. J. Sammler, “Endangered
by the language but saved by the compiler: Robust safety via semantic back-translation,”
Proceedings of the ACM on Programming Languages, vol. 10. Association for
Computing Machinery, pp. 1153–1182, 2026.'
ista: 'Mück N, Georges AL, Dreyer D, Garg D, Sammler MJ. 2026. Endangered by the
language but saved by the compiler: Robust safety via semantic back-translation.
Proceedings of the ACM on Programming Languages. 10, 1153–1182.'
mla: 'Mück, Niklas, et al. “Endangered by the Language but Saved by the Compiler:
Robust Safety via Semantic Back-Translation.” Proceedings of the ACM on Programming
Languages, vol. 10, Association for Computing Machinery, 2026, pp. 1153–82,
doi:10.1145/3776682.'
short: N. Mück, A.L. Georges, D. Dreyer, D. Garg, M.J. Sammler, Proceedings of the
ACM on Programming Languages 10 (2026) 1153–1182.
date_created: 2026-01-25T23:01:40Z
date_published: 2026-01-08T00:00:00Z
date_updated: 2026-02-12T13:53:04Z
day: '08'
ddc:
- '000'
department:
- _id: MiSa
doi: 10.1145/3776682
file:
- access_level: open_access
checksum: 79be391061efbf9542638996959ce11a
content_type: application/pdf
creator: dernst
date_created: 2026-02-12T13:51:03Z
date_updated: 2026-02-12T13:51:03Z
file_id: '21221'
file_name: 2026_ProcACMProgrammingLanguages_Mueck.pdf
file_size: 1058876
relation: main_file
success: 1
file_date_updated: 2026-02-12T13:51:03Z
fulldoi: https://doi.org/10.1145/3776682
has_accepted_license: '1'
intvolume: ' 10'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Published Version
page: 1153-1182
publication: Proceedings of the ACM on Programming Languages
publication_identifier:
eissn:
- 2475-1421
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Endangered by the language but saved by the compiler: Robust safety via semantic
back-translation'
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 10
year: '2026'
...
---
OA_place: publisher
OA_type: gold
_id: '21133'
abstract:
- lang: eng
text: "Data structures based on trees and tree traversals are ubiquitous in computer
systems. Many low-level programs, including some implementations of critical systems
like page tables and the web browser DOM, rely on generic tree-traversal functions
that traverse tree nodes in a pre-determined order, applying a client-provided
operation to each visited node. Developing a general approach to specifying and
verifying such traversals is tricky since the client-provided per-node operation
can be stateful and may potentially depend on or modify the structure of the tree
being traversed.\r\nIn this paper, we present a recipe for (semi-)automated verification
of such generic, stateful tree traversals. Our recipe is (a) general: it applies
to a range of tree traversals, in particular, pre-, post- and in-order depth-first
traversals; (b) modular: parts of a traversal’s proof can be reused in verifying
other similar traversals; (c) expressive: using the specification of a tree traversal,
we can verify clients that use the traversal in a variety of different ways; and
(d) automatable: many proof obligations can be discharged automatically.\r\nAt
the heart of our recipe is a novel use of tree zippers to represent a logical
abstraction of the tree traversal state, and zipper transitions as an abstraction
of traversal steps. We realize our recipe in the RefinedC framework in Rocq, which
allows us to verify a number of different tree traversals and their clients written
in C."
acknowledgement: We thank the anonymous reviewers for their insightful suggestions.
This research is supported in part by generous awards from Android Security’s ASPIRE
program and from Google Research. The third author is supported, in part, by ERC
grant COCONUT (grant no. 101171349), funded by the European Union. Views and opinions
expressed are however those of the author(s) only and do not necessarily reflect
those of the European Union or the European Research Council Executive Agency. Neither
the European Union nor the granting authority can be held responsible for them.
article_processing_charge: No
author:
- first_name: Laila
full_name: Elbeheiry, Laila
last_name: Elbeheiry
- first_name: Michael Joachim
full_name: Sammler, Michael Joachim
id: 510d3901-2a03-11ee-914d-d9ae9011f0a7
last_name: Sammler
- first_name: Robbert
full_name: Krebbers, Robbert
last_name: Krebbers
- first_name: Derek
full_name: Dreyer, Derek
last_name: Dreyer
- first_name: Deepak
full_name: Garg, Deepak
last_name: Garg
citation:
ama: 'Elbeheiry L, Sammler MJ, Krebbers R, Dreyer D, Garg D. A recipe for modular
verification of generic tree traversals. In: Proceedings of the 15th ACM SIGPLAN
International Conference on Certified Programs and Proofs. Association for
Computing Machinery; 2026:339-352. doi:10.1145/3779031.3779110'
apa: 'Elbeheiry, L., Sammler, M. J., Krebbers, R., Dreyer, D., & Garg, D. (2026).
A recipe for modular verification of generic tree traversals. In Proceedings
of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs
(pp. 339–352). Rennes, France: Association for Computing Machinery. https://doi.org/10.1145/3779031.3779110'
chicago: Elbeheiry, Laila, Michael Joachim Sammler, Robbert Krebbers, Derek Dreyer,
and Deepak Garg. “A Recipe for Modular Verification of Generic Tree Traversals.”
In Proceedings of the 15th ACM SIGPLAN International Conference on Certified
Programs and Proofs, 339–52. Association for Computing Machinery, 2026. https://doi.org/10.1145/3779031.3779110.
ieee: L. Elbeheiry, M. J. Sammler, R. Krebbers, D. Dreyer, and D. Garg, “A recipe
for modular verification of generic tree traversals,” in Proceedings of the
15th ACM SIGPLAN International Conference on Certified Programs and Proofs,
Rennes, France, 2026, pp. 339–352.
ista: 'Elbeheiry L, Sammler MJ, Krebbers R, Dreyer D, Garg D. 2026. A recipe for
modular verification of generic tree traversals. Proceedings of the 15th ACM SIGPLAN
International Conference on Certified Programs and Proofs. CPP: Conference on
Certified Programs and Proofs, 339–352.'
mla: Elbeheiry, Laila, et al. “A Recipe for Modular Verification of Generic Tree
Traversals.” Proceedings of the 15th ACM SIGPLAN International Conference on
Certified Programs and Proofs, Association for Computing Machinery, 2026,
pp. 339–52, doi:10.1145/3779031.3779110.
short: L. Elbeheiry, M.J. Sammler, R. Krebbers, D. Dreyer, D. Garg, in:, Proceedings
of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs,
Association for Computing Machinery, 2026, pp. 339–352.
conference:
end_date: 2026-01-13
location: Rennes, France
name: 'CPP: Conference on Certified Programs and Proofs'
start_date: 2026-01-12
date_created: 2026-02-01T23:01:43Z
date_published: 2026-01-08T00:00:00Z
date_updated: 2026-02-16T08:43:24Z
day: '08'
ddc:
- '000'
department:
- _id: MiSa
doi: 10.1145/3779031.3779110
file:
- access_level: open_access
checksum: 7df99991493e907d83a197151f378e3e
content_type: application/pdf
creator: dernst
date_created: 2026-02-16T08:40:29Z
date_updated: 2026-02-16T08:40:29Z
file_id: '21225'
file_name: 2026_CPP_Elbeheiry.pdf
file_size: 811872
relation: main_file
success: 1
file_date_updated: 2026-02-16T08:40:29Z
fulldoi: https://doi.org/10.1145/3779031.3779110
has_accepted_license: '1'
language:
- iso: eng
month: '01'
oa: 1
oa_version: Published Version
page: 339-352
publication: Proceedings of the 15th ACM SIGPLAN International Conference on Certified
Programs and Proofs
publication_identifier:
isbn:
- '9798400723414'
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
scopus_import: '1'
status: public
title: A recipe for modular verification of generic tree traversals
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
year: '2026'
...
---
OA_place: publisher
OA_type: hybrid
PlanS_conform: '1'
_id: '21052'
abstract:
- lang: eng
text: "Program logics have proven a successful strategy for verification of complex
programs. By providing local reasoning and means of abstraction and composition,
they allow reasoning principles for individual components of a program to be combined
to prove guarantees about a whole program. Crucially, these components and their
proofs can be reused. However, this reuse is only available once the program logic
has been defined. It is a frustrating fact of the status quo that whoever defines
a new program logic must establish every part, both semantics and proof rules,
from scratch. In spite of programming languages and program logics typically sharing
many core features, reuse is generally not available across languages. Even inside
one language, if the same underlying operation appears in multiple language primitives,
reuse is typically not possible when establishing proof rules for the program
logic.\r\nTo enable reuse across and inside languages when defining complex program
logics (and proving them sound), we serve program logics à la carte by combining
program logic fragments for the various effects of the language. Among other language
features, the menu includes shared state, concurrency, and non-determinism as
reusable, composable blocks that can be combined to define a program logic modularly.
Our theory builds on ITrees as a framework to express language semantics and Iris
as the underlying separation logic; the work has been mechanized in the Coq proof
assistant."
article_processing_charge: No
article_type: original
author:
- first_name: Max
full_name: Vistrup, Max
last_name: Vistrup
- first_name: Michael Joachim
full_name: Sammler, Michael Joachim
id: 510d3901-2a03-11ee-914d-d9ae9011f0a7
last_name: Sammler
- first_name: Ralf
full_name: Jung, Ralf
last_name: Jung
citation:
ama: Vistrup M, Sammler MJ, Jung R. Program logics à la Carte. Proceedings of
the ACM on Programming Languages. 2025;9(POPL):300-331. doi:10.1145/3704847
apa: Vistrup, M., Sammler, M. J., & Jung, R. (2025). Program logics à la Carte.
Proceedings of the ACM on Programming Languages. Association for Computing
Machinery. https://doi.org/10.1145/3704847
chicago: Vistrup, Max, Michael Joachim Sammler, and Ralf Jung. “Program Logics à
La Carte.” Proceedings of the ACM on Programming Languages. Association
for Computing Machinery, 2025. https://doi.org/10.1145/3704847.
ieee: M. Vistrup, M. J. Sammler, and R. Jung, “Program logics à la Carte,” Proceedings
of the ACM on Programming Languages, vol. 9, no. POPL. Association for Computing
Machinery, pp. 300–331, 2025.
ista: Vistrup M, Sammler MJ, Jung R. 2025. Program logics à la Carte. Proceedings
of the ACM on Programming Languages. 9(POPL), 300–331.
mla: Vistrup, Max, et al. “Program Logics à La Carte.” Proceedings of the ACM
on Programming Languages, vol. 9, no. POPL, Association for Computing Machinery,
2025, pp. 300–31, doi:10.1145/3704847.
short: M. Vistrup, M.J. Sammler, R. Jung, Proceedings of the ACM on Programming
Languages 9 (2025) 300–331.
date_created: 2026-01-28T06:35:47Z
date_published: 2025-01-09T00:00:00Z
date_updated: 2026-02-09T06:19:36Z
day: '09'
doi: 10.1145/3704847
extern: '1'
fulldoi: https://doi.org/10.1145/3704847
has_accepted_license: '1'
intvolume: ' 9'
issue: POPL
language:
- iso: eng
main_file_link:
- open_access: '1'
month: '01'
oa: 1
oa_version: Published Version
page: 300-331
publication: Proceedings of the ACM on Programming Languages
publication_identifier:
issn:
- 2475-1421
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
scopus_import: '1'
status: public
title: Program logics à la Carte
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 9
year: '2025'
...
---
OA_place: publisher
OA_type: hybrid
PlanS_conform: '1'
_id: '21053'
abstract:
- lang: eng
text: "Program verification tools are often implemented as front-end translations
of an input program into an intermediate verification language (IVL) such as Boogie,
GIL, Viper, or Why3. The resulting IVL program is then verified using an existing
back-end verifier. A soundness proof for such a translational verifier needs to
relate the input program and verification logic to the semantics of the IVL, which
in turn needs to be connected with the verification logic implemented in the back-end
verifiers. Performing such proofs is challenging due to the large semantic gap
between the input and output programs and logics, especially for complex verification
logics such as separation logic.\r\nThis paper presents a formal framework for
reasoning about translational separation logic verifiers. At its center is a generic
core IVL that captures the essence of different separation logics. We define its
operational semantics and formally connect it to two different back-end verifiers,
which use symbolic execution and verification condition generation, resp. Crucially,
this semantics uses angelic non-determinism to enable the application of different
proof search algorithms and heuristics in the back-end verifiers. An axiomatic
semantics for the core IVL simplifies reasoning about the front-end translation
by performing essential proof steps once and for all in the equivalence proof
with the operational semantics rather than for each concrete front-end translation.\r\nWe
illustrate the usefulness of our formal framework by instantiating our core IVL
with elements of Viper and connecting it to two Viper back-ends as well as a front-end
for concurrent separation logic. All our technical results have been formalized
in Isabelle/HOL, including the core IVL and its semantics, the semantics of two
back-ends for a subset of Viper, and all proofs."
article_processing_charge: No
article_type: original
arxiv: 1
author:
- first_name: Thibault
full_name: Dardinier, Thibault
last_name: Dardinier
- first_name: Michael Joachim
full_name: Sammler, Michael Joachim
id: 510d3901-2a03-11ee-914d-d9ae9011f0a7
last_name: Sammler
- first_name: Gaurav
full_name: Parthasarathy, Gaurav
last_name: Parthasarathy
- first_name: Alexander J.
full_name: Summers, Alexander J.
last_name: Summers
- first_name: Peter
full_name: Müller, Peter
last_name: Müller
citation:
ama: Dardinier T, Sammler MJ, Parthasarathy G, Summers AJ, Müller P. Formal foundations
for translational separation logic verifiers. Proceedings of the ACM on Programming
Languages. 2025;9(POPL):569-599. doi:10.1145/3704856
apa: Dardinier, T., Sammler, M. J., Parthasarathy, G., Summers, A. J., & Müller,
P. (2025). Formal foundations for translational separation logic verifiers. Proceedings
of the ACM on Programming Languages. Association for Computing Machinery.
https://doi.org/10.1145/3704856
chicago: Dardinier, Thibault, Michael Joachim Sammler, Gaurav Parthasarathy, Alexander
J. Summers, and Peter Müller. “Formal Foundations for Translational Separation
Logic Verifiers.” Proceedings of the ACM on Programming Languages. Association
for Computing Machinery, 2025. https://doi.org/10.1145/3704856.
ieee: T. Dardinier, M. J. Sammler, G. Parthasarathy, A. J. Summers, and P. Müller,
“Formal foundations for translational separation logic verifiers,” Proceedings
of the ACM on Programming Languages, vol. 9, no. POPL. Association for Computing
Machinery, pp. 569–599, 2025.
ista: Dardinier T, Sammler MJ, Parthasarathy G, Summers AJ, Müller P. 2025. Formal
foundations for translational separation logic verifiers. Proceedings of the ACM
on Programming Languages. 9(POPL), 569–599.
mla: Dardinier, Thibault, et al. “Formal Foundations for Translational Separation
Logic Verifiers.” Proceedings of the ACM on Programming Languages, vol.
9, no. POPL, Association for Computing Machinery, 2025, pp. 569–99, doi:10.1145/3704856.
short: T. Dardinier, M.J. Sammler, G. Parthasarathy, A.J. Summers, P. Müller, Proceedings
of the ACM on Programming Languages 9 (2025) 569–599.
date_created: 2026-01-28T06:36:57Z
date_published: 2025-01-09T00:00:00Z
date_updated: 2026-02-09T06:25:01Z
day: '09'
ddc:
- '000'
doi: 10.1145/3704856
extern: '1'
external_id:
arxiv:
- '2407.20002'
fulldoi: https://doi.org/10.1145/3704856
has_accepted_license: '1'
intvolume: ' 9'
issue: POPL
language:
- iso: eng
month: '01'
oa_version: Published Version
page: 569-599
publication: Proceedings of the ACM on Programming Languages
publication_identifier:
issn:
- 2475-1421
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
status: public
title: Formal foundations for translational separation logic verifiers
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 9
year: '2025'
...
---
OA_place: publisher
OA_type: hybrid
_id: '19935'
abstract:
- lang: eng
text: "The separation logic framework Iris has been built on the premise that all
assertions are stable, meaning they unconditionally enjoy the famous frame rule.
This gives Iris—and the numerous program logics that build on it—very modular
reasoning principles. But stability also comes at a cost. It excludes a core feature
of the Viper verifier family, heap-dependent expression assertions, which lift
program expressions to the assertion level in order to reduce redundancy between
code and specifications and better facilitate SMT-based automation.\r\nIn this
paper, we bring heap-dependent expression assertions to Iris with Daenerys. To
do so, we must first revisit the very core of Iris, extending it with a new form
of unstable resources (and adapting the frame rule accordingly). On top, we then
build a program logic with heap-dependent expression assertions and lay the foundations
for connecting Iris to SMT solvers. We apply Daenerys to several case studies,
including some that go beyond what Viper and Iris can do individually and others
that benefit from the connection to SMT."
acknowledgement: "We would like to thank the anonymous reviewers for their helpful
feedback and Alex Summers\r\nfor insightful discussions. This work was funded in
part by a Google PhD Fellowship for the first\r\nauthor."
article_processing_charge: Yes (in subscription journal)
article_type: original
author:
- first_name: Simon
full_name: Spies, Simon
last_name: Spies
- first_name: Niklas
full_name: Mück, Niklas
last_name: Mück
- first_name: Haoyi
full_name: Zeng, Haoyi
last_name: Zeng
- first_name: Michael Joachim
full_name: Sammler, Michael Joachim
id: 510d3901-2a03-11ee-914d-d9ae9011f0a7
last_name: Sammler
- first_name: Andrea
full_name: Lattuada, Andrea
last_name: Lattuada
- first_name: Peter
full_name: Müller, Peter
last_name: Müller
- first_name: Derek
full_name: Dreyer, Derek
last_name: Dreyer
citation:
ama: Spies S, Mück N, Zeng H, et al. Destabilizing Iris. Proceedings of the ACM
on Programming Languages. 2025;9(PLDI):848-873. doi:10.1145/3729284
apa: Spies, S., Mück, N., Zeng, H., Sammler, M. J., Lattuada, A., Müller, P., &
Dreyer, D. (2025). Destabilizing Iris. Proceedings of the ACM on Programming
Languages. Association for Computing Machinery. https://doi.org/10.1145/3729284
chicago: Spies, Simon, Niklas Mück, Haoyi Zeng, Michael Joachim Sammler, Andrea
Lattuada, Peter Müller, and Derek Dreyer. “Destabilizing Iris.” Proceedings
of the ACM on Programming Languages. Association for Computing Machinery,
2025. https://doi.org/10.1145/3729284.
ieee: S. Spies et al., “Destabilizing Iris,” Proceedings of the ACM on
Programming Languages, vol. 9, no. PLDI. Association for Computing Machinery,
pp. 848–873, 2025.
ista: Spies S, Mück N, Zeng H, Sammler MJ, Lattuada A, Müller P, Dreyer D. 2025.
Destabilizing Iris. Proceedings of the ACM on Programming Languages. 9(PLDI),
848–873.
mla: Spies, Simon, et al. “Destabilizing Iris.” Proceedings of the ACM on Programming
Languages, vol. 9, no. PLDI, Association for Computing Machinery, 2025, pp.
848–73, doi:10.1145/3729284.
short: S. Spies, N. Mück, H. Zeng, M.J. Sammler, A. Lattuada, P. Müller, D. Dreyer,
Proceedings of the ACM on Programming Languages 9 (2025) 848–873.
corr_author: '1'
date_created: 2025-06-30T08:47:31Z
date_published: 2025-06-01T00:00:00Z
date_updated: 2025-06-30T09:10:11Z
day: '01'
ddc:
- '000'
department:
- _id: MiSa
doi: 10.1145/3729284
file:
- access_level: open_access
checksum: 6b72d84c10a10ba7cd1646e2c36dc1ff
content_type: application/pdf
creator: dernst
date_created: 2025-06-30T09:01:08Z
date_updated: 2025-06-30T09:01:08Z
file_id: '19938'
file_name: 2025_ProcACMProg_Spies.pdf
file_size: 843343
relation: main_file
success: 1
file_date_updated: 2025-06-30T09:01:08Z
fulldoi: https://doi.org/10.1145/3729284
has_accepted_license: '1'
intvolume: ' 9'
issue: PLDI
language:
- iso: eng
month: '06'
oa: 1
oa_version: Published Version
page: 848-873
publication: Proceedings of the ACM on Programming Languages
publication_identifier:
eissn:
- 2475-1421
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
scopus_import: '1'
status: public
title: Destabilizing Iris
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 9
year: '2025'
...
---
OA_place: publisher
OA_type: hybrid
_id: '19936'
abstract:
- lang: eng
text: 'There has been a recent upsurge of interest in formal, machine-checked verification
of timing guarantees for C implementations of real-time system schedulers. However,
prior work has only considered tick-based schedulers, which enjoy a clearly defined
notion of time: the time "quantum". In this work, we present a new approach to
real-time systems verification for interrupt-free schedulers, which are commonly
used in deeply embedded and resource-constrained systems but which do not enjoy
a natural notion of periodic time. Our approach builds on and connects two recently
developed Rocq-based systems—RefinedC (for foundational C verification) and Prosa
(for verified response-time analysis)—adapting the former to reason about timed
traces and the latter to reason about overheads. We apply the resulting system,
which we call RefinedProsa, to verify Rössl, a simple yet representative, fixed-priority,
non-preemptive, interrupt-free scheduler implemented in C.'
acknowledgement: "We would like to thank the anonymous reviewers for their helpful
feedback.\r\nThis project has received funding from the European Research Council
(ERC) under the European\r\nUnion’s Horizon 2020 research and innovation programme
(grant agreement No 803111)."
article_processing_charge: Yes (in subscription journal)
article_type: original
author:
- first_name: Kimaya
full_name: Bedarkar, Kimaya
last_name: Bedarkar
- first_name: Laila
full_name: Elbeheiry, Laila
last_name: Elbeheiry
- first_name: Michael Joachim
full_name: Sammler, Michael Joachim
id: 510d3901-2a03-11ee-914d-d9ae9011f0a7
last_name: Sammler
- first_name: Lennard
full_name: Gäher, Lennard
last_name: Gäher
- first_name: Björn
full_name: Brandenburg, Björn
last_name: Brandenburg
- first_name: Derek
full_name: Dreyer, Derek
last_name: Dreyer
- first_name: Deepak
full_name: Garg, Deepak
last_name: Garg
citation:
ama: 'Bedarkar K, Elbeheiry L, Sammler MJ, et al. RefinedProsa: Connecting response-time
analysis with C verification for interrupt-free schedulers. Proceedings of
the ACM on Programming Languages. 2025;9(PLDI):73-97. doi:10.1145/3729249'
apa: 'Bedarkar, K., Elbeheiry, L., Sammler, M. J., Gäher, L., Brandenburg, B., Dreyer,
D., & Garg, D. (2025). RefinedProsa: Connecting response-time analysis with
C verification for interrupt-free schedulers. Proceedings of the ACM on Programming
Languages. Association for Computing Machinery. https://doi.org/10.1145/3729249'
chicago: 'Bedarkar, Kimaya, Laila Elbeheiry, Michael Joachim Sammler, Lennard Gäher,
Björn Brandenburg, Derek Dreyer, and Deepak Garg. “RefinedProsa: Connecting Response-Time
Analysis with C Verification for Interrupt-Free Schedulers.” Proceedings of
the ACM on Programming Languages. Association for Computing Machinery, 2025.
https://doi.org/10.1145/3729249.'
ieee: 'K. Bedarkar et al., “RefinedProsa: Connecting response-time analysis
with C verification for interrupt-free schedulers,” Proceedings of the ACM
on Programming Languages, vol. 9, no. PLDI. Association for Computing Machinery,
pp. 73–97, 2025.'
ista: 'Bedarkar K, Elbeheiry L, Sammler MJ, Gäher L, Brandenburg B, Dreyer D, Garg
D. 2025. RefinedProsa: Connecting response-time analysis with C verification for
interrupt-free schedulers. Proceedings of the ACM on Programming Languages. 9(PLDI),
73–97.'
mla: 'Bedarkar, Kimaya, et al. “RefinedProsa: Connecting Response-Time Analysis
with C Verification for Interrupt-Free Schedulers.” Proceedings of the ACM
on Programming Languages, vol. 9, no. PLDI, Association for Computing Machinery,
2025, pp. 73–97, doi:10.1145/3729249.'
short: K. Bedarkar, L. Elbeheiry, M.J. Sammler, L. Gäher, B. Brandenburg, D. Dreyer,
D. Garg, Proceedings of the ACM on Programming Languages 9 (2025) 73–97.
corr_author: '1'
date_created: 2025-06-30T08:47:58Z
date_published: 2025-06-13T00:00:00Z
date_updated: 2025-06-30T09:09:55Z
day: '13'
ddc:
- '000'
department:
- _id: MiSa
doi: 10.1145/3729249
file:
- access_level: open_access
checksum: 8c18d777feb342a7265c54b16205ec4c
content_type: application/pdf
creator: dernst
date_created: 2025-06-30T09:08:05Z
date_updated: 2025-06-30T09:08:05Z
file_id: '19939'
file_name: 2025_ProcACMProg_Bedarkar.pdf
file_size: 1043790
relation: main_file
success: 1
file_date_updated: 2025-06-30T09:08:05Z
fulldoi: https://doi.org/10.1145/3729249
has_accepted_license: '1'
intvolume: ' 9'
issue: PLDI
language:
- iso: eng
month: '06'
oa: 1
oa_version: Published Version
page: 73-97
publication: Proceedings of the ACM on Programming Languages
publication_identifier:
issn:
- 2475-1421
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'RefinedProsa: Connecting response-time analysis with C verification for interrupt-free
schedulers'
tmp:
image: /images/cc_by.png
legal_code_url: https://creativecommons.org/licenses/by/4.0/legalcode
name: Creative Commons Attribution 4.0 International Public License (CC-BY 4.0)
short: CC BY (4.0)
type: journal_article
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 9
year: '2025'
...
---
_id: '17495'
abstract:
- lang: eng
text: Rust is a modern systems programming language whose ownership-based type system
statically guarantees memory safety, making it particularly well-suited to the
domain of safety-critical systems. In recent years, a wellspring of automated
deductive verification tools have emerged for establishing functional correctness
of Rust code. However, none of the previous tools produce foundational proofs
(machine-checkable in a general-purpose proof assistant), and all of them are
restricted to the safe fragment of Rust. This is a problem because the vast majority
of Rust programs make use of unsafe code at critical points, such as in the implementation
of widely-used APIs. We propose RefinedRust, a refinement type system—proven sound
in the Coq proof assistant—with the goal of establishing foundational semi-automated
functional correctness verification of both safe and unsafe Rust code. We have
developed a prototype verification tool implementing RefinedRust. Our tool translates
Rust code (with user annotations) into a model of Rust embedded in Coq, and then
checks its adherence to the RefinedRust type system using separation logic automation
in Coq. All proofs generated by RefinedRust are checked by the Coq proof assistant,
so the automation and type system do not have to be trusted. We evaluate the effectiveness
of RefinedRust by verifying a variant of Rust’s Vec implementation that involves
intricate reasoning about unsafe pointer-manipulating code.
article_processing_charge: No
article_type: original
author:
- first_name: Lennard
full_name: Gäher, Lennard
last_name: Gäher
- first_name: Michael Joachim
full_name: Sammler, Michael Joachim
id: 510d3901-2a03-11ee-914d-d9ae9011f0a7
last_name: Sammler
- first_name: Ralf
full_name: Jung, Ralf
last_name: Jung
- first_name: Robbert
full_name: Krebbers, Robbert
last_name: Krebbers
- first_name: Derek
full_name: Dreyer, Derek
last_name: Dreyer
citation:
ama: 'Gäher L, Sammler MJ, Jung R, Krebbers R, Dreyer D. RefinedRust: A type system
for high-assurance verification of rust programs. Proceedings of the ACM on
Programming Languages. 2024;8(PLDI):1115-1139. doi:10.1145/3656422'
apa: 'Gäher, L., Sammler, M. J., Jung, R., Krebbers, R., & Dreyer, D. (2024).
RefinedRust: A type system for high-assurance verification of rust programs. Proceedings
of the ACM on Programming Languages. Association for Computing Machinery.
https://doi.org/10.1145/3656422'
chicago: 'Gäher, Lennard, Michael Joachim Sammler, Ralf Jung, Robbert Krebbers,
and Derek Dreyer. “RefinedRust: A Type System for High-Assurance Verification
of Rust Programs.” Proceedings of the ACM on Programming Languages. Association
for Computing Machinery, 2024. https://doi.org/10.1145/3656422.'
ieee: 'L. Gäher, M. J. Sammler, R. Jung, R. Krebbers, and D. Dreyer, “RefinedRust:
A type system for high-assurance verification of rust programs,” Proceedings
of the ACM on Programming Languages, vol. 8, no. PLDI. Association for Computing
Machinery, pp. 1115–1139, 2024.'
ista: 'Gäher L, Sammler MJ, Jung R, Krebbers R, Dreyer D. 2024. RefinedRust: A type
system for high-assurance verification of rust programs. Proceedings of the ACM
on Programming Languages. 8(PLDI), 1115–1139.'
mla: 'Gäher, Lennard, et al. “RefinedRust: A Type System for High-Assurance Verification
of Rust Programs.” Proceedings of the ACM on Programming Languages, vol.
8, no. PLDI, Association for Computing Machinery, 2024, pp. 1115–39, doi:10.1145/3656422.'
short: L. Gäher, M.J. Sammler, R. Jung, R. Krebbers, D. Dreyer, Proceedings of the
ACM on Programming Languages 8 (2024) 1115–1139.
date_created: 2024-09-05T07:52:27Z
date_published: 2024-06-20T00:00:00Z
date_updated: 2024-09-10T07:16:49Z
day: '20'
doi: 10.1145/3656422
extern: '1'
fulldoi: https://doi.org/10.1145/3656422
intvolume: ' 8'
issue: PLDI
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.1145/3656422
month: '06'
oa: 1
oa_version: Published Version
page: 1115-1139
publication: Proceedings of the ACM on Programming Languages
publication_identifier:
issn:
- 2475-1421
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'RefinedRust: A type system for high-assurance verification of rust programs'
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 8
year: '2024'
...
---
_id: '17497'
abstract:
- lang: eng
text: 'Over the past two decades, there has been a great deal of progress on verification
of full functional correctness of programs using separation logic, sometimes even
producing “foundational” proofs in proof assistants like Coq. Unfortunately, even
though existing approaches to this problem provide significant support for automated
verification, they still incur a significant specification overhead: the user
must supply the specification against which the program is verified, and the specification
may be long, complex, or tedious to formulate. In this paper, we introduce Quiver,
the first technique for inferring functional correctness specifications in separation
logic while simultaneously verifying foundationally that they are correct. To
guide Quiver towards the final specification, we take hints from the user in the
form of a specification sketch, and then complete the sketch using inference.
To do so, Quiver introduces a new abductive deductive verification technique,
which integrates ideas from abductive inference (for specification inference)
together with deductive separation logic automation (for foundational verification).
The result is that users have to provide some guidance, but significantly less
than with traditional deductive verification techniques based on separation logic.
We have evaluated Quiver on a range of case studies, including code from popular
open-source libraries.'
article_processing_charge: No
article_type: original
author:
- first_name: Simon
full_name: Spies, Simon
last_name: Spies
- first_name: Lennard
full_name: Gäher, Lennard
last_name: Gäher
- first_name: Michael Joachim
full_name: Sammler, Michael Joachim
id: 510d3901-2a03-11ee-914d-d9ae9011f0a7
last_name: Sammler
- first_name: Derek
full_name: Dreyer, Derek
last_name: Dreyer
citation:
ama: 'Spies S, Gäher L, Sammler MJ, Dreyer D. Quiver: Guided abductive inference
of separation logic specifications in coq. Proceedings of the ACM on Programming
Languages. 2024;8(PLDI):889-913. doi:10.1145/3656413'
apa: 'Spies, S., Gäher, L., Sammler, M. J., & Dreyer, D. (2024). Quiver: Guided
abductive inference of separation logic specifications in coq. Proceedings
of the ACM on Programming Languages. Association for Computing Machinery.
https://doi.org/10.1145/3656413'
chicago: 'Spies, Simon, Lennard Gäher, Michael Joachim Sammler, and Derek Dreyer.
“Quiver: Guided Abductive Inference of Separation Logic Specifications in Coq.”
Proceedings of the ACM on Programming Languages. Association for Computing
Machinery, 2024. https://doi.org/10.1145/3656413.'
ieee: 'S. Spies, L. Gäher, M. J. Sammler, and D. Dreyer, “Quiver: Guided abductive
inference of separation logic specifications in coq,” Proceedings of the ACM
on Programming Languages, vol. 8, no. PLDI. Association for Computing Machinery,
pp. 889–913, 2024.'
ista: 'Spies S, Gäher L, Sammler MJ, Dreyer D. 2024. Quiver: Guided abductive inference
of separation logic specifications in coq. Proceedings of the ACM on Programming
Languages. 8(PLDI), 889–913.'
mla: 'Spies, Simon, et al. “Quiver: Guided Abductive Inference of Separation Logic
Specifications in Coq.” Proceedings of the ACM on Programming Languages,
vol. 8, no. PLDI, Association for Computing Machinery, 2024, pp. 889–913, doi:10.1145/3656413.'
short: S. Spies, L. Gäher, M.J. Sammler, D. Dreyer, Proceedings of the ACM on Programming
Languages 8 (2024) 889–913.
date_created: 2024-09-05T08:10:41Z
date_published: 2024-06-20T00:00:00Z
date_updated: 2024-09-10T12:00:57Z
day: '20'
doi: 10.1145/3656413
extern: '1'
fulldoi: https://doi.org/10.1145/3656413
intvolume: ' 8'
issue: PLDI
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.1145/3656413
month: '06'
oa: 1
oa_version: Published Version
page: 889-913
publication: Proceedings of the ACM on Programming Languages
publication_identifier:
issn:
- 2475-1421
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Quiver: Guided abductive inference of separation logic specifications in coq'
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 8
year: '2024'
...
---
_id: '17498'
abstract:
- lang: eng
text: In recent years, there has been tremendous progress on developing program
logics for verifying the correctness of programs in a rich and diverse array of
languages. Thus far, however, such logics have assumed that programs are written
entirely in a single programming language. In practice, this assumption rarely
holds since programs are often composed of components written in different programming
languages, which interact with one another via some kind of foreign function interface
(FFI). In this paper, we take the first steps towards the goal of developing program
logics for multi-language verification. Specifically, we present Melocoton, a
multi-language program verification system for reasoning about OCaml, C, and their
interactions through the OCaml FFI. Melocoton consists of the first formal semantics
of (a large subset of) the OCaml FFI—previously only described in prose in the
OCaml manual—as well as the first program logic to reason about the interactions
of program components written in OCaml and C. Melocoton is fully mechanized in
Coq on top of the Iris separation logic framework.
article_processing_charge: No
article_type: original
author:
- first_name: Armaël
full_name: Guéneau, Armaël
last_name: Guéneau
- first_name: Johannes
full_name: Hostert, Johannes
last_name: Hostert
- first_name: Simon
full_name: Spies, Simon
last_name: Spies
- first_name: Michael Joachim
full_name: Sammler, Michael Joachim
id: 510d3901-2a03-11ee-914d-d9ae9011f0a7
last_name: Sammler
- first_name: Lars
full_name: Birkedal, Lars
last_name: Birkedal
- first_name: Derek
full_name: Dreyer, Derek
last_name: Dreyer
citation:
ama: 'Guéneau A, Hostert J, Spies S, Sammler MJ, Birkedal L, Dreyer D. Melocoton:
A program logic for verified interoperability between OCaml and C. Proceedings
of the ACM on Programming Languages. 2023;7(OOPSLA2):716-744. doi:10.1145/3622823'
apa: 'Guéneau, A., Hostert, J., Spies, S., Sammler, M. J., Birkedal, L., & Dreyer,
D. (2023). Melocoton: A program logic for verified interoperability between OCaml
and C. Proceedings of the ACM on Programming Languages. Association for
Computing Machinery. https://doi.org/10.1145/3622823'
chicago: 'Guéneau, Armaël, Johannes Hostert, Simon Spies, Michael Joachim Sammler,
Lars Birkedal, and Derek Dreyer. “Melocoton: A Program Logic for Verified Interoperability
between OCaml and C.” Proceedings of the ACM on Programming Languages.
Association for Computing Machinery, 2023. https://doi.org/10.1145/3622823.'
ieee: 'A. Guéneau, J. Hostert, S. Spies, M. J. Sammler, L. Birkedal, and D. Dreyer,
“Melocoton: A program logic for verified interoperability between OCaml and C,”
Proceedings of the ACM on Programming Languages, vol. 7, no. OOPSLA2. Association
for Computing Machinery, pp. 716–744, 2023.'
ista: 'Guéneau A, Hostert J, Spies S, Sammler MJ, Birkedal L, Dreyer D. 2023. Melocoton:
A program logic for verified interoperability between OCaml and C. Proceedings
of the ACM on Programming Languages. 7(OOPSLA2), 716–744.'
mla: 'Guéneau, Armaël, et al. “Melocoton: A Program Logic for Verified Interoperability
between OCaml and C.” Proceedings of the ACM on Programming Languages,
vol. 7, no. OOPSLA2, Association for Computing Machinery, 2023, pp. 716–44, doi:10.1145/3622823.'
short: A. Guéneau, J. Hostert, S. Spies, M.J. Sammler, L. Birkedal, D. Dreyer, Proceedings
of the ACM on Programming Languages 7 (2023) 716–744.
date_created: 2024-09-05T08:17:10Z
date_published: 2023-10-16T00:00:00Z
date_updated: 2024-09-10T09:04:24Z
day: '16'
doi: 10.1145/3622823
extern: '1'
fulldoi: https://doi.org/10.1145/3622823
intvolume: ' 7'
issue: OOPSLA2
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.1145/3622823
month: '10'
oa: 1
oa_version: Published Version
page: 716-744
publication: Proceedings of the ACM on Programming Languages
publication_identifier:
issn:
- 2475-1421
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Melocoton: A program logic for verified interoperability between OCaml and
C'
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 7
year: '2023'
...
---
_id: '17499'
abstract:
- lang: eng
text: "Much work in formal verification of low-level systems is based on one of
two approaches: refinement or separation logic. These two approaches have complementary
benefits: refinement supports the use of programs as specifications, as well as
transitive composition of proofs, whereas separation logic supports conditional
specifications, as well as modular ownership reasoning about shared state. A number
of verification frameworks employ these techniques in tandem, but in all such
cases the benefits of the two techniques remain separate. For example, in frameworks
that use relational separation logic to prove contextual refinement, the relational
separation logic judgment does not support transitive composition of proofs, while
the contextual refinement judgment does not support conditional specifications.
\ \r\nIn this paper, we propose Conditional Contextual Refinement (or CCR, for
short), the first verification system to not only combine refinement and separation
logic in a single framework but also to truly marry them together into a unified
mechanism enjoying all the benefits of refinement and separation logic simultaneously.
Specifically, unlike in prior work, CCR’s refinement specifications are both conditional
(with separation logic pre- and post-conditions) and transitively composable.
We implement CCR in Coq and evaluate its effectiveness on a range of interesting
examples."
article_processing_charge: No
article_type: original
author:
- first_name: Youngju
full_name: Song, Youngju
last_name: Song
- first_name: Minki
full_name: Cho, Minki
last_name: Cho
- first_name: Dongjae
full_name: Lee, Dongjae
last_name: Lee
- first_name: Chung-Kil
full_name: Hur, Chung-Kil
last_name: Hur
- first_name: Michael Joachim
full_name: Sammler, Michael Joachim
id: 510d3901-2a03-11ee-914d-d9ae9011f0a7
last_name: Sammler
- first_name: Derek
full_name: Dreyer, Derek
last_name: Dreyer
citation:
ama: Song Y, Cho M, Lee D, Hur C-K, Sammler MJ, Dreyer D. Conditional contextual
refinement. Proceedings of the ACM on Programming Languages. 2023;7(POPL):1121-1151.
doi:10.1145/3571232
apa: Song, Y., Cho, M., Lee, D., Hur, C.-K., Sammler, M. J., & Dreyer, D. (2023).
Conditional contextual refinement. Proceedings of the ACM on Programming Languages.
Association for Computing Machinery. https://doi.org/10.1145/3571232
chicago: Song, Youngju, Minki Cho, Dongjae Lee, Chung-Kil Hur, Michael Joachim Sammler,
and Derek Dreyer. “Conditional Contextual Refinement.” Proceedings of the ACM
on Programming Languages. Association for Computing Machinery, 2023. https://doi.org/10.1145/3571232.
ieee: Y. Song, M. Cho, D. Lee, C.-K. Hur, M. J. Sammler, and D. Dreyer, “Conditional
contextual refinement,” Proceedings of the ACM on Programming Languages,
vol. 7, no. POPL. Association for Computing Machinery, pp. 1121–1151, 2023.
ista: Song Y, Cho M, Lee D, Hur C-K, Sammler MJ, Dreyer D. 2023. Conditional contextual
refinement. Proceedings of the ACM on Programming Languages. 7(POPL), 1121–1151.
mla: Song, Youngju, et al. “Conditional Contextual Refinement.” Proceedings of
the ACM on Programming Languages, vol. 7, no. POPL, Association for Computing
Machinery, 2023, pp. 1121–51, doi:10.1145/3571232.
short: Y. Song, M. Cho, D. Lee, C.-K. Hur, M.J. Sammler, D. Dreyer, Proceedings
of the ACM on Programming Languages 7 (2023) 1121–1151.
date_created: 2024-09-05T08:21:51Z
date_published: 2023-01-11T00:00:00Z
date_updated: 2024-09-10T09:03:17Z
day: '11'
doi: 10.1145/3571232
extern: '1'
fulldoi: https://doi.org/10.1145/3571232
intvolume: ' 7'
issue: POPL
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.1145/3571232
month: '01'
oa: 1
oa_version: Published Version
page: 1121-1151
publication: Proceedings of the ACM on Programming Languages
publication_identifier:
issn:
- 2475-1421
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
scopus_import: '1'
status: public
title: Conditional contextual refinement
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 7
year: '2023'
...
---
_id: '17500'
abstract:
- lang: eng
text: "Prior work on multi-language program verification has achieved impressive
results, including the compositional verification of complex compilers. But the
existing approaches to this problem impose a variety of restrictions on the overall
structure of multi-language programs (e.g. fixing the source language, fixing
the set of involved languages, fixing the memory model, or fixing the semantics
of interoperation). In this paper, we explore the problem of how to avoid such
global restrictions.\r\nConcretely, we present DimSum: a new, decentralized approach
to multi-language semantics and verification, which we have implemented in the
Coq proof assistant. Decentralization means that we can define and reason about
languages independently from each other (as independent modules communicating
via events), but also combine and translate between them when necessary (via a
library of combinators).\r\nWe apply DimSum to a high-level imperative language
Rec (with an abstract memory model and function calls), a low-level assembly language
Asm (with a concrete memory model, arbitrary jumps, and syscalls), and a mathematical
specification language Spec. We evaluate DimSum on two case studies: an Asm library
extending Rec with support for pointer comparison, and a coroutine library for
Rec written in Asm. In both cases, we show how DimSum allows the Asm libraries
to be abstracted to Rec-level specifications, despite the behavior of the Asm
libraries not being syntactically expressible in Rec itself. We also verify an
optimizing multi-pass compiler from Rec to Asm, showing that it is compatible
with these Asm libraries."
article_processing_charge: No
article_type: original
author:
- first_name: Michael Joachim
full_name: Sammler, Michael Joachim
id: 510d3901-2a03-11ee-914d-d9ae9011f0a7
last_name: Sammler
- first_name: Simon
full_name: Spies, Simon
last_name: Spies
- first_name: Youngju
full_name: Song, Youngju
last_name: Song
- first_name: Emanuele
full_name: D'Osualdo, Emanuele
last_name: D'Osualdo
- first_name: Robbert
full_name: Krebbers, Robbert
last_name: Krebbers
- first_name: Deepak
full_name: Garg, Deepak
last_name: Garg
- first_name: Derek
full_name: Dreyer, Derek
last_name: Dreyer
citation:
ama: 'Sammler MJ, Spies S, Song Y, et al. DimSum: A decentralized approach to multi-language
semantics and verification. Proceedings of the ACM on Programming Languages.
2023;7(POPL):775-805. doi:10.1145/3571220'
apa: 'Sammler, M. J., Spies, S., Song, Y., D’Osualdo, E., Krebbers, R., Garg, D.,
& Dreyer, D. (2023). DimSum: A decentralized approach to multi-language semantics
and verification. Proceedings of the ACM on Programming Languages. Association
for Computing Machinery. https://doi.org/10.1145/3571220'
chicago: 'Sammler, Michael Joachim, Simon Spies, Youngju Song, Emanuele D’Osualdo,
Robbert Krebbers, Deepak Garg, and Derek Dreyer. “DimSum: A Decentralized Approach
to Multi-Language Semantics and Verification.” Proceedings of the ACM on Programming
Languages. Association for Computing Machinery, 2023. https://doi.org/10.1145/3571220.'
ieee: 'M. J. Sammler et al., “DimSum: A decentralized approach to multi-language
semantics and verification,” Proceedings of the ACM on Programming Languages,
vol. 7, no. POPL. Association for Computing Machinery, pp. 775–805, 2023.'
ista: 'Sammler MJ, Spies S, Song Y, D’Osualdo E, Krebbers R, Garg D, Dreyer D. 2023.
DimSum: A decentralized approach to multi-language semantics and verification.
Proceedings of the ACM on Programming Languages. 7(POPL), 775–805.'
mla: 'Sammler, Michael Joachim, et al. “DimSum: A Decentralized Approach to Multi-Language
Semantics and Verification.” Proceedings of the ACM on Programming Languages,
vol. 7, no. POPL, Association for Computing Machinery, 2023, pp. 775–805, doi:10.1145/3571220.'
short: M.J. Sammler, S. Spies, Y. Song, E. D’Osualdo, R. Krebbers, D. Garg, D. Dreyer,
Proceedings of the ACM on Programming Languages 7 (2023) 775–805.
date_created: 2024-09-05T08:24:06Z
date_published: 2023-01-11T00:00:00Z
date_updated: 2024-09-10T09:13:02Z
day: '11'
doi: 10.1145/3571220
extern: '1'
fulldoi: https://doi.org/10.1145/3571220
intvolume: ' 7'
issue: POPL
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.1145/3571220
month: '01'
oa: 1
oa_version: Published Version
page: 775-805
publication: Proceedings of the ACM on Programming Languages
publication_identifier:
issn:
- 2475-1421
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'DimSum: A decentralized approach to multi-language semantics and verification'
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 7
year: '2023'
...
---
_id: '17501'
abstract:
- lang: eng
text: "Low-level systems code often needs to interact with data, such as page table
entries or network packet headers, in which multiple pieces of information are
packaged together as bitfield components of a single machine integer and accessed
via bitfield manipulations (e.g., shifts and masking). Most existing approaches
to verifying such code employ SMT solvers, instantiated with theories for bit
vector reasoning: these provide a powerful hammer, but also significantly increase
the trusted computing base of the verification toolchain.\r\nIn this work, we
propose an alternative approach to the verification of bitfield-manipulating systems
code, which we call BFF. Building on the RefinedC framework, BFF is not only highly
automated (as SMT-based approaches are) but also foundational---i.e., it produces
a machine-checked proof of program correctness against a formal semantics for
C programs, fully mechanized in Coq. Unlike SMT-based approaches, we do not try
to solve the general problem of arbitrary bit vector reasoning, but rather observe
that real systems code typically accesses bitfields using simple, well-understood
programming patterns: the layout of a bit vector is known up front, and its bitfields
are accessed in predictable ways through a handful of bitwise operations involving
bit masks. Correspondingly, we center our approach around the concept of a structured
bit vector---i.e., a bit vector with a known bitfield layout---which we use to
drive simple and predictable automation. We validate the BFF approach by verifying
a range of bitfield-manipulating C functions drawn from real systems code, including
page table manipulation code from the Linux kernel and the pKVM hypervisor."
article_processing_charge: No
article_type: original
author:
- first_name: Fengmin
full_name: Zhu, Fengmin
last_name: Zhu
- first_name: Michael Joachim
full_name: Sammler, Michael Joachim
id: 510d3901-2a03-11ee-914d-d9ae9011f0a7
last_name: Sammler
- first_name: Rodolphe
full_name: Lepigre, Rodolphe
last_name: Lepigre
- first_name: Derek
full_name: Dreyer, Derek
last_name: Dreyer
- first_name: Deepak
full_name: Garg, Deepak
last_name: Garg
citation:
ama: 'Zhu F, Sammler MJ, Lepigre R, Dreyer D, Garg D. BFF: Foundational and automated
verification of bitfield-manipulating programs. Proceedings of the ACM on Programming
Languages. 2022;6(OOPSLA2):1613-1638. doi:10.1145/3563345'
apa: 'Zhu, F., Sammler, M. J., Lepigre, R., Dreyer, D., & Garg, D. (2022). BFF:
Foundational and automated verification of bitfield-manipulating programs. Proceedings
of the ACM on Programming Languages. Association for Computing Machinery.
https://doi.org/10.1145/3563345'
chicago: 'Zhu, Fengmin, Michael Joachim Sammler, Rodolphe Lepigre, Derek Dreyer,
and Deepak Garg. “BFF: Foundational and Automated Verification of Bitfield-Manipulating
Programs.” Proceedings of the ACM on Programming Languages. Association
for Computing Machinery, 2022. https://doi.org/10.1145/3563345.'
ieee: 'F. Zhu, M. J. Sammler, R. Lepigre, D. Dreyer, and D. Garg, “BFF: Foundational
and automated verification of bitfield-manipulating programs,” Proceedings
of the ACM on Programming Languages, vol. 6, no. OOPSLA2. Association for
Computing Machinery, pp. 1613–1638, 2022.'
ista: 'Zhu F, Sammler MJ, Lepigre R, Dreyer D, Garg D. 2022. BFF: Foundational and
automated verification of bitfield-manipulating programs. Proceedings of the ACM
on Programming Languages. 6(OOPSLA2), 1613–1638.'
mla: 'Zhu, Fengmin, et al. “BFF: Foundational and Automated Verification of Bitfield-Manipulating
Programs.” Proceedings of the ACM on Programming Languages, vol. 6, no.
OOPSLA2, Association for Computing Machinery, 2022, pp. 1613–38, doi:10.1145/3563345.'
short: F. Zhu, M.J. Sammler, R. Lepigre, D. Dreyer, D. Garg, Proceedings of the
ACM on Programming Languages 6 (2022) 1613–1638.
date_created: 2024-09-05T08:27:17Z
date_published: 2022-10-31T00:00:00Z
date_updated: 2024-09-10T09:49:18Z
day: '31'
doi: 10.1145/3563345
extern: '1'
fulldoi: https://doi.org/10.1145/3563345
intvolume: ' 6'
issue: OOPSLA2
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.1145/3563345
month: '10'
oa: 1
oa_version: Published Version
page: 1613-1638
publication: Proceedings of the ACM on Programming Languages
publication_identifier:
issn:
- 2475-1421
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'BFF: Foundational and automated verification of bitfield-manipulating programs'
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 6
year: '2022'
...
---
_id: '17502'
abstract:
- lang: eng
text: "Recent years have seen great advances towards verifying large-scale systems
code. However, these verifications are usually based on hand-written assembly
or machine-code semantics for the underlying architecture that only cover a small
part of the instruction set architecture (ISA). In contrast, other recent work
has used Sail to establish formal models for large real-world architectures, including
Armv8-A and RISC-V, that are comprehensive (complete enough to boot an operating
system or hypervisor) and authoritative (automatically derived from the Arm internal
model and validated against the Arm validation suite, and adopted as the official
formal specification by RISC-V International, respectively). But the scale and
complexity of these models makes them challenging to use as a basis for verification.\r\nIn
this paper, we propose Islaris, the first system to support verification of machine
code above these complete and authoritative real-world ISA specifications. Islaris
uses a novel combination of SMT-solver-based symbolic execution (the Isla symbolic
executor) and automated reasoning in a foundational program logic (a new separation
logic we derive using Iris in Coq). We show that this approach can handle Armv8-A
and RISC-V machine code exercising a wide range of systems features, including
installing and calling exception vectors, code parametric on a relocation address
offset (from the production pKVM hypervisor); unaligned access faults; memory-mapped
IO; and compiled C code using inline assembly and function pointers."
article_processing_charge: No
author:
- first_name: Michael Joachim
full_name: Sammler, Michael Joachim
id: 510d3901-2a03-11ee-914d-d9ae9011f0a7
last_name: Sammler
- first_name: Angus
full_name: Hammond, Angus
last_name: Hammond
- first_name: Rodolphe
full_name: Lepigre, Rodolphe
last_name: Lepigre
- first_name: Brian
full_name: Campbell, Brian
last_name: Campbell
- first_name: Jean
full_name: Pichon-Pharabod, Jean
last_name: Pichon-Pharabod
- first_name: Derek
full_name: Dreyer, Derek
last_name: Dreyer
- first_name: Deepak
full_name: Garg, Deepak
last_name: Garg
- first_name: Peter
full_name: Sewell, Peter
last_name: Sewell
citation:
ama: 'Sammler MJ, Hammond A, Lepigre R, et al. Islaris: Verification of machine
code against authoritative ISA semantics. In: Proceedings of the 43rd ACM SIGPLAN
International Conference on Programming Language Design and Implementation.
Association for Computing Machinery; 2022:825-840. doi:10.1145/3519939.3523434'
apa: 'Sammler, M. J., Hammond, A., Lepigre, R., Campbell, B., Pichon-Pharabod, J.,
Dreyer, D., … Sewell, P. (2022). Islaris: Verification of machine code against
authoritative ISA semantics. In Proceedings of the 43rd ACM SIGPLAN International
Conference on Programming Language Design and Implementation (pp. 825–840).
San Diego, CA, United States: Association for Computing Machinery. https://doi.org/10.1145/3519939.3523434'
chicago: 'Sammler, Michael Joachim, Angus Hammond, Rodolphe Lepigre, Brian Campbell,
Jean Pichon-Pharabod, Derek Dreyer, Deepak Garg, and Peter Sewell. “Islaris: Verification
of Machine Code against Authoritative ISA Semantics.” In Proceedings of the
43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation,
825–40. Association for Computing Machinery, 2022. https://doi.org/10.1145/3519939.3523434.'
ieee: 'M. J. Sammler et al., “Islaris: Verification of machine code against
authoritative ISA semantics,” in Proceedings of the 43rd ACM SIGPLAN International
Conference on Programming Language Design and Implementation, San Diego, CA,
United States, 2022, pp. 825–840.'
ista: 'Sammler MJ, Hammond A, Lepigre R, Campbell B, Pichon-Pharabod J, Dreyer D,
Garg D, Sewell P. 2022. Islaris: Verification of machine code against authoritative
ISA semantics. Proceedings of the 43rd ACM SIGPLAN International Conference on
Programming Language Design and Implementation. PLDI: Conference on Programming
Language Design and Implementation, 825–840.'
mla: 'Sammler, Michael Joachim, et al. “Islaris: Verification of Machine Code against
Authoritative ISA Semantics.” Proceedings of the 43rd ACM SIGPLAN International
Conference on Programming Language Design and Implementation, Association
for Computing Machinery, 2022, pp. 825–40, doi:10.1145/3519939.3523434.'
short: M.J. Sammler, A. Hammond, R. Lepigre, B. Campbell, J. Pichon-Pharabod, D.
Dreyer, D. Garg, P. Sewell, in:, Proceedings of the 43rd ACM SIGPLAN International
Conference on Programming Language Design and Implementation, Association for
Computing Machinery, 2022, pp. 825–840.
conference:
end_date: 2022-06-17
location: San Diego, CA, United States
name: 'PLDI: Conference on Programming Language Design and Implementation'
start_date: 2022-06-13
date_created: 2024-09-05T08:29:08Z
date_published: 2022-06-09T00:00:00Z
date_updated: 2024-09-10T11:08:03Z
day: '09'
doi: 10.1145/3519939.3523434
extern: '1'
fulldoi: https://doi.org/10.1145/3519939.3523434
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.1145/3519939.3523434
month: '06'
oa: 1
oa_version: Published Version
page: 825-840
publication: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming
Language Design and Implementation
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Islaris: Verification of machine code against authoritative ISA semantics'
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
year: '2022'
...
---
_id: '17503'
abstract:
- lang: eng
text: "Systems code often requires fine-grained control over memory layout and pointers,
expressed using low-level (e.g., bitwise) operations on pointer values. Since
these operations go beyond what basic pointer arithmetic in C allows, they are
performed with the help of integer-pointer casts. Prior work has explored increasingly
realistic memory object models for C that account for the desired semantics of
integer-pointer casts while also being sound w.r.t. compiler optimisations, culminating
in PNVI, the preferred memory object model in ongoing discussions within the ISO
WG14 C standards committee. However, its complexity makes it an unappealing target
for verification, and no tools currently exist to verify C programs under PNVI.\r\nIn
this paper, we introduce VIP, a new memory object model aimed at supporting C
verification. VIP sidesteps the complexities of PNVI with a simple but effective
idea: a new construct that lets programmers express the intended provenances of
integer-pointer casts explicitly. At the same time, we prove VIP compatible with
PNVI, thus enabling verification on top of VIP to benefit from PNVI’s validation
with respect to practice. In particular, we build a verification tool, RefinedC-VIP,
for verifying programs under VIP semantics. As the name suggests, RefinedC-VIP
extends the recently developed RefinedC tool, which is automated yet also produces
foundational proofs in Coq. We evaluate RefinedC-VIP on a range of systems-code
idioms, and validate VIP’s expressiveness via an implementation in the Cerberus
C semantics."
article_processing_charge: No
article_type: original
author:
- first_name: Rodolphe
full_name: Lepigre, Rodolphe
last_name: Lepigre
- first_name: Michael Joachim
full_name: Sammler, Michael Joachim
id: 510d3901-2a03-11ee-914d-d9ae9011f0a7
last_name: Sammler
- first_name: Kayvan
full_name: Memarian, Kayvan
last_name: Memarian
- first_name: Robbert
full_name: Krebbers, Robbert
last_name: Krebbers
- first_name: Derek
full_name: Dreyer, Derek
last_name: Dreyer
- first_name: Peter
full_name: Sewell, Peter
last_name: Sewell
citation:
ama: 'Lepigre R, Sammler MJ, Memarian K, Krebbers R, Dreyer D, Sewell P. VIP: Verifying
real-world C idioms with integer-pointer casts. Proceedings of the ACM on Programming
Languages. 2022;6(POPL):1-32. doi:10.1145/3498681'
apa: 'Lepigre, R., Sammler, M. J., Memarian, K., Krebbers, R., Dreyer, D., &
Sewell, P. (2022). VIP: Verifying real-world C idioms with integer-pointer casts.
Proceedings of the ACM on Programming Languages. Association for Computing
Machinery. https://doi.org/10.1145/3498681'
chicago: 'Lepigre, Rodolphe, Michael Joachim Sammler, Kayvan Memarian, Robbert Krebbers,
Derek Dreyer, and Peter Sewell. “VIP: Verifying Real-World C Idioms with Integer-Pointer
Casts.” Proceedings of the ACM on Programming Languages. Association for
Computing Machinery, 2022. https://doi.org/10.1145/3498681.'
ieee: 'R. Lepigre, M. J. Sammler, K. Memarian, R. Krebbers, D. Dreyer, and P. Sewell,
“VIP: Verifying real-world C idioms with integer-pointer casts,” Proceedings
of the ACM on Programming Languages, vol. 6, no. POPL. Association for Computing
Machinery, pp. 1–32, 2022.'
ista: 'Lepigre R, Sammler MJ, Memarian K, Krebbers R, Dreyer D, Sewell P. 2022.
VIP: Verifying real-world C idioms with integer-pointer casts. Proceedings of
the ACM on Programming Languages. 6(POPL), 1–32.'
mla: 'Lepigre, Rodolphe, et al. “VIP: Verifying Real-World C Idioms with Integer-Pointer
Casts.” Proceedings of the ACM on Programming Languages, vol. 6, no. POPL,
Association for Computing Machinery, 2022, pp. 1–32, doi:10.1145/3498681.'
short: R. Lepigre, M.J. Sammler, K. Memarian, R. Krebbers, D. Dreyer, P. Sewell,
Proceedings of the ACM on Programming Languages 6 (2022) 1–32.
date_created: 2024-09-05T08:31:09Z
date_published: 2022-01-12T00:00:00Z
date_updated: 2024-09-10T09:48:57Z
day: '12'
doi: 10.1145/3498681
extern: '1'
fulldoi: https://doi.org/10.1145/3498681
intvolume: ' 6'
issue: POPL
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.1145/3498681
month: '01'
oa: 1
oa_version: Published Version
page: 1-32
publication: Proceedings of the ACM on Programming Languages
publication_identifier:
issn:
- 2475-1421
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'VIP: Verifying real-world C idioms with integer-pointer casts'
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 6
year: '2022'
...
---
_id: '17504'
abstract:
- lang: eng
text: "Today’s compilers employ a variety of non-trivial optimizations to achieve
good performance. One key trick compilers use to justify transformations of concurrent
programs is to assume that the source program has no data races: if it does, they
cause the program to have undefined behavior (UB) and give the compiler free rein.
However, verifying correctness of optimizations that exploit this assumption is
a non-trivial problem. In particular, prior work either has not proven that such
optimizations preserve program termination (particularly non-obvious when considering
optimizations that move instructions out of loop bodies), or has treated all synchronization
operations as external functions (losing the ability to reorder instructions around
them).\r\nIn this work we present Simuliris, the first simulation technique to
establish termination preservation (under a fair scheduler) for a range of concurrent
program transformations that exploit UB in the source language. Simuliris is based
on the idea of using ownership to reason modularly about the assumptions the compiler
makes about programs with well-defined behavior. This brings the benefits of concurrent
separation logics to the space of verifying program transformations: we can combine
powerful reasoning techniques such as framing and coinduction to perform thread-local
proofs of non-trivial concurrent program optimizations. Simuliris is built on
a (non-step-indexed) variant of the Coq-based Iris framework, and is thus not
tied to a particular language. In addition to demonstrating the effectiveness
of Simuliris on standard compiler optimizations involving data race UB, we also
instantiate it with Jung et al.’s Stacked Borrows semantics for Rust and generalize
their proofs of interesting type-based aliasing optimizations to account for concurrency."
article_processing_charge: No
article_type: original
author:
- first_name: Lennard
full_name: Gäher, Lennard
last_name: Gäher
- first_name: Michael Joachim
full_name: Sammler, Michael Joachim
id: 510d3901-2a03-11ee-914d-d9ae9011f0a7
last_name: Sammler
- first_name: Simon
full_name: Spies, Simon
last_name: Spies
- first_name: Ralf
full_name: Jung, Ralf
last_name: Jung
- first_name: Hoang-Hai
full_name: Dang, Hoang-Hai
last_name: Dang
- first_name: Robbert
full_name: Krebbers, Robbert
last_name: Krebbers
- first_name: Jeehoon
full_name: Kang, Jeehoon
last_name: Kang
- first_name: Derek
full_name: Dreyer, Derek
last_name: Dreyer
citation:
ama: 'Gäher L, Sammler MJ, Spies S, et al. Simuliris: A separation logic framework
for verifying concurrent program optimizations. Proceedings of the ACM on Programming
Languages. 2022;6(POPL):1-31. doi:10.1145/3498689'
apa: 'Gäher, L., Sammler, M. J., Spies, S., Jung, R., Dang, H.-H., Krebbers, R.,
… Dreyer, D. (2022). Simuliris: A separation logic framework for verifying concurrent
program optimizations. Proceedings of the ACM on Programming Languages.
Association for Computing Machinery. https://doi.org/10.1145/3498689'
chicago: 'Gäher, Lennard, Michael Joachim Sammler, Simon Spies, Ralf Jung, Hoang-Hai
Dang, Robbert Krebbers, Jeehoon Kang, and Derek Dreyer. “Simuliris: A Separation
Logic Framework for Verifying Concurrent Program Optimizations.” Proceedings
of the ACM on Programming Languages. Association for Computing Machinery,
2022. https://doi.org/10.1145/3498689.'
ieee: 'L. Gäher et al., “Simuliris: A separation logic framework for verifying
concurrent program optimizations,” Proceedings of the ACM on Programming Languages,
vol. 6, no. POPL. Association for Computing Machinery, pp. 1–31, 2022.'
ista: 'Gäher L, Sammler MJ, Spies S, Jung R, Dang H-H, Krebbers R, Kang J, Dreyer
D. 2022. Simuliris: A separation logic framework for verifying concurrent program
optimizations. Proceedings of the ACM on Programming Languages. 6(POPL), 1–31.'
mla: 'Gäher, Lennard, et al. “Simuliris: A Separation Logic Framework for Verifying
Concurrent Program Optimizations.” Proceedings of the ACM on Programming Languages,
vol. 6, no. POPL, Association for Computing Machinery, 2022, pp. 1–31, doi:10.1145/3498689.'
short: L. Gäher, M.J. Sammler, S. Spies, R. Jung, H.-H. Dang, R. Krebbers, J. Kang,
D. Dreyer, Proceedings of the ACM on Programming Languages 6 (2022) 1–31.
date_created: 2024-09-05T08:32:16Z
date_published: 2022-01-12T00:00:00Z
date_updated: 2024-09-10T09:48:37Z
day: '12'
doi: 10.1145/3498689
extern: '1'
fulldoi: https://doi.org/10.1145/3498689
intvolume: ' 6'
issue: POPL
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.1145/3498689
month: '01'
oa: 1
oa_version: Published Version
page: 1-31
publication: Proceedings of the ACM on Programming Languages
publication_identifier:
issn:
- 2475-1421
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'Simuliris: A separation logic framework for verifying concurrent program optimizations'
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 6
year: '2022'
...
---
_id: '17505'
abstract:
- lang: eng
text: "Given the central role that C continues to play in systems software, and
the difficulty of writing safe and correct C code, it remains a grand challenge
to develop effective formal methods for verifying C programs. In this paper, we
propose a new approach to this problem: a type system we call RefinedC, which
combines ownership types (for modular reasoning about shared state and concurrency)
with refinement types (for encoding precise invariants on C data types and Hoare-style
specifications for C functions).\r\nRefinedC is both automated (requiring minimal
user intervention) and foundational (producing a proof of program correctness
in Coq), while at the same time handling a range of low-level programming idioms
such as pointer arithmetic. In particular, following the approach of RustBelt,
the soundness of the RefinedC type system is justified semantically by interpretation
into the Coq-based Iris framework for higher-order concurrent separation logic.
However, the typing rules of RefinedC are also designed to be encodable in a new
“separation logic programming” language we call Lithium. By restricting to a carefully
chosen (yet expressive) fragment of separation logic, Lithium supports predictable,
automatic, goal-directed proof search without backtracking. We demonstrate the
effectiveness of RefinedC on a range of representative examples of C code."
article_processing_charge: No
author:
- first_name: Michael Joachim
full_name: Sammler, Michael Joachim
id: 510d3901-2a03-11ee-914d-d9ae9011f0a7
last_name: Sammler
- first_name: Rodolphe
full_name: Lepigre, Rodolphe
last_name: Lepigre
- first_name: Robbert
full_name: Krebbers, Robbert
last_name: Krebbers
- first_name: Kayvan
full_name: Memarian, Kayvan
last_name: Memarian
- first_name: Derek
full_name: Dreyer, Derek
last_name: Dreyer
- first_name: Deepak
full_name: Garg, Deepak
last_name: Garg
citation:
ama: 'Sammler MJ, Lepigre R, Krebbers R, Memarian K, Dreyer D, Garg D. RefinedC:
Automating the foundational verification of C code with refined ownership types.
In: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming
Language Design and Implementation. Association for Computing Machinery; 2021:158-174.
doi:10.1145/3453483.3454036'
apa: 'Sammler, M. J., Lepigre, R., Krebbers, R., Memarian, K., Dreyer, D., &
Garg, D. (2021). RefinedC: Automating the foundational verification of C code
with refined ownership types. In Proceedings of the 42nd ACM SIGPLAN International
Conference on Programming Language Design and Implementation (pp. 158–174).
virtual: Association for Computing Machinery. https://doi.org/10.1145/3453483.3454036'
chicago: 'Sammler, Michael Joachim, Rodolphe Lepigre, Robbert Krebbers, Kayvan Memarian,
Derek Dreyer, and Deepak Garg. “RefinedC: Automating the Foundational Verification
of C Code with Refined Ownership Types.” In Proceedings of the 42nd ACM SIGPLAN
International Conference on Programming Language Design and Implementation,
158–74. Association for Computing Machinery, 2021. https://doi.org/10.1145/3453483.3454036.'
ieee: 'M. J. Sammler, R. Lepigre, R. Krebbers, K. Memarian, D. Dreyer, and D. Garg,
“RefinedC: Automating the foundational verification of C code with refined ownership
types,” in Proceedings of the 42nd ACM SIGPLAN International Conference on
Programming Language Design and Implementation, virtual, 2021, pp. 158–174.'
ista: 'Sammler MJ, Lepigre R, Krebbers R, Memarian K, Dreyer D, Garg D. 2021. RefinedC:
Automating the foundational verification of C code with refined ownership types.
Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language
Design and Implementation. PLDI: Conference on Programming Language Design and
Implementation, 158–174.'
mla: 'Sammler, Michael Joachim, et al. “RefinedC: Automating the Foundational Verification
of C Code with Refined Ownership Types.” Proceedings of the 42nd ACM SIGPLAN
International Conference on Programming Language Design and Implementation,
Association for Computing Machinery, 2021, pp. 158–74, doi:10.1145/3453483.3454036.'
short: M.J. Sammler, R. Lepigre, R. Krebbers, K. Memarian, D. Dreyer, D. Garg, in:,
Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language
Design and Implementation, Association for Computing Machinery, 2021, pp. 158–174.
conference:
end_date: 2021-06-25
location: virtual
name: 'PLDI: Conference on Programming Language Design and Implementation'
start_date: 2021-06-20
date_created: 2024-09-05T08:34:50Z
date_published: 2021-06-18T00:00:00Z
date_updated: 2024-09-10T11:54:22Z
day: '18'
doi: 10.1145/3453483.3454036
extern: '1'
fulldoi: https://doi.org/10.1145/3453483.3454036
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.1145/3453483.3454036
month: '06'
oa: 1
oa_version: Published Version
page: 158-174
publication: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming
Language Design and Implementation
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
scopus_import: '1'
status: public
title: 'RefinedC: Automating the foundational verification of C code with refined
ownership types'
type: conference
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
year: '2021'
...
---
_id: '17506'
abstract:
- lang: eng
text: Sandboxing is a common technique that allows low-level, untrusted components
to safely interact with trusted code. However, previous work has only investigated
the low-level memory isolation guarantees of sandboxing, leaving open the question
of the end-to-end guarantees that sandboxing affords programmers. In this paper,
we fill this gap by showing that sandboxing enables reasoning about the known
concept of robust safety, i.e., safety of the trusted code even in the presence
of arbitrary untrusted code. To do this, we first present an idealized operational
semantics for a language that combines trusted code with untrusted code. Sandboxing
is built into our semantics. Then, we prove that safety properties of the trusted
code (as enforced through a rich type system) are upheld in the presence of arbitrary
untrusted code, so long as all interactions with untrusted code occur at the “any”
type (a type inhabited by all values). Finally, to alleviate the burden of having
to interact with untrusted code at only the “any” type, we formalize and prove
safe several wrappers, which automatically convert values between the “any” type
and much richer types. All our results are mechanized in the Coq proof assistant.
article_processing_charge: No
article_type: original
author:
- first_name: Michael Joachim
full_name: Sammler, Michael Joachim
id: 510d3901-2a03-11ee-914d-d9ae9011f0a7
last_name: Sammler
- first_name: Deepak
full_name: Garg, Deepak
last_name: Garg
- first_name: Derek
full_name: Dreyer, Derek
last_name: Dreyer
- first_name: Tadeusz
full_name: Litak, Tadeusz
last_name: Litak
citation:
ama: Sammler MJ, Garg D, Dreyer D, Litak T. The high-level benefits of low-level
sandboxing. Proceedings of the ACM on Programming Languages. 2019;4(POPL):1-32.
doi:10.1145/3371100
apa: Sammler, M. J., Garg, D., Dreyer, D., & Litak, T. (2019). The high-level
benefits of low-level sandboxing. Proceedings of the ACM on Programming Languages.
Association for Computing Machinery. https://doi.org/10.1145/3371100
chicago: Sammler, Michael Joachim, Deepak Garg, Derek Dreyer, and Tadeusz Litak.
“The High-Level Benefits of Low-Level Sandboxing.” Proceedings of the ACM on
Programming Languages. Association for Computing Machinery, 2019. https://doi.org/10.1145/3371100.
ieee: M. J. Sammler, D. Garg, D. Dreyer, and T. Litak, “The high-level benefits
of low-level sandboxing,” Proceedings of the ACM on Programming Languages,
vol. 4, no. POPL. Association for Computing Machinery, pp. 1–32, 2019.
ista: Sammler MJ, Garg D, Dreyer D, Litak T. 2019. The high-level benefits of low-level
sandboxing. Proceedings of the ACM on Programming Languages. 4(POPL), 1–32.
mla: Sammler, Michael Joachim, et al. “The High-Level Benefits of Low-Level Sandboxing.”
Proceedings of the ACM on Programming Languages, vol. 4, no. POPL, Association
for Computing Machinery, 2019, pp. 1–32, doi:10.1145/3371100.
short: M.J. Sammler, D. Garg, D. Dreyer, T. Litak, Proceedings of the ACM on Programming
Languages 4 (2019) 1–32.
date_created: 2024-09-05T08:36:52Z
date_published: 2019-12-20T00:00:00Z
date_updated: 2024-09-10T09:58:57Z
day: '20'
doi: 10.1145/3371100
extern: '1'
fulldoi: https://doi.org/10.1145/3371100
intvolume: ' 4'
issue: POPL
language:
- iso: eng
main_file_link:
- open_access: '1'
url: https://doi.org/10.1145/3371100
month: '12'
oa: 1
oa_version: Published Version
page: 1-32
publication: Proceedings of the ACM on Programming Languages
publication_identifier:
issn:
- 2475-1421
publication_status: published
publisher: Association for Computing Machinery
quality_controlled: '1'
scopus_import: '1'
status: public
title: The high-level benefits of low-level sandboxing
type: journal_article
user_id: 317138e5-6ab7-11ef-aa6d-ffef3953e345
volume: 4
year: '2019'
...