Re: how to make code stay invariant

[Rolf Schumacher <rolf at august dot de>]

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
Thanks for that link John. Wheeler has collected and weighted a snapshot
of open source projects anyhow related to security issues.
Unfortunately I can't find much safety. All the levels are security levels
no safety level. And - to be honest - no one could persuade me yet
that formal methods overcome semi-formals like UML.
In practice they do not do better.
But I might not be at the state of the art.

However, it's the relationship to our subject here is loose.
> But hmm, you said debug not test... So I think there is more to that
> issue than meets the eye...
hmm, nice, you catched this difference.
Yes, that was the problem:
Debugging is about reducing the number of errors.
Apart from statistics no public demonstration has to come up.
Testing a module is about proving the absence of failures
as far as possible in that step.
With strong demonstration to independent people, representing the public.
And I agree this has to be and will be done on the target system.
Debugging is not testing.
> 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
Sorry, I didn't mean to impress nor to loose you here.
Just to show the art how safety targets function,
ok, how they function currently, we are learning all the time.
It takes time to smell 10**-9. Your dog is born with it, you got to 
train it.
> http://www.dwheeler.com/program-library/Program-Library-HOWTO/x36.html
> http://people.redhat.com/drepper/dsohowto.pdf
Thanks, the latter one made me learn something: ELF and PIE, GOT and PLT
(About every time they talk about "cost" in terms of speed and memory
I'm reading "solution" in terms of independence and invariance.)
> In fact Drepper's whole page is a gold mine of detailed info on ELF.
> http://people.redhat.com/~drepper/
He seems to know what he's talking about.
> 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.
That not a wild guess, for what I see it's true.
What I also see is, that could be a lot of tricky work
as I mentioned above: I'm not so much interested in cost
(memory and speed) as all others are.
Would be nice if someone already has done that work
with more knowledge about ELF as I'm equipped with.

> > 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.
Yes, here is what I understood so far to find the solution I'm looking for:

1. Understand ELF until you're able to play with it
2. Generate PIEs in ELF format
3. Animate gcc to pack every link in GOTs and PLTs, check that the code 
stays invariant, if needed define coding rules, build a checker.
4. Make sure the GOTs and PLTs are not contained in code regions
5. Give programmers a handy tool to reach functions as usual (may be, 
this step is not needed)
6. Generate meta info on the absolute start and length of a code region 
in memory and do the checksumming
7. check checksumming by moving the code around and using different 
implementations of e.g. MD5.

Thought it would be easier and I would not be the first to ask for such 
a thing.

What do I have overlooked, John?
What could be made simpler?
I'm mostly worrying about step 1.
Also there's a risk to be unsuccessful in step 3 and 4.
What are other risks that I haven't identified?



Rolf

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature