对 CHERI 处理器进行全面的安全验证.pdf

1、VeriCHERI:Exhaustive Security Verification of CHERI ProcessorsRISC-V Summit Europe12.15.05.2025,ParisAnna Lena Duque Antn,Johannes Mller,Philipp Schmitz,Tobias Jauch,Alex Wezel,Lucas Deutschmann,Mohammed R.Fadiheh,Dominik Stoffel,and Wolfgang KunzSpeaker:Tobias Jauch2RISC-V Summit Europe 2025,ParisM

2、otivationGoal:robust and trustworthy security mechanismsMajor challenge:memory safetySolution:Capabilities/CHERI3RISC-V Summit Europe 2025,ParisSolution:Capabilities/CHERICHERICapability Hardware Enhanced RISC InstructionsFine-grained memory protection in hardwareGaining traction in industry4RISC-V

3、Summit Europe 2025,ParisCHERIMemoryArrayPointer+offsetCapabilitylower boundupper bound+permissions5RISC-V Summit Europe 2025,ParisChallenge:MotivationComprehensive security verification necessary6RISC-V Summit Europe 2025,ParisVerification based on a formal ISA model,rendering a high manual effort N

4、ienhuis et al.,Grisenthwaite et al.Related verification approaches:MotivationFunctional correctness proofs,automatically derived from the SAIL specification Ploix et al.7RISC-V Summit Europe 2025,ParisPitfalls:MotivationManual translation of functional security properties might not cover every aspec

5、t and corner case of the design Security verification based on time-abstract ISA models misses non-functional vulnerabilities(timing side channels)8RISC-V Summit Europe 2025,ParisProves global security objectives(confidentiality,integrity)VeriCHERIUses the timing-accurate RTL impementation9RISC-V Su

6、mmit Europe 2025,ParisAttacker ModelProcessortrustedMemory10RISC-V Summit Europe 2025,ParisProve global security objectives(confidentiality,integrity)Security ObjectiveGoal:Model security objectives using non-interferenceApproach:11RISC-V Summit Europe 2025,ParisSecurity ObjectiveModel security obje