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]
The opinions expressed are my own views and not my employer’s.