Ralf's Ramblings: Rust

Dec 27, 2023 • RustEditsPermalink

Google Open Source Peer Bonus

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 released which lists me as a recipient of this bonus as a thank you for my work on Rust. So this one time, it wasn’t spam after all!

Read more...

Jun 13, 2023 • RustEditsPermalink

Talk about Undefined Behavior, unsafe Rust, and Miri

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. :)

Read more...

Jun 2, 2023 • Research, RustEditsPermalink

From Stacks to Trees: A new aliasing model for Rust

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 problems. The purpose of Tree Borrows is to take the lessons learned from Stacked Borrows to build a new model with fewer issues, and to take some different design decisions such that we get an idea of some of the trade-offs and fine-tuning we might do with these models before deciding on the official model for Rust.

Neven has written a detailed introduction to Tree Borrows on his blog, which you should go read first. He presented this talk at a recent RFMIG meeting, so you can also watch his talk here. In this post, I will focus on the differences to Stacked Borrows. I assume you already know Stacked Borrows and want to understand what changes with Tree Borrows and why.

Read more...

Sep 26, 2022 • RustEditsPermalink

cargo careful: run your Rust code with extra careful debug checking

Did you know that the standard library is full of useful checks that users never get to see? There are plenty of debug assertions in the standard library that will do things like check that char::from_u32_unchecked is called on a valid char, that CStr::from_bytes_with_nul_unchecked does not have internal nul bytes, or that pointer functions such as copy or copy_nonoverlapping are called on suitably aligned non-null (and non-overlapping) pointers. However, the regular standard library that is distributed by rustup is compiled without debug assertions, so there is no easy way for users to benefit from all this extra checking.

Read more...

Aug 16, 2022 • Research, RustEditsPermalink

A New Beginning

I have some very exciting news to share: starting November 1st, I will work at ETH Zürich as an assistant professor! Becoming a professor in the first place is a dream come true, and becoming a professor at a place like ETH Zürich is not something I even dared to dream of. I still cannot quite believe that this is actually happening (I will be professor?!??), but the news is out so I guess this is real. :D

Read more...

Aug 8, 2022 • Research, RustEditsPermalink

Announcing: MiniRust

I have been thinking about the semantics of Rust – as in, the intended behavior of Rust programs when executed, in particular those containing unsafe code – a lot. Probably too much. But all of these thoughts are just in my head, which is not very useful when someone else wants to try and figure out how some tricky bit of unsafe Rust code behaves. As part of the Unsafe Code Guidelines project, we often get questions asking whether a concrete piece of code is fine or whether it has Undefined Behavior. But clearly, that doesn’t scale: there are just too many questions to be asked, and figuring out the semantics by interacting with an oracle with many-day latency is rather frustrating. We have Miri, which is a much quicker oracle, but it’s also not always right and even then, it can just answer questions of the form “is this particular program fine”; users have to do all the work of figuring out the model that generates those answers themselves.

Read more...

Jul 2, 2022 • RustEditsPermalink

The last two years in Miri

It has been almost two years since my last Miri status update. A lot has happened in the mean time that I would like to tell you all about! If you are using Miri, you might also be seeing new errors in code that previously worked fine; read on for more details on that.

For the uninitiated, Miri is an interpreter that runs your Rust code and checks if it triggers any Undefined Behavior (UB for short). You can think of it a as very thorough (and very slow) version of valgrind/ASan/TSan/UBSan: Miri will detect when your program uses uninitialized memory incorrectly, performs out-of-bounds memory accesses or pointer arithmetic, causes a data race, violates key language invariants, does not ensure proper pointer alignment, or causes incorrect aliasing. As such, it is most helpful when writing unsafe code, as it aids in ensuring that you follow all the rules required for unsafe code to be correct and safe. Miri also detects memory leaks, i.e., it informs you at the end of program execution if there is any memory that was not deallocated properly.

Read more...

Apr 11, 2022 • Programming, Research, RustEditsPermalink

Pointers Are Complicated III, or: Pointer-integer casts exposed

