fdupress

It's almost always done to argue for testing, too. But the point of verification as an engineering tool was never to replace testing, but to focus it. (Just like the point of a mathematical proof is not to offer 100% proof of the truth of a statement, but to reduce its truth to the truth of some other statement---usually "ZF holds".)

So you do some formal verification, good. But you still need to: - validate your model; and - validate your assumptions. This would always have to be done, but the fact that GP did not think about it means that, in the case of testing, it's not done. It's just "extensive testing", perhaps with some metric if we're lucky. Never "what are we testing for, and under what circumstances". (Except in places---aerospace, hardware---that welcome formal verification.)

Now, why does the above rant matter? Because GP is advocating the use of testing for a security property. Writing that test means you suspect there's something iffy that can happen with speculation. And if you know something iffy can happen, you can figure out what's not iffy and make that your spec for formal verification. You then get a proof that only the good (secure) behaviour takes place under clear assumptions, instead of getting the guarantee that none of the bad behaviours are exercised by your test suite.

People may not die if I cheat on my exam, but casting doubt on the accuracy of the results by eroding trust in the examination process certainly affects all who took the exam when they end up not getting a job.

So it turns out Materialistic doesn't even show responses to my comments unless I go back to the thread itself...

The point I was making was in context of a discussion focused on mission-critical system. In that context, you can't just add a beautifier to your compilation pipeline with the argument that "the only way things will go wrong is if the beautifier is broken".

The need for bureaucracy is only there because of people like you. People who, when an inequality is pointed out, simply knee-jerk their way into "I worked hard to be born a white man, I've earned this," instead of reflecting on what they have and where it came from.

This also papers over a potential defect, but also introduces a potentially semantic-breaking process into your compilation pipe.

Say you've proved memory safety on your source. What you're compiling is no longer that source you have a proof about.

- Didn't remove its privileges (moderation) before transferring ownership.

A good example would be a complex state machine, where you rely on the fact that the state is only modified by the state machine code to make sure it remains well-formed, and the control-flow itself heavily relies on the state being well-formed (think of a TLS session, for example).

But then again, what you want there is modularity, which OOP provides, but is also well-supported in other paradigms.

In the case of Samsung and smart TVs, and to fully support the argument you are supporting, it is not sufficient that Samsung makes a lot of money. They need to make a lot more per user selling data than they would adding $20 to the price of that TV.

But that $20 price difference would probably mean that less people buy Samsung, so the maths isn't going to be that straightforward.

Checking that the output is sorted is the easy part.

Checking that the output is a (optionally stable) permutation of the input is the hard part. You can't do that dynamically if you have, for example, overwritten your input by sorting in place. And making a copy of your input is only going to be affordable in very specific and small instances on which you might as well just run a well-understood algorithm.

Only if it's irrelevant. If it's relevant, it's a necessary correction.

Because they are known in advance and you could design to exploit their structure.

Hard to say when the US doesn't test.

One-time MACs... The most widely used constructions are based on polynomials: GHASH (from GCM) and Poly1305.