The Rust Abstract Machine is full of wonderful oddities that do not exist on the actual hardware . Inevitably, every time this is discussed, someone asks: “But, what if I use inline assembly? What happens with provenance and uninitialized memory and Tree Borrows and all these other fun things you made up that don’t actually exist?” This is a great question, but answering it properly requires some…
It is time for another “what is happening in Miri” post. In fact this is way overdue, with the previous update being from more than 3 years ago (what even is time?!?), but it is also increasingly hard to find the time to blog, so… here we are. Better late than never. :) For the uninitiated, Miri is an Undefined Behavior testing tool for Rust. This means it can find bugs in your unsafe code where…
Memory safety is all the rage these days. But what does the term even mean? That turns out to be harder to nail down than you may think. Typically, people use this term to refer to languages that make sure that there are no use-after-free or out-of-bounds memory accesses in the program. This is then often seen as distinct from other notions of safety such as thread safety, which refers to programs…
After several years of work, our Tree Borrows paper has finally been presented recently at PLDI 2025 in Seoul. Tree Borrows has not changed much compared to what has previously been mentioned in this blog and on Neven’s website . We used all that extra time for formal proofs that Tree Borrows indeed allows at least some of the optimizations that we hope to gain from it, and to carry out an…
A few weeks ago, many Rust folks met in Utrecht for RustWeek and we all had a great time. As part of that, I also gave a talk titled “MiniRust: A core language for specifying Rust” about the current state of MiniRust. This was my first time giving a talk in a (fully packed) movie theater; unfortunately, my special effects budget cannot keep up with the shows that would usually be presented there.…
The first paper by a PhD student I supervise has been accepted into POPL: “Program Logics à la Carte” will be presented in Denver next week. The paper proposes a framework of reusable building blocks to simplify constructing a program logic with its associated soundness proof. This is built in Iris, and is similar to how Iris provides reusable building blocks for the ingredients of a powerful…
The first paper produced entirely by my group has recently been published at OOPSLA. :) The paper is about fuzzing the optimizations and code generation of the Rust compiler by randomly generating MIR programs and ensuring they behave the same across different backends, different optimization levels, and in Miri. The core part of this work was done by Andy (Qian Wang) for his master thesis . This…
One of the more subtle aspects of the Rust language is the fact that there are actually two kinds of expressions: value expressions and place expressions . Most of the time, programmers do not have to think much about that distinction, as Rust will helpfully insert automatic conversions when one kind of expression is encountered but the other was expected. However, when it comes to unsafe code, a…
A few years ago, I have blogged about my approach to sandboxing less-trusted applications that I have to or want to run on my main machine. The approach has changed since then, so it is time for an update. Over time I grew increasingly frustrated with Firejail: configurations would frequently break on updates, and debugging Firejail profiles is extremely hard. When considering all the included…
We are all used to spam emails, supposedly from Google, that say “You won” and I just need to send all my data to somewhere to receive my lottery payout. When I recently received an email about Google’s “Open Source Peer Bonus” program, I almost discarded it as yet another version of that kind of spam. But it turns out sometimes these emails are real! Meanwhile the official announcement has been…
I recently gave a talk at a local Rust meetup in Zürich about Undefined Behavior, unsafe Rust, and Miri. The recording is available here . It targets an audience that is familiar with Rust but not with the nasty details of unsafe code, so I hope many of you will enjoy it! Have fun. :)
Since last fall, Neven has been doing an internship to develop a new aliasing model for Rust: Tree Borrows. Hang on a second, I hear you say – doesn’t Rust already have an aliasing model? Isn’t there this “Stacked Borrows” that Ralf keeps talking about? Indeed there is, but Stacked Borrows is just one proposal for a possible aliasing model – and it has its fair share of problems . The purpose of…