In my previous blog post on pointer provenance, I have shown that not thinking carefully about pointers can lead to a compiler that is internally inconsistent: programs that are intended to be well-behaved get miscompiled by a sequence of optimizations, each of which seems intuitively correct in isolation. We thus have to remove or at least restrict at least one of these optimizations. In this post I will continue that trend with another example, and then I will lay down my general thoughts on how this relates to the recent Strict Provenance proposal, what it could mean for Rust more generally, and compare with C’s PNVI-ae-udi. We will end on a very hopeful note about what this could all mean for Rust’s memory model. There’s a lot of information packed into this post, so better find a comfortable reading position. :)

Read more...

Nov 24, 2021 • Research, RustEditsPermalink

Do we really need Undefined Behavior?

I recently published a blog post on why Undefined Behavior is actually not a bad idea. Coincidentally, this is just a few weeks after the publication of this paper by Victor Yodaiken which basically argues that Undefined Behavior (UB for short) made C unusable for one of its core audiences, OS developers. Here I refer to the typical modern interpretation of UB: assumptions the compiler may trust, without bounds on what happens if they are violated. The paper makes many good points, but I think the author is throwing out the baby with the bathwater by concluding that we should entirely get rid of this kind of Undefined Behavior. The point of this blog post is to argue that we do need UB by showing that even some of the most basic optimizations that all compilers perform require this far-reaching notion of Undefined Behavior.

Read more...

Nov 18, 2021 • Research, RustEditsPermalink

Undefined Behavior deserves a better reputation

This is a cross-post of an article that I wrote for the SIGPLAN blog.

“Undefined Behavior” often has a bad reputation. People see it as an excuse compiler writers use to break code, or an excuse by a lazy language designer to not complete the specification and properly define all this behavior. But what, really, is Undefined Behavior, and is it as bad as its reputation? In this blog post, I will look at this topic from a PL perspective, and argue that Undefined Behavior (or UB for short) is a valuable tool in a language designer’s toolbox, and that it can be used responsibly to convey more of the programmer’s insight about their code to the compiler with the goal of enabling more optimizations. I will also explain why I spent a significant amount of time adding more UB to Rust.

Read more...

Jun 10, 2021 • Research, RustEditsPermalink

A podcast about GhostCell

I recently got asked to appear as a guest on the podcast Building with Rust to talk about our recent work on GhostCell. I never was a guest on a podcast before, so this was very exciting and of course I said yes. :) That episode has been released now, so you can listen to an hour of me talking about GhostCell and about PL research more generally:

Ralf Jung on GhostCell and Working as a PL Researcher

Have fun, and I am sorry for talking so fast. ;)

Read more...

Mar 23, 2021 • Research, RustEditsPermalink

Safe Systems Programming in Rust

It has been a long time coming; now our Communications of the ACM article Safe Systems Programming in Rust has finally been published. A pdf version is also available. We explain at a high level what makes Rust so innovative and interesting, and how we are studying Rust formally in the RustBelt project. The ACM even produced a short video which includes Derek and me explaining the main points of the article. Have fun. :)

Read more...

Dec 14, 2020 • Programming, Research, RustEditsPermalink

Pointers Are Complicated II, or: We need better language specs

Some time ago, I wrote a blog post about how there’s more to a pointer than meets the eye. One key point I was trying to make is that

just because two pointers point to the same address, does not mean they are equal in the sense that they can be used interchangeably.

This “extra information” that distinguishes different pointers to the same address is typically called provenance. This post is another attempt to convince you that provenance is “real”, by telling a cautionary tale of what can go wrong when provenance is not considered sufficiently carefully in an optimizing compiler. The post is self-contained; I am not assuming that you have read the first one. There is also a larger message here about how we could prevent such issues from coming up in the future by spending more effort on the specification of compiler IRs.

Read more...

Sep 28, 2020 • RustEditsPermalink

What (not so) recently happened in Miri

A lot has happened in Miri over the last year and a half, and I figured it would be a good idea to advertise all this progress a bit more widely, so here we go. We also recently performed a breaking change that affects some CI configurations, so this post serves as an announcement for you to update your CI configuration if needed.

