undefined | Better HN

0 pointszozbot23422d ago0 comments

Memory safety is absolute table stakes when it comes to formal verification. You can't endow your code with meaningful semantics if you don't have some way of ensuring memory safety.

0 comments

foldr22d ago

That's far from trivial in Rust because of 'unsafe' blocks. There are approaches to verifying unsafe code in Rust, but formally verifying a Rust program is still likely to be significantly more complex than formally verifying, say, a Java program.

(And before someone says it: no you don't only have to verify the small amount of code in 'unsafe' blocks. Memory safety errors can be caused by the interaction of safe and unsafe code.)

pjmlp21d ago

At least you can grep for unsafe/system/unchecked in several alternative systems languages.

For C and C++, we have to hope the static analysis tool actually found all possible spots.

Despite the way it is going on as a drama between WG21 and community, C++ might eventually get Ada style profiles in C++29, lets see how it plays out.

Then you also would have something to grep for, [[profile:...]]

C? Same business as usual.

foldr21d ago

Grepping for unsafe blocks doesn’t help that much for formal verification, because you have to verify all of the code.

The easiest way to see this is to note that ‘unsafe’ itself doesn’t have any semantics, so it can’t possibly allow anything to be proved that couldn’t have been proved otherwise.

pjmlp21d ago

It helps finding locations for possible flaws outside the type system soundness.

Now if we go discussing formal verification in general, even something like Dafny or Lean may fail, if the proofs aren't correctly written for the deployment scenario.

Just like one may still die while wearing helmets, airbags, and security belts, yet the casualties amount is much worse without them.

1 more reply

uecker22d ago

Indeed, and this is why people who care about this are also proving memory safety in C. The issue is that we do not have good open-source tooling that specifically focuses on formal verification of memory safety in C.

j / k navigate · click thread line to collapse

0 comments

foldr22d ago

(And before someone says it: no you don't only have to verify the small amount of code in 'unsafe' blocks. Memory safety errors can be caused by the interaction of safe and unsafe code.)

pjmlp21d ago

At least you can grep for unsafe/system/unchecked in several alternative systems languages.

For C and C++, we have to hope the static analysis tool actually found all possible spots.

Despite the way it is going on as a drama between WG21 and community, C++ might eventually get Ada style profiles in C++29, lets see how it plays out.

Then you also would have something to grep for, [[profile:...]]

C? Same business as usual.

foldr21d ago

Grepping for unsafe blocks doesn’t help that much for formal verification, because you have to verify all of the code.

The easiest way to see this is to note that ‘unsafe’ itself doesn’t have any semantics, so it can’t possibly allow anything to be proved that couldn’t have been proved otherwise.

pjmlp21d ago

It helps finding locations for possible flaws outside the type system soundness.

Now if we go discussing formal verification in general, even something like Dafny or Lean may fail, if the proofs aren't correctly written for the deployment scenario.

Just like one may still die while wearing helmets, airbags, and security belts, yet the casualties amount is much worse without them.

1 more reply

uecker22d ago

j / k navigate · click thread line to collapse