undefined | Better HN

0 pointspjmlp21d ago0 comments

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.

0 comments

foldr21d ago

It helps a human armed with only a tool as crude as grep. But if Rust didn't have the requirement to mark unsafe operations with the 'unsafe' keyword, that information could trivially be added back automatically. If you're doing correctness proofs of realistic Rust code, you'd better already have tools that are at least capable of looking through your codebase for any instances of raw pointer access, etc.

There's a lot of mythology around Rust unsafe blocks. They're a useful lint, but they don't alter the fundamental safety properties of the language.

pjmlpOP21d ago

The mythology of unsafe blocks goes all the way back to ESPOL on Burroughs, still sold nowadays by Unisys, for customers that want OS security as the number one feature, before anything else.

It was also adopted by several systems and application programming languages outside C geology, until C# came to be, which is probably the first curly brackets language with unsafe code blocks.

The first error naysayers make on the eyes of SecDevOps, thus losing credibility points, is to focus too much on Rust, and too little on history of secure systems.

The first fundamental rule is to reduce attack surface, on C, and C++ (until and if profiles come to be), it is all over the place.

I don't see folks that usually post on HN or Reddit going to buy Astrée licenses, or integrate Frama-C into their development process.

foldr21d ago

I am not sure what point you're trying to make. Who are the 'naysayers', and what are they saying 'nay' to? And what do they have to do with anything I commented on?

pjmlpOP21d ago

Anyone that downplays unsafe code blocks as it was a Rust invention, available nowhere else.

Then uses it as argument, that since Rust has unsafe, there is no benefit over using C or C++ with a plain static analysis tool, but a basic one, because they are unwilling to actually use the ones people pay for on high integrity computing certifications.

Your comment to me seemed a bit going towards that direction.

1 more reply

j / k navigate · click thread line to collapse

0 comments

foldr21d ago

There's a lot of mythology around Rust unsafe blocks. They're a useful lint, but they don't alter the fundamental safety properties of the language.

pjmlpOP21d ago

The mythology of unsafe blocks goes all the way back to ESPOL on Burroughs, still sold nowadays by Unisys, for customers that want OS security as the number one feature, before anything else.

It was also adopted by several systems and application programming languages outside C geology, until C# came to be, which is probably the first curly brackets language with unsafe code blocks.

The first error naysayers make on the eyes of SecDevOps, thus losing credibility points, is to focus too much on Rust, and too little on history of secure systems.

The first fundamental rule is to reduce attack surface, on C, and C++ (until and if profiles come to be), it is all over the place.

I don't see folks that usually post on HN or Reddit going to buy Astrée licenses, or integrate Frama-C into their development process.

foldr21d ago

I am not sure what point you're trying to make. Who are the 'naysayers', and what are they saying 'nay' to? And what do they have to do with anything I commented on?

pjmlpOP21d ago

Anyone that downplays unsafe code blocks as it was a Rust invention, available nowhere else.

Your comment to me seemed a bit going towards that direction.

1 more reply

j / k navigate · click thread line to collapse