Miri can detect Undefined Behavior, Memory Bugs and a lot more.
Making this hard is that Miri is not meant to be run for a kernel, so it doesn't know about certain memory mapped devices, changes to address translation, but also Miri cannot interpret programs that contain asm macros.
Describe your solution
Two things have to happen for this to work.
Firstly, Miri has to be modified to support address translation, this can be implemented similar to a real CPU with a TLB to accelerate translation.
Secondly, Microdragon needs to be changed to be more Miri frendly, mainly that asm macros have to be stubbed or replaced with Miri intrinsics.
Alternatives to your solution
We could just not run the kernel through Miri, but adding a tool like this to our pipeline is very valuable, so I would prefer to have it.
Describe your use case
Miri can detect Undefined Behavior, Memory Bugs and a lot more. Making this hard is that Miri is not meant to be run for a kernel, so it doesn't know about certain memory mapped devices, changes to address translation, but also Miri cannot interpret programs that contain asm macros.
Describe your solution
Two things have to happen for this to work. Firstly, Miri has to be modified to support address translation, this can be implemented similar to a real CPU with a TLB to accelerate translation. Secondly, Microdragon needs to be changed to be more Miri frendly, mainly that asm macros have to be stubbed or replaced with Miri intrinsics.
Alternatives to your solution
We could just not run the kernel through Miri, but adding a tool like this to our pipeline is very valuable, so I would prefer to have it.