[Pl-seminar] TODAY: 10/4 Seminar: Ralf Jung: "Understanding and evolving the Rust programming language"

[Amal Ahmed]

Reminder: This talk is today at 11am in 366 WVH...

> On Sep 30, 2019, at 1:09 PM, Nathaniel Yazdani <yazdani.n at husky.neu.edu> wrote:
> 
> NUPRL Seminar Presents
> 
> Ralf Jung
> MPI-SWS
> 
> 11:00AM to 12:15PM
> Friday, October 4th, 2019
> Room 366 WVH (http://www.ccs.neu.edu/home/wand/directions.html <http://www.ccs.neu.edu/home/wand/directions.html>)
> 
> Understanding and evolving the Rust programming language
> 
> Abstract
> 
> Rust is a young and actively developed "systems programming language" that
> promises to overcome the seemingly fundamental tradeoff between high-level
> safety guarantees and low-level control over resource management.  This talk is
> about my research on understanding and evolving this groundbreaking new
> language.
> 
> The first part of the talk is about building formal foundations for the existing
> Rust language.  Rust employs a strong, ownership-based type system to rule out
> common systems programming anomalies, but then extends the expressive power of
> this core type system through libraries that internally use unsafe features.
> Unfortunately, this ``extensible'' aspect of the Rust language makes Rust's
> safety claims rather non-obvious, and there is good reason to question whether
> they actually hold.  To address this, we have developed RustBelt, the first
> formal (and machine-checked) safety proof for a language representing a
> realistic subset of Rust.  Our proof supports the extensible nature of Rust's
> safety story 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 and compositional extension to the language.
> 
> The second part is about evolving the semantics of Rust to better support
> compiler optimizations.  In particular, Rust's reference types provide strong
> aliasing guarantees, which a clever optimizing compiler should be able to
> exploit.  However, if no care is taken, unsafe code (which plays an essential
> role in the Rust ecosystem, as mentioned above) can subvert these guarantees.
> To address this, we have developed Stacked Borrows, a new operational semantics
> for memory accesses in Rust.  On the one hand, Stacked Borrows defines an
> aliasing discipline and declares programs violating it to have undefined
> behavior, thus making it possible for us to formally verify the soundness of a
> number of useful type-based intraprocedural optimizations.  On the other hand,
> we have also implemented the Stacked Borrows semantics in Miri, an interpreter
> for Rust, and run large parts of the Rust standard library test suite in Miri.
> In so doing, we have validated that our semantics is sufficiently permissive to
> account for real-world unsafe Rust code.
> 
> Bio
> 
> Ralf Jung is a PhD student at MPI-SWS in Saarbrücken, where he previously
> completed his undergraduate degree with Saarland University. Ralf’s research
> interests center around separation logic, operational semantics for low-level languages,
> (semantic) type systems, and mechanized+modular proof for program verification. Ralf
> also loves to learn about anything people do with Rust and the ways in which formal
> methods could help.
> _______________________________________________
> pl-seminar mailing list
> pl-seminar at lists.ccs.neu.edu
> https://lists.ccs.neu.edu/bin/listinfo/pl-seminar

-------------- next part --------------
HTML attachment scrubbed and removed