'It will go wrong. There's no question of time... on safety or security side'

Disassembling the binary only gives you the instruction sequencing if it is single threaded application (and not even that if there are many loops and branches dependent upon external inputs). In a multi-threaded or distributed application there is generally no way to enumerate all possible interleaved sequencing of events, particularly when those events may include hardware operation and error scenarios (such as patterns of packet loss).

Carefully choosing a range of inputs is hard, very hard, how do you determine in a complex system that you have selected enough variation, particularly taking into account all possible fault conditions and event sequencing. In a complex system just because input A gives output B when you ran it in test on your perfect network at 12:32pm doesn't prove that it will give output B on a real laggy network at 12:00am. You can't test all possible scenarios so you have to narrow down the set, based on the understanding of the code and platform and where the risk is perceived to be, of course with any risk based approach sometimes you get unlucky.

If code inspection was easy then this obviously means that code that has been reviewed won't introduce any bugs and work perfectly in the system. Experience shows even with thorough code review and test definition and multi layers of validations bugs still get through to the customer.

The simple fact is most computer software is too complex for a single person to fully maintain a mental model of how it works and all the possible interactions and knock on effects of changes. Modularization and clear specification helps mitigate some of this, though that can actually sometimes be where the security or resilience holes appear.

Not so simple

Also note such things as branch prediction in modern CPUs, for example.

How can you then predict the exact sequence of instructions from the software alone? The exact sequence can surely only be determined for a defined combination of hardware, software and input data.

That seems to be make certainty exponentially more difficult to obtain.

"It's also very easy to test software, you run it for a range of carefully chosen inputs and compare the result to the expected outputs."

And now you know how the software responds to a small range of carefully chosen inputs. Every single software bug or security vulnerability is the result of someone assuming that because the software responds correctly in a limited test, it must therefore be safe and secure (or alternatively, knowing that it isn't perfectly secure but releasing it anyway). The big problem is that no matter how much you expand your list of chosen inputs, there are an infinite number possible so you can never test them all. All you can do is try to think up the sort of things that are likely to cause problems; every bug that makes it into the wild is the result of someone thinking up an input that the developer didn't consider (or again, did consider but didn't bother fixing). Hence - software is impossible to test; no matter how thorough the testing you do, you're trying to prove a negative by searching every part of an infinite space.

Not that easy

You also need to check what happens with inputs outside of carefully your chosen list.

Reality is not neat, corrupted data, intergference, malicious actors, etc, etc.

For non trivial code sequencing is not easy - e.g. multi threading

If code is simple and crystal clear when looked at in isolation, things can get a lot more complex if multiple instances of this code are running and accessing a shared resource - - race conditions, contention, timeouts, deadlocks, etc.

Once you go beyond trivial code, running petri net analysis soon shows how complex even "simple code" can be.

Then theres all the "code" you do not really control - if you are using anything higher level than assembler then a lot of the produced code is outside of your control (e.g. I may define baud rate, com port etc in my serial port read / write code but when I do a serial port write the nitty gritty is done by code written by someone else)

There's a good reason I'm currently running hundreds of instances of 3 different applications (all being fed with auto generated random test data) that all read from / write to a common database ... and when that's all complete comparing database contents / error logs with expected results based on the auto generated inputs.

Meanwhile I have several instances of test aid application that frequently write locks different parts of the database.

..I'm doing that because I want to check error handling, 2 phase commit etc. all works when there's contention, database access issues.

Everything was hunky dory on nice simple unit tests, but I need to ensure it works when there's nasty real world complexity.

> It's actually very easy to inspect software. You just open the source code in your favourite editor.

Read "Reflections on Trusting Trust," by Ken Thompson.

> It's also very easy to test software, you run it for a range of carefully chosen inputs

I fear that's the sort of hopelessly naive thinking that helps this industry deliver such unreliable bug ridden security vulnerable crap.

@sealand: common mode errors

"the [toolchain] had made an error, but the simulator had the exact same flaw that cancelled the error out in the simulation."

For the same kind of reason it can help to have very independent people writing the code and writing the test data, too, at least for part of the exercise. Doesn't stop them both making complementary errors - been there seen that got the scars.

"[...] but the simulator had the exact same flaw that cancelled the error out in the simulation. [...]"

A case of two wrongs do make a right.

Several times I have seen people fix an obvious error in the code - that they just happened to notice in passing. Only when things then started failing did they discover the other bit of code that was complementary. Possibly the origin of the wise advice - "if it ain't broke - don't fix it".

"It is a truism that "If anything can go wrong - it will go wrong - at the worst possible moment"."

Would this be true even of formally proven code? Just saying...

"Perhaps what we need is not to fruitlessly pursue absolute software testing but rather to implement completely separate DBSBS processes that are not integrated with the checked system. Maybe two levels of DBSBS like a co-pilot cross checking the main pilot's setting of the autopilot."

Not even that's going to help because then you'll run into things like common mode failure (or to use your analogy, the pilot and copilot make the same mistake--or worse, are in cahoots) that hit all the redundancies at once.

"You don't expect a £1 watch from Poundland to keep good time, [...]"

If the tolerances just happen to be in harmony then it could keep very good time. I have a cheap plastic Accutime bedside clock that runs on one AA battery for several years. It never needs adjustment between battery changes.

In the 1970/80s you could buy a high end camera maker's lens that guaranteed a good spec - or buy a much cheaper lens from people like Vivitar. If you were lucky the latter could be as good as the high end one.

In appearance they were identical - and in fact they were from the same manufacturing line. The high-end camera makers merely selected the ones with the best test performance. In the same way you can get a very good car engine by carefully matching the components for ordinary car engines.

Re: @various

"Arguably doesn't even need a trustworthy compiler, certainly doesn't need a complex untestable unprovable compiler."

Unless the H/W executes Forth directly (in which case you simply push the problem down a level) it needs an interpreter. What's the interpreter written in and how's it compiled if it's in a higher level language?

However, if the code inspection reveals a hard-coded root password you can stop right there and throw the whole lot out.

Re: @various

"[...] but when push comes to shove, processors don't execute source [1], they execute binaries."

I have a C program which has evolved over nearly 30 years through various 8/16/32 bit compilers. The current version is stuck on MS Visual Studio 6, It compiles with later MS C compilers - but even with all optimisations switched off it just won't run properly.

The last gotcha from a compiler update was when it assumed that identical code inside differently named functions meant that they could all be optimised to one instance - with a single undifferentiated entry point. They had different names for the reason that their calls were differentiated elsewhere.

Re: You'd never think the Shuttle flew for 30 years without a flight bug.

"1)Design the code.Break it up into segements. Design the detailed equations it implements"

But then how do you deal with gestalt problems like race conditions that never appear in the individual components but only in the whole (thus gestalt: worse than the sum of the components) and even then only under certain edge case conditions?