Ralf's Ramblings

Jul 17, 2017 • Internship, RustPermalink

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, RustPermalink

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, RustPermalink

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 • RustPermalink

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, RustPermalink

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, RustPermalink

Day 1 of My Mozilla Internship, or: How to Specify Program 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, RustPermalink

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, RustPermalink

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 (Jan 11th): Clarified the role of privacy; argued why evil is the problem.

Read more...

Oct 12, 2015 • Research, RustPermalink

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

Oct 9, 2015 • FunPermalink

Breaking All the Way Out

Do you know the feeling of having done something, and having a website for it somewhere, but not finding the right spot to put a link to that website? I certainly do, and, well… now that I have a blog, I finally do have a place for such links!

Read more...

Oct 8, 2015 • MetaPermalink

Welcome

I’ll use this blog to write random articles on things that matter to me, and that I want to share. So far, I don’t know what this will end up being about - probably mostly about programming languages research and related topics, as that’s what I do.

Read more...