pith. sign in

arxiv: 2507.11282 · v2 · submitted 2025-07-15 · 💻 cs.PL

The downgrading semantics of memory safety (Extended version)

Ren\'e Rydhof Hansen , Andreas Stenb{\ae}k Larsen , Aslan Askarov This is my paper

Pith reviewed 2026-05-19 04:41 UTC · model grok-4.3

classification 💻 cs.PL
keywords memory safetyallocator independencedowngradingnoninterferenceinformation flowsemanticslow-level languages
0
0 comments X

The pith

Memory safety for allocator-dependent behaviors is defined as gradual allocator independence by treating out-of-memory events and pointer-to-integer casts as controlled downgrades.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

Traditional memory safety definitions list forbidden events such as use-after-free or heap overflow. This paper instead defines the allocator-specific part of safety through gradual allocator independence, a property that programs must satisfy regardless of which concrete allocator is used. The definition starts from a noninterference intuition but refines it to permit two realistic forms of information release: allocators running out of memory and programs performing pointer-to-integer casts. These releases are modeled as downgrading steps inside an information-flow framework, so that standard noninterference machinery can still certify the remaining safety guarantees. If the definition is sound, then many allocator-related bugs become detectable by checking whether a program leaks allocator-specific details beyond the allowed downgrades.

Core claim

In a low-level language with integer pointers and explicit malloc/free in a flat memory model, gradual allocator independence requires that, apart from explicit downgrades for out-of-memory and pointer casts, the observable behavior of a program does not depend on the particular allocator implementation. The definition is obtained by extending noninterference with downgrading policies that receive technical treatment using existing information-flow techniques.

What carries the argument

gradual allocator independence: a noninterference property refined with explicit downgrading for out-of-memory conditions and pointer-to-integer casts

If this is right

  • Allocator-specific memory-safety bugs become expressible as violations of an independence property rather than as ad-hoc negative conditions.
  • Existing information-flow tools can be reused to check memory safety once the downgrading rules for casts and out-of-memory are fixed.
  • Memory safety proofs no longer need to enumerate every forbidden operation; instead they enforce that allocator choices remain invisible except at the allowed downgrade points.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The same downgrading approach could be applied to other hidden resources such as timing or cache state in security-critical code.
  • A compiler could emit runtime checks only for the downgrading points, reducing the cost of memory-safety instrumentation.
  • The definition might generalize to concurrent or distributed allocators by adding further downgrade rules for synchronization events.

Load-bearing premise

Out-of-memory conditions and pointer-to-integer casts can be treated as downgrading that still permits the rest of the safety property to be verified with information-flow methods.

What would settle it

A concrete program and allocator pair where the program satisfies gradual allocator independence yet still exhibits a use-after-free or double-free under that allocator.

Figures

Figures reproduced from arXiv: 2507.11282 by Andreas Stenb{\ae}k Larsen, Aslan Askarov, Ren\'e Rydhof Hansen.

