Hardware

[Google Scholar]

Notes:
Papers:

Hardware Faults

  • Stealthy dopant-level hardware Trojans [becker:ches:2013]
  • Formal verification of pipelined Y86-64 microprocessors with UCLID5 [bryant:cmu:2018]
  • SoK: Design tools for side-channel-aware implementations [buhan:ccs:2022]
  • Kami: A platform for high-level parametric hardware specification and its modular verification [choi:icfp:2017]
  • The last mile: An empirical study of timing channels on seL4 [cock:ccs:2014]
  • HyperFlow: A processor architecture for nonmalleable, timing-safe information flow security [ferraiuolo:ccs:2018]
  • Secure information flow verification with mutable dependent types [ferraiuolo:dac:2017]
  • Solver-aided constant-time hardware verification [gleissenthall:ccs:2021]
  • Balancing automation and control for formal verification of microprocessors [goel:cav:2021]
  • Verifying x86 instruction implementations [goel:cpp:2020]
  • Using x86isa for microcode verification [goel:spisa:2019]
  • Spectector: Principled detection of speculative information flows [guarnieri:sandp:2020]
  • ExTensor: An accelerator for sparse tensor algebra [hedge:micro:2019]
  • In-datacenter performance analysis of a tensor processing unit [jouppi:isca:2017]
  • Motivation for and evaluation of the first tensor processing unit [jouppi:micro:2018]
  • Secure autonomous cyber-physical systems through verifiable information flow control [liu:cpsspc:2018]
  • Verified compilation on a verified processor [loow:pldi:2019]
  • Theoretical analysis of gate level information flow tracking [oberg:dac:2010]
  • SIGMA: A sparse and irregular GEMM accelerator with flexible interconnects for DNN training [qin:hpca:2020]
  • Reasoning about a machine with local capabilities [skorstengaard:esop:2018]
  • StkTokens: Enforcing well-bracketed control flow and stack encapsulation using linear capabilities [skorstengaard:popl:2019]
  • Complete information flow tracking from the gates up [tiwari:asplos:2009]
  • Execution leases: A hardware-supported mechanism for enforcing strong non-interference [tiwari:isca:2009]
  • Crafting a usable microkernel, processor, and I/O system with strict and provable information flow security [tiwari:isca:2011]
  • Reticle: A virtual machine for programming modern FPGAs [vega:pldi:2021]
  • CacheQuery: Learning replacement policies from hardware caches [vila:pldi:2020]
  • A hardware design language for timing-sensitive information flow security [zhang:asplos:2015]