For the uninitiated, Miri is an interpreter that runs your Rust code and checks if it triggers any Undefined Behavior. You can think of it a as very thorough (and very slow) version of valgrind: Miri will detect when your program uses uninitialized memory incorrectly, performs out-of-bounds memory accesses or pointer arithmetic, violates key language invariants, does not ensure proper pointer alignment, or causes incorrect aliasing. As such, it is most helpful when writing unsafe code, as it aids in ensuring that you follow all the rules required for unsafe code to be correct and safe. Miri also detects memory leaks, i.e., it informs you at the end of program execution if there is any memory that was not deallocated properly.

Read more...

Sep 3, 2020 • Research, RustEditsPermalink

Achievement 'PhD' unlocked

It is done! My dissertation is finally complete. So if you always wanted an in-depth account of my research on Rust (and more), you can go read my dissertation. With its almost 300 pages, it should keep you busy for a while. ;)

Read more...

Jul 15, 2020 • RustEditsPermalink

Why even unused data needs to be valid

The Rust compiler has a few assumptions that it makes about the behavior of all code. Violations of those assumptions are referred to as Undefined Behavior. Since Rust is a safe-by-default language, programmers usually do not have to worry about those rules (the compiler and libraries ensure that safe code always satisfies the assumptions), but authors of unsafe code are themselves responsible for upholding these requirements.

Those assumptions are listed in the Rust reference. The one that seems to be most surprising to many people is the clause which says that Rust code may not produce “[…] an invalid value, even in private fields and locals”. The reference goes on to explain that “producing a value happens any time a value is assigned to or read from a place, passed to a function/primitive operation or returned from a function/primitive operation”. In other words, even just constructing, for example, an invalid bool, is Undefined Behavior—no matter whether that bool is ever actually “used” by the program. The purpose of this post is to explain why that rule is so strict.

Read more...

Apr 4, 2020 • RustEditsPermalink

Debugging rustc type layouts

This post is a “public service announcement” for people working on the guts of rustc. I wish I had known about this a year ago, so I hope this post can make this feature more widely known.

Read more...

Nov 25, 2019 • RustEditsPermalink

How to Panic in Rust

What exactly happens when you panic!()? I recently spent a lot of time looking at the parts of the standard library concerned with this, and it turns out the answer is quite complicated! I have not been able to find docs explaining the high-level picture of panicking in Rust, so this feels worth writing down.

Read more...

Nov 18, 2019 • Research, RustEditsPermalink

Stacked Borrows: An Aliasing Model for Rust (the paper)

I have blogged a few times before about Stacked Borrows, my proposed aliasing model for Rust. But I am a researcher, and what researchers (are expected to) do is write papers—so that’s what we did for Stacked Borrows as well. After a lot of work, I can now finally present to you our paper Stacked Borrows: An Aliasing Model for Rust (thanks to open access, the paper is available under the CC-BY 4.0 license).

Read more...

Oct 20, 2019 • Research, RustEditsPermalink

What Type Soundness Theorem Do You Really Want to Prove?

My advisor Derek and some of my coauthors Amin, Robbert and Lars just put out a blog post on the SIGPLAN blog on the idea of “semantic typing”. This is the methodology behind RustBelt, so the post is a great starting point for understanding the context of that paper and the key bits of prior research that it rests on. In fact they used Rust as their main example language for that post, and I helped them out a bit with some of the technical details there so they kindly added me to the author list.

The approach they describe is much more widely applicable than Rust though; it provides a whole new perspective on type systems that I think deserves way more attention than it gets. If you are interested in formal methods for type systems and in particular for Rust, you should check it out! It’s a great read:

“What Type Soundness Theorem Do You Really Want to Prove?” on PL Perspectives

Read more...

Jul 14, 2019 • Programming, Research, RustEditsPermalink

"What The Hardware Does" is not What Your Program Does: Uninitialized Memory

This post is about uninitialized memory, but also about the semantics of highly optimized “low-level” languages in general. I will try to convince you that reasoning by “what the hardware does” is inherently flawed when talking about languages such as Rust, C or C++. These are not low-level languages. I have made this point before in the context of pointers; this time it is going to be about uninitialized memory.

The trigger for this post is the deprecation of mem::uninitialized() with Rust 1.36, but the post is just as relevant for C/C++ as it is for Rust.1

  1. This deprecation has been in the works for more than two years, and it has been almost a year since I took over pushing for this. I am very happy that we are finally there! 

