{"id":"5d738986-3b9f-4953-b3a4-ab56891c73b8","arxiv_id":"2507.03344","paper_version":1,"verdict":"CONDITIONAL","confidence":"MODERATE","novelty_score":7.0,"correctness_risk":"medium","formal_verification":"none","parameter_count":2,"one_line_summary":"CapsLock uses a revoke-on-use hardware capability mechanism to detect Rust principle violations at machine-code level, covering FFI and inline assembly that Miri cannot handle.","lead":"A hardware-capability design called CapsLock enforces Rust's ownership, borrowing, and aliasing rules at the machine-code level, including code reached through FFI and inline assembly where the Rust compiler cannot check. It introduces revoke-on-use: each memory access automatically invalidates conflicting pointer capabilities, and a QEMU prototype found 8 previously unknown bugs in popular Rust crates.","discovery_kind":"new_method","skeptic_critique":{"model":"deepseek-v4-flash","headline":"Pointer-provenance resolution in §5.1 is the load-bearing step for cross-language enforcement; when two live capabilities share identical bounds, the heuristic can pick the wrong one, causing missed or false violations.","rationale":"The reader's weakest-assumption analysis identifies exactly the §5.1 pointer-provenance heuristic, and I agree it is the load-bearing point. The other two concerns noted in the reader's verdict are real but are explicitly acknowledged limitations: foreign-allocated memory is unprotected by the prototype, and the model is deliberately more relaxed than Stacked Borrows or Tree Borrows. Those affect the breadth of the 'cross-language enforcement' claim, but they do not threaten the mechanism's core operation the way provenance resolution does. If the heuristic mis-resolves an ambiguous pointer in uninstrumented foreign code, CapsLock cannot even reliably implement its own revoke-on-use invariants, and the central claim collapses regardless of how the acknowledged limitations are patched. The paper deserves credit for releasing artifacts, for the manual confirmation of the eight reported bugs via simplified Miri reproductions, and for the proof sketches of the invariants, but those do not cover the provenance-resolution step. The proposed test is small, uses only the released artifact, and directly distinguishes correct from incorrect resolution of two identical-bounds capabilities, so it would settle whether the concern lands. Because this is a strengthening of the reader's existing CONDITIONAL verdict rather than a new direction, the verdict should remain UNCHANGED.","tokens_in":26436,"tokens_out":6876,"duration_ms":84750,"concrete_test":"In the released CapsLock artifact, add a mixed Rust/C regression test. Rust code creates a Box<u64>, then creates two raw pointers p1 and p2 via two separate address-of/cast borrows so that CapsLock records two sibling capabilities with identical bounds. A C function receives both pointers, computes q = p2 + (p1 - p2) (so q is a valid alias of p1 but the tracker associates q with both capability lists), stores through q, and returns. Rust then reads through p2. Under CapsLock's own Table 2 semantics, the store through q should revoke the sibling p2, so the read should report a violation. If CapsLock reports no violation (because resolution kept p2) or reports a violation when p2 is untouched, the §5.1 heuristic demonstrably picks the wrong capability for identical-bounds aliases. Running this one test on the released Docker image settles whether the concern lands.","verdict_should_be":"UNCHANGED","load_bearing_attack":"The claim that CapsLock enforces Rust principles across FFI and inline assembly rests on the §5.1 provenance-resolution heuristic: when a value is used for a load/store for the first time, the implementation keeps only the associated capability whose memory bounds match the requested address. This is sound only if at most one live capability can match any dereferenced address in uninstrumented foreign code. That condition is not guaranteed: two capabilities derived from the same object (e.g., two raw-pointer borrows of one Box) have identical bounds and permissions, and C code can legitimately combine two such pointer values with arithmetic, so the result is associated with both capability lists. If the implementation resolves to the wrong sibling, revoke-on-use either invalidates a capability that should remain live (a false positive) or leaves live a capability that should have been revoked (a missed violation). The paper gives no formal argument, adversarial test, or coverage measurement for this resolution, and the §5.1 Rust-specific relaxations were tuned against the same 100-crate benchmark used for the 99.7% compatibility claim, so the benchmark pass rate does not validate the heuristic's generality. Because all foreign-code enforcement flows through this step, this is the most load-bearing assumption in the central claim.","agreement_with_reader":"agree"},"referee_report":{"model":"deepseek-v4-flash","summary":"The paper presents CapsLock, a capability-based mechanism that aims to enforce Rust's ownership, borrowing, and aliasing-xor-mutability principles at the machine-code level, so that violations in mixed Rust code (including unsafe Rust, FFI, and inline assembly) can be detected at run time. The design is built on the Capstone capability architecture and introduces a revoke-on-use operation that invalidates conflicting capabilities implicitly at each load/store. The authors formalize capabilities and instructions in Table 2 and Appendix A, give informal proof sketches for two invariants (well-nested borrowing and exclusive access), and implement a QEMU/RISC-V prototype with rustc instrumentation. The evaluation reports 99.7% compatibility on the built-in tests of the 100 most popular crates, detection of all 15 RustSec PoCs tested, 8 previously unknown bugs in crates using FFI or inline assembly, and an average runtime speedup of over 2x relative to Miri.","tokens_in":26620,"tokens_out":8021,"duration_ms":103074,"significance":"If the central claims hold, CapsLock is a significant contribution: it is a language-agnostic, hardware-oriented mechanism that goes beyond spatial memory safety to detect violations of Rust-specific aliasing principles across language boundaries, and it is evaluated with a public artifact against standard tools (Miri, AddressSanitizer, ThreadSanitizer) on a large corpus. The 8 reported bugs, several confirmed and fixed by maintainers, provide concrete evidence of practical utility. The design is notably simple and the paper is generally well written. However, the formal semantics as printed contain inconsistencies that the proofs rely on, and the implementation's pointer-provenance resolution is load-bearing for the cross-language claim but is neither formally justified nor adversarially evaluated.","major_comments":[{"comment":"The formal definitions contradict the prose and the proof sketches. The Store and Load rules define S = O_m(a) ∩ A_m(i), while the text immediately above says S contains overlapping capabilities that are not ancestors of i, and the Section 4.3 proof requires the set-difference reading (it concludes i1 is revoked from i1 ∉ A_m0(i2)). In addition, RevokeW(m,S) is described as invalidating the capabilities in S, but Eq. (5) keeps exactly S valid and invalidates the complement; RevokeR's prose says it demotes capabilities not in S to RO, but Eq. (7) maps RW capabilities outside S to NA. With the definitions as printed, the two invariants in Section 3.4 are not established, and the formal semantics do not correspond to the revoke-on-use behavior described in Section 3.2. Please correct these errors and re-verify the proofs.","section":"§4.2, Table 2 and Appendix A"},{"comment":"The pointer-provenance heuristic is load-bearing for the central claim that external code requires no instrumentation. The implementation resolves a value's provenance at its first load/store use by keeping \"only the associated capability with memory bounds matching the requested load/store address.\" If two live capabilities have identical bounds and permissions, or if uninstrumented code computes a pointer from two capabilities (e.g., via pointer arithmetic), this resolution can select the wrong capability, causing either a missed violation or a false positive. This step is not modeled in the formal semantics of Table 2/Appendix A, which associate each memory location with a single capability identifier, and no formal argument, adversarial test, or coverage measurement is provided. The 99.7% compatibility rate in Section 6.1 is measured on the same 100-crate corpus used to motivate the §5.1 relaxations, so it does not validate the heuristic's generality for arbitrary foreign code.","section":"§5.1"},{"comment":"The paper explicitly states that the prototype \"does not protect memory allocated in foreign code\" because only the Rust-side heap allocator is interposed. This is a scoping gap for the cross-language claim: pointers to foreign-allocated objects carry no capability, so violations involving such objects are invisible to the QEMU prototype. Since the evaluation in Sections 6.2-6.3 and the bugs found are specifically about FFI, the implementation and evaluation should either interpose foreign allocators as well, or the abstract and evaluation claims should be restricted to Rust-allocated objects with the foreign-allocation limitation stated prominently.","section":"§5.3"}],"minor_comments":[{"comment":"The proof of exclusive access contains a contradictory phrase: \"i2 ∉ D_m0(i1) is the identifier of a capability in the subtree of i1.\" The intended statement appears to be that i2 is outside the subtree of i1, and the prose should be corrected.","section":"§4.3"},{"comment":"The prose says RevokeR \"demotes capabilities not in S to RO,\" but the definition maps read-write capabilities not in S to NA, which is a different operation. Please clarify which behavior is intended and align the text with the definition.","section":"Appendix A, Eq. (7)"},{"comment":"The category labels are confusing: \"O\" is used both as a column/row label and as part of the legend, and the Venn diagram's numbers are not immediately reconcilable with Table 3. A more explicit legend would help.","section":"§6.1, Table 3 and Figure 6"},{"comment":"The \"logically impossible double free\" example is explained tersely; a short step-by-step trace of why the optimized program reaches an always-true branch would make the argument easier to verify.","section":"§2.2, Listing 3"}],"recommendation":"major_revision","confidential_remarks":"The two load-bearing issues are fixable: the formal semantics in Table 2/Appendix A appear to contain correctable sign errors, and the provenance heuristic needs additional validation rather than a fundamentally new design. I would be willing to review a revised version."},"author_rebuttal":null,"desk_editor":{"model":"deepseek-v4-flash","letter":"Colleague,\n\nCapsLock is worth your time. The revoke-on-use idea is genuinely new: a single capability type that implicitly invalidates conflicting capabilities on each load/store, distilling the authors' earlier Capstone work into something that operates at machine level and catches Rust ownership, borrowing, and AXM violations through FFI and inline assembly—which Miri cannot handle. The paper gives clear operational semantics, plausible invariants with proof sketches, and a QEMU prototype with released artifacts. The evaluation is meaningful: 99.7% pass on the top-100 crates, 15/15 RustSec PoCs detected, and 8 new real-world bugs with maintainer feedback. That is real evidence, not a toy.\n\nThe soft spots are real but not fatal. First, the \"first mechanism capable of providing cross-language enforcement of Rust principles\" claim is stronger than the prototype. The prototype does not protect foreign-allocated memory, and the model is deliberately more relaxed than Stacked or Tree Borrows. The authors admit both points, but the abstract still over-sells. Second, the §5.1 pointer-provenance heuristic is load-bearing for external code: when a value can be derived from two capabilities with identical bounds and permissions, the resolution by address match can pick the wrong one. The stress-test note is fair to call this out. The paper does not formally validate the heuristic, and the benchmark pass rate does not prove its generality. That said, the heuristic is plausible, and the compatibility data shows it works on real Rust code; the issue is missing rigorous analysis, not a demonstrated break. Third, the 8 new bugs come without a false-positive count for the 10,000+ test cases run, so precision is unknown. The 12 failed cases in §6.1 are discussed but not systematically.\n\nWho should read this: anyone working on Rust memory safety, hardware capabilities, or cross-language bug detection. The artifacts make the claims reproducible. I would send it to a serious referee; the core mechanism deserves scrutiny, and the evaluation is worth verifying. The needed fixes are tempering the scope claim and adding precision and robustness analysis for the heuristic—not a redesign.","headline":"Genuinely new revoke-on-use mechanism with a solid, reproducible evaluation; the 'cross-language enforcement' claim is a bit too strong for the prototype, and the §5.1 pointer-provenance heuristic is the main soft spot.","tokens_in":27237,"tokens_out":2948,"would_cite":true,"duration_ms":35159,"reading_group":"maybe","serious_thinker":"yes","would_accept_peer_review":true},"rs_alignment":null,"lean_confirmation":null,"pith_extraction":{"msc":[],"pacs":[],"model":"deepseek-v4-flash","headline":"CapsLock claims to be the first mechanism that enforces Rust's ownership, borrowing, and aliasing rules in mixed code at machine-code level, using a revoke-on-use capability design.","keywords":["Rust memory safety","hardware capabilities","revoke-on-use","aliasing models","foreign function interface","cross-language enforcement","temporal memory safety","dynamic bug detection"],"falsifier":"Take a C function that receives two pointers to the same buffer with identical bounds and live capabilities, computes a third pointer from them by arithmetic such as subtraction or xor, and writes through that computed pointer; run it linked into a Rust program under CapsLock. If the write is a genuine AXM violation that goes unreported, or a benign write that is reported, the provenance heuristic of Section 5.1 is refuted.","tokens_in":26187,"feed_emoji":"🔒","tokens_out":5209,"duration_ms":56933,"temperature":0.7,"pith_summary":"This paper argues that Rust's safety guarantees can be enforced even in the parts of a program the Rust compiler cannot see: unsafe blocks, foreign function calls, and inline assembly. The proposed system, CapsLock, does this at machine-code level by replacing raw pointers with hardware capabilities that carry bounds, permissions, and a record of which capability borrowed from which. Whenever a capability is used to read or write memory, CapsLock automatically invalidates other capabilities whose later use would conflict, an operation the paper calls revoke-on-use. The result is a run-time checker that a QEMU-based prototype applies to existing Rust code without recompiling external libraries, passing 99.7% of the test suites of the 100 most popular crates and surfacing 8 previously unknown principle violations in FFI-using crates. If this holds, Rust's guarantees extend across the boundary where they currently lapse.","feed_headline":"Capability hardware enforces Rust rules across C and assembly","feed_subtitle":"Revoke-on-use capabilities flag ownership and aliasing violations that rustc cannot see, finding 8 new bugs in real crates.","key_machinery":"The central object is the revoke-on-use capability: a hardware capability carrying an address range, a permission (read-write, read-only, or no-access), and a parent identifier that links it into a borrow tree. When software uses such a capability for a load or store, the hardware implicitly revokes every conflicting capability in the tree, as formalized by the RevokeW and RevokeR rules. This distills the aliasing models Stacked Borrows and Tree Borrows into two invariants, well-nested borrowing and exclusive access, while removing the separate revocation-capability type and the linear/non-linear distinction of the baseline Capstone design. Borrow instructions are injected into Rust code by a modified rustc MIR pass, while foreign code needs no instrumentation; pointer provenance in uninstrumented code is resolved lazily at the first load or store by retaining the capability whose bounds match the accessed address.","core_discovery":"The paper's central claim is that the three Rust principles — ownership, borrowing, and Aliasing Xor Mutability (AXM) — can be captured by a single machine-level abstraction, revoke-on-use, and that this abstraction is implementable on recent capability-based hardware. CapsLock maintains a borrow tree for every memory object: a root capability is created at allocation, each new reference or raw pointer borrows a capability from an existing one, and each load or store implicitly revokes all conflicting capabilities in the tree. The security invariants are well-nested borrowing (a capability cannot outlive its parent) and exclusive access (no store from outside a capability's subtree before its last use, and no load from outside the subtree before a capability's last store). Because the checks live in the hardware, code that was not compiled by rustc, including C libraries and inline assembly, participates in the same enforcement. The paper presents proof sketches for the two invariants and evaluates a QEMU prototype on the 100 most popular crates, on 15 RustSec proof-of-concept exploits, and on crates whose FFI use makes Miri abort.","pith_inferences":["The lazy provenance-resolution heuristic in Section 5.1 is where the cross-language claim rests: if a pointer is recomputed through arithmetic that combines two live capabilities with identical bounds, or through a foreign routine, CapsLock may attach the wrong capability and either miss a violation or raise a false positive; the paper reports high compatibility but does not quantify how often suc","Because CapsLock's model is deliberately more relaxed than both Stacked Borrows and Tree Borrows (no protectors for function arguments, lazy invalidation), there exist violations that Miri flags but CapsLock will not; the paper acknowledges this, so the system is a detector of a useful subset rather than a complete oracle.","The revoke-on-use abstraction could be lifted out of Rust entirely: it is a general aliasing discipline for capability hardware, so the same mechanism could enforce similar exclusive-access contracts in other languages that adopt borrow-like rules, or enforce alias annotations if such annotations were introduced.","A testable extension would be to run CapsLock under a fuzzer: since it flags violations at the violating instruction rather than at a later crash, it could make Rust-principle violations a directly optimizable coverage signal, provided the false-positive rate from provenance ambiguity stays low."],"forward_implications":["CapsLock can flag runs where Rust principles are violated even when the violation never produces a crash or memory error, because it checks the assumption violation itself rather than its after-effects.","Existing Rust code can be checked largely as-is: 99.7% of the top-100 crates' test cases pass, with only 12 failures on CapsLock while passing on Miri, all traced to UnsafeCell corner cases.","In mixed projects that Miri cannot run, CapsLock found eight previously unknown violations, seven of them AXM violations, using only the crates' ordinary built-in tests.","Memory-safety and data-race sanitizers are not a substitute for Rust-principle checking: AddressSanitizer and ThreadSanitizer together miss 6 of the 15 RustSec principle-violation PoCs that CapsLock catches.","A hardware implementation would likely enforce these invariants on all memory, including memory allocated by foreign allocators, since the prototype's heap protection is limited only by interposing on Rust's allocator."],"supporting_citations":[{"why":"Supplies the baseline Capstone capability design, including linear and revocation capabilities, that CapsLock simplifies into revoke-on-use.","marker":"[41]"},{"why":"Defines Stacked Borrows, the aliasing model whose core Rust principles CapsLock approximates at machine level and which Miri uses.","marker":"[18]"},{"why":"Defines Tree Borrows, the alternative aliasing model used for comparison and for explaining CapsLock's corner-case mismatches.","marker":"[35]"},{"why":"Miri is the official Rust undefined-behaviour detector that CapsLock compares against and surpasses in FFI and inline-assembly settings.","marker":"[4]"},{"why":"AddressSanitizer serves as the memory-safety checker baseline in the empirical comparison, showing the gap between memory safety and Rust principles.","marker":"[30]"},{"why":"ThreadSanitizer serves as the data-race detection baseline in the comparison, showing its inability to catch most AXM violations.","marker":"[31]"},{"why":"RustSec advisory database supplies the 15 known Rust principle violations used to evaluate CapsLock's detection effectiveness.","marker":"[1]"},{"why":"crates.io supplies the top-100 crates and the FFI-using crates from which compatibility and bug-finding benchmarks are drawn.","marker":"[2]"}],"fun_headline_variants":["CapsLock: hardware-enforced Rust safety for mixed code","Mixed Rust gets hardware teeth: CapsLock finds 8 bugs","Revoke-on-use: the hardware lock that enforces Rust's rules","Capability hardware catches Rust violations C can't see"],"cache_read_input_tokens":3200,"weakest_assumption_plain":"Everything depends on a pointer-provenance heuristic: when a value computed in foreign code is used for its first memory access, CapsLock assumes that keeping only the capability whose bounds match the address is enough to know which pointer it really is and which other capabilities should be revoked.","fun_headline_variants_meta":{"raw":{"variants":["CapsLock: hardware-enforced Rust safety for mixed code","Mixed Rust gets hardware teeth: CapsLock finds 8 bugs","Revoke-on-use: the hardware lock that enforces Rust's rules","Capability hardware catches Rust violations C can't see"]},"model":"deepseek-v4-flash","effort":"low","cost_usd":0.000989,"raw_usage":{"total_tokens":4244,"prompt_tokens":1049,"completion_tokens":3195,"prompt_tokens_details":{"cached_tokens":384},"prompt_cache_hit_tokens":384,"prompt_cache_miss_tokens":665,"completion_tokens_details":{"reasoning_tokens":3124}},"tokens_in":665,"tokens_out":3195,"duration_ms":25440,"temperature":1.0,"reasoning_tokens":3124,"cache_read_input_tokens":384,"cache_creation_input_tokens":0},"cache_creation_input_tokens":0},"created_at":"2026-08-06T20:12:49.148071+00:00","model_set":{"reader":"deepseek-v4-flash"},"falsifier":"Take a C function that receives two pointers to the same buffer with identical bounds and live capabilities, computes a third pointer from them by arithmetic such as subtraction or xor, and writes through that computed pointer; run it linked into a Rust program under CapsLock. If the write is a genuine AXM violation that goes unreported, or a benign write that is reported, the provenance heuristic of Section 5.1 is refuted.","supporting_citations":[{"cited_title":"Carlson, and Prateek Saxena","cited_arxiv_id":null,"evidence_quote":"Supplies the baseline Capstone capability design, including linear and revocation capabilities, that CapsLock simplifies into revoke-on-use."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"Defines Tree Borrows, the alternative aliasing model used for comparison and for explaining CapsLock's corner-case mismatches."},{"cited_title":"Rust-Lang/Miri","cited_arxiv_id":null,"evidence_quote":"Miri is the official Rust undefined-behaviour detector that CapsLock compares against and surpasses in FFI and inline-assembly settings."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"AddressSanitizer serves as the memory-safety checker baseline in the empirical comparison, showing the gap between memory safety and Rust principles."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"RustSec advisory database supplies the 15 known Rust principle violations used to evaluate CapsLock's detection effectiveness."},{"cited_title":null,"cited_arxiv_id":null,"evidence_quote":"crates.io supplies the top-100 crates and the FFI-using crates from which compatibility and bug-finding benchmarks are drawn."}],"review_version":1}