Pith. sign in

REVIEW 4 major objections 5 minor 90 references

On the Verification of Control Flow Attestation Evidence

T0 review · 4 major / 5 minor · reviewed 2026-08-12 · deepseek-v4-flash

Challenge this review Re-run · record.json Download PDF Read on arXiv ↗ Review JSON

Pith's one-line read If control-flow attestation evidence is recorded verbatim, a remote verifier can localize the corrupting instruction and automatically patch the underlying memory bug; SABRE demonstrates this end to end.

desk verdict SABRE's verifier-side analysis of verbatim CFA logs is a real step forward, and the open prototype makes it worth engaging, but the evaluation does not yet prove the patching claims. read the letter →

arxiv 2411.10855 v3 pith:M3TQSY7E submitted 2024-11-16 cs.CR

Adam Caulfield , Norrathep Rattanavipanon , Ivan De Oliveira Nunes This is my paper · ORCID
classification cs.CR
keywords controlflowattestationrun-timeauditingrootcauseanalysisbinarypatchingbufferoverflowuse-after-freesymbolicdataembeddedsystemssecurity
verification ladder T0 review T1 audit T2 compute T3 formal

The pith

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

The reading

Remote control-flow attestation (CFA) promises to give a verifier authentic evidence of what code actually executed on a possibly compromised device, but prior work concentrated on how the device generates that evidence rather than on whether the verifier can do anything useful with it. This paper argues that run-time auditing is only as good as the verifier's analysis, and it classifies CFA evidence into three types: hash-based digests, verbatim control-flow logs, and hybrid logs. The central claim is that only verbatim evidence lets the verifier pinpoint the corrupted return address or indirect-call target, identify the exact instruction that corrupted it, and go on to patch the underlying memory vulnerability. To make this concrete, the paper presents SABRE, a security analysis and binary repair engine that takes an application binary and a verbatim control-flow log, detects the attack, locates the exploit, and generates and validates binary patches for buffer overflows and use-after-free bugs without source code. The payoff is that a verifier can turn an attested attack trace into an automated remediation loop for memory-unsafe embedded software.

What carries the argument

The object that carries the argument is verbatim control-flow evidence: a control-flow log that records branch destinations, optionally with loop counters for simple loops, rather than accumulating destinations into hashes. SABRE's second load-bearing mechanism is symbolic data-flow analysis over a slice of that log: the base location holding the corrupted control data is initialized to a special symbolic value $X$, the slice is replayed with symbolic memory and register maps, and the first instruction whose write changes $X$ is identified as the corrupting access. The third mechanism is the binary patching strategy, which either removes an offending free by replacing it with nops for use-after-free, or copies the vulnerable function, adds trampolines that record buffer bounds derived from backward and forward definition traversal, and prepends bounds checks so out-of-range writes are skipped.

What would settle it

A concrete test is to construct a single out-of-bounds write outside any loop that directly overwrites a return address or function pointer, run the same style of benchmark embedded binary under one of the two open-source CFA architectures used in the evaluation, and feed SABRE the resulting verbatim log; if the engine flags the wrong instruction or fails to produce a patch, its first-write and loop-repetition heuristics are refuted for that class of vulnerability.

Watch

Extended reading notes

Core claim

The paper's central claim is a mapping between evidence fidelity and verifier capability: when control-flow transitions are accumulated into a hash chain or when returns are folded into a hash, the verifier can know that something went wrong but cannot reconstruct the illegal path or determine which return was corrupted, whereas a verbatim log records every destination, so the verifier can detect the exact invalid transfer, emulate a shadow stack, and follow the data flow backward to the instruction that overwrote the control data. SABRE operationalizes this by combining a statically built control-flow graph with the runtime log: its Exploit Locator first walks backwards through the log and the binary to find the slice where the corrupted value was initialized, then runs symbolic data-flow analysis starting from a special symbolic value $X$ assigned to the base location, and flags the first memory write to $X$ as the corrupting instruction. If that base was already freed, SABRE reports a use-after-free; if the writing node executed repeatedly in the slice, it reports a buffer overflow. The Patch Generator then replaces the offending free with nops or inserts bounds-checking trampolines around the overflowing write, redirecting the specific call site to a safe copy of the function, and the Patch Validator re-runs the symbolic analysis on the patched binary to confirm the corruption no longer occurs.

Load-bearing premise

The load-bearing premise is that the first write to the memory location holding a protected control value inside the relevant logged slice is the write that corrupted it, and that tracing definitions backward from the corrupted instruction always reaches the point where that location was initialized.

Editorial extensions