Read more...

May 21, 2019 • Research, RustEditsPermalink

Putting the stack back into Stacked Borrows

Less than a month ago, I announced Stacked Borrows 2. In particular, I hoped that that version would bring us closer to proper support for two-phase borrows. Turns out I was a bit too optimistic! Last week, @Manishearth asked on Zulip why Miri rejected a certain program, and it turned out that the issue was related to two-phase borrows: in combination with interior mutability, behavior wasn’t always what we wanted it to be. So, I went back to the drawing board and tried to adjust Stacked Borrows.

In the end, I decided to give up on “proper” support for two-phase borrows for now, which I explained here. But I also made some tweaks to Stacked Borrows that affect all accesses (not just two-phase borrows), and that’s what this post is about. I am referring to this as “Stacked Borrows 2.1”.

Read more...

Apr 30, 2019 • Research, RustEditsPermalink

Stacked Borrows 2

Recently, I have significantly updated Stacked Borrows in order to fix some issues with the handling of shared references that were uncovered in the previous version. In this post, I will describe what the new version looks like and how it differs from Stacked Borrows 1. I assume some familiarity with the prior version and will not explain everything from scratch.

Read more...

Mar 26, 2019 • RustEditsPermalink

Miri available as rustup component

Running your unsafe code test suite in Miri has just gotten even easier: Miri is now available as a rustup component! Huge thanks to @oli-obk and @mati865 who made this happen.

Miri can run your test suite in a very slow, interpreted mode that enables it to test for undefined behavior: if an out-of-bounds array access happens, uninitialized memory gets used the wrong way or a dangling raw pointer gets dereferenced, Miri will notice and tell you. However, Miri cannot execute all programs, and it also cannot detect all forms of misbehavior. For further information, please check out Miri’s README.

Read more...

Feb 12, 2019 • RustEditsPermalink

All-Hands 2019 Recap

Last week, I was in Berlin at the Rust All-Hands 2019. It was great! I will miss nerding out in discussions about type theory and having every question answered by just going to the person who’s the expert in that area, and asking them. In this post, I am summarizing the progress we made in my main areas of interest and the discussions I was involved in—this is obviously just a small slice of all the things that happened.

Read more...

Jan 12, 2019 • RustEditsPermalink

Rust 2019: Solid Foundations for Unsafe Code

It is that time of the year again where our feedreaders are filled with people’s visions for what Rust should become in the next year. Coming up with a vision is not exactly my strong suit, but it is probably something I should learn, so here’s my episode of the “Rust 2019” blog post series.

I think in 2019, we should make a coordinated effort to improving the foundations for writing unsafe code. Of course my particular Rust bubble is mostly about unsafe code, as you will know if you have read some of my previous posts – but safety is a core value proposition of Rust, and the entire ecosystem rests on a foundation of crates that make heavy use of unsafe code, so I believe that caring about unsafe code is an important piece to Rust’s overall success.

Read more...

Dec 26, 2018 • Internship, RustEditsPermalink

Barriers and Two-phase Borrows in Stacked Borrows

My internship (“research assistantship”) with Mozilla has ended several weeks ago, and this post is a report of the most recent tweaks I made to Miri and Stacked Borrows. Neither project is by any means “done”, of course. However, both have reached a fairly reasonable state, so I felt some kind of closing report made sense. Also, if I ever want to finish my PhD, I’ll have to seriously scale down the amount of time I work on Rust – so at least from my side, things will move more slowly from now on.

In particular, installing Miri and running your test suite in it is now just a single command away! Scroll all the way down if you are not interested in the rest.

Read more...

Nov 16, 2018 • Internship, RustEditsPermalink

Stacked Borrows Implemented

Three months ago, I proposed Stacked Borrows as a model for defining what kinds of aliasing are allowed in Rust, and the idea of a validity invariant that has to be maintained by all code at all times. Since then I have been busy implementing both of these, and developed Stacked Borrows further in doing so. This post describes the latest version of Stacked Borrows, and reports my findings from the implementation phase: What worked, what did not, and what remains to be done. There will also be an opportunity for you to help the effort!