Figure 1
Figure 1. Figure 1: Standard implicit flow, pointer comparison, and NULL comparison [PITH_FULL_IMAGE:figures/full_fig_p003_1.png] view at source ↗
Figure 2
Figure 2. Figure 2: Example program and a corresponding symbolic allocation sequence [PITH_FULL_IMAGE:figures/full_fig_p008_2.png] view at source ↗
Figure 3
Figure 3. Figure 3: Example unsafe allocation decisions about whether an allocation succeeds or fails, must not depend on how the client code uses the allocated memory. The subtlety of the second aspect is also the cause of the technical complexity of this section. We avoid specifically operationalizing aspects of allocator behavior such as where on the heap and how the allocator stores meta-information. Consider the example … view at source ↗
Figure 4
Figure 4. Figure 4: Sequence feasibility (fast-forward ▷▷ notation) and step feasibility (play ▷ notation) Definition 6 (Seqence Feasibility). An allocation sequence 𝜎® is feasible for a given allocation strategy 𝛼, reserved memory 𝑅, heap 𝐻, allocator state 𝐴, and update sequence 𝑢® if, for some 𝐻 ′ , 𝐴′ , Φ ′ , the sequence feasibility relation 𝛼, 𝑅 ⊢ ∅, 𝐻, 𝐴 | ®𝑢, 𝜎® ▷▷ 𝐻 ′ , 𝐴′ , Φ ′ , defined in [PITH_FULL_IMAGE:figures… view at source ↗
Figure 5
Figure 5. Figure 5: Notac syntax Exp-Const 𝐸, 𝐻, 𝛼 ⊢ 𝑛 ⇓ 𝑛 Exp-Var 𝑣 = 𝐻(𝐸(𝑥)) 𝐸, 𝐻, 𝛼 ⊢ 𝑥 ⇓ 𝑣 Exp-Null 𝐸, 𝐻, 𝛼 ⊢ NULL ⇓ 𝛼.null Exp-Addressof 𝐸, 𝐻, 𝛼 ⊢ &𝑥 ⇓ 𝐸(𝑥) Exp-Deref 𝐸, 𝐻, 𝛼 ⊢ 𝑒 ⇓ 𝑎 𝑣 = 𝐻(𝑎) 𝐸, 𝐻, 𝛼 ⊢ ∗𝑒 ⇓ 𝑣 Exp-Binop 𝐸, 𝐻, 𝛼 ⊢ 𝑒𝑖 ⇓ 𝑛𝑖 , 𝑖 = 1, 2 𝐸, 𝐻, 𝛼 ⊢ 𝑒1 bop 𝑒2 ⇓ 𝑛1 bop 𝑛2 Lval-Var 𝐸(𝑥) = 𝑎 𝐸, 𝐻, 𝛼 ⊢ 𝑥 ↓ 𝑎 Lval-Deref 𝐸, 𝐻, 𝛼 ⊢ 𝑒 ⇓ 𝑎 𝐸, 𝐻, 𝛼 ⊢ ∗(𝑒) ↓ 𝑎 [PITH_FULL_IMAGE:figures/full_fig_p014_5.png] view at source ↗
Figure 6
Figure 6. Figure 6: Notac semantics of expressions and lvals [PITH_FULL_IMAGE:figures/full_fig_p014_6.png] view at source ↗
Figure 7
Figure 7. Figure 7: Notac semantics of commands, selected rules [PITH_FULL_IMAGE:figures/full_fig_p015_7.png] view at source ↗
Figure 8
Figure 8. Figure 8: Symbolic filter m(8) f⟨0⟩ malloc(8, 0x1000) free (0x1000) (a) No residue m(8) f⟨0⟩ malloc(8, 0x1000) free (0x1001) (b) The free event is in the residue [PITH_FULL_IMAGE:figures/full_fig_p017_8.png] view at source ↗
Figure 9
Figure 9. Figure 9: Example of symbolic filtering for two traces with the filter [PITH_FULL_IMAGE:figures/full_fig_p017_9.png] view at source ↗
Figure 10
Figure 10. Figure 10: Trace similarity example The symbolic allocation sequence 𝜎®, if it exists, connects the two traces when they originate from different allocators [PITH_FULL_IMAGE:figures/full_fig_p018_10.png] view at source ↗
Figure 11
Figure 11. Figure 11: Null pointer dereference examples 1 /* UNSAFE - use after 2 free */ 3 p = malloc (42); 4 if( p == NULL ) error (); 5 free ( p ); 6 * p = 87; // use after 7 // free 8 observe (* p ); (a) Use after free 1 /* ( P1a) UNSAFE - buffer overflow */ 2 p = malloc (4); 3 q = malloc (4); 4 if( p == NULL || q == NULL ) error (); 5 * q = 42; 6 i = 0; 7 while ( i < 6) { 8 *( p + i ) = i ; // buffer overflow 9 i = i + 1;… view at source ↗
Figure 12
Figure 12. Figure 12: Use after free and buffer overflow the event traces generated by two allocators: one that uses zero (0) as the null address and one that uses a different address. Memory allocation failure would yield two non-similar traces, one that includes the result of the observe instruction and one that does not. In the final variation of the program, in Figure 11c, the error check is performed correctly, using the … view at source ↗
Figure 13
Figure 13. Figure 13: Double free and pointer comparison examples [PITH_FULL_IMAGE:figures/full_fig_p021_13.png] view at source ↗
Figure 14
Figure 14. Figure 14: Technical examples [PITH_FULL_IMAGE:figures/full_fig_p022_14.png] view at source ↗
Figure 15
Figure 15. Figure 15: Memsafe expressions to Notac translation. [PITH_FULL_IMAGE:figures/full_fig_p023_15.png] view at source ↗
Figure 16
Figure 16. Figure 16: Memsafe commands to Notac translation. guarded; the translation ensures that the actual loop guard is not evaluated (as it may deviate) when $oom is true, using a fresh (for each syntactically occurring while-statement) variable $$g. For the translation theorem, note that in Memsafe a local store is a finite map from variables to values, a heap is a finite map from pointers to values, and a state is then … view at source ↗
Figure 17
Figure 17. Figure 17: Notac semantics of commands, extended rules [PITH_FULL_IMAGE:figures/full_fig_p029_17.png] view at source ↗
Figure 18
Figure 18. Figure 18: Memsafe syntax and program states The appendix contains extended semantic rules, a more detailed review of the curious allocator, of the translation from Memsafe to Notac, and the translation theorem. A Extended semantic rules [PITH_FULL_IMAGE:figures/full_fig_p029_18.png] view at source ↗
Figure 19
Figure 19. Figure 19: Memsafe expression evaluation bind(𝑓 , ⊥) ≜ ⊥ bind(𝑓 , error) ≜ error bind(𝑓 , (𝐼,𝑙,𝑚)) ≜    (𝐼 ∪ 𝐼 ′ ,𝑙′ ,𝑚′ ), if 𝑓 (𝑙,𝑚) = (𝐼 ′ ,𝑙′ ,𝑚′ ) error, if 𝑓 (𝑙,𝑚) = error ⊥, otherwise if(𝑏, 𝑥, 𝑦) ≜    𝑥, if 𝑏 ≠ 0 and 𝑏 ∈ Z 𝑦, if 𝑏 = 0 and 𝑏 ∈ Z error, otherwise [PITH_FULL_IMAGE:figures/full_fig_p030_19.png] view at source ↗
Figure 20
Figure 20. Figure 20: Memsafe auxiliary operators allocator strategy 𝛼, are compatible, written (𝑙,𝑚)⇀𝜃 (𝐸, 𝐻, 𝛼), when the following properties are satisfied: • dom(𝑙) ⊆ dom(𝐸) • dom(𝑚) ⊆ dom(𝜃) • ∀(𝑖, 𝑏, 𝑛) ∈ dom(𝑚), 𝑗 ∈ Z. (𝑖, 𝑏, 𝑛 + 𝑗) ∈ dom(𝑚) ⇒ 𝜃 (𝑖, 𝑏, 𝑛 + 𝑗) = 𝜃 (𝑖, 𝑏, 𝑛) + 𝑗 • ∀𝑥 ∈ dom(𝑙). 𝑙(𝑥) = 𝑛 ⇔ 𝐻(𝐸(𝑥)) = 𝑛 • ∀𝑥 ∈ dom(𝑙). 𝑙(𝑥) = nil ⇔ 𝐻(𝐸(𝑥)) = 𝛼.null • ∀𝑥 ∈ dom(𝑙). 𝑙(𝑥) = (𝑖, 𝑏, 𝑛) ⇔ 𝐻(𝐸(𝑥)) = 𝜃 (𝑖, 𝑏, 𝑛) • ∀(𝑖,… view at source ↗
Figure 21
Figure 21. Figure 21: Memsafe command evaluation Lemma B.1 (Semantic correctness of expression translation). Let 𝑒 be an expression and (𝑙,𝑚) a state in Memsafe. Then for map 𝜃, Notac environment 𝐸, heap 𝐻, and allocator strategy 𝛼, where (𝑙,𝑚)⇀𝜃 (𝐸, 𝐻, 𝛼), the following holds: • If J𝑒K(𝑙,𝑚) = 𝑛 then 𝐸, 𝐻, 𝛼 ⊢ L𝑒M ⇓ 𝑛 • If J𝑒K(𝑙,𝑚) = nil then 𝐸, 𝐻, 𝛼 ⊢ L𝑒M ⇓ 𝛼.null • If J𝑒K(𝑙,𝑚) = (𝑖, 𝑏, 𝑛) then 𝐸, 𝐻, 𝛼 ⊢ L𝑒M ⇓ 𝜃 (𝑖, 𝑏, 0) + 𝑛… view at source ↗
Figure 22
Figure 22. Figure 22: new function of XOR linked list Push. Assuming some element stored in variable elem and pointer to an XOR linked list ptr, [PITH_FULL_IMAGE:figures/full_fig_p053_22.png] view at source ↗
Figure 23
Figure 23. Figure 23: pushFront function of XOR linked list Pop [PITH_FULL_IMAGE:figures/full_fig_p054_23.png] view at source ↗
Figure 24
Figure 24. Figure 24: popFront function of XOR linked list Get [PITH_FULL_IMAGE:figures/full_fig_p054_24.png] view at source ↗
Figure 25
Figure 25. Figure 25: get function of XOR linked list Delete [PITH_FULL_IMAGE:figures/full_fig_p055_25.png] view at source ↗
Figure 26
Figure 26. Figure 26: delete function of XOR linked list , Vol. 1, No. 1, Article . Publication date: August 2025 [PITH_FULL_IMAGE:figures/full_fig_p055_26.png] view at source ↗
Figure 27
Figure 27. Figure 27: insert function of XOR linked list , Vol. 1, No. 1, Article . Publication date: August 2025 [PITH_FULL_IMAGE:figures/full_fig_p056_27.png] view at source ↗
read the original abstract

Memory safety is traditionally characterized in terms of bad things that cannot happen. This approach is currently embraced in the literature on formal methods for memory safety. However, a general semantic principle for memory safety, that implies the negative items, remains elusive. This paper focuses on the allocator-specific aspects of memory safety, such as null-pointer dereference, use after free, double free, and heap overflow. To that extent, we propose a notion of gradual allocator independence that accurately captures the allocator-dependent aspects of memory safety. Our approach is inspired by the previously suggested connection between memory safety and noninterference, but extends that connection in a fundamentally important direction towards downgrading. We consider a low-level language with access to an allocator that provides malloc and free primitives in a flat memory model. Pointers are just integers, and as such it is trivial to write memory-unsafe programs. The basic intuition of gradual allocator independence is that of noninterference, namely that allocators must not influence program execution. This intuition is refined in two important ways that account for the allocators running out-of-memory and for programs to have pointer-to-integer casts. The key insight of the definition is to treat these extensions as forms of downgrading and give them satisfactory technical treatment using the state-of-the-art information flow machinery.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

2 major / 3 minor

Summary. The paper proposes a notion of gradual allocator independence as a semantic characterization of the allocator-dependent aspects of memory safety (null dereference, use-after-free, double free, heap overflow) in a low-level language with malloc/free over a flat integer-pointer memory model. It extends the noninterference connection by treating out-of-memory conditions and pointer-to-integer casts as downgrading events and applies state-of-the-art information-flow machinery to obtain a positive principle that implies the usual negative safety properties.

Significance. If the formal development is sound, the work supplies a general semantic principle for memory safety that unifies several negative properties under a single noninterference-style definition with controlled downgrading. The explicit treatment of allocator OOM and pointer casts as downgrading is a natural and technically interesting extension of prior information-flow accounts of memory safety; the extended version appears to contain the required definitions, lemmas, and proofs.

major comments (2)
  1. [§4] §4, Definition 4.3 (gradual allocator independence): the security lattice and the precise placement of the OOM downgrading label are not stated explicitly; without this it is difficult to verify that the noninterference statement remains non-trivial once allocation failure is observable.
  2. [Theorem 5.2] Theorem 5.2 (implication to absence of use-after-free): the proof sketch relies on the claim that all pointer-to-integer casts are the only downgrading points, yet the language includes pointer arithmetic; it is unclear whether arithmetic on cast pointers is conservatively treated or requires an additional rule.
minor comments (3)
  1. [Abstract] The abstract refers to 'state-of-the-art information flow machinery' without a citation; add references to the specific downgrading frameworks used (e.g., the cited works on noninterference with declassification).
  2. [§2] Figure 2 (language syntax) uses an unusual notation for the cast operator; a short remark relating it to standard C-like casts would improve readability for readers outside the immediate subfield.
  3. [§3.4] The running example in §3.4 is helpful but the heap layout after the second malloc is shown only informally; a small diagram or explicit address table would make the allocator-dependence clearer.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the positive assessment, the recommendation of minor revision, and the constructive comments that help strengthen the clarity of the formal development. We respond to each major comment below.

read point-by-point responses

  1. Referee: [§4] §4, Definition 4.3 (gradual allocator independence): the security lattice and the precise placement of the OOM downgrading label are not stated explicitly; without this it is difficult to verify that the noninterference statement remains non-trivial once allocation failure is observable.

    Authors: We agree that an explicit statement of the security lattice and the placement of the OOM downgrading label would aid verification. The lattice is the standard two-element lattice with Low (public/observable) and High (secret) levels; OOM is a downgrading event that moves information from High to Low. In the revised manuscript we will augment Definition 4.3 with a short paragraph and a diagram that make the lattice and label placement explicit, confirming that the resulting noninterference statement remains non-trivial. revision: yes

  2. Referee: [Theorem 5.2] Theorem 5.2 (implication to absence of use-after-free): the proof sketch relies on the claim that all pointer-to-integer casts are the only downgrading points, yet the language includes pointer arithmetic; it is unclear whether arithmetic on cast pointers is conservatively treated or requires an additional rule.

    Authors: We thank the referee for this observation. In the language semantics, pointer-to-integer casts constitute the sole downgrading points; any subsequent pointer arithmetic is performed on the resulting integer values inside the already-downgraded (Low) context and is therefore conservatively covered by the existing noninterference relation. No additional rule is required. We will expand the proof sketch of Theorem 5.2 in the revision to state this treatment explicitly. revision: yes

Circularity Check

0 steps flagged

No significant circularity; new notion extends prior noninterference machinery independently

full rationale

The paper defines gradual allocator independence directly as an extension of noninterference that treats OOM conditions and pointer-to-integer casts as downgrading, using standard information-flow techniques. No step reduces a claimed prediction or result to a fitted parameter, self-definition, or load-bearing self-citation chain. The central definition is introduced as a fresh semantic principle rather than derived from prior results by the same authors in a way that collapses the argument. The derivation remains self-contained against external benchmarks of noninterference and downgrading.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 0 invented entities

The central claim rests on a flat memory model with integer pointers and on the adequacy of treating OOM and casts as downgrading within existing information-flow frameworks.

axioms (1)
  • domain assumption The language provides malloc and free in a flat memory model where pointers are integers.
    Explicitly stated as the setting in which memory-unsafe programs are trivial to write.

pith-pipeline@v0.9.0 · 5772 in / 1178 out tokens · 58342 ms · 2026-05-19T04:41:39.434432+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

What do these tags mean?
matches
The paper's claim is directly supported by a theorem in the formal canon.
supports
The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends
The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses
The paper appears to rely on the theorem as machinery.
contradicts
The paper's claim conflicts with a theorem or certificate in the canon.
unclear
Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

83 extracted references · 83 canonical work pages

  1. [1]

    Dynamic policies revisited

    A. M. Ahmadian and M. Balliu. “Dynamic policies revisited”. In: 2022 IEEE 7th European Symposium on Security and Privacy (EuroS&P) . IEEE. 2022, pp. 448–466

    work page 2022

  2. [2]

    Verified sequential malloc/free

    A. W. Appel and D. A. Naumann. “Verified sequential malloc/free”. In:Proceedings of the 2020 ACM SIGPLAN international symposium on memory management . 2020, pp. 48–59

    work page 2020

  3. [3]

    Termination-insensitive noninterference leaks more than just a bit

    A. Askarov, S. Hunt, A. Sabelfeld, and D. Sands. “Termination-insensitive noninterference leaks more than just a bit”. In: Computer Security-ESORICS 2008: 13th European Symposium on Research in Computer Security, Málaga, Spain, October 6-8, 2008. Proceedings 13 . Springer. 2008, pp. 333–348

    work page 2008

  4. [4]

    Attacker Control and Impact for Confidentiality and Integrity

    A. Askarov and A. C. Myers. “Attacker Control and Impact for Confidentiality and Integrity”. In: Logical Methods in Computer Science 7.3 (2011). doi: 10.2168/LMCS-7(3:17)2011. url: https://lmcs.episciences.org/987

    work page doi:10.2168/lmcs-7(3:17)2011 2011

  5. [5]

    Gradual release: Unifying declassification, encryption and key release policies

    A. Askarov and A. Sabelfeld. “Gradual release: Unifying declassification, encryption and key release policies”. In: 2007 IEEE Symposium on Security and Privacy (SP’07) . IEEE. 2007, pp. 207–221

    work page 2007

  6. [6]

    Tight enforcement of information-release policies for dynamic languages

    A. Askarov and A. Sabelfeld. “Tight enforcement of information-release policies for dynamic languages”. In:2009 22nd IEEE Computer Security Foundations Symposium . IEEE. 2009, pp. 43– 59

    work page 2009

  7. [7]

    The meaning of memory safety

    A. Azevedo de Amorim, C. Hriţcu, and B. C. Pierce. “The meaning of memory safety”. In: Principles of Security and Trust: 7th International Conference, POST 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14-20, 2018, Proceedings 7 . Springer. 2018, pp. 79–105

    work page 2018

  8. [8]

    Expressive declassification policies and modular static enforcement

    A. Banerjee, D. A. Naumann, and S. Rosenberg. “Expressive declassification policies and modular static enforcement”. In:2008 IEEE Symposium on Security and Privacy (sp 2008) . IEEE. 2008, pp. 339–353

    work page 2008

  9. [9]

    Secure information flow by self-composition

    G. Barthe, P. R. D’argenio, and T. Rezk. “Secure information flow by self-composition”. In: Mathematical Structures in Computer Science 21.6 (2011), pp. 1207–1252

    work page 2011

  10. [10]

    Prudent design principles for information flow control

    I. Bastys, F. Piessens, and A. Sabelfeld. “Prudent design principles for information flow control”. In: Proceedings of the 13th Workshop on Programming Languages and Analysis for Security. 2018, pp. 17–23

    work page 2018

  11. [11]

    Reconciling progress-insensitive noninterference and declassifi- cation

    J. Bay and A. Askarov. “Reconciling progress-insensitive noninterference and declassifi- cation”. In: 2020 IEEE 33rd Computer Security Foundations Symposium (CSF) . IEEE. 2020, pp. 95–106

    work page 2020

  12. [12]

    A two-phase infinite/finite low- level memory model: Reconciling integer–pointer casts, finite space, and undef at the LLVM IR level of abstraction

    C. Beck, I. Yoon, H. Chen, Y. Zakowski, and S. Zdancewic. “A two-phase infinite/finite low- level memory model: Reconciling integer–pointer casts, finite space, and undef at the LLVM IR level of abstraction”. In: Proceedings of the ACM on Programming Languages 8.ICFP (2024), pp. 789–817

    work page 2024

  13. [13]

    DieHard: probabilistic memory safety for unsafe languages

    E. D. Berger and B. G. Zorn. “DieHard: probabilistic memory safety for unsafe languages”. In: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2006). 2006, pp. 158–168. doi: 10.1145/1133981.1134000

    work page doi:10.1145/1133981.1134000 2006

  14. [14]

    Omnisemantics: Smooth handling of nondeterminism

    A. Charguéraud, A. Chlipala, A. Erbsen, and S. Gruetter. “Omnisemantics: Smooth handling of nondeterminism”. In: ACM Transactions on Programming Languages and Systems 45.1 (2023), pp. 1–43

    work page 2023

  15. [15]

    Hyperproperties

    M. R. Clarkson and F. B. Schneider. “Hyperproperties”. In:Journal of Computer Security 18.6 (2010), pp. 1157–1210

    work page 2010

  16. [16]

    Noninterference through Secure Multi-execution

    D. Devriese and F. Piessens. “Noninterference through Secure Multi-execution”. In:2010 IEEE Symposium on Security and Privacy . 2010, pp. 109–124. doi: 10.1109/SP.2010.15. , Vol. 1, No. 1, Article . Publication date: August 2025. The downgrading semantics of memory safety 27

    work page doi:10.1109/sp.2010.15 2010

  17. [17]

    Checked C: Making C Safe by Extension

    A. S. Elliott, A. Ruef, M. Hicks, and D. Tarditi. “Checked C: Making C Safe by Extension”. In: Proceedings of IEEE Cybersecurity Development (SecDev 2018) . 2018, pp. 53–60. doi: 10.1109/ SecDev.2018.00015. url: https://www.microsoft.com/en-us/research/uploads/prod/2018/09/ checkedc-secdev2018-preprint.pdf

    work page arXiv 2018

  18. [18]

    Integration verification across software and hardware for a simple embedded system

    A. Erbsen, S. Gruetter, J. Choi, C. Wood, and A. Chlipala. “Integration verification across software and hardware for a simple embedded system”. In: Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation . 2021, pp. 604–619

    work page 2021

  19. [19]

    Security policies and security models

    J. A. Goguen and J. Meseguer. “Security policies and security models”. In:1982 IEEE Sympo- sium on Security and Privacy . IEEE. 1982, pp. 11–11

    work page 1982

  20. [20]

    A perspective on information-flow control

    D. Hedin and A. Sabelfeld. “A perspective on information-flow control”. In:Software safety and security. IOS Press, 2012, pp. 319–347

    work page 2012

  21. [21]

    M. Hicks. What is memory safety? Blog post. Last accessed on 30NOV2023. url: http : //www.pl-enthusiast.net/2014/07/21/memory-safety/

    work page 2014

  22. [22]

    Iris from the ground up: A modular foundation for higher-order concurrent separation logic

    R. Jung, R. Krebbers, J. -H. Jourdan, A. Bizjak, L. Birkedal, and D. Dreyer. “Iris from the ground up: A modular foundation for higher-order concurrent separation logic”. In: Journal of Functional Programming 28 (2018), e20

    work page 2018

  23. [23]

    A formal C memory model supporting integer-pointer casts

    J. Kang, C. Hur, W. Mansky, D. Garbuzov, S. Zdancewic, and V. Vafeiadis. “A formal C memory model supporting integer-pointer casts”. In:Proceedings of the 36th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI 2015) . 2015, pp. 326–335. doi: 10.1145/2737924.2738005

    work page doi:10.1145/2737924.2738005 2015

  24. [24]

    Some were meant for C: the endurance of an unmanageable language

    S. Kell. “Some were meant for C: the endurance of an unmanageable language”. In:Proceedings of the 2017 ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software (Onward! 2017) . 2017, pp. 229–245. doi: 10.1145/ 3133850.3133867

    work page arXiv 2017

  25. [25]

    A Formal C Memory Model for Separation Logic

    R. Krebbers. “A Formal C Memory Model for Separation Logic”. In:J. Autom. Reason. 57.4 (2016), pp. 319–387. doi: 10.1007/S10817-016-9369-1. url: https://link.springer.com/article/ 10.1007/S10817-016-9369-1

    work page doi:10.1007/s10817-016-9369-1 2016

  26. [26]

    The CompCert memory model

    X. Leroy, S. Blazy, A. W. Appel, and G. Stewart. “The CompCert memory model”. In:Program Logics for Certified Compilers . Cambridge University Press, 2014, pp. 237–271

    work page 2014

  27. [27]

    Exploring C semantics and pointer provenance

    K. Memarian, V. B. Gomes, B. Davis, S. Kell, A. Richardson, R. N. Watson, and P. Sewell. “Exploring C semantics and pointer provenance”. In:Proceedings of the ACM on Programming Languages 3.POPL (2019), pp. 1–32

    work page 2019

  28. [28]

    Into the depths of C: elaborating the de facto standards

    K. Memarian, J. Matthiesen, J. Lingard, K. Nienhuis, D. Chisnall, R. N. Watson, and P. Sewell. “Into the depths of C: elaborating the de facto standards”. In: ACM SIGPLAN Notices 51.6 (2016), pp. 1–15

    work page 2016

  29. [29]

    Mswasm: Soundly enforcing memory-safe execution of unsafe code

    A. E. Michael, A. Gollamudi, J. Bosamiya, E. Johnson, A. Denlinger, C. Disselkoen, C. Watt, B. Parno, M. Patrignani, M. Vassena, et al. “Mswasm: Soundly enforcing memory-safe execution of unsafe code”. In: Proceedings of the ACM on Programming Languages 7.POPL (2023), pp. 425–454

    work page 2023

  30. [30]

    DieHarder: Securing the Heap

    G. Novark and E. D. Berger. “DieHarder: Securing the Heap”. In: Proceedings of the 5th USENIX Workshop on Offensive Technologies (WOOT 2011) . 2011, pp. 103–117. url: http: //static.usenix.org/event/woot11/tech/final%5C_files/Novark.pdf

    work page 2011

  31. [31]

    Information-flow security for interactive programs

    K. R. O’Neill, M. R. Clarkson, and S. Chong. “Information-flow security for interactive programs”. In: 19th IEEE Computer Security Foundations Workshop (CSFW’06). IEEE. 2006, 12–pp. , Vol. 1, No. 1, Article . Publication date: August 2025. 28 René Rydhof Hansen, Andreas Stenbæk Larsen, and Aslan Askarov

    work page 2006

  32. [32]

    StarMalloc: Verifying a Modern, Hardened Mem- ory Allocator

    A. Reitz, A. Fromherz, and J. Protzenko. “StarMalloc: Verifying a Modern, Hardened Mem- ory Allocator”. In: Proceedings of the ACM on Programming Languages 8.OOPSLA2 (2024), pp. 1757–1786

    work page 2024

  33. [33]

    GlobalAlloc Trait - Rust

    Rust Project Developers. GlobalAlloc Trait - Rust . https://doc.rust-lang.org/stable/std/alloc/ trait.GlobalAlloc.html. Accessed: 2025-05-30. 2025

    work page 2025

  34. [34]

    Language-based information-flow security

    A. Sabelfeld and A. C. Myers. “Language-based information-flow security”. In:IEEE Journal on selected areas in communications 21.1 (2003), pp. 5–19

    work page 2003

  35. [35]

    Dimensions and principles of declassification

    A. Sabelfeld and D. Sands. “Dimensions and principles of declassification”. In: 18th IEEE Computer Security Foundations Workshop (CSFW’05). IEEE. 2005, pp. 255–269

    work page 2005

  36. [36]

    Schoepe, M

    D. Schoepe, M. Balliu, B. C. Pierce, and A. Sabelfeld. Explicit Secrecy: A Policy for Taint Tracking. English. 2016 IEEE European Symposium on Security and Privacy (EuroS&P). IEEE,

    work page 2016

  37. [37]

    doi: 10.1109/eurosp.2016.14

    isbn: 978-1-5090-1751-5. doi: 10.1109/eurosp.2016.14

    work page doi:10.1109/eurosp.2016.14 2016

  38. [38]

    In: Computer Vision – ECCV 2018

    J. Spolsky. “The Law of Leaky Abstractions”. In: Joel on Software: And on Diverse and Oc- casionally Related Matters That Will Prove of Interest to Software Developers, Designers, and Managers, and to Those Who, Whether by Good Fortune or Ill Luck, Work with Them in Some Capacity. Berkeley, CA: Apress, 2004, pp. 197–202. isbn: 978-1-4302-0753-5. doi: 10.1...

    work page doi:10.1007/978- 2004

  39. [39]

    Torvalds

    L. Torvalds. Re: [RFC] [PATCH] cpuset operations causes Badness at mm/slab.c:777 warning . Linux Kernel Mailing List (LKML). Message ID and full thread available via LKML archive. June 2007. url: https://lkml.org/lkml/2007/6/1/440

    work page 2007

  40. [40]

    Types, bytes, and separation logic

    H. Tuch, G. Klein, and M. Norrish. “Types, bytes, and separation logic”. In:Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, (POPL 2007). 2007, pp. 97–108. doi: 10.1145/1190216.1190234. , Vol. 1, No. 1, Article . Publication date: August 2025. The downgrading semantics of memory safety 29 C-Skip 𝐸, 𝛼 ⊢ ⟨skip; 𝐻,...

    work page doi:10.1145/1190216.1190234 2007

  41. [41]

    ( ▷-malloc-ok): For a successful allocation of 𝑘 addresses, we have 𝐻1 = 𝐻 ′′ 1 [𝑎

    = JΦ′ 1K ∪ 𝑅 and Ø (𝑎,𝑠) ∈𝐴′ 1 [𝑎, 𝑎 + 𝑠) = JΦ′ 1K Since client updates cannot change the domain of the heap, the induction hypothesis gives us that dom(𝐻 ′′ 1 ) = JΦ′ 1K ∪ 𝑅 The proof now follows by case analysis in the ▷ relation on 𝛼eager ⊢ Φ′ 1, 𝐻′′ 1 , 𝐴′ 1 | ®𝜎pre · 𝜎 ▷ 𝐻1, 𝐴1, Φ1 ⟨2⟩1. ( ▷-malloc-ok): For a successful allocation of 𝑘 addresses, we ...

    work page 2025

  42. [42]

    Since (𝑎, 𝑘) is not in 𝐴′ 1 our induction hypothesis tells us that [𝑎, 𝑎 + 𝑘) ∩ JΦ′ 1K = ∅, which would mean Φ′ 1 ∩ {( 𝑎, 𝑘; 𝑖)} = ∅

    In this case we get 𝐴1 = 𝐴′ 1 and 𝐻1 = 𝐻 ′′ 1 . Since (𝑎, 𝑘) is not in 𝐴′ 1 our induction hypothesis tells us that [𝑎, 𝑎 + 𝑘) ∩ JΦ′ 1K = ∅, which would mean Φ′ 1 ∩ {( 𝑎, 𝑘; 𝑖)} = ∅. But in that case we also have Φ1 = Φ′ 1 \ {( 𝑎, 𝑘; 𝑖)} = Φ′ 1 Therefore, showingdom(𝐻1) = JΦ1K∪𝑅 is equivalent to showingdom(𝐻 ′

    work page

  43. [43]

    But this is exactly what our induction hypothesis states

    = JΦ′ 1K∪𝑅. But this is exactly what our induction hypothesis states. Similarly, showingÐ (𝑎′,𝑠) ∈𝐴1 [𝑎′, 𝑎′ +𝑠) = JΦ1K is equivalent to showing Ð (𝑎′,𝑠) ∈𝐴′ 1 [𝑎′, 𝑎′ + 𝑠) = JΦ′ 1K, which we also know from our induction hypothesis. Now let us instead consider the case where (𝑎, 𝑠) ∈ 𝐴′

    work page

  44. [44]

    In this case we instead have: dom(𝐻1) = dom(𝐻 ′

    work page

  45. [45]

    \ [ 𝑎, 𝑎 + 𝑠) and 𝐴1 = 𝐴′ 1 \ {( 𝑎, 𝑠)} and JΦ1K = JΦ′ 1K \ [𝑎, 𝑎 + 𝑠) The first part of the statement then follows from: dom(𝐻1) = dom(𝐻 ′

    work page

  46. [46]

    □ Theorem C.2 (Eager allocator strategy 𝛼eager is well-formed)

    \ [ 𝑎, 𝑎 + 𝑠) = JΦ′ 1K ∪ 𝑅 \ [𝑎, 𝑎 + 𝑠) induction hypothesis = JΦ′ 1K \ [𝑎, 𝑎 + 𝑠) ∪ 𝑅 since 𝑅 ∩ [𝑎, 𝑎 + 𝑠) = ∅ = JΦ1K ∪ 𝑅 JΦ1K = JΦ′ 1K \ [𝑎, 𝑎 + 𝑠) The second part of the statement follows from: Ø (𝑎′,𝑠′ ) ∈𝐴1 [𝑎′, 𝑎′ + 𝑠 ′) = ©­ « Ø (𝑎′,𝑠′ ) ∈𝐴′ 1 [𝑎′, 𝑎′ + 𝑠 ′)ª® ¬ \ [𝑎, 𝑎 + 𝑠) 𝐴1 = 𝐴′ 1 \ {( 𝑎, 𝑠)} = JΦ′ 1K \ [𝑎, 𝑎 + 𝑠) induction hypothesis = JΦ1K J ...

    work page 2025

  47. [47]

    This allows us to deduce the following: ∅ = dom(𝐻 ′

    work page

  48. [48]

    ∩ [ 𝑎, 𝑎 + 𝑘) = JΦ′ 1K ∪ 𝑅 ∩ [𝑎, 𝑎 + 𝑘) by Lemma C.1 = JΦ′ 1K ∩ [𝑎, 𝑎 + 𝑘) ∪ (𝑅 ∩ [𝑎, 𝑎 + 𝑘)) = JΦ′ 1K ∩ [𝑎, 𝑎 + 𝑘) since 𝑅 ∩ [𝑎, 𝑎 + 𝑘) = ∅ This is exactly what we needed to show, concluding the case. ⟨1⟩2. client-accessible memory is in the final heaps: Follows directly from Lemma C.1. ⟨1⟩3. allocator initialization does not update reserved memory: We k...

    work page 2025

  49. [49]

    But in that case Lemma C.1 tells us that this 𝑎 is also not present in Φ′

    For the ▷-malloc-ok case we start by noting that whichever 𝑎 is allocated cannot be in 𝐴′ 1, by the definition 𝛼eager .malloc(). But in that case Lemma C.1 tells us that this 𝑎 is also not present in Φ′

    work page

  50. [50]

    bump pointer

    This gives us, together with the induction hypothesis, that no address therefore appears twice in Φ1, which concludes the proof. ⟨1⟩8. zero-sized allocations are disjoint from the client-updateable memory: Induction in the ▷ ▷relation. Base case is trivial since here Φ1 = ∅. The inductive case is then by case analysis on the resulting ▷ relation. Failed m...

    work page 2025

  51. [51]

    𝑅 is a contiguous memory interval [𝑁1, 𝑁2)

    work page

  52. [52]

    (𝐻0, 𝐴0) = 𝛼bump.init(𝐻 )

    work page

  53. [53]

    𝛼bump, 𝑅 ⊢ ∅, 𝐻0, 𝐴0 | ®𝑢1, ®𝜎 ▷ ▷𝐻1, 𝐴1, Φ1 The proof now follows by proving each well-formedness property for 𝛼bump. ⟨1⟩1. allocated regions are disjoint: By induction in the ▷ ▷relation on 𝛼bump, 𝑅 ⊢ ∅, 𝐻0, 𝐴0 | ®𝑢1, ®𝜎 ▷ ▷𝐻1, 𝐴1, Φ1. ⟨2⟩1. ▷ ▷-empty (𝛼bump, 𝑅 ⊢ ∅, 𝐻0, 𝐴0 | ®𝑢1, 𝜖 ▷ ▷𝐻0, 𝐴0, ∅): Trivial since Φ1 = ∅. ⟨2⟩2. ▷ ▷-step (𝛼bump, 𝑅 ⊢ ∅, 𝐻0, 𝐴...

    work page

  54. [54]

    𝑖 ≠ 𝑖′ =⇒ [ 𝑎, 𝑎 + 𝑘) ∩ [ 𝑎′, 𝑎′ + 𝑘 ′) = ∅ meaning we just need to show that ∀(𝑎, 𝑘; 𝑖) ∈ Φ′

    work page

  55. [55]

    [𝑎, 𝑎 + 𝑘) ∩ [ 𝐴′ 1, 𝐴′ 1 + 𝑠) = ∅ , Vol. 1, No. 1, Article . Publication date: August 2025. 42 René Rydhof Hansen, Andreas Stenbæk Larsen, and Aslan Askarov By Lemma C.3 we know 𝐴′ 1 is strictly greater than any address in JΦ′ 1K. But in that means JΦ′ 1K ∩ [𝐴′ 1, 𝐴′ 1 + 𝑠) = ∅, which in turn means [𝐴′ 1, 𝐴′ 1 + 𝑠) is disjoint from any other allocated me...

    work page 2025

  56. [56]

    (𝐻0, 𝐴0) = 𝛼curio.init(𝐻 )

    work page

  57. [57]

    ®𝑢1 is a client update sequence

    work page

  58. [58]

    there exists 𝐻1, 𝐴1, Φ1 such that 𝛼curio, ∅ ⊢ ∅, 𝐻0, 𝐴0 | ®𝑢1, ®𝜎 ▷ ▷𝐻1, 𝐴1, Φ1 Prove: Basic-1 ∀(𝑎, 𝑘; 𝑖), (𝑎′, 𝑘′; 𝑖′) ∈ Φ1 : 𝑖 ≠ 𝑖′ =⇒ [ 𝑎, 𝑎 + 𝑘) ∩ [ 𝑎′, 𝑎′ + 𝑘 ′) = ∅ Basic-2 JΦ1K ∪ 𝑅 ⊆ dom(𝐻1) Basic-3 𝐻 =𝑅 𝐻0 Basic-4 if ®𝜎 = ®𝜎pre · 𝜎 then for any 𝐻 ′, 𝐴′, Φ′, such that 𝛼curio, 𝑅 ⊢ ∅, 𝐻0, 𝐴0 | ®𝑢, ®𝜎pre ▷ ▷ 𝐻 ′, 𝐴′, Φ′ and 𝛼curio ⊢ Φ′, 𝐻′, 𝐴′ | ®𝜎pre...

    work page

  59. [59]

    ®𝑢1 = ®𝑢′ 1 ·𝑢1 , Vol. 1, No. 1, Article . Publication date: August 2025. 46 René Rydhof Hansen, Andreas Stenbæk Larsen, and Aslan Askarov ⟨1⟩8. 1. 𝛼curio, ∅ ⊢ ∅, 𝐻0, 𝐴0 | ®𝑢′ 1, ®𝜎 ′ ▷ ▷𝐻 ′ 0, 𝐴′ 0, Φ′ 0

    work page 2025

  60. [60]

    𝐻 ′′ 0 = 𝑢1(𝐻 ′ 0, JΦ′ 0K)

    work page

  61. [61]

    𝛼curio ⊢ Φ′ 0, 𝐻′′ 0 , 𝐴′ 0 | ®𝜎 ·𝜎 ▷ 𝐻1, 𝐴1, Φ1 Proof: Follows from assumptions and ▷ ▷-step. ⟨1⟩9. Case: | ®𝜎 | = 1 (base case) ⟨2⟩1. ®𝜎 ′ = 𝜖 Proof: Trivial. ⟨2⟩2. 𝐻 ′ 0 = 𝐻0, 𝐴′ 0 = 𝐴0, and Φ′ 0 = ∅ Proof: Follows from ⟨1⟩8 and ▷ ▷-empty since ®𝜎 ′ = 𝜖. ⟨2⟩3. 𝐻 ′′ 0 = 𝐻0 Proof: 𝐻 ′′ 0 = 𝑢1(𝐻 ′ 0, JΦ′ 0K) = 𝑢1(𝐻0, J∅K) (from ⟨2⟩2) = 𝑢1(𝐻0, ∅) (def. J·K...

    work page

  62. [62]

    Φ1 = ∅ Proof: Follows from ▷-malloc-fail and ⟨2⟩4. ⟨3⟩2. 𝐻1 = 𝐻0 and 𝐴1 = 𝐴0 Proof: Follows from definition of 𝛼curio, in particular the failure case where null is returned. ⟨3⟩3. Basic-1: ∀(𝑎, 𝑘; 𝑖), (𝑎′, 𝑘′; 𝑖′) ∈ Φ1 : 𝑖 ≠ 𝑖′ =⇒ [ 𝑎, 𝑎 + 𝑘) ∩ [ 𝑎′, 𝑎′ + 𝑘 ′) = ∅ Proof: Holds vacuously, since Φ1 = ∅. ⟨3⟩4. Basic-2: JΦ1K ⊆ dom(𝐻1) Proof: JΦ1K = J∅K = ∅ ⊆ ...

    work page 2025

  63. [63]

    (𝐻1, 𝐴1, 𝑎) = 𝛼curio.malloc(𝐻0, 𝐴0, 𝑘)

    work page

  64. [64]

    𝑖 = |𝜖 | + 1 = 0 + 1 = 1

    work page

  65. [65]

    Φ1 = {(𝑎, 𝑘; 1)} Proof: Follows from definition of 𝛼curio (zero sized allocations return null), ▷-malloc-ok, and ⟨2⟩4. ⟨3⟩2. 𝐻1 = 𝐻0 [[𝑎, 𝑎 + 𝑘) ↦→ 0] Proof: Follows from definition of 𝛼curio. ⟨3⟩3. dom(𝐻1) = [𝑎, 𝑎 + 𝑘) Proof: dom(𝐻1) = dom(𝐻0 [[𝑎, 𝑎 + 𝑘) ↦→ 0]) (from ⟨3⟩2) = dom(𝐻⊥ [[𝑎, 𝑎 + 𝑘) ↦→ 0]) (from ⟨1⟩6) = [𝑎, 𝑎 + 𝑘) ⟨3⟩4. JΦ1K = [𝑎, 𝑎 + 𝑘) Proof...

    work page 2025

  66. [66]

    Φ1 = Φ′ 0 Proof: From ⟨1⟩8. ⟨3⟩2. 𝐻1 = 𝐻 ′′ 0 and 𝐴1 = 𝐴′ 0 Proof: Follows from definition of 𝛼curio, in particular the failure case where null is returned. ⟨3⟩3. Basic-1: ∀(𝑎, 𝑘; 𝑖), (𝑎′, 𝑘′; 𝑖′) ∈ Φ1 : 𝑖 ≠ 𝑖′ =⇒ [ 𝑎, 𝑎 + 𝑘) ∩ [ 𝑎′, 𝑎′ + 𝑘 ′) = ∅ Proof: Follows from (IH) since Φ1 = Φ′ 0 (from ⟨3⟩1). ⟨3⟩4. Basic-2: JΦ1K ⊆ dom(𝐻1) Proof: JΦ1K = JΦ′ 0K (by ...

    work page

  67. [67]

    (by (IH)) = dom(𝐻 ′′ 0 ) (by ⟨1⟩1) = dom(𝐻1) (by ⟨3⟩2) ⟨3⟩5. Basic-4: ∀𝐻 ′, 𝐴′, Φ′, such that 𝛼curio, ∅ ⊢ ∅, 𝐻0, 𝐴0 | ®𝑢, ®𝜎 ′ ▷ ▷𝐻 ′, 𝐴′, Φ′ and 𝛼curio ⊢ Φ′, 𝐻′, 𝐴′ | ®𝜎 ′ ·𝜎 ▷ 𝐻1, 𝐴1, Φ1 then 𝐻 ′ =JΦ′K 𝐻1 Proof: Trivial, since 𝐻1 = 𝐻 ′ (from the definition of 𝛼curio when failing to allocate). ⟨3⟩6. Zero-Alloc-1: ∀(𝑎, 𝑘; 𝑖), (𝑎′, 𝑘′; 𝑖′) ∈ Φ1 : 𝑖 ≠ 𝑖′ =⇒...

    work page

  68. [68]

    𝛼curio, ∅ ⊢ ∅, 𝐻0, 𝐴0 | ®𝑢′ 2, ®𝜎 ′ ▷ ▷𝐻 ′ 0, 𝐴′ 0, Φ′ 0

    work page

  69. [69]

    ∀(𝑎, 𝑘; 𝑖) ∈ Φ1 : ∃(𝑎′, 𝑘′; 𝑖′) ∈ Φ′ 0 : 𝑘 = 𝑘 ′ ∧ 𝑖 = 𝑖′ Proof: Follows from (IH). ⟨4⟩2. Rel-1: 𝛼curio, ∅ ⊢ ∅, 𝐻0, 𝐴0 | ®𝑢2, ®𝜎 ▷ ▷𝐻2, 𝐴2, Φ2 ⟨5⟩1. 𝛼curio, ∅ ⊢ ∅, 𝐻0, 𝐴0 | ®𝑢′ 2, ®𝜎 ′ ▷ ▷𝐻 ′ 0, 𝐴′ 0, Φ′ 0 Proof: Follows from ⟨4⟩1. Let: 1. ®𝑢′ 2 = ®𝑢′′ 2 ·𝑢′ 2 (since | ®𝑢2| > 1) , Vol. 1, No. 1, Article . Publication date: August 2025. The downgrading sem...

    work page 2025

  70. [70]

    𝛼curio ⊢ Φ′ 0, 𝐻′′ 0 , 𝐴′ 0 | ®𝜎 ′ ·n(𝑘) ▷ 𝐻2, 𝐴2, Φ2 Proof: Follows from above with 𝐻2 = 𝐻 ′′ 0 , 𝐴2 = 𝐴′ 0, and Φ2 = Φ′ 0

    𝐻 ′′ 0 = 𝑢′ 2(𝐻 ′ 0, Φ′ 0) ⟨5⟩2. 𝛼curio ⊢ Φ′ 0, 𝐻′′ 0 , 𝐴′ 0 | ®𝜎 ′ ·n(𝑘) ▷ 𝐻2, 𝐴2, Φ2 Proof: Follows from above with 𝐻2 = 𝐻 ′′ 0 , 𝐴2 = 𝐴′ 0, and Φ2 = Φ′ 0. ⟨4⟩3. Rel-2: ∀(𝑎, 𝑘; 𝑖) ∈ Φ1 : ∃(𝑎′, 𝑘′; 𝑖′) ∈ Φ2 : 𝑘 = 𝑘 ′ ∧ 𝑖 = 𝑖′ Proof: Follows from (IH), ⟨4⟩1, and above (Φ2 = Φ′ 0). ⟨3⟩9. Q.E.D. Proof: The induction step for case 𝜎 = n(𝑘) follows from ⟨1⟩4,...

    work page

  71. [71]

    𝑖 = | ®𝜎 ′ | + 1 = | ®𝜎 | = 𝑛 > 1

    work page

  72. [72]

    Φ1 = Φ′ 0 ∪ {( 𝑎, 𝑘; 𝑖)} Proof: From ⟨1⟩8 and ▷-malloc-ok. ⟨3⟩2. 𝐻1 = 𝐻 ′′ 0 [[𝑎, 𝑎 + 𝑘) ↦→ 0] Proof: Follows from ⟨3⟩1 and the definiiotn of 𝛼curio. ⟨3⟩3. dom(𝐻1) = dom(𝐻 ′′ 0 ) ∪ [ 𝑎, 𝑎 + 𝑘) Proof: Follows from ⟨3⟩1 and the definiiotn of 𝛼curio. ⟨3⟩4. dom(𝐻 ′′ 0 ) = dom(𝐻 ′ 0) Proof: Follows from ⟨1⟩1. ⟨3⟩5. Basic-1: ∀(𝑎, 𝑘; 𝑖), (𝑎′, 𝑘′; 𝑖′) ∈ Φ1 : 𝑖 ≠ ...

    work page

  73. [73]

    Basic-4: ∀𝐻 ′, 𝐴′, Φ′, such that 𝛼curio, ∅ ⊢ ∅, 𝐻0, 𝐴0 | ®𝑢1, ®𝜎 ′ ▷ ▷𝐻 ′, 𝐴′, Φ′ and 𝛼curio ⊢ Φ′, 𝐻′, 𝐴′ | ®𝜎 ′ ·m(𝑘) ▷ 𝐻1, 𝐴1, Φ1 then 𝐻 ′ =JΦ′K 𝐻1 ⟨4⟩1

    ∪ [ 𝑎, 𝑎 + 𝑘) (by (IH)) = dom(𝐻 ′′ 0 ) ∪ [ 𝑎, 𝑎 + 𝑘) (by ⟨3⟩4) = dom(𝐻1) (by ⟨3⟩3) ⟨3⟩7. Basic-4: ∀𝐻 ′, 𝐴′, Φ′, such that 𝛼curio, ∅ ⊢ ∅, 𝐻0, 𝐴0 | ®𝑢1, ®𝜎 ′ ▷ ▷𝐻 ′, 𝐴′, Φ′ and 𝛼curio ⊢ Φ′, 𝐻′, 𝐴′ | ®𝜎 ′ ·m(𝑘) ▷ 𝐻1, 𝐴1, Φ1 then 𝐻 ′ =JΦ′K 𝐻1 ⟨4⟩1. JΦ′K ⊆ dom(𝐻 ′) Proof: Follows from (IH). ⟨4⟩2. 𝐻1 = 𝐻 ′ [[𝑎, 𝑎 + 𝑘) ↦→ 0] and 𝐻 ′ ⊥( [𝑎, 𝑎 + 𝑘)) Proof: Follows...

    work page 2025

  74. [75]

    ∀(𝑎, 𝑘; 𝑖) ∈ Φ1 : ∃(𝑎′, 𝑘′; 𝑖′) ∈ Φ′′ : 𝑘 = 𝑘 ′ ∧ 𝑖 = 𝑖′ Proof: Follows from (IH). ⟨4⟩2. Rel-1: 𝛼curio, ∅ ⊢ ∅, 𝐻0, 𝐴0 | ®𝑢2, ®𝜎 ▷ ▷𝐻2, 𝐴2, Φ2 ⟨5⟩1. 𝛼curio, ∅ ⊢ ∅, 𝐻0, 𝐴0 | ®𝑢′ 2, ®𝜎 ′ ▷ ▷𝐻 ′′, 𝐴′′, Φ′′ Proof: Follows from ⟨4⟩1. Let: 1. ®𝑢′ 2 = ®𝑢′′ 2 ·𝑢′ 2 (since | ®𝑢2| > 1)

    work page

  75. [76]

    𝛼curio ⊢ Φ′′, 𝐻′′ 𝑢′ 2 , 𝐴′′ | ®𝜎 ′ ·m(𝑘) ▷ 𝐻2, 𝐴2, Φ2 Proof: Since 𝛼curio is deterministic and does not read from the client accessible heap, except for the initial allocation

    𝐻 ′′ 𝑢′ 2 = 𝑢′ 2(𝐻 ′′, Φ′′) ⟨5⟩2. 𝛼curio ⊢ Φ′′, 𝐻′′ 𝑢′ 2 , 𝐴′′ | ®𝜎 ′ ·m(𝑘) ▷ 𝐻2, 𝐴2, Φ2 Proof: Since 𝛼curio is deterministic and does not read from the client accessible heap, except for the initial allocation. ⟨4⟩3. Rel-2: ∀(𝑎, 𝑘; 𝑖) ∈ Φ1 : ∃(𝑎′, 𝑘′; 𝑖′) ∈ Φ2 : 𝑘 = 𝑘 ′ ∧ 𝑖 = 𝑖′ Proof: Follows from ⟨4⟩1 and since Φ2 = Φ′′ ∪ {( 𝑎′′, 𝑘, 𝑖)}. ⟨2⟩3. Case: 𝜎 ...

    work page

  76. [77]

    Φ1 = Φ′ 0 \ {( 𝑎, 𝑘; 𝑖)}

    work page

  77. [78]

    𝑗 = | ®𝜎 ′ | + 1 = 𝑛 > 1

    work page

  78. [79]

    𝐻1 = 𝐻 ′′ 0 [[𝑎, 𝑎 + 𝑘) ↦→ ⊥] Proof: From ⟨1⟩8 and ▷-free. ⟨3⟩2. dom(𝐻1) = dom(𝐻 ′′ 0 ) \ [ 𝑎, 𝑎 + 𝑘) Proof: dom(𝐻1) = 𝐻 ′′ 0 [[𝑎, 𝑎 + 𝑘) ↦→ ⊥] = dom(𝐻 ′′ 0 ) \ [ 𝑎, 𝑎 + 𝑘). ⟨3⟩3. dom(𝐻 ′

    work page

  79. [80]

    = dom(𝐻 ′′ 0 ) Proof: Follows from ⟨1⟩1. ⟨3⟩4. Basic-1: ∀(𝑎, 𝑘; 𝑖), (𝑎′, 𝑘′; 𝑖′) ∈ Φ1 : 𝑖 ≠ 𝑖′ =⇒ [ 𝑎, 𝑎 + 𝑘) ∩ [ 𝑎′, 𝑎′ + 𝑘 ′) = ∅ Proof: Follows from (IH) and ⟨3⟩1. ⟨3⟩5. Basic-2: JΦ1K ⊆ dom(𝐻1) Proof: JΦ1K = JΦ′ 0 \ {( 𝑎, 𝑘; 𝑖)} K (by ⟨3⟩1) = JΦ′ 0K \ [𝑎, 𝑎 + 𝑘) (by def. J·K) ⊆ dom(𝐻 ′

    work page

  80. [81]

    \ [ 𝑎, 𝑎 + 𝑘) (by (IH)) = dom(𝐻 ′′ 0 ) \ [ 𝑎, 𝑎 + 𝑘) (by ⟨3⟩3) = dom(𝐻1) (by ⟨3⟩2) ⟨3⟩6. Basic-4: For all 𝐻 ′, 𝐴′, Φ′, such that 𝛼curio, ∅ ⊢ ∅, 𝐻0, 𝐴0 | ®𝑢′ 1, ®𝜎 ′ ▷ ▷𝐻 ′, 𝐴′, Φ′ and 𝛼curio, ∅ ⊢ Φ′, 𝐻′, 𝐴′ | ®𝜎 ′ ·f ⟨𝑧⟩ ▷ 𝐻1, 𝐴1, Φ1 then 𝐻 ′ =JΦ1K 𝐻1 Proof: Follows from 𝐻1 = 𝐻 ′ [[𝑎, 𝑎 + 𝑘) ↦→ ⊥] (by ⟨3⟩1) and JΦ1K ⊆ dom(𝐻1) (by ⟨3⟩5). ⟨3⟩7. Zero-Alloc-1...

    work page 2025

Showing first 80 references.