If this is right

  • If the paper is right, the same verbatim evidence a CFA root of trust already produces is sufficient for automatic localization of the corrupting instruction and for automatic generation of a validated binary patch.
  • Hash-based and hybrid evidence formats can only support violation detection, not the audit-and-remediate loop, so attestation architectures that want remote remediation should keep verbatim destinations rather than compressing them into digests.
  • Because SABRE works from the binary alone, it can patch proprietary or third-party embedded components whose source code is unavailable, as long as the binary and the verbatim log reach the verifier.
  • The patched binary is itself rechecked by the same symbolic analysis over a translated log, so the verifier can distinguish a successful remediation from an attack caused by a second vulnerability.

Reading between the lines

Editorial extensions of the paper, not claims the author makes directly.

  • The paper's evidence-fidelity argument suggests a design principle for future CFA systems: any optimization that loses verbatim destination information trades away verifier-side auditability, so those savings should be weighed against the loss of automatic remediation rather than against detection alone.
  • The same slice-based symbolic data-flow analysis could plausibly be applied to data-flow attestation logs to localize non-control-data attacks, an extension the paper explicitly leaves open.
  • SABRE's heuristics could be stress-tested beyond the evaluated benchmark set by compiling real-world MCU firmware with known vulnerabilities and checking whether the first-write and repeated-node assumptions still identify the correct fault for heap overflows and single-shot stack overflows.
Share X Bluesky LinkedIn Reddit HN

Signed reviews

No signed human review yet.

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, and a circularity audit.

Referee Report

4 major / 5 minor

Summary. The paper argues that run-time attestation and auditing are only useful if the verifier (Vrf) can analyze the received evidence. It classifies existing CFA evidence into three types: hash-based (E1), verbatim (E2), and hybrid (E3), and argues that E2 is the only type that supports root-cause analysis and remediation. As a case study, it presents SABRE, a verifier-side analysis engine that takes an application binary and a verbatim CFLog, verifies the path, locates the corrupting instruction via backward traversal and symbolic data-flow analysis, classifies the vulnerability as buffer overflow or use-after-free, generates binary patches without source code, and validates those patches by re-running symbolic analysis on the patched binary. The prototype is evaluated on MSP430 and ARM Cortex-M33 binaries using the ACFA and TRACES CFA architectures, with crafted exploits inserted into BEEBS benchmark programs, measuring per-module run-times and patch sizes.

Significance. If the claimed capability holds, SABRE would be a valuable step toward verifier-side auditing for low-end MCUs, addressing a largely unexplored part of the CFA workflow. The taxonomy of evidence types (E1/E2/E3) and the explicit focus on Vrf's analytical capabilities are useful conceptual contributions, and the authors provide an open-source prototype running on two different architectures and two real CFA systems. However, the current evaluation does not establish the headline claim of automatically generated, validated binary patches: the experiments report only run-times and patch sizes, not detection success/failure rates, false positives, or independent validation that the patches block the original attacks on real hardware. The Patch Validator reuses the same symbolic analysis that found the vulnerability, and the core heuristics in the Exploit Locator are not stress-tested against realistic failure modes. The approach is therefore promising and the manuscript is likely fixable, but the evidence as presented is insufficient for acceptance in its current form.

major comments (4)
  1. [Section 5.1, Fig. 10] The evaluation reports only per-module run-times (Fig. 10) and patch sizes (Section 5.2). It never reports detection success/failure counts, false positive/negative rates, whether the Patch Validator ever rejected a patch, or whether the patched binaries were re-executed against the original exploits on real hardware or in an emulator. Without these correctness measures, the claim in Section 7 that the prototype 'demonstrates its effectiveness' is not supported by the presented data.
  2. [Section 4.4] The Patch Validator reuses the same symbolic data-flow analysis as the Exploit Locator (Section 4.2, Algorithm 1): it performs symbolic DF analysis over the translated CFSlice and declares the patch effective when addr_target is no longer corrupted. Because the underlying model, memory tracking, and heuristics are identical, any false positive in the Exploit Locator (e.g., misattributing the corrupting write due to aliasing, unmodeled memory effects, or the loop/stack-frame heuristics) will also make the validator report success for a patch that does not actually block the attack. The paper does not provide independent validation, such as re-executing the patched binary against the original exploit or functional regression tests, so the 'validated' claim in contribution (3) is circular and remains unestablished.
  3. [Section 4.2, Algorithm 1 and Phase 3] The Exploit Locator's correctness rests on load-bearing assumptions: (a) the corrupting write is the first memory write to the symbolic base value X in CFSlice, (b) a buffer overflow manifests as a CFG node executed multiple times in the slice, and (c) buffer bounds can be approximated from stack-frame structure when source-code semantics are absent. The evaluation uses crafted, simple vulnerabilities inserted into BEEBS programs (Section 5.1) and does not exercise cases where these assumptions break, such as aliasing or address arithmetic that symbolic execution cannot resolve, single-shot overflows outside a loop, or bounds that cannot be inferred from the binary. Appendix B acknowledges some of these restrictions, but the paper does not quantify how often SABRE succeeds or fails under such conditions. The generality of the root-cause-analysis claim is therefore not yet supported.
  4. [Section 4.3.2, T1] The buffer-bounds estimation can over-approximate the buffer's bounds, and the generated patch silently skips out-of-bounds writes. The paper does not evaluate functional regressions of the patched binaries or verify that the bounds checks preserve the intended behavior of the benchmark programs beyond the single injected attack. For a system whose stated purpose is remediation, the lack of regression testing and the absence of any independent confirmation that the patched binaries are both secure and functionally equivalent are significant gaps in the evidence.