This post is a self-contained introduction to Stacked Borrows. Other than historical curiosity and some comparison with my earlier work on Types as Contracts there is no reason to read the original post at this point.

Read more...

Aug 22, 2018 • Internship, RustEditsPermalink

Two Kinds of Invariants: Safety and Validity

When talking about the Rust type system in the context of unsafe code, the discussion often revolves around invariants: Properties that must always hold, because the language generally assumes that they do. In fact, an important part of the mission of the Unsafe Code Guidelines strike force is to deepen our understanding of what these invariants are.

However, in my view, there is also more than one invariant, matching the fact that there are (at least) two distinct parties relying on these invariants: The compiler, and (authors of) safely usable code. This came up often enough in recent discussions that I think it is worth writing it down properly once, so I can just link here in the future. :)

Read more...

Aug 7, 2018 • Internship, RustEditsPermalink

Stacked Borrows: An Aliasing Model For Rust

In this post, I am proposing “Stacked Borrows”: A set of rules defining which kinds of aliasing are allowed in Rust. This is intended to answer the question which pointer may be used when to perform which kinds of memory accesses.

This is a long-standing open question of many unsafe code authors, and also by compiler authors who want to add more optimizations. The model I am proposing here is by far not the first attempt at giving a definition: The model is heavily based on ideas by @arielb1 and @ubsan, and of course taking into account the lessons I learned last year when I took my first stab at defining such a model, dubbed “Types as Contracts”.

Read more...

Jul 24, 2018 • Internship, Programming, RustEditsPermalink

Pointers Are Complicated, or: What's in a Byte?

This summer, I am again working on Rust full-time, and again I will work (amongst other things) on a “memory model” for Rust/MIR. However, before I can talk about the ideas I have for this year, I have to finally take the time and dispel the myth that “pointers are simple: they are just integers”. Both parts of this statement are false, at least in languages with unsafe features like Rust or C: Pointers are neither simple nor (just) integers.

I also want to define a piece of the memory model that has to be fixed before we can even talk about some of the more complex parts: Just what is the data that is stored in memory? It is organized in bytes, the minimal addressable unit and the smallest piece that can be accessed (at least on most platforms), but what are the possible values of a byte? Again, it turns out “it’s just an 8-bit integer” does not actually work as the answer.

I hope that by the end of this post, you will agree with me on both of these statements. :)

Read more...

Jul 19, 2018 • Internship, RustEditsPermalink

Thoughts on Compile-Time Function Evaluation and Type Systems

For some time now (since the 1.26 release, to be precise), Rust has a very powerful machinery for CTFE, or compile-time function evaluation. Since then, there have been various discussions about which operations should be allowed during CTFE, which checks the compiler should do, how this all relates to promotion and which kinds of guarantees we should be able to expect around CTFE. This post is my take on those topics, and it should not be surprising that I am going to take a very type-system centric view. Expect something like a structured brain dump, so there are some unanswered questions towards the end as well.

Read more...

Jul 13, 2018 • Research, RustEditsPermalink

The Tale of a Bug in Arc: Synchronization and Data Races

While I was busy doing Rust-unrelated research, RustBelt continues to move and recently found another bug (after a missing impl !Sync that we found previously): It turns out that Arc::get_mut did not perform sufficient synchronization, leading to a data race.

Notice that I am just the messenger here, the bug was actually found by Hai and Jacques-Henri. Still, I’d like to use this opportunity to talk a bit about weak memory, synchronization and data races. This is just a primer, there are tons of resources on the web that go into more detail (for example here).

Read more...

Jul 11, 2018 • Internship, RustEditsPermalink

Back at Mozilla

After my internship last year has ended, I naturally became somewhat less active in the Rust community as I could not work on Rust full-time any more. Well, for the following months I am going to be back full-time. :) Thanks to @aturon, I am able to work as a research assistant for Mozilla during this summer (until the end of November). I don’t really know what a “research assistant” is, but I am going to continue the work on Rust memory models, and hopefully also have some time to make progress on union semantics.

Read more...

Apr 10, 2018 • Research, RustEditsPermalink

Safe Intrusive Collections with Pinning

