Stream: t-lang/wg-unsafe-code-guidelines

Topic: Mathematical, rigorous safety proofs

RalfJ (Jun 10 2019 at 09:27, on Zulip):

To answer one of your questions @Ehsan M. Kermani:

Things discussed here are new to me but I'm curious and want to know more. I've been trying to educate myself with UB (what is it exactly?) reading John Regehr's and Ralf's blogs etc. I have to confess that I've got an uneasy feeling that many unanswered questions have deep roots in LLVM itself. I'd like to ask you to what extent we can prove safety? (I mean mathematical, rigorous proofs). I'm aware of miri and Rustbelt, though these're not accessible to me and I don't know the minimum requirements, but what I'm looking at is ideas and intuitions behind validity and safety proofs (if there're some!). Is there any place I can get most of the idea from? (blogs etc.)

Good question! The fully correct answer is that it is impossible to prove mathematical rigorous things about any compute system. Ultimately these are physical artifacts (hardware and software combined), and physics is outside of what math can prove.
What math can prove things about this is models of physical systems. You start with some assumptions e.g. about how a CPU works, and then you show that if the CPU really works that way, then certain things are true. You can even prove that if the CPU really matches some HDL like Verilog or so, then it works the way we need. But there always is an "if".

RalfJ (Jun 10 2019 at 09:30, on Zulip):

One of the most rigorously-proven-correct compilers out there is CompCert, but it, too, has assumptions: the parser is not verified (and there were bugs in there, and now they are proving more things about the parser), and you have to trust that CompCert's idea of "what x86 does" is actually correct (and there were bugs there for some architectures that lead to incorrect compilation). So CompCert's proof is more like if the program got parsed correctly and if an x86/ARM/... CPU really works the way this definition says it does and if the output of CompCert (which is textual assembly, no binary) is correctly translated to (binary) machine code and ... then the program will do what it should be doing.
This is still extremely useful though! Not all bugs are excluded, but many, and that is demonstrably useful in practical evaluation:

The striking thing about our CompCert results is that the middle-end bugs we
found in all other compilers are absent. As of early 2011, the
under-development version of CompCert is the only compiler we have tested for
which Csmith cannot find wrong-code errors. This isnot for lack of trying: we
have devoted about six CPU-years to the task. The apparent unbreakability of
CompCert supports a strong argument that developing compiler optimizations
within a proof framework, where safety checks are explicit and
machine-checked, has tangible benefits for compiler users.

RalfJ (Jun 10 2019 at 09:32, on Zulip):

so, coming to Rust, we are far from CompCert. ;) What RustBelt shows is that if our model (I am an author of RustBelt) of the borrow checker matches the real borrow checker, and if our model of how MIR programs behave matches what they really do, then we get safety. That's two big IFs, and the are likely both not true!

centril (Jun 10 2019 at 09:33, on Zulip):

Personally, I would settle for a soundness proof of Rust's type system according to our TBD chosen operational semantics. :slight_smile:

RalfJ (Jun 10 2019 at 09:34, on Zulip):

however, when you bring in LLVM, the question actually to some extend gets worse than just "we have no proof". The problem is that we don't even have a theorem one might want to prove! Before you can prove anything you need a precise statement of what it is you want to prove. In particular we need an operational semantics for what Rust code is actually doing when being executed, and (as @Centril just mentioned) we don't have that currently.

RalfJ (Jun 10 2019 at 09:35, on Zulip):

And that's where LLVM comes in: defining the operation semantics has the interesting and conflicting set of goals of being a reasonable, understandable semantics on the one hand while at the same time it has to be possible to compile our code to efficient LLVM. But to analyze if that translation is correct, we need both a semantics for Rust/MIR and for LLVM, and currently we have neither...

Ehsan M. Kermani (Jun 10 2019 at 15:26, on Zulip):

Thank you @RalfJ and @centril for the clarifications! Most of my concerns is about Rust Abstract Machine (given some fundamental assumptions) that right now seems to be far away from being well-defined, yet I cannot get my head around how we can say rustc optimizations are safe and free of UBs!

Can we have an FAQ in the github wg to address what the goals are and what are non-goals? For some time I was under the impression that the goal is to surface what we don't know to future RFC and the ultimate goal is (as Mazdak said) soundness proof of Rust's type system or even coming up with all the necessary definitions for Rust Abstract Machine that future compiler writers, when adhere to, will be provided with all the safety guarantees.

RalfJ (Jun 10 2019 at 15:44, on Zulip):

well defining the Rust Abstract Machine is also a goal

Last update: May 27 2020 at 22:25UTC