Miralis at SOSP'2025

I'm happy to announce that I will be presenting Miralis at SOSP'25 in Seoul!

Our paper on Miralis got accepted to SOSP 2025 (the "Symposium on Operating Systems Principles"), which is one of the two flagship systems conferences. This is the result of more than a year and a half of work by all the contributors to the Miralis project, and the logical continuation of our previous workshop papers at KISV'24 and HotOS'25. Once again, I would like to thank all of those who helped to get to that point, this would not have been possible without you!

SOSP'25

If you are attending SOSP this year, be sure to attend the Operating Systems session on Monday morning if you would like to see the presentation. I will also bring stickers of the Miralis logo, if you would like one just drop by to say hi, I have too many to keep them all for myself!

What is Next?

Although publishing papers is sort of the final objective of research projects in academia, this doesn't mean that we are done with Miralis. In fact, there are many more things we would like to do!

In particular, one of our next objectives is to continue our line of work on lightweight formal methods and to continue making Miralis more secure. This effort has now been externalized to a separate repository, as we believe it may be helpful for many more software projects beyond Miralis itself! I will write more about all of this in the future, but in short we now have a compiler that translates ISA specifications (such as RISC-V and Arm) into Rust, which we can leverage to verify various properties about low-level systems software. The SOSP paper talks about the verification of the virtualization subsystem of Miralis. One of the current avenues we are exploring is testing and verification of mixed Rust and assembly code. This is still a very early project, but if you are interested you can look at the current prototype here and follow the main Miralis repository to see how it can be integrated in system software.