In my last post, I talked about the new “pinned references” which guarantee that the data at the memory it points to will not, ever, be moved elsewhere. I explained how they enable giving a safe API to code that could previously only be exposed with unsafe, and how one could go about proving such a thing. This post is about another application of pinned references—another API whose safety relies on the pinning guarantees: Intrusive collections. It turns out that pinned references can almost be used for this, but not quite. However, this can be fixed by extending the guarantees provided by pinned references, as suggested by @cramertj.

Read more...

Apr 5, 2018 • Research, RustEditsPermalink

A Formal Look at Pinning

Recently, a new API for “pinned references” has landed as a new unstable feature in the standard library. The purpose of these references is to express that the data at the memory it points to will not, ever, be moved elsewhere. @withoutboats has written about how this solves a problem in the context of async IO. In this post, we take a closer, more formal look at that API: We are going to take a stab at extending the RustBelt model of types with support for pinning.

Read more...

Jan 31, 2018 • Research, RustEditsPermalink

Sharing for a Lifetime

This post is about an aspect of the RustBelt paper. Concretely, I’d like to share some of our thoughts on the nature of types and shared references. Let’s see how well this goes. :)

Shared references are an extremely powerful mechanism in the Rust type system, and we’ve had quite some trouble finding a good way of handling them in our formal model. In this post, I will present the model that we came up with.

Read more...

Jan 21, 2018 • Research, RustEditsPermalink

RustBelt Conference Talk

Last week, I was in Los Angeles at POPL 2018 to present our paper RustBelt: Securing the Foundations of the Rust Programming Language. The talk has been recorded, so if you want to get a 20-minute summary of the paper, go watch it on YouTube. If you have any questions, feel free to join the forum thread linked below :)

Read more...

Aug 12, 2017 • Internship, RustEditsPermalink

So Long, and Thanks for All the Fish

Yesterday was the last day of my Rust internship at Mozilla. I can hardly believe that twelve weeks have passed since that post, but my calendar insists. If you want to see what I have done, you can go read the posts that I wrote during the internship. (I almost kept up with the plan of bi-weekly blog posts…) You can also watch the 10-minute video version of this that I made for the internship presentation. The recording is available on Air Mozilla; my talk starts at 2h 14:30.

Read more...

Aug 11, 2017 • Internship, RustEditsPermalink

Types as Contracts: Implementation and Evaluation

Some weeks ago, I described Types as Contracts as an approach for how to go about defining Rust’s aliasing-related undefined behavior. One key property of this approach is that it is executable, which means we can actually have a program (in this case, miri) tell us whether some particular Rust test case exhibits undefined behavior or not. I have since then spent most of my time completing and refining this implementation, and running it on miri’s test suite to exercise various bits of the standard library and see whether they are actually following the rules I have been suggesting.

This post is my report on what I found, and how the approach itself changed in response to these findings. It also explains how you can run miri yourself and have it check your code for undefined behavior according to this model. Finally, I discuss some of the things that I would like to look at going forward.

Read more...

Jul 17, 2017 • Internship, RustEditsPermalink

Types as Contracts

Over the last couple of weeks of my internship, I have been working on a proposal for the “Unsafe Code Guidelines”. I got some very encouraging feedback at the Mozilla All-Hands, and now I’d like to put this proposal out there and start having a discussion.

Read more...

Jul 14, 2017 • Internship, RustEditsPermalink

Undefined Behavior and Unsafe Code Guidelines

Last year, the Rust unsafe code guidelines strike team was founded, and I am on it. :-) So, finally, just one year later, this post is my take at what the purpose of that team is.

Read more...

Jul 8, 2017 • Research, RustEditsPermalink

RustBelt: Securing the Foundations of the Rust Programming Language

Just yesterday, we submitted our paper RustBelt: Securing the Foundations of the Rust Programming Language. Quoting from the abstract:

Rust is a new systems programming language that promises to overcome the seemingly fundamental tradeoff between high-level safety guarantees and low-level control over resource management. Unfortunately, none of Rust’s safety claims have been formally proven, and there is good reason to question whether they actually hold. Specifically, Rust employs a strong, ownership-based type system, but then extends the expressive power of this core type system through libraries that internally use unsafe features. In this paper, we give the first formal (and machine-checked) safety proof for a language representing a realistic subset of Rust. Our proof is extensible in the sense that, for each new Rust library that uses unsafe features, we can say what verification condition it must satisfy in order for it to be deemed a safe extension to the language. We have carried out this verification for some of the most important libraries that are used throughout the Rust ecosystem.

