Opendata, web and dolomites

Report

Teaser, summary, work performed and final results

Periodic Reporting for period 2 - RustBelt (Logical Foundations for the Future of Safe Systems Programming)

Teaser

\"The RustBelt project is motivated by a longstanding open question inthe design of languages for programming complex software systems,namely: How can we provide programmers with both safety and control?Systems programming languages like C and C++ give programmerslow-level...

Summary

\"The RustBelt project is motivated by a longstanding open question in
the design of languages for programming complex software systems,
namely: How can we provide programmers with both safety and control?
Systems programming languages like C and C++ give programmers
low-level control over resource management at the expense of safety,
whereas most other modern languages give programmers safe, high-level
abstractions at the expense of control. It has long been a \"\"holy
grail\"\" of programming languages research to overcome this seemingly
fundamental tradeoff and design a language that offers programmers
both high-level safety and low-level control.

Rust is a new language developed at Mozilla Research that marries
together the low-level flexibility of modern C++ with a strong
\"\"ownership-based\"\" type system guaranteeing type safety, memory
safety, and data race freedom. As such, Rust has the potential
to revolutionize systems programming, making it possible to build
software systems that are safe by construction, without having
to give up low-level control over performance.

Unfortunately, none of Rust\'s safety claims have been formally
investigated, and there is reason to doubt whether they hold. To rule
out data races and other common programming errors, Rust\'s core type
system prohibits the aliasing of mutable state, but this is too
restrictive for implementing some low-level data structures.
Consequently, Rust\'s standard libraries make widespread internal use
of \"\"unsafe blocks\"\", which enable the implementations to make use of
potentially dangerous operations. The hope is that such unsafe code
is properly encapsulated, so that Rust\'s language-level safety
guarantees are preserved. But due to Rust\'s reliance on a weak memory
model of concurrency, along with its bleeding-edge type system,
verifying that Rust and its libraries are actually safe requires
fundamental advances to the state of the art.

In this project, we aim to equip Rust programmers with the first
formal tools for verifying safe encapsulation of unsafe code. Any
realistic languages targeting this domain in the future will encounter
the same problem, so we expect our results to have lasting impact. To
achieve this goal, we are building on recent breakthrough developments
by the PI and collaborators in the areas of concurrent program logics,
relaxed memory models, and semantics of type systems.

