pith. sign in

arxiv: 2510.27485 · v2 · submitted 2025-10-31 · 💻 cs.CR · cs.OS· cs.PL

Sockeye: a language for analyzing hardware documentation

Ben Fiedler , Samuel Gruetter , Timothy Roscoe This is my paper

Pith reviewed 2026-05-18 02:50 UTC · model grok-4.3

classification 💻 cs.CR cs.OScs.PL
keywords hardware documentationformal verificationsecurity propertiesdomain-specific languagememory confidentialityreference manualsplatform securityvulnerability discovery
0
0 comments X

The pith

Sockeye turns prose hardware reference manuals into machine-readable models that support formal proofs of platform security or discovery of violations.

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

The paper introduces a domain-specific language called Sockeye for capturing hardware component semantics, software assumptions, and security goals directly from reference manuals. Authors built specifications for eight different platforms and used them to prove memory confidentiality and integrity in some cases while finding counterexamples in others. The work also surfaced several inaccuracies in the original documentation and identified a vulnerability in a real server chip that the vendor confirmed affects a broad line of deployed network appliances. This approach matters to systems programmers because informal prose descriptions make rigorous whole-platform security statements nearly impossible. If the modeling holds, integrators gain a concrete way to describe desired properties and either prove them or locate concrete flaws.

Core claim

We introduce a domain-specific language to describe hardware semantics, assumptions about software behavior, and desired security properties. We then create machine-readable specifications for a diverse set of eight platforms from their reference manuals, and formally prove their (in-)security. In addition to security proofs about memory confidentiality and integrity, we discover a handful of documentation errors. Finally, our analysis also revealed a vulnerability on a real-world server chip, which was confirmed by the vendor to apply to a wide family of deployed network appliances.

What carries the argument

Sockeye, a domain-specific language that encodes hardware semantics, software assumptions, and security properties from prose manuals into forms that support formal proof or counterexample search.

If this is right

  • Formal proofs of memory confidentiality and integrity become possible for complete hardware platforms rather than isolated components.
  • Systematic comparison of modeled behavior against manuals can surface documentation inaccuracies.
  • Analysis can reveal concrete vulnerabilities in deployed chips that vendors later confirm apply to families of products.

Where Pith is reading between the lines

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

  • The same modeling technique could be applied to interactions among multiple chips or boards rather than single platforms.
  • Hardware vendors might adopt similar formal descriptions to replace or supplement prose manuals in future releases.
  • Extending the language with timing or side-channel properties would allow checking additional classes of hardware attacks.

Load-bearing premise

The prose descriptions in reference manuals can be translated into the Sockeye language so that the resulting models faithfully represent actual hardware behavior.

What would settle it

A direct test on one of the modeled platforms where the real hardware exhibits a memory confidentiality or integrity violation that the Sockeye specification claims cannot occur.

Figures

Figures reproduced from arXiv: 2510.27485 by Ben Fiedler, Samuel Gruetter, Timothy Roscoe.

