Re: how to make code stay invariant

John Carter <john.carter@xxxxxxxxxx> · Mon, 31 Jul 2006 10:32:53 +1200 (NZST)

Ok, so let's threat model that....

Let's say probability of bug per line of code is p.

Let's say the number of bugs of the sort of bug you are trying to
prevent (link time corruption bugs not found on initial test) is q.

Let's say the probability of bug removal from ordinary code (by
inspection, by test, by static tool etc.) is d

So the number of bugs in the ordinary code (as written) is pN where N is
the number of lines of code in the program

The number of bugs after bug removal is with link time / corruption bugs
is pN(1-d)+q

Now you have introduced a further M lines of interface code. Assume approximately
the same bug rate, maybe less. Let's say the bug rate in the interface
code is a*p where a is a number between 0.1 and 1

So you now have (pN+apM)(1-d) == p(1+aM/N)N(1-d)

So compare the two bug rates...

pN(1-d)+q vs p(1+aM/N)N(1-d)
  or
pN(1-d)+q vs pN(1-d)+apM(1-d)

So whether you have gained anything from this activity depends on whether
 q is greater than apM(1-d)

You will have to plug you own numbers into that.

My guess is the answer is a resounding "No!" since q is so very small
compared to pM.

On Sat, 29 Jul 2006, Rolf Schumacher wrote:

Hi, John.

for the first place I found a much simpler solution.
I checked it with gcc -fPIC, and than applied prelink.

Consider a module m1 calling function o2 in module m2.
If we define an interface compilation unit for m2, say m2if,
that implements o2if just calling o2 and m1 is not using
o2 anymore instead of o2if, m1 stays invariant as long
as the interface is invariant. I can do as much "small changes"
to m2 as I like, the checksum of m1 (in memory and on disk)
stays invariant.

in code now, prior to invariance:

m1.c:
#include "m2.h"
int main(void){o2();}

m2.h:
void o2();

m2.c:
#include "m2.h"
void o2() {printf("hello world");}

and now after changes for invariance:

m1.c:
#include "m2if.h"
int main(void){o2if();}

m2if.h:
void o2if();

m2if.c:
#include "m2if.h"
#include "m2.h"
void o2if(){o2();}

m2.h:
void o2();

m2.c:
#include "m2.h"
void o2() {printf("hello world");}

Conclusion:
The object code invariance is gained just by coding rules.
Introduce of object code invariance is applicable even to existing software.
Benefit: all my module tests to m1 apply in the new software
regardless of changes to m2. I haven't to repeat them.

Remark:
For reduction of validation tests of the software product
as a whole against requirements I still need a reliable
impact analysis in order to reduce tests. Invariance doesn't help here.
Code object invariance gives evidence only for code integrity on
the invariant part of the software, nothing more.
However, that's still a lot.

I'll do that!

Thanks for your great help and all the philosophical hints.
I wouldn't have done without even if the resulting solution is that simple.

kind regards

Rolf

John Carter wrote:
Hmm, you probably should be scanning Miller's handy...
http://www.dwheeler.com/essays/high-assurance-floss.html

High Assurance (for Security or Safety) and Free-Libre / Open Source
Software (FLOSS)... with Lots on Formal Methods

On Wed, 26 Jul 2006, Rolf Schumacher wrote:

Pretty rare, but they happen.
We just had to recall projects in an expensive way
upon a difference in gcc compiling for SUN
and for Intel. (const in parameters)
Debuggin was done on a SUN, delivery was for Intel.

Test like you fly, fly what you tested...

But hmm, you said debug not test... So I think there is more to that
issue than meets the eye...

In safety critical systems we have to demonstrate (!) 10**-9.
For example, systems in an atomic power plant
have to be secure to 10**-13 (asaik). They are not allowed to add more 
risk.
You have to have risk reduction technologies because you can't reach that
figures with software.

I'm reminded of the Bad Old Days when there were MilSpec computers.

Until they realized that the sheer weight of consumer COTS products
meant that what was available from the corner store was...
* Way way cheaper.
* Way way faster.
* And much more reliable!

Happened again with handheld GPS during the Gulf War. The COTS /
Consumer GPS's were just so much better than the MilSpec ones (even with
the delibrate signal fuzzing!!) that they gave up and used the COTS.

The other thought that comes to mind is a variant of a very old joke....

Patient to Doctor, "Doctor! Doctor! I need to be incredibly hugely
impossibly painfully costly reliable to do this."

Doctor, "Well don't do that then."

Just the fact that you can think about an error draws the responsibility
to give an accepted figure for it: 1. HAZOP, 2. FMEA at least FTA,
you do not have any statistics. It hasn't to be real at all in any past.

Wow! That is really Amazing! You are _so_ deep in the Dilbert Zone! Do
you _ever_ see sunlight there?

http://www.dilbert.com/comics/dilbert/archive/dilbert-20060724.html

Some (targets/versions) of the GCC linker do relaxation passes. ie.
Change long jumps to short jumps, change long references to short
offsets. And since the size of the code has shrunk, they do that again,
and again until it converges.
Can I switch that off?

Only applies to very few CPU's, don't know which one you are using. I
met it on the HC12. Search "info gcc" for "relax".

Basically you want each module to be a DLL/sharable object so the linker
does the absolute minimum of fix ups.

You also need a strict acyclic dependency graph between the sharable
objects and then link each layer with lower layers.

Follow the standard tricks to make a sharable object / DLL.
Now that's it: I need a link here to update my knowledge.

http://www.dwheeler.com/program-library/Program-Library-HOWTO/x36.html
http://people.redhat.com/drepper/dsohowto.pdf

In fact Drepper's whole page is a gold mine of detailed info on ELF.
http://people.redhat.com/~drepper/

In fact I'll make a wild guess....

If you really understood all the niches and corners of ELF, which is
quite a large and hairy domain, what you want is already in there
somewhere.

You still need the objdump tricks I mentioned to pull just the sections
you care about out.
dito

info binutils

What I wanted to tell you is,
that you're completely right with the example of the Unix loader
separating tasks by means of address space.

I have to look at a module as a task that takes messages and respond
with messages. As in UML sequence charts.

What is the easiest way to implement a messaging system e.g. by macros
for programmers that like to use function calls?

Make it simple to use, complex == more lines of code == programmer
mistakes.

The one we are using involves declaring and packing and unpacking
structs all over the place. Yuck! Tedious and error prone.

I itch to rewrite using a simple convention that looks like an ordinary
function declaration, definition and reference.

And then add a bit of Ruby code generation magic to generate a header
pulled in by the client and a header to be pulled in by the server. Oh,
and glue it together with a small, possibly entirely non-portable bit of
C that understands varargs to serialize the arguments across the
messaging interface.

I bet I can get a huge reduction in code size, much simpler, much more
reliable and better code.

John Carter Phone : (64)(3) 358 6639
Tait Electronics Fax : (64)(3) 359 4632
PO Box 1645 Christchurch Email : john.carter@xxxxxxxxxx
New Zealand

Carter's Clarification of Murphy's Law.

"Things only ever go right so that they may go more spectacularly wrong 
later."

From this principle, all of life and physics may be deduced.

John Carter                             Phone : (64)(3) 358 6639
Tait Electronics                        Fax   : (64)(3) 359 4632
PO Box 1645 Christchurch                Email : john.carter@xxxxxxxxxx
New Zealand

Carter's Clarification of Murphy's Law.

"Things only ever go right so that they may go more spectacularly wrong later."

From this principle, all of life and physics may be deduced.