The project is divided into two key research vectors. In the first
research vector, we will develop RustL, a program logic for Rust,
which must be capable of expressing and verifying the proof
obligations that we wish to impose on unsafe Rust code in order to
prove it \"\"safe\"\". A core challenge will be accounting for the relaxed
(or \"\"weak\"\") concurrency model that Rust inherits from C/C++, which is
much trickier to reason about than the standard \"\"sequentially
consistent\"\" concurrency model that most prior program logics assume.
Moreover, to build confidence in our verification efforts, we want
RustL proofs to be machine-checked using an interactive theorem
prover. Realizing this goal will require significant innovations in
theorem-proving technology.

In the second research vector, we will develop RustBelt itself: a
semantic soundness proof for the Rust language. RustBelt will
interpret the interfaces of Rust libraries as specifications (in
RustL) which their implementations must satisfy in order to be
considered \"\"safe\"\". For unsafe Rust libraries, we will then use RustL
to verify that their implementations satisfy their required
specifications according to RustBelt. The core challenge here will be
figuring out how to model the many novel features of Rust\'s
sophisticated ownership-based type system.
\"

Work performed

\"Thus far, we have made major breakthroughs on both research vectors of
the project.

Concerning Research Vector #1:

- Concurrency Model: Rust inherits its relaxed-memory concurrency
model from C/C++11, but the C11 model is known to suffer from a fatal
flaw called the \"\"out-of-thin-air\"\" (OOTA) problem. We have proposed a
breakthrough solution to this problem, which we dubbed the \"\"promising
semantics\"\". In addition, we have identified a previously unknown flaw
in C11 pertaining to the treatment of sequentially consistent (SC)
accesses, and we proposed a revised semantics, dubbed RC11, that fixes
this flaw.

- Program Logic for Rust: We have developed a general logical
framework for Rust programs called Iris. Crucially, Iris is
*parameterized* by the semantics of the language we are reasoning
about, which enables us to experiment with different semantics and
memory models for Rust. In addition, Iris was designed to make it
easy to derive custom logics for different application domains, a
facility we make use of in Research Vector #2.

- Support for Machine-Checked Proofs: We have developed effective
interactive theorem-proving support for Iris in the form of a
Coq-based tool we call MoSeL. MoSeL is a library for the Coq proof
assistant that provides convenient tactical support for doing
interactive proofs in a variety of different separation logics. It is
especially tuned to support machine-checked proofs in the kinds of
custom logics that we derive within Iris.

- Reasoning about Different Concurrency Models: We have instantiated
Iris/MoSeL with both sequentially consistent and relaxed-memory
semantics for Rust programs, and applied it to derive useful
high-level reasoning principles for both types of concurrency models.

Concerning Research Vector #2:

- Formalizing the Rust Language: We have given a formal definition of
a core typed calculus called LambdaRust, which encapsulates the
central features of the Rust language.

- Proving Safety of Rust: We have developed a first version of the
RustBelt semantic soundness proof, which establishes formally that
Rust\'s safety guarantees do in fact hold for both the LambdaRust type
system, as well as for a variety of widely-used Rust libraries that
internally make use of unsafe features. This constitutes the first
formal validation of the safety of the Rust language.

To keep the problem tractable at first, this first version of RustBelt
is built on top of Iris/MoSeL instantiated with a sequentially
consistent semantics for Rust rather than the true relaxed-memory
semantics. The proof makes essential use of Iris\'s key feature,
namely its ability to derive custom, domain-specific logics. In
particular, we use Iris to derive a Rust-oriented logic we call the
\"\"lifetime logic\"\". The lifetime logic makes it possible to give a
relatively simple and direct semantic model of Rust\'s \"\"lifetimes\"\" and
\"\"borrowing\"\" mechanisms, thus considerably simplifying the verification
effort.
\"

Final results

\"There are several important directions to be explored further in the
second half of the project, which will require progress beyond the
present state of the art.

Concerning Research Vector #1:

- Improvements to the Concurrency Model: The \"\"promising semantics\"\" we
have proposed for C/C++ concurrency currently fails to validate some
global program analyses that compilers may perform. We plan to
develop a more flexible version of the promising semantics that
validates these analyses.

- Reasoning about the Promising Semantics: Currently, the Iris program
logic is only proven sound with respect to RC11, not our \"\"promising
semantics\"\". (The promising semantics is preferable to RC11 in that it
is more efficient to implement on modern hardware.) We plan to extend
Iris to reason about programs under the promising semantics.

- Reasoning About the Combination of Strong and Relaxed Memory: Thus
far, we have instantiated Iris with both a sequentially-consistent
semantics and a relaxed-memory semantics, but we lack the means to
reason about programs that use both strong and relaxed operations in
tandem. We plan to develop an extension of Iris that will support
such reasoning, thus expanding the scope of the RustBelt verification.

Concerning Research Vector #2:

- Proving Safety of Rust Under Relaxed Memory: Thus far, we have only
proved safety of LambdaRust under a sequentially-consistent concurrency
model. We plan to rebuild our RustBelt semantic soundness proof on
top of a relaxed memory model, either RC11 or preferably the promising
semantics.

- Proving Safety of More Complex Libraries: We have thus far verified
a number of widely-used Rust libraries, including Arc, Mutex, RwLock,
Rc, Cell, and RefCell. We plan to verify additional libraries that
utilize combinations of strong and relaxed-memory features, such as
the Crossbeam library for building lock-free data structures.

- Developing a More Faithful Model of Rust: Thus far, the LambdaRust
type system only accounts for the core features of Rust, but omits
several interesting features, such as traits, panics, and automatic
destruction of objects. It also assumes a naive model for Rust\'s
pointer accesses, which fails to validate optimizations performed by
the Rust compiler. We plan to enrich LambdaRust and RustBelt to make
them more faithful with respect to the reality of the Rust language.
\"

Website & more info

More info: http://plv.mpi-sws.org/rustbelt/.