minor comments (5)
  1. [Section 3.2] The claim that E1 evidence 'completely precludes any analysis of exploit root causes' is stated categorically; while the path-explosion argument is plausible, the discussion would benefit from acknowledging that even for E2 the analysis relies on heuristics, and from citing the relevant complexity argument more precisely.
  2. [Figure 10] The figure caption lists ARM-UAF, ARM-OVF, MSP-UAF, and MSP-OVF in the legend, but the legend is not visually clear in the figure as rendered; a table with the numerical run-times per benchmark and per vulnerability type would be easier for readers to verify the claims in Section 5.1.
  3. [Algorithm 1] The pseudocode uses the helper functions AddConsts and eval without defining their semantics; a short description, or a pointer to the implementation in the open-source repository, would make the algorithm self-contained.
  4. [Table 1] The notation for addr_lower, addr_upper, reg_acc, and reg_init_acc is introduced in Table 1 but some symbols are only explained later in Section 4.3.2; consider adding a cross-reference or a consolidated notational example near the table.
  5. [References] Reference [12] contains a typo in the author list: 'Adam Caulfield and otehrs' should be 'Adam Caulfield et al.'

Circularity Check

0 steps flagged · score 0.0 of 10

No significant circularity: SABRE's analyses are computed from independent inputs (binary + verbatim CFlLog); the patch-validator reuse is a validation limitation, not a circular reduction.

full rationale

SABRE's derivation chain is self-contained. The Exploit Locator consumes App.elf and E2 CFlLog and computes CFSlice, base, and the corrupting instruction through backward traversal and symbolic data-flow analysis (Sec. 4.2, Algorithm 1); no parameter is fitted to data, and no output is restated as an input. The Patch Validator (Sec. 4.4) reuses the same symbolic data-flow analysis on the patched binary: 'Patch Validator then performs symbolic DF analysis over the translated CFlSlice, similar to how it is done in Sec. 4.2. When the analysis reaches the end of CFlSlice without addr_target being corrupted, Patch Validator considers this patch effective.' This makes validation model-internal—a false positive in the locator would be re-confirmed by the validator—and the evaluation reports only sub-module run-times rather than independent success/failure or re-execution on hardware. That is an evidence/correctness limitation, not circularity: the validator's verdict is a fresh computation on the patched binary and translated trace, not an input that is returned unchanged. Self-citations (ACFA, TRACES, SpecCFA) are used as external open-source testbeds/options, not as load-bearing mathematical premises; removing them would not affect the formal structure of SABRE's algorithms.

Assumptions & free parameters 0 free parameters · 5 assumptions · 0 invented entities

The central claims rest on the CFA evidence being authentic and verbatim (from prior architectures), and on several modeling heuristics in SABRE that are not validated against diverse attack patterns: single-write corruption detection, loop-based overflow classification, and stack-frame buffer bounds. No numeric free parameters are fitted to data.

assumptions (5)
  • ad hoc to paper The corrupted control data is always overwritten by a memory write directly to a location that symbolic execution can identify as the symbolic base X, and the first such write in CFSlice is the corrupting instruction.
    Algorithm 1 returns at the first memory write where a = X, so multi-path or aliased corruption that symbolic analysis cannot resolve is outside the model.
  • ad hoc to paper A buffer overflow vulnerability is detectable by the heuristic that the CFG node containing the offending write executes multiple times in CFSlice.
    Section 4.2 Phase 3: when base is not in FreeList and the CFG node containing addr_acc has been executed multiple times in CFSlice, single-instruction or non-loop overflows are misclassified.
  • domain assumption The CFG reconstructed from objdump disassembly is complete and correct for the attested binary.
    Section 4.1 relies on objdump for static analysis; obfuscation or indirect control flow beyond simple MCU binaries could break CFG construction.
  • domain assumption The verifier receives authentic and complete verbatim E2 evidence, with loop counters and branch destinations in the format produced by ACFA and TRACES.
    SABRE assumes the evidence format and integrity are guaranteed by the underlying CFA root of trust, as stated in Sections 2.3 and 4.1.
  • ad hoc to paper The upper bound of an overflowing buffer can be approximated by the stack frame or by base when the true bounds are not inferable from the binary.
    Section 4.3.2 T1: when addr_upper cannot be determined, SABRE defaults to using base as the upper bound, which may over- or under-estimate the true buffer size.

