Charly
@charlycst.bsky.social
Computer system researcher, working on OS, virtualization, and confidential computing.
The new `unsafe_op_in_unsafe_fn` warning in #rust 2024 is good in general, but for small functions with a single expression it creates a lot of unnecessary indentation... It would be cool if it were allowed to add `unsafe` in front of a `match` or `if` to reduce indentation in those cases.
October 23, 2025 at 3:34 PM
The new `unsafe_op_in_unsafe_fn` warning in #rust 2024 is good in general, but for small functions with a single expression it creates a lot of unnecessary indentation... It would be cool if it were allowed to add `unsafe` in front of a `match` or `if` to reduce indentation in those cases.
Packing for SOSP 2025!
October 10, 2025 at 10:40 PM
Packing for SOSP 2025!
I am building a tool to test and verify inline assembly in Rust, and of course I am finding bugs in my code.
Quiz: what is wrong there?
```
// Skip illegal instruction (pc += 4)
csrrw x5, mepc, x5
addi x5, x5, 4
csrrw x5, mepc, x5
```
Quiz: what is wrong there?
```
// Skip illegal instruction (pc += 4)
csrrw x5, mepc, x5
addi x5, x5, 4
csrrw x5, mepc, x5
```
September 4, 2025 at 3:32 AM
I am building a tool to test and verify inline assembly in Rust, and of course I am finding bugs in my code.
Quiz: what is wrong there?
```
// Skip illegal instruction (pc += 4)
csrrw x5, mepc, x5
addi x5, x5, 4
csrrw x5, mepc, x5
```
Quiz: what is wrong there?
```
// Skip illegal instruction (pc += 4)
csrrw x5, mepc, x5
addi x5, x5, 4
csrrw x5, mepc, x5
```
Those last few weeks I have been working on translating the RISC-V spec into Rust. The compiler can't handle the full spec just yet, but I have an initial prototype with support for the full RISC-V decoder and physical memory protection.
Here is the repo for the curious: github.com/CharlyCst/so...
Here is the repo for the curious: github.com/CharlyCst/so...
June 17, 2025 at 8:36 AM
Those last few weeks I have been working on translating the RISC-V spec into Rust. The compiler can't handle the full spec just yet, but I have an initial prototype with support for the full RISC-V decoder and physical memory protection.
Here is the repo for the curious: github.com/CharlyCst/so...
Here is the repo for the curious: github.com/CharlyCst/so...
Tomorrow I am flying to Alberta to attend HotOS, I will be presenting our work on lightweight hypervisor verification.
In a nutshell, we translated the RISC-V spec to Rust (with an in-house Sail-to-Rust transpiler), and used the Kani model checker to verify key components of Miralis.
In a nutshell, we translated the RISC-V spec to Rust (with an in-house Sail-to-Rust transpiler), and used the Kani model checker to verify key components of Miralis.
![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"
);
}
```](https://cdn.bsky.app/img/feed_thumbnail/plain/did:plc:obihnetcvw3qgxzj5644ikeb/bafkreibkro2q2kn4yiskv4mxfxyfz6cerblfuujypspsqhfwhddxo4vtr4@jpeg)
May 11, 2025 at 9:49 PM
Tomorrow I am flying to Alberta to attend HotOS, I will be presenting our work on lightweight hypervisor verification.
In a nutshell, we translated the RISC-V spec to Rust (with an in-house Sail-to-Rust transpiler), and used the Kani model checker to verify key components of Miralis.
In a nutshell, we translated the RISC-V spec to Rust (with an in-house Sail-to-Rust transpiler), and used the Kani model checker to verify key components of Miralis.
We just received the new HiFive P550, a tiny bit too late for Christmas.
Time to try out this H extension!
Time to try out this H extension!
January 10, 2025 at 10:13 AM
We just received the new HiFive P550, a tiny bit too late for Christmas.
Time to try out this H extension!
Time to try out this H extension!
We finally track the cost of traps and world switches between the virtual firmware and the OS in the Miralis dashboard: miralis-firmware.github.io/dashboard
Now let's bring those numbers down!
Now let's bring those numbers down!
December 18, 2024 at 9:02 AM
We finally track the cost of traps and world switches between the virtual firmware and the OS in the Miralis dashboard: miralis-firmware.github.io/dashboard
Now let's bring those numbers down!
Now let's bring those numbers down!
Those days I am reading "The Art of Doing Science And Engineering" by Richard Hamming, the book was published in 1997 but it is astonishing how clearly he was reading into the future in so many aspects.
December 8, 2024 at 10:04 PM
Those days I am reading "The Art of Doing Science And Engineering" by Richard Hamming, the book was published in 1997 but it is astonishing how clearly he was reading into the future in so many aspects.
Miralis progress report: miralis-firmware.github.io/blog/summer-...
Over the summer we reached two major milestones: running unmodified Linux with a virtualized OpenSBI on QEMU, and porting Miralis to the VisionFive 2.
Over the summer we reached two major milestones: running unmodified Linux with a virtualized OpenSBI on QEMU, and porting Miralis to the VisionFive 2.
Summer 2024 progress report | Miralis
Three months and 110 commits after the open-sourcing of Miralis we have come a long way, and now sounds like a good time for our first ever progress report.
miralis-firmware.github.io
October 1, 2024 at 10:20 AM
Miralis progress report: miralis-firmware.github.io/blog/summer-...
Over the summer we reached two major milestones: running unmodified Linux with a virtualized OpenSBI on QEMU, and porting Miralis to the VisionFive 2.
Over the summer we reached two major milestones: running unmodified Linux with a virtualized OpenSBI on QEMU, and porting Miralis to the VisionFive 2.
My OSFC'24 talk on virtualizing firmware on RISC-V is now online:
vimeo.com/1007742198
vimeo.com/1007742198
Everything Old is New Again: Virtualizing Firmware on RISC-V - Charly Castes
The concept of virtualization is almost as old as computer science itself, with a rich history of intertwined software and hardware evolution. Today virtualization…
vimeo.com
September 27, 2024 at 9:45 PM
My OSFC'24 talk on virtualizing firmware on RISC-V is now online:
vimeo.com/1007742198
vimeo.com/1007742198
For the last few months I have been working on a RISC-V security monitor that virtualizes M-mode, we just open-sourced our prototype at github.com/CharlyCst/mi.... I'm looking forward to see how far we can go and what kind of interesting use cases we can build on top.
GitHub - CharlyCst/miralis: Miralis is an experimental system that virtualises firmware
Miralis is an experimental system that virtualises firmware - CharlyCst/miralis
github.com
July 27, 2024 at 10:57 AM
For the last few months I have been working on a RISC-V security monitor that virtualizes M-mode, we just open-sourced our prototype at github.com/CharlyCst/mi.... I'm looking forward to see how far we can go and what kind of interesting use cases we can build on top.