Read more...

Jun 9, 2017 • Research, RustEditsPermalink

How MutexGuard was Sync When It Should Not Have Been

A couple of weeks ago, our ongoing effort to formalize Rust’s type system lead to us actually discovering a bug in the Rust standard library: MutexGuard implemented Sync in cases where it should not. This could lead to data races in safe programs. Ouch.

Read more...

Jun 6, 2017 • Internship, RustEditsPermalink

Exploring MIR Semantics through miri

It’s now been two weeks since my internship started (two weeks already, can you believe it?). In other words, if I want to post “weekly or bi-weekly” updates, I better write one today ;) .

As already mentioned, the goal for this internship is to experiment with unsafe code guidelines by implementing them in miri. Before I tackle that, however, it seemed sensible for me to grab some low-hanging fruit in miri just to make myself familiar with the codebase. It turns out I entered “unsafe code guidelines” territory much quicker than expected. This post is about what I found, and it also serves as a nice demonstration of how we envision my unsafe code guidelines workflow to look like.

Read more...

May 23, 2017 • Internship, RustEditsPermalink

How to Specify Program (Undefined) Behavior?

This summer, I am given the awesome opportunity of spending three months in the Mozilla offices in Portland, working on Rust. I am extremely grateful that Mozilla is providing this opportunity to me; hopefully I can give something back by making some hands-on contributions to the Rust ecosystem.

Read more...

Jan 20, 2017 • Research, RustEditsPermalink

Talk @ Paris Rust Meetup

This week, I have been at the Paris Rust Meetup. Meeting all sorts of Rust people was great fun, and the Mozilla offices in Paris are absolutely impressive. You should totally check them out if you have a chance.

On that meetup, I gave a short talk about the current status of my formalization of the Rust type system.

Read more...

Jan 9, 2016 • Research, RustEditsPermalink

The Scope of Unsafe

I’d like to talk about an important aspect of dealing with unsafe code, that still regularly seems to catch people on the wrong foot:

When checking unsafe code, it is not enough to just check the contents of every unsafe block.

The “scope” in the title refers to the extent of the code that has to be manually checked for correctness, once unsafe is used. What I am saying is that the scope of unsafe is larger than the unsafe block itself.

It turns out that the underlying reason for this observation is also a nice illustration for the concept of semantic types that comes up in my work on formalizing Rust (or rather, its type system). Finally, this discussion will once again lead us to realize that we rely on our type systems to provide much more than just type safety.

Update (2016-01-11): Clarified the role of privacy; argued why evil is the problem.

Read more...

Oct 12, 2015 • Research, RustEditsPermalink

Formalizing Rust

My current research project – and the main topic of my PhD thesis – is about developing a semantic model of the Rust programming language and, most importantly, its type system. Rust is an attempt of Mozilla to find a sweet spot in the design space of programming languages: A language that provides low-level resource management (making it a systems language), is convenient for programmers and guards against memory errors and thread unsafety. Other have said and written a lot on why we need such a language, so I won’t lose any more words on this. Let me just use this opportunity for a shameless plug: If you are curious and want to learn Rust, check out Rust-101, a hands-on Rust tutorial I wrote. I am going to assume some basic familiarity with Rust in the following.

Why do we want to do research on Rust? First of all, I’m (becoming) a programming languages researcher, and Rust is an interesting new language to study. It’s going to be fun! Honestly, that’s enough of a reason for me. But there are other reasons: It shouldn’t be a surprise that bugs have been found in Rust. There are lots of things that can be done about such bugs – my take on this is that we should try to prove, in a mathematical rigorous way, that no such bugs exist in Rust. This goes hand-in-hand with other approaches like testing, fuzzing and static analysis. However, we (at my research group) are into formalizing things, so that’s what we are going to do as part of the RustBelt research project.

Update: Added link to RustBelt website.

Read more...