how reviews work

0 comments
Cite this review

Pith. "Pith review of On the Verification of Control Flow Attestation Evidence." pith.science (2026). https://pith.science/paper/M3TQSY7E

@misc{pith2026241110855,
  author       = {Pith},
  title        = {Pith review of: On the Verification of Control Flow Attestation Evidence},
  year         = {2026},
  howpublished = {\url{https://pith.science/paper/M3TQSY7E}},
  note         = {Machine review of arXiv:2411.10855}
}
read the original abstract

Remote run-time attestation methods, including Control Flow Attestation (CFA) and Data Flow Attestation (DFA), have been proposed to generate precise evidence of execution's control flow path (in CFA) and optionally execution data inputs (in DFA) on a remote and potentially compromised embedded device, hereby referred to as a Prover (Prv). Recent advances in run-time attestation architectures are also able to guarantee that a remote Verifier (Vrf) reliably receives this evidence from Prv, even when Prv's software state is fully compromised. This, in theory, enables secure "run-time auditing" in addition to best-effort attestation, i.e., it guarantees that Vrf can examine execution evidence to identify previously unknown compromises as soon as they are exploited, pinpoint their root cause(s), and remediate them. However, prior work has for the most part focused on securely implementing Prv's root of trust (responsible for generating authentic run-time evidence), leaving Vrf 's perspective in this security service unexplored. In this work, we argue that run-time attestation and auditing are only truly useful if Vrf can effectively analyze received evidence. From this premise, we characterize different types of evidence produced by existing run-time attestation/auditing architectures in terms of Vrf 's ability to detect and remediate (previously unknown) vulnerabilities. As a case study for practical uses of run-time evidence by Vrf, we propose SABRE: a Security Analysis and Binary Repair Engine. SABRE showcases how Vrf can systematically leverage run-time evidence to detect control flow attacks, pinpoint corrupted control data and specific instructions used to corrupt them, and leverage this evidence to automatically generate binary patches to buffer overflow and use-after-free vulnerabilities without source code knowledge.

Figures

Figures reproduced from arXiv: 2411.10855 by the authors.

Figure 1
Figure 1. RA interaction approaches incorporate dedicated hardware RoT for storing secret keys and computing the measurement [36, 49, 56, 62, 72]. Since such hardware is too costly for low-end MCUs, recent approaches have proposed “hybrid” RoTs [6, 24, 50], which use hardware for storing secret keys and trusted software for performing the authenticated measurement. 2.2 Code Reuse and Control Flow Attacks Control flow attacks … view at source ↗
Figure 2
Figure 2. A conditional branch (CB), indirect/direct calls [PITH_FULL_IMAGE:figures/full_fig_p003_2.png] view at source ↗
Figure 3
Figure 3. SABRE sub-modules and internal workflow Evidence types E2 and E3 allow Vrf to use reported traces to traverse the CFG, checking the reported destination against valid destinations. When there is a mismatch between the reported destination and the set of valid destinations for that branching instruction, Vrf determines that Prv executed an invalid path. With both E2 and E3, Vrf is able to emulate an SS of return addr… view at source ↗
Figures from the paper (4 more)
Figure 4
Figure 4. Figure 4: CFG and C𝐹𝐿𝑜𝑔 [PITH_FULL_IMAGE:figures/full_fig_p005_4.png]
Figure 7
Figure 7. Figure 7: Example patch for use￾after-free vulnerabilities [PITH_FULL_IMAGE:figures/full_fig_p007_7.png]
Figure 9
Figure 9. Figure 9: Example patch for buffer overflow vulnerabilities. [PITH_FULL_IMAGE:figures/full_fig_p008_9.png]
Figure 10
Figure 10. Figure 10: Run-time of SABRE submodules (ms) to analyze evidence of buffer overflow (OVF) and use-after-free (UAF) vulnerabil￾ities on two MCUs and CFA architectures: hardware-based CFA atop MSP430 [12] and TEE-based CFA atop ARM Cortex-M33 [10]. the main function, causing an in…

Discussion (0). Continue with ORCID to comment.

Reference graph

Works this paper leans on

90 extracted references · 77 canonical work pages

  1. [1]

    Tigist Abera et al. 2016. C-FLAT: control-flow attestation for embedded systems software. In Proceedings of the 2016 ACM SIGSAC Conference on Computer and Communications Security (CCS). 743–754

    2016

  2. [2]

    Mahmoud Ammar et al . 2024. SoK: Integrity, Attestation, and Auditing of Program Execution. In 2025 IEEE Symposium on Security and Privacy (SP) . IEEE Computer Society, 77–77

    2024

  3. [3]

    Md Armanuzzaman et al. 2025. ENOLA: Efficient Control-Flow Attestation for Embedded Systems. arXiv preprint arXiv:2501.11207 (2025)

    arXiv 2025

  4. [4]

    Roberto Baldoni et al. 2018. A survey of symbolic execution techniques. ACM Computing Surveys (CSUR) 51, 3 (2018), 1–39

    2018

  5. [5]

    Tyler Bletsch et al. 2011. Jump-oriented programming: a new class of code-reuse attack. In Proceedings of the 6th ACM symposium on information, computer and communications security (CCS). 30–40

    2011

  6. [6]

    Ferdinand Brasser et al . 2015. TyTAN: Tiny trust anchor for tiny devices. In Proceedings of the 52nd annual design automation conference (DAC) . 1–6

    2015

  7. [7]

    Nathan Burow et al. 2019. SoK: Shining light on shadow stacks. In IEEE Sympo- sium on Security and Privacy (SP) . IEEE, 985–999

    2019

  8. [8]

    Adam Caulfield et al. 2022. ASAP: reconciling asynchronous real-time operations and proofs of execution in simple embedded systems. In Proceedings of the 59th ACM/IEEE Design Automation Conference (DAC). 721–726

    2022

Show all 90 references
  1. [9]

    Adam Caulfield et al. 2024. SpecCFA: Enhancing Control Flow Attestation/Au- diting via Application-Aware Sub-Path Speculation. (2024), 563–578

    2024

  2. [10]

    Adam Caulfield et al. 2024. TRACES: TEE-based Runtime Auditing for Commod- ity Embedded Systems. (2024), 257–270

    2024

  3. [11]

    Adam Caulfield et al . 2025. Github Repository for SABRE Prototype. https: //github.com/SPINS-RG/SABRE

    2025

  4. [12]

    Adam Caulfield and otehrs. 2023. ACFA: Secure Runtime Auditing & Guaranteed Device Healing via Active Control Flow Attestation. In 32nd USENIX Security Symposium. USENIX Association, 5827–5844

    2023

  5. [13]

    Long Cheng et al. 2019. Exploitation techniques and defenses for data-oriented attacks. In 2019 IEEE Cybersecurity Development (SecDev) . IEEE, 114–128

    2019

  6. [14]

    Marco Chilese et al. 2024. One for All and All for One: GNN-based Control-Flow Attestation for Embedded Devices. In IEEE Symposium on Security and Privacy (SP). IEEE, 203–203

    2024

  7. [15]

    Bob Lord (CISA). 2023. The Urgent Need for Memory Safety in Software Prod- ucts. https://www.cisa.gov/news-events/news/urgent-need-memory-safety- software-products

    2023

  8. [16]

    George Coker et al. 2011. Principles of remote attestation. International Journal of Information Security 10 (2011), 63–81

    2011

  9. [17]

    Crispin Cowan et al . 2000. Buffer overflows: Attacks and defenses for the vulnerability of the decade. In Proceedings DARPA Information Survivability Conference and Exposition (DISCEX) , Vol. 2. IEEE, 119–129

    2000

  10. [18]

    Heini Bergsson Debes et al. 2023. ZEKRA: Zero-Knowledge Control-Flow At- testation. In Proceedings of the 2023 ACM Asia Conference on Computer and Communications Security (AsiaCCS). 357–371

    2023

  11. [19]

    Ioannis Deligiannis and George Kornaros. 2016. Adaptive memory manage- ment scheme for MMU-less embedded systems. In 11th Symposium on Industrial Embedded Systems (SIES). IEEE, 1–8

    2016

  12. [20]

    Ghada Dessouky et al. 2017. LO-FAT: Low-overhead control flow attestation in hardware. In Proceedings of the 54th Annual Design Automation Conference (DAC). 1–6

    2017

  13. [21]

    Ghada Dessouky et al. 2018. Litehax: lightweight hardware-assisted attestation of program execution. In International Conference on Computer-Aided Design (ICCAD). IEEE, 1–8

    2018

  14. [22]

    Ruian Duan et al. 2019. Automating Patching of Vulnerable Open-Source Soft- ware Versions in Application Binaries.. InNetwork and Distributed System Security (NDSS) Symposium

    2019

  15. [23]

    Gregory J Duck et al. 2020. Binary rewriting without control flow recovery. In Proceedings of the 41st ACM SIGPLAN conference on programming language design and implementation (PLDI). 151–163

    2020

  16. [24]

    Karim Eldefrawy et al . 2012. SMART: Secure and Minimal Architecture for (Establishing Dynamic) Root of Trust. InNetwork and Distributed System Security (NDSS) Symposium, Vol. 12. 1–15

    2012

  17. [25]

    Karim Eldefrawy, Michael Locasto, Norrathep Rattanavipanon, and Hassen Saidi

  18. [26]

    Free Software Foundation. 2024. arm-none-eabi-objdump man page. https://manpages.debian.org/unstable/binutils-arm-none-eabi/arm-none-eabi- objdump.1.en.html

    2024

  19. [27]

    Free Software Foundation. 2024. msp430-objdump man page. https://manpages. debian.org/testing/binutils-msp430/msp430-objdump.1.en.html

    2024

  20. [28]

    Python Software Foundation. 2024. Python libary pyelftools. https://pypi.org/ project/pyelftools/0.20/

    2024

  21. [29]

    Munir Geden and Kasper Rasmussen. 2019. Hardware-assisted remote runtime attestation for critical embedded systems. In 17th International Conference on Privacy, Security and Trust (PST) . IEEE, 1–10

    2019

  22. [30]

    Intel. 2015. Intel Processor Trace. https://edc.intel.com/content/www/ us/en/design/ipla/software-development-platforms/client/platforms/alder- lake-desktop/12th-generation-intel-core-processors-datasheet-volume-1-of- 2/010/intel-processor-trace/. [Online; accessed 14-March-2025]

    2015

  23. [31]

    Hakan Kayan et al. 2022. Cybersecurity of industrial cyber-physical systems: a review. ACM Computing Surveys (CSUR) 54, 11s (2022), 1–35

    2022

  24. [32]

    Rick Kennell and Leah H Jamieson. 2003. Establishing the genuinity of remote computer systems. In 12th USENIX Security Symposium

    2003

  25. [33]

    Keystone. 2024. Keystone: the ultimate assembler. https://www.keystone- engine.org/

    2024

  26. [34]

    Pantea Kiaei et al . 2021. Rewrite to reinforce: Rewriting the binary to apply countermeasures against fault injection. In 58th Design Automation Conference (DAC). IEEE, 319–324

    2021

  27. [35]

    James C King. 1976. Symbolic execution and program testing. Commun. ACM 19, 7 (1976), 385–394

    1976

  28. [36]

    Xeno Kovah et al. 2012. New results for timing-based attestation. In IEEE Sym- posium on Security and Privacy (SP) . IEEE, 239–253

    2012

  29. [37]

    Runhao Liu et al. 2022. SEEKER: A root cause analysis method based on deter- ministic replay for multi-type network protocol vulnerabilities. In International Conference on Trust, Security and Privacy in Computing and Communications (TrustCom). IEEE, 131–138

    2022

  30. [38]

    Miguel Masmano et al. 2003. Dynamic storage allocation for real-time embedded systems. Proc. of Real-Time System Simposium WIP (2003)

    2003

  31. [39]

    The MITRE Corporation (MITRE). 2024. 2024 CWE Top 25 Most Dangerous Soft- ware Weaknesses. https://cwe.mitre.org/top25/archive/2024/2024_cwe_top25. html

    2024

  32. [40]

    Muhammad Nouman Nafees et al. 2023. Smart grid cyber-physical situational awareness of complex operational technology attacks: A review.Comput. Surveys 55, 10 (2023), 1–36

    2023

  33. [41]

    National Vulnerability Database. 2017. CVE-2017-14201. https://nvd.nist.gov/ vuln/detail/CVE-2017-14201 Accessed: 2025-May-04

    2017

  34. [42]

    National Vulnerability Database. 2020. CVE-2019-16127. https://nvd.nist.gov/ vuln/detail/CVE-2019-16127 Accessed: 2025-May-04

    2020

  35. [43]

    National Vulnerability Database. 2020. CVE-2020-10019. https://nvd.nist.gov/ vuln/detail/CVE-2020-10019 Accessed: 2025-May-04

    2020

  36. [44]

    National Vulnerability Database. 2020. CVE-2020-10023. https://nvd.nist.gov/ vuln/detail/CVE-2020-10023 Accessed: 2025-May-04

    2020

  37. [45]

    National Vulnerability Database. 2021. CVE-2021-0920. https://nvd.nist.gov/ vuln/detail/CVE-2021-0920 Accessed: 2025-May-04

    2021

  38. [46]

    National Vulnerability Database. 2021. CVE-2021-35395. https://nvd.nist.gov/ vuln/detail/CVE-2021-35395 Accessed: 2025-May-04

    2021

  39. [47]

    National Vulnerability Database. 2022. CVE-2022-34835. https://nvd.nist.gov/ vuln/detail/CVE-2022-34835 Accessed: 2025-May-04

    2022

  40. [48]

    Antonio Joia Neto and Ivan De Oliveira Nunes. 2023. ISC-FLAT: On the Conflict Between Control Flow Attestation and Real-Time Operations. In 29th Real-Time and Embedded Technology and Applications Symposium (RTAS) . IEEE, 133–146

    2023

  41. [49]

    Job Noorman et al. 2017. Sancus 2.0: A low-cost security architecture for iot devices. ACM Transactions on Privacy and Security (TOPS) 20, 3 (2017), 1–33

    2017

  42. [50]

    Ivan De Oliveira Nunes et al. 2019. VRASED: A Verified Hardware/Software Co- Design for Remote Attestation. In 28th USENIX Security Symposium . 1429–1446

    2019

  43. [51]

    Ivan De Oliveira Nunes et al. 2020. APEX: A verified architecture for proofs of execution on remote devices under full software compromise. In 29th USENIX Security Symposium. 771–788

    2020

  44. [52]

    Ivan De Oliveira Nunes et al. 2021. Dialed: Data integrity attestation for low-end embedded devices. In 58th Design Automation Conference (DAC). IEEE, 313–318

    2021

  45. [53]

    Ivan De Oliveira Nunes et al. 2021. Tiny-CFA: Minimalistic control-flow attes- tation using verified proofs of execution. In 2021 Design, Automation & Test in Europe Conference & Exhibition (DATE). IEEE, 641–646

    2021

  46. [54]

    James Pallister et al. 2013. BEEBS: Open benchmarks for energy measurements on embedded platforms. arXiv preprint arXiv:1308.5174 (2013)

    2013 arXiv

  47. [55]

    Younggi Park et al. 2024. BENZENE: A Practical Root Cause Analysis System with an Under-Constrained State Mutation. In IEEE Symposium on Security and Privacy (SP). IEEE, 1865–1883

    2024

  48. [56]

    Nick L Petroni Jr et al. 2004. Copilot-a coprocessor-based kernel runtime integrity monitor.. In USENIX security symposium. San Diego, USA, 179–194

    2004

  49. [57]

    Prashant Hari Narayan Rajput et al. 2023. ICSPatch: Automated Vulnerability Localization and{Non-Intrusive} Hotpatching in Industrial Control Systems using Data Dependence Graphs. In32nd USENIX Security Symposium. 6861–6876

    2023

  50. [58]

    M Ramakrishna et al . 2008. Smart dynamic memory allocator for embedded systems. In 23rd International Symposium on Computer and Information Sciences (ISCIS). IEEE, 1–6

    2008

  51. [59]

    Ganesan Ramalingam. 1994. The undecidability of aliasing. ACM Transactions on Programming Languages and Systems (TOPLAS) 16, 5 (1994), 1467–1471

    1994

  52. [60]

    Realtek Semiconductor Corp. 2021. Realtek AP-Router SDK Advi- sory. https://www.realtek.com/images/safe-report/Realtek_APRouter_SDK_ Advisory-CVE-2021-35392_35395.pdf Accessed: 2025-May-04. Adam Ilyas Caulfield, Norrathep Rattanavipanon, and Ivan De Oliveira Nunes

    2021

  53. [61]

    Ryan Roemer et al. 2012. Return-oriented programming: Systems, languages, and applications. ACM Transactions on Information and System Security (TISSEC) 15, 1 (2012), 1–34

    2012

  54. [62]

    Dries Schellekens, Brecht Wyseur, and Bart Preneel. 2008. Remote attestation on legacy operating systems with trusted platform modules. Science of Computer Programming 74, 1-2 (2008), 13–22

    2008

  55. [63]

    Arvind Seshadri et al. 2004. SWATT: Software-based attestation for embedded devices. In IEEE Symposium on Security and Privacy (SP) . IEEE, 272–282

    2004

  56. [64]

    Arvind Seshadri et al . 2005. Pioneer: verifying code integrity and enforcing untampered code execution on legacy systems. In Proceedings of the twentieth ACM symposium on Operating Systems Principles (SOSP) . 1–16

    2005

  57. [65]

    Arvind Seshadri et al. 2008. SAKE: Software attestation for key establishment in sensor networks. In Distributed Computing in Sensor Systems (DCOSS) . 372–385

    2008

  58. [66]

    Hovav Shacham et al. 2004. On the effectiveness of address-space randomization. In Proceedings of the 11th ACM conference on Computer and communications security (CCS). 298–307

    2004

  59. [67]

    Zhichuang Sun et al . 2020. OAT: Attesting operation integrity of embedded devices. In IEEE Symposium on Security and Privacy (SP) . IEEE, 1433–1449

    2020

  60. [68]

    Swiftloke. 2024. Github Repository for MSProbe. https://github.com/Swiftloke/ MSProbe

    2024

  61. [69]

    Xi Tan et al. 2024. SoK:Where’s the “up”?! A Comprehensive (bottom-up) Study on the Security of Arm Cortex-M Systems. In 18th USENIX WOOT Conference on Offensive Technologies (WOOT). 149–169

    2024

  62. [70]

    SymPy Development Team. 2024. sympy. https://docs.sympy.org/latest/index. html

    2024

  63. [71]

    Flavio Toffalini et al. 2019. ScaRR: Scalable Runtime Remote Attestation for Com- plex Systems. In 22nd International Symposium on Research in Attacks, Intrusions and Defenses (RAID). 121–134

    2019

  64. [72]

    Jo Vliegen et al. 2019. SACHa: Self-attestation of configurable hardware. InDesign, Automation & Test in Europe Conference & Exhibition (DATE) . IEEE, 746–751

    2019

  65. [73]

    Jinwen Wang et al . 2023. ARI: Attestation of Real-time Mission Execution Integrity. In 32nd USENIX Security Symposium . 2761–2778

    2023

  66. [74]

    Minghua Wang et al. 2015. Binary code continent: Finer-grained control flow integrity for stripped binaries. In Proceedings of the 31st annual computer security applications conference (ACSAC). 331–340

    2015

  67. [75]

    Richard Wartell et al . 2012. Securing untrusted code via compiler-agnostic binary rewriting. InProceedings of the 28th Annual Computer Security Applications Conference (ACSAC). 299–308

    2012

  68. [76]

    Matthias Wenzl et al. 2019. From hack to elaborate technique—a survey on binary rewriting. ACM Computing Surveys (CSUR) 52, 3 (2019), 1–37

    2019

  69. [77]

    David Williams-King et al. 2020. Egalito: Layout-agnostic binary recompilation. In Proceedings of the 25th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS) . 133–147

    2020

  70. [78]

    Zhengzi Xu et al. 2020. Automatic hot patch generation for android kernels. In 29th USENIX Security Symposium . 2397–2414

    2020

  71. [79]

    Nikita Yadav and Vinod Ganapathy. 2023. Whole-Program Control-Flow Path Attestation. In Proceedings of the 2023 ACM SIGSAC Conference on Computer and Communications Security (CCS). 2680–2694

    2023

  72. [80]

    Carter Yagemann et al. 2021. ARCUS: symbolic root cause analysis of exploits in production systems. In 30th USENIX Security Symposium . 1989–2006

    2021

  73. [81]

    Carter Yagemann et al. 2021. Automated bug hunting with data-driven sym- bolic root cause analysis. In Proceedings of the 2021 ACM SIGSAC Conference on Computer and Communications Security (CCS) . 320–336

    2021

  74. [82]

    Shaza Zeitouni et al. 2017. ATRIUM: Runtime attestation resilient under memory attacks. In 2017 IEEE/ACM International Conference on Computer-Aided Design (ICCAD). IEEE, 384–391

    2017

  75. [83]

    Jun Zeng et al. 2022. Palantír: Optimizing attack provenance with hardware- enhanced system observability. InProceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security (CCS) . 3135–3149

    2022

  76. [84]

    Zephyr Project. 2016. Zephyr Repository. https://github.com/zephyrproject-rtos. Accessed: 2025-May-04

    2016

  77. [85]

    Chao Zhang et al . 2013. Practical control flow integrity and randomization for binary executables. In IEEE Symposium on Security and Privacy (SP) . IEEE, 559–573

    2013

  78. [86]

    Mingwei Zhang and R Sekar. 2015. Control flow and code integrity for COTS binaries: An effective defense against real-world ROP attacks. In Proceedings of the 31st Annual Computer Security Applications Conference (ACSAC) . 91–100

    2015

  79. [87]

    Xuewen Zhang et al. 2017. Embroidery: Patching vulnerable binary code of frag- mentized android devices. In International Conference on Software Maintenance and Evolution (ICSME). IEEE, 47–57

    2017

  80. [88]

    Yumei Zhang et al. 2021. ReCFA: resilient control-flow attestation. In Annual Computer Security Applications Conference (ACSAC). 311–322

    2021

  81. [89]

    Hao Zhou et al. 2022. NCScope: hardware-assisted analyzer for native code in android apps. In Proceedings of the 31st ACM SIGSOFT International Symposium on Software Testing and Analysis (ISSTA). 629–641. APPENDIX A Alternative Prover Configurations Alternative mechanisms such...

    2022

  82. [2020]

    In Applied Cryptography and Network Security (ACNS)

    Towards Automated Augmentation and Instrumentation of Legacy Cryp- tographic Executables. In Applied Cryptography and Network Security (ACNS) . Springer, 364–384

Pith tools

Reviewed August 12, 2026 · model on record in the stance chip above.