Figure 1
Figure 1. Figure 1: shows, at a high level, the process by which a secure configuration of the hardware is achieved, together with how Sockeye operates. Vendors create programming documentation for a modern SoC from the hardware design either manually, or semi-automatically. Based on this documentation, developers write system software (firmware or the OS) to configure the hardware. Executing this software results in a config… view at source ↗
Figure 2
Figure 2. Figure 2: shows how we represent this graph structure textually, as well as the corresponding graphical representation. As a future application of Sockeye, such diagrams could be automatically derived from the source code. A module specifies a blueprint for a component which can be instantiated multiple times as the child of another module, using the instance keyword. Instances thus form a tree, but if an instance n… view at source ↗
Figure 4
Figure 4. Figure 4: Record types for requests and responses 1 mut fn request(r: Request) -> Response { 2 if is_region_config_addr(r.address) { 3 let region_id = r.address[6 downto 5]; 4 let register_id = r.address[4 downto 3]; 5 if r.is_write { 6 config_write(region_id, register_id, r.value) 7 } else { 8 config_read(region_id, register_id) 9 } 10 } else if is_allowed_dram_addr(r) { 11 if r.is_write { 12 dram.store(r.address, … view at source ↗
Figure 5
Figure 5. Figure 5: shows the request handler inside module ASC that encodes (a simplification of) our understanding of the ThunderX-1’s hardware reference manual parts that specify how memory requests are handled. On line 2, the is_region_config_addr function (omitted here, but shown in full in appendix A) determines if an address lies in the MMIO address range of the region-configuring registers, while the config_write and … view at source ↗
Figure 7
Figure 7. Figure 7: Step function of the CPU CPU: request is { address: 0x8000_0000_0070u48, is_secure: false, is_write: true, value: 1 } ASC: Setting region3.ATTR to 1 CPU: request is { address: 0, is_secure: false, is_write: true, value: 0x48ad_c33c_fdc9_99d4u64 } DRAM: Storing 0x48ad_c33c_fdc9_99d4u64 to 0 [PITH_FULL_IMAGE:figures/full_fig_p004_7.png] view at source ↗
Figure 9
Figure 9. Figure 9: Induction proof HW safe? Documentation safe? Documentation faithful (i.e. unsafe in the same way)? Y N Y N Y N Y N Configuration safe? Anon finds spurious exploit (doc error) Anon finds exploit Anon can show that security property holds This is a HW bug out of the scope of our approach [PITH_FULL_IMAGE:figures/full_fig_p005_9.png] view at source ↗
Figure 10
Figure 10. Figure 10: Classification of Bugs for this invariant is given in appendix A. If no assertion violations are found in base_case or inductive_step, we know that invariant always holds, and using a third sce￾nario, invariant_is_useful, we can check that our invariant implies the desired security property. 5 [PITH_FULL_IMAGE:figures/full_fig_p005_10.png] view at source ↗
read the original abstract

The ever increasing complexity of hardware platforms poses a challenge to systems programmers. Correctly programming a multitude of components, providing functionality and security, is difficult: semantics of individual units are described in prose, underspecified, and prone to inaccuracies. Rigorous statements about platform security are often impossible. We introduce a domain-specific language to describe hardware semantics, assumptions about software behavior, and desired security properties. We then create machine-readable specifications for a diverse set of eight platforms from their reference manuals, and formally prove their (in-)security. In addition to security proofs about memory confidentiality and integrity, we discover a handful of documentation errors. Finally, our analysis also revealed a vulnerability on a real-world server chip, which was confirmed by the vendor to apply to a wide family of deployed network appliances. Our tooling offers system integrators a way of formally describing security properties for whole platforms, and the means to find counterexamples, or proving them correct.

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 / 1 minor

Summary. The paper introduces Sockeye, a domain-specific language to describe hardware semantics, software assumptions, and security properties. Machine-readable specifications are derived for eight diverse platforms directly from their reference manuals. Formal proofs are presented for memory confidentiality and integrity properties, a handful of documentation errors are identified, and a vulnerability is discovered on a real-world server chip that was confirmed by the vendor to affect a wide family of deployed network appliances.

Significance. If the Sockeye models accurately reflect deployed hardware, the work supplies a practical method for system integrators to obtain machine-checked statements about whole-platform security properties that are currently impossible from prose manuals alone. The combination of formal proofs, documentation-error discovery, and a vendor-confirmed real-world vulnerability demonstrates concrete utility in hardware security analysis.

major comments (2)
  1. [Abstract] Abstract: the central claim that formal proofs of (in-)security were obtained for eight platforms rests on the fidelity of the manual-to-Sockeye translation, yet the abstract supplies no information on the underlying logic, proof automation, or resolution of underspecification; this leaves the soundness of the security results only partially supported.
  2. [Specification construction] Specification construction sections: because every subsequent proof and the discovered vulnerability depend on the Sockeye artifacts matching actual hardware behavior, the paper must supply explicit validation steps (e.g., cross-checks against executable models, simulation traces, or additional silicon measurements) for the eight platforms; the single vendor confirmation does not substitute for systematic evidence across the corpus.
minor comments (1)
  1. [Language definition] Ensure that the definition of the Sockeye language constructs and the precise semantics of its security-property primitives appear before any claims that rely on them.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for their constructive comments on our manuscript. We address each of the major comments below, indicating the revisions we plan to make to improve the clarity and support for our claims.

read point-by-point responses

  1. Referee: [Abstract] Abstract: the central claim that formal proofs of (in-)security were obtained for eight platforms rests on the fidelity of the manual-to-Sockeye translation, yet the abstract supplies no information on the underlying logic, proof automation, or resolution of underspecification; this leaves the soundness of the security results only partially supported.

    Authors: We agree that the abstract should better contextualize the formal aspects of our work to support the soundness of the security results. The Sockeye DSL is defined over a logic that explicitly models hardware semantics, software assumptions, and handles underspecification by allowing for non-deterministic behaviors where manuals are ambiguous. Proofs are performed using automated tactics within a theorem prover. In the revised manuscript, we will expand the abstract to include a concise description of the underlying logic, the proof automation approach, and how underspecification is resolved, thereby strengthening the presentation of our central claims. revision: yes

  2. Referee: [Specification construction] Specification construction sections: because every subsequent proof and the discovered vulnerability depend on the Sockeye artifacts matching actual hardware behavior, the paper must supply explicit validation steps (e.g., cross-checks against executable models, simulation traces, or additional silicon measurements) for the eight platforms; the single vendor confirmation does not substitute for systematic evidence across the corpus.

    Authors: We acknowledge the referee's point that systematic validation evidence would further bolster confidence in the models. The manuscript details the construction process from reference manuals for the eight platforms and includes a vendor confirmation for the identified vulnerability on the server chip. For the remaining platforms, we performed internal consistency checks and cross-referenced with additional documentation sources. We will revise the specification construction sections to explicitly outline these validation steps and to discuss the limitations, including the absence of silicon measurements for all platforms due to practical constraints. This will provide a more transparent account of the evidence supporting the models. revision: partial

Circularity Check

0 steps flagged

No circularity: Sockeye is a constructive introduction of new language and platform models

full rationale

The paper introduces a new domain-specific language Sockeye to encode hardware semantics, software assumptions, and security properties directly from prose reference manuals. It then constructs machine-readable specifications for eight platforms and performs formal proofs of memory confidentiality and integrity within those models, along with empirical discovery of documentation errors and a vendor-confirmed vulnerability. These steps are additive and constructive rather than reductive; no equations, fitted parameters, or self-citations are invoked to derive the central results from the inputs by construction. The translation from manual prose to Sockeye is presented as a manual modeling effort whose fidelity is supported by the discovery of real errors and external confirmation, not by any internal self-definition or renaming of prior results. The derivation chain therefore remains self-contained and non-circular.

Axiom & Free-Parameter Ledger

0 free parameters · 1 axioms · 1 invented entities

The central claim rests on the ability to create faithful formal models from prose manuals; the main addition is therefore the new language and its verification workflow rather than new physical constants or fitted parameters.

axioms (1)
  • domain assumption Hardware reference manuals contain enough information to produce accurate formal models of component semantics and security properties
    The paper's workflow begins by translating prose manuals into Sockeye specifications; if this translation step systematically omits or misrepresents behavior, the subsequent proofs do not apply to real hardware.
invented entities (1)
  • Sockeye domain-specific language no independent evidence
    purpose: To express hardware semantics, software assumptions, and security properties in a machine-checkable form
    Newly defined in the paper as the core artifact enabling the formal analysis.

pith-pipeline@v0.9.0 · 5691 in / 1446 out tokens · 41753 ms · 2026-05-18T02:50:08.385762+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

40 extracted references · 40 canonical work pages

  1. [1]

    Velosiraptor: Code synthesis for memory translation

    Reto Achermann, Em Chu, Ryan Mehri, Ilias Karimalis, and Margo Seltzer. Velosiraptor: Code synthesis for memory translation. In Proceedingsofthe30thACMInternationalConferenceonArchitectural SupportforProgrammingLanguagesandOperatingSystems,Volume2 , ASPLOS’25,page1365–1381,NewYork,NY,USA,2025.Association for Computing Machinery

    work page 2025

  2. [2]

    Physical addressing on real hardware in isabelle/hol

    Reto Achermann, Lukas Humbel, David Cock, and Timothy Roscoe. Physical addressing on real hardware in isabelle/hol. InInternational Conference on Interactive Theorem Proving, pages 1–19. Springer, 2018

    work page 2018

  3. [3]

    Advanced Micro Devices, Inc.Processor Programming Reference (PPR) for AMD Family 17h Models A0h-AFh, Revision A0 Processors (PUB) (57243), August 2022

    work page 2022

  4. [4]

    Gray, Robert M

    Alasdair Armstrong, Thomas Bauereiss, Brian Campbell, Alastair Reid, Kathryn E. Gray, Robert M. Norton, Prashanth Mundkur, Mark Wassell, Jon French, Christopher Pulte, Shaked Flur, Ian Stark, Neel 12 Sockeye: a language for analyzing hardware documentation Krishnaswami, and Peter Sewell. Isa semantics for armv8-a, risc-v, and cheri-mips. Proc. ACM Program...

    work page 2019

  5. [5]

    ASPEED Technology, Inc.AST2600 Integrated Remote Management Processor A3 Datasheet, June 2022

    work page 2022

  6. [6]

    Klee: unassisted and automatic generation of high-coverage tests for complex systems programs

    Cristian Cadar, Daniel Dunbar, and Dawson Engler. Klee: unassisted and automatic generation of high-coverage tests for complex systems programs. InProceedingsofthe8thUSENIXConferenceonOperating Systems Design and Implementation, OSDI’08, page 209–224, USA,

    work page

  7. [7]

    CaviumThunderXCN88XX,Pass2 ,September

    Cavium(nowMarvell). CaviumThunderXCN88XX,Pass2 ,September

    work page

  8. [8]

    Document number CN88XX-HM-2.7P

    work page

  9. [9]

    Abstract interpretation: A uni- fied lattice model for static analysis of programs by construction or approximation of fixpoints

    Patrick Cousot and Radhia Cousot. Abstract interpretation: A uni- fied lattice model for static analysis of programs by construction or approximation of fixpoints. InProceedings of the 4th ACM SIGACT- SIGPLANSymposiumonPrinciplesofProgrammingLanguages ,POPL ’77, pages 238–252, New York, NY, USA, January 1977. Association for Computing Machinery

    work page 1977

  10. [10]

    Z3:anefficientsmtsolver

    LeonardoDeMouraandNikolajBjørner. Z3:anefficientsmtsolver. In Proceedings of the Theory and Practice of Software, 14th International Conference on Tools and Algorithms for the Construction and Analysis of Systems, TACAS’08/ETAPS’08, page 337–340, Berlin, Heidelberg,

    work page

  11. [11]

    Bidirectional Typing.ACM Comput

    Jana Dunfield and Neel Krishnaswami. Bidirectional Typing.ACM Comput. Surv., 54(5):98:1–98:38, May 2021

    work page 2021

  12. [12]

    Komodo: Using verification to disentangle secure-enclave hardware from software

    Andrew Ferraiuolo, Andrew Baumann, Chris Hawblitzel, and Bryan Parno. Komodo: Using verification to disentangle secure-enclave hardware from software. InProceedings of the 26th Symposium on Operating Systems Principles, SOSP ’17, page 287–305, New York, NY, USA, 2017. Association for Computing Machinery

    work page 2017

  13. [13]

    AFL++: Combining incremental steps of fuzzing research

    Andrea Fioraldi, Dominik Maier, Heiko Eißfeldt, and Marc Heuse. AFL++: Combining incremental steps of fuzzing research. In14th USENIX Workshop on Offensive Technologies (WOOT 20). USENIX Association, August 2020

    work page 2020

  14. [14]

    Libafl: A framework to build modular and reusable fuzzers

    AndreaFioraldi,DominikChristianMaier,DongjiaZhang, andDavide Balzarotti. Libafl: A framework to build modular and reusable fuzzers. In Proceedings of the 2022 ACM SIGSAC Conference on Computer and Communications Security, CCS ’22, page 1051–1065, New York, NY, USA, 2022. Association for Computing Machinery

    work page 2022

  15. [15]

    SoCFuzzer: SoCvulnerabilitydetectionusingcostfunctionenabledfuzz testing

    Muhammad Monir Hossain, Arash Vafaei, Kimia Zamiri Azar, Fahim Rahman, Farimah Farahmandi, and Mark Tehranipoor. SoCFuzzer: SoCvulnerabilitydetectionusingcostfunctionenabledfuzz testing. In 2023 Design, Automation & Test in Europe Conference & Exhibition (DATE), pages 1–6, 2023

    work page 2023

  16. [16]

    Proverit: A parame- terized, composable, and verified model of tee protection profile.IEEE Transactions on Dependable and Secure Computing, 21(6):5341–5358, 2024

    Jilin Hu, Fanlang Zeng, Yongwang Zhao, Zhuoruo Zhang, Leping Zhang, Jianhong Zhao, Rui Chang, and Kui Ren. Proverit: A parame- terized, composable, and verified model of tee protection profile.IEEE Transactions on Dependable and Secure Computing, 21(6):5341–5358, 2024

    work page 2024

  17. [17]

    Cbmc–c bounded model checker: (competition contribution)

    Daniel Kroening and Michael Tautschnig. Cbmc–c bounded model checker: (competition contribution). InInternational Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 389–391. Springer, 2014

    work page 2014

  18. [18]

    Specification and Verification of Strong Timing Isolation of Hardware Enclaves

    StellaLau,ThomasBourgeat,ClémentPit-Claudel,andAdamChlipala. Specification and Verification of Strong Timing Isolation of Hardware Enclaves. InProceedings of the 2024 on ACM SIGSAC Conference on Computer and Communications Security, CCS ’24, pages 1121–1135, New York, NY, USA, December 2024. Association for Computing Machinery

    work page 2024

  19. [19]

    Seshia, and Krste Asanovic

    Dayeol Lee, Kevin Cheang, Alexander Thomas, Catherine Lu, Pranav Gaddamadugu, Anjo Vahldiek-Oberwagner, Mona Vij, Dawn Song, Sanjit A. Seshia, and Krste Asanovic. Cerberus: A formal approach to secureandefficientenclavememorysharing.In Proceedingsofthe2022 ACM SIGSAC Conference on Computer and Communications Security, CCS ’22, page 1871–1885, New York, NY,...

    work page 2022

  20. [20]

    Design and verification of the arm confidential compute architecture

    Xupeng Li, Xuheng Li, Christoffer Dall, Ronghui Gu, Jason Nieh, Yousuf Sait, and Gareth Stockwell. Design and verification of the arm confidential compute architecture. In16th USENIX Symposium on Operating Systems Design and Implementation (OSDI 22), pages 465–484, Carlsbad, CA, July 2022. USENIX Association

    work page 2022

  21. [21]

    A FormalApproachtoConfidentialityVerificationinSoCsattheRegister TransferLevel

    Johannes Müller, Mohammad Rahmani Fadiheh, Anna Lena Duque Antón, Thomas Eisenbarth, Dominik Stoffel, and Wolfgang Kunz. A FormalApproachtoConfidentialityVerificationinSoCsattheRegister TransferLevel. In202158thACM/IEEEDesignAutomationConference (DAC), pages 991–996, December 2021

    work page 2021

  22. [22]

    AMD Sinkclose: Universal SMM Privilege Escalation

    Enrique Nissim and Krzysztof Okupski. AMD Sinkclose: Universal SMM Privilege Escalation. Presentation at DEFCON 32, August

    work page

  23. [23]

    https://www.ioactive.com/event/def-con-talk-amd-sinkclose- universal-ring-2-privilege-escalation/

    work page

  24. [24]

    NVIDIA Corporation.NVIDIA Parker Series SoC, v1.0p edition, June 2017

    work page 2017

  25. [25]

    Pierce and David N

    Benjamin C. Pierce and David N. Turner. Local type inference. In Proceedings of the 25th ACM SIGPLAN-SIGACT Symposium on Prin- ciples of Programming Languages, POPL ’98, pages 252–265, New York, NY, USA, January 1998. Association for Computing Machinery

    work page 1998

  26. [26]

    RP2350Datasheet:AmicrocontrollerbyRaspberry Pi, July 2025

    RaspberryPi,Ltd. RP2350Datasheet:AmicrocontrollerbyRaspberry Pi, July 2025

    work page 2025

  27. [27]

    Trustworthy specifications of ARM® v8-A and v8-M system level architecture

    Alastair Reid. Trustworthy specifications of ARM® v8-A and v8-M system level architecture. In2016 Formal Methods in Computer-Aided Design (FMCAD), pages 161–168, October 2016

    work page 2016

  28. [28]

    Who guards the guards? formal validation of the Arm v8-m architecture specification.Proc

    Alastair Reid. Who guards the guards? formal validation of the Arm v8-m architecture specification.Proc. ACM Program. Lang., 1(OOPSLA):88:1–88:24, October 2017

    work page 2017

  29. [29]

    Automaticdevicedriversynthesiswithtermite

    Leonid Ryzhyk, Peter Chubb, Ihor Kuz, Etienne Le Sueur, and Gernot Heiser. Automaticdevicedriversynthesiswithtermite. In Proceedings of the ACM SIGOPS 22nd Symposium on Operating Systems Princi- ples, SOSP ’09, pages 73–86, New York, NY, USA, October 2009. Association for Computing Machinery

    work page 2009

  30. [30]

    Cute: a concolic unit testingengineforc

    Koushik Sen, Darko Marinov, and Gul Agha. Cute: a concolic unit testingengineforc. In Proceedingsofthe10thEuropeanSoftwareEngi- neeringConferenceHeldJointlywith13thACMSIGSOFTInternational Symposium on Foundations of Software Engineering, ESEC/FSE-13, page 263–272, New York, NY, USA, 2005. Association for Computing Machinery

    work page 2005

  31. [31]

    RM0433 Reference manual, STM32H742, STM32H743/753 and STM32H750 Value line advanced Arm-based 32-bit MCUs, January 2023

    STMicroelectronics. RM0433 Reference manual, STM32H742, STM32H743/753 and STM32H750 Value line advanced Arm-based 32-bit MCUs, January 2023

    work page 2023

  32. [32]

    Texas Instruments.OMAP4460 Multimedia Device Silicon Revision 1.x Technical Reference Manual, version ab edition.http://www.ti.com/ product/omap4460, accessed 2015-02-10

    work page 2015

  33. [33]

    Growing solver-aided languages withRosette

    Emina Torlak and Rastislav Bodik. Growing solver-aided languages withRosette. InProceedingsofthe2013ACMInternationalSymposium on New Ideas, New Paradigms, and Reflections on Programming & Software,Onward!2013,pages135–152,NewYork,NY,USA,October

    work page 2013

  34. [35]

    A lightweight symbolic virtual machine for solver-aided host languages

    Emina Torlak and Rastislav Bodik. A lightweight symbolic virtual machine for solver-aided host languages. InProceedings of the 35th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI ’14, pages 530–541, New York, NY, USA, June

    work page

  35. [36]

    Association for Computing Machinery

    work page

  36. [37]

    Asurveyonassertion-basedhardwareverification

    Hasini Witharana, Yangdi Lyu, Subodha Charles, and Prabhat Mishra. Asurveyonassertion-basedhardwareverification. ACMComput.Surv. , 54(11s), September 2022

    work page 2022

  37. [38]

    ZynqUltraScale+MPSoCTechnicalReferenceManual ,ug1085 (v1.2) edition, June 2016

    Xilinx. ZynqUltraScale+MPSoCTechnicalReferenceManual ,ug1085 (v1.2) edition, June 2016

    work page 2016

  38. [39]

    YuhengYang,ThomasBourgeat,StellaLau,andMengjiaYan.Pensieve: Microarchitectural Modeling for Security Evaluation. InProceedings of the 50th Annual International Symposium on Computer Architecture, 13 Ben Fiedler, Samuel Gruetter, and Timothy Roscoe ISCA ’23, pages 1–15, New York, NY, USA, June 2023. Association for Computing Machinery

    work page 2023

  39. [40]

    Timing side-channel attacks and countermeasures in cpu microarchitectures

    Jiliang Zhang, Congcong Chen, Jinhua Cui, and Keqin Li. Timing side-channel attacks and countermeasures in cpu microarchitectures. ACM Comput. Surv., 56(7), April 2024

    work page 2024

  40. [41]

    DRAM: Loading {v} from {a}\n

    Junming Zhao, Miki Tanaka, Johannes Åman Pohjola, Alessandro Legnani,TianaTsangUng,H.Truong,TsunWangSau,ThomasSewell, Rob Sison, Hira Syeda, Magnus Myreen, Michael Norrish, and Gernot Heiser. Verifying device drivers with pancake, 2025. 14 Sockeye: a language for analyzing hardware documentation A Full source code of minimized example type PhysAddr = BitI...

    work page 2025