Interpretable Noninterference Measurement and its Application to Processor Designs
summary
DINoMe scales quantitative noninterference measurement to a full RISC-V BOOM Verilog core by translating Verilog to SMT2 with Yosys-to-SMT2, composing one-cycle transition formulas with #SAT-preserving optimizations, using model counting and sampling to compute a Jaccard distance leakage metric, and permitting declassification to exclude intended leaks. It trains gradient-boosted classifiers and extracts readable decision rules (precision/recall ranked) that explain leaks; case studies on cache side channels and Spectre rules show specific conditions—out-of-bounds offset plus particular branch predictor state plus differing secret bits—that cause measurable leakage.
AI-written summary · about
chapters (11)
- 0:00Introduction
- 0:14Data Privacy
- 0:53Complexity
- 2:03Problems
- 3:39Approach
- 5:54Security Model
- 6:44Quantitative Measurement
- 10:24Interpretability
- 11:30Code
- 12:59Information Linkage
- 14:34Conclusion
related talks
12mLeakage models are a leaky abstraction (...)
12mHardware Verification of Timing Side Channel Freedom in the Spectre Era
22mSNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations
24mSystem Level Security Verification of RISC V Based SoCs
35mTalk by Adria Gascon (Google)
14mCollapsing Towers for Side-Channel Security
17mSecuring High-performance RISC V-Processors from Time Speculation
01h 33mRISC V Verification for Processor Cores and Optional Custom Extensions