Undefined Behaviour as usual

Posted Feb 26, 2024 7:50 UTC (Mon) by NYKevin (subscriber, #129325)
In reply to: Undefined Behaviour as usual by mb
Parent article: Stenberg: DISPUTED, not REJECTED

In principle, it is possible to compose a complete, usable system entirely out of a combination of:

* "Safe" code (where the compiler will not let you write code that contains UB).
* "Verified" code (where the compiler will let you write whatever you want, but you also write a machine-verified proof that no UB will actually occur).

But then this is just a matter of definitions - You can set up your build system in such a way that it will refuse to compile unsafe code without a valid proof of soundness. Then you can consider the proof to be part of the source code, and now your unsafe language, plus the theorem proving language, together function as a safe language.

Formally verified microkernels already exist. The sticking point, to my understanding, is the lack (or at least incompleteness) of a verified-or-safe userland.

Undefined Behaviour as usual

Posted Feb 26, 2024 10:02 UTC (Mon) by farnz (subscriber, #17727) [Link] (1 responses)

The other sticking point is the difficulty of formal verification using current techniques. Formally verifying seL4 took about 20 person-years to verify code that took 2 person-years to write.

Undefined Behaviour as usual

Posted Feb 26, 2024 10:12 UTC (Mon) by NYKevin (subscriber, #129325) [Link]

The thing to bear in mind is that, technically, the type checking in a safe language is also a valid proof of safety (or else it would not type check). So every safe Rust program (and every Java program, etc.) is verifiably safe, assuming the type system is sound.*

The question is, is that good enough? Most formal verification wants to prove more than "mere" type safety or soundness, and that tends to be hard because the property you're trying to prove is complex and highly specific to the individual application. But if you just want to prove a lack of UB, that's probably more feasible.

* There are soundness bugs in the current implementation of Rust. Most of them are rather hard to trigger accidentally, but they do exist.