PhD candidate @EPFL, I design and build systems we can trust.
- Tweets 28
- Following 144
- Followers 55
- Likes 134
![A snippet of code to verify the implementation of `mret` emulation in the Miralis virtual firmware monitor.
The function first create two symbolic contexts (i.e. where all registers are symbolic, that is they can be arbitrary values), and execute the `mret` instruction with both the Miralis instruction emulator and the reference Sail RISC-V model. If the resulting symbolic contexts are equal, the Miralis implementation is correct for all possible inputs.
```rust
/// Verify the emulation of the `mret` instruction.
#[cfg_attr(kani, kani::proof)]
pub fn check_mret() {
let (mut ctx, mut mctx, mut sail_ctx) =
symbolic::new_symbolic_contexts();
ctx.emulate_mret(&mut mctx); // Miralis implementation
execute_MRET(&mut sail_ctx); // Sail implementation
assert_eq!(
ctx,
adapters::sail_to_miralis(sail_ctx, &mctx),
"mret instruction emulation is not correct"
);
}
```](/pic/orig/media%2FGqsxzqaXUAIORkI.jpg)
ALT A snippet of code to verify the implementation of `mret` emulation in the Miralis virtual firmware monitor. The function first create two symbolic contexts (i.e. where all registers are symbolic, that is they can be arbitrary values), and execute the `mret` instruction with both the Miralis instruction emulator and the reference Sail RISC-V model. If the resulting symbolic contexts are equal, the Miralis implementation is correct for all possible inputs. ```rust /// Verify the emulation of the `mret` instruction. #[cfg_attr(kani, kani::proof)] pub fn check_mret() { let (mut ctx, mut mctx, mut sail_ctx) = symbolic::new_symbolic_contexts(); ctx.emulate_mret(&mut mctx); // Miralis implementation execute_MRET(&mut sail_ctx); // Sail implementation assert_eq!( ctx, adapters::sail_to_miralis(sail_ctx, &mctx), "mret instruction emulation is not correct" ); } ```
ALT A picture of the HiFive P550 development board.
