Validating Side Channel models in RISC-V using Model-Based Testing

Sammanfattning: Microarchitecture’s optimizations have increased the performance but lowered the security. Speculative execution is one of the optimizations that was thought to be secure, but it is exploitable to leak information. The problem with these exploits is that there is no easy software defence and many exploits could be unexplored due to it being a fairly recent discovery. This thesis explores a way to find code that is vulnerable to this. The solution to the problem is to use the tool Side Channel Abstract Model Validator (SCAMV) which implements the method Model-Based Testing (MBT). We examine the core CVA6, which is a RISCV Central Processing Unit (CPU). Test cases are generated by program generators and interesting ones are selected by applying an observational model to them. The observational model abstracts side-channel leakage of the microarchitecture. The selected test cases are executed on the platform to validate the used observational models. The results of the test cases showed no indication of modifying the side channels under speculative execution. The results showed that SCAMV can examine timing-based channels. The conclusion is that our findings indicate that the CVA6 core is not vulnerable to speculative cache or timing-